We need the language of category theory in order to talk about sheaves. This language is very fundamental to mathematics, so much that in the course of setting it up one has to consider foundational issues: all of mathematics is supposed to be chain of rigorous deduction, but some very basic concepts need to be assumed be be universally understood by grace, and all deduction is based on these universally understood concepts.
This basic concept has traditionally be taken to be that of a collection of elements – a set – with a global binary relation – – that determines which sets are elements of other sets. Naïve and obvious as it may seem, there is some subtlety hidden here, related to the global nature of the inclusion relation.
After the advent of category theory it was argued by Lawvere and others, that, roughly, what is truly fundamental is not so much the concept of a set itself, but rather the interrelation between sets in terms of functions between them. These form the category Set of sets.
In every development – notably in that that of sheaves and stacks — for which category theoretic language is crucial anyway, it is natural to take as foundations Lawvere’s Elementary Theory of the Category of Sets (ETCS), which takes as the fundamental concept the naïve theory of the category of sets and then develops everything else from within this context. Here “naïve” means “understood by grace” and not further deriveable.
One advantage of this perspective is that it allows to naturally address and handle concerns and disagreement about what actually does count as naive and universally accepted basis of all reasoning. This is because the crucial property of the naïve category of sets is that it is a kind of category called a topos: a “place” in which mathematics may be developed. When one strictly sticks in the development of mathematical notions to constructions within ETCS as opposed to, say, the traditional Zermelo-Fraenkel axiomatics for set theory, then all constructions and results make sense in any other topos. For instance in constructivism is a school which asserts that some axioms about naïve sets are not quite naïve enough and reject them, notably the axiom of excluded middle. This point of view turns out to be perfectly compatible, and in fact enforced, by the topos-theoretic perspective on foundations.
But because ETCS contains nonconstructive axioms (the axiom of choice, also strong extensionality if it is written in classical predicate calculus), not everything done there is acceptable to a constructivist. Similarly, these same axioms, as well as infinity, fail in some toposes, so not everything in ETCS works in any other topos. —Toby
Elementary Theory of the Category of Sets – ETCS
a “structural” formalization of set theory which combines the rich tradition of naïve (= pre-axiomatic) set theory with the insights of category theory
literature:
Lawvere, Rosebrugh: Sets for Mathematics
ETCS differs from non-structural material set theory in the way it handles the membership relation :
in ETCS “sets” and “elemens” are of different type: not every element of a set is necessarily a set itself;
no element exists in isolation: it always exists relative to the set that it is an element of.
there are also generalized elements: functions – conversely, functions between sets – called then morphisms in the category of sets – are regarded as primary, and the notion of element is derived from that: an element of a set is regarded as the function that sends the single element of the singleton set to .
general category theoretic perspective: what matters are the morphisms , not so much any imagined “inner structure” of the objects , .
in techical terms the categroy of sets Set to be described now is
a topos;
which is well-pointed;
satisfies the axiom of choice;
and is equipped with a natural numbers object
Now the definition.
Set consists of
a collection of “objects” called “sets”, ;
a collection of “arrows” called “morphisms” called “functions” that go between pairs of objects,
a composition operation on all pairs of composable morphisms;
such that this comoposition is associative;
such that the morphisms of the form are units with respect to this compositon.
Remark So far this would say that Set is a category: but the point is that we take the above now as a primitive notion and avoid saying “a category consists of a set/class of objects, etc.”. Rather, below we define the notion of category as a concept internal to Set.
Notation
A function we also call an element of with domain (or “stage of definition” ).
If we allow ourselves to denote comopsition simply by juxtaposition then for a function and regarded as an element of (over domain ), the notation denotes consistently both the composition of two functions and the application of th function to the element .
This is the sense in which ETCS is “structural”: there is no separate notion of element, everything is in the relational structure defined by composition of morphisms.
This structure of Set is required to satisfy the following axioms.
Axiom of products.
This means first of all: For any two sets , there is a set and functions , , such that given two elements over the same domain, there exists a unique element over that domain for which
A choice of product is usually denoted . To make a bridge with naive set-theory notation, we may suggestively write
where the funny equality sign and bracketing notation on the right simply mean that the cartesian product is uniquely defined up to isomorphism by its collection of (generalized) elements, which correspond to pairs of elements.
Moreover, admitting finite products also means that there is the empty product exists: there is an object in Set
which has a unique element over any domain;
equivalently: such that for every other object there is a unique morphism
Notation
The above implies in particulat that for two functions and there is canonically a function denoted
induced by the universal property of by from the existence of the two functions and
Axiom of equalizers.
For any two functions , there exists a function such that
Equivalently, in morphism language:
An equalizer is again defined up to isomorphism by its collection of generalized elements, denoted .
Consequence: pullbacks
The axiom of products and the axiom of equalizers already ensure that Set has pullbacks
Given functions there exists a set and functions and such that the diagram
commutes and such that for every other such diagram
there is a unique function such that
One checks that indeed is equivalently the equalizer of and :
Hence we may write
is the fiber product of with : over it is the product of the fibers and .
Terminology.
With this structure in hand, we obtain the useful notions of subsets and relations in Set.
A function is injective if for every over the same domain, implies .
Equivalently, in morphism notation: is a monomorphism if for every and , implies .
Dually, a is a a surjective function or epimorphism if for every and , implies .
Given a monomorphism we may think of it as defining a “subset” of , whose (generalized) elements correspond to those elements which factor (evidently uniquely) through . It is in that sense that we say also “belongs to” a subset , while, contrary to non-structural set theory, strictly speaking every element in the language of ETCS is element only of one single set.
A relation from to is an injective function or subset .
Now we can state the next axiom
Axiom of power sets.
For every set there is a set denoted or and called the power set of and a relation to be thought of as “is element of subset in ” so that for every relation , there exists a unique function such that is obtained up to isomorphism as the pullback
i.e the universal commutative diagram
In other words, belongs to if and only if belongs to .
Axiom of strong extensionality.
An element with domain the terminal object we call an “ordinary element” of . Then:
for functions
we have if and only if for all ordinary elements .
Consequence: ordinary element-based notions
Using this principle of extensionality, all the properties of Set described here in terms of generalized elements over varying domains, or, equivalently, described diagrammatically, translate equivalently to the usual element-based definitions. For instance, recall that a function is a monomorphism if implies . So in particular, for and , ordinary elements, this says that implis . The converse statement follows similarly.
Axiom of natural numbers object.
There is a set , together with an element and a function , which is initial among sets equipped with such data. That is, given a set together with an element and a function , there exists a unique function such that
Or, in elementwise notation, for every (generalized) element , where means . Under strong extensionality, we may drop the qualifier “generalized”.
Axiom of choice?.
Every surjective function admits a section, i.e., a function such that , the identity function.
Remark The axiom of choice tends to sound a bit mysterious in non-structural ZFC
set theory. The above structural formulation
gives a rather clear heuristic picture for what the axiom means. See the further remarks and examples at axiom of choice.
** Consequences and further axioms **
This defines the Elementary Theory of the Category of Sets. From these axioms now various further properties follow: notably Set can be shown to be a topos and in particular it is cartesian closed.
There is however so far one axiom missing, that we need. This is the axiom of universes that we will motivate now.
In category theory we frequently want to deal with entities that are “collections of all collections of some sort”. It is familiar that one has to exercise some care here: famously, attempts to define concepts such as “the set of all sets” leads to inconsistencies. These are always due to a failure to preserve a hierarchy of notions of collections: if “Col” is some kind of collections, then “the collection of all Cols” is not in general a Col itself, and should be considered a a new notion, a “col+”, say.
The notion of Grothendieck universe is one way to formalize such a hierarchy of notions of collections. In this context, every collection is always a set in the sense that it is an object in the theory ETCS axiomatized above. But some of these sets behave essentially as if they were a “set+ of all set’s”, for some notion of set’.
A universe in a topos is a morphism satisfying the axioms to follow. We think of as a -indexed family of objects (sets), and we define a morphism (regarded as an -indexed family of objects) to be -small if there exists a morphism and a pullback? square
Note that is not, in general, unique: a universe can contain many isomorphic sets. With this definition, the pullback of a -small morphism is automatically again -small. We say that an object is -small if is -small.
The axioms which must be satisfied are:
Every monomorphism? is -small.
The composite of -small morphisms is -small.
If and are -small, then so is the dependent product? (where is the right adjoint to ).
The subobject classifier? is -small.
Let us unwrap what this means:
For an ordinary element of , write for the fiber of over , i.e. for the pullback . We are to think of as the set of all sets .
By definition, a single set , regarded as the unique function , is -small if it is isomorphic to one of these .
As for , any function may be thought of as a family of sets parameterized by . One finds that itself is the disjoint union of all the . Therefore the first first axiom says that with -small and a -small family, also is -small, hence that is -small:
-small indexed families of -small sets are -small.
Since is a monomorphism, and is small by axiom 4), it follows that is small and hence is a small set. Which sounds very reasonable.
The first axiom says that with a -small set, also every subset of is -small.
Let be any category. A category internal to consists of
an object of objects ;
an object of morphisms ;
together with
such that the following diagrams commute, expressing the usual category laws:
Here, the pullback is defined via the square
Internal to? an ambient category , a functor is
a morphism of objects in ;
a morphisms of morphisms in ;
such that the following diagrams commute
respect for the source map: ;
respect for the target map: ;
respect for identities ;
respect for composition .
Prägarben;
Yoneda Lemma;
adjungierte Funktoren
previous: heuristic introduction to sheaves, cohomology and higher stacks
– home: Garben und Stacks
Last revised on April 14, 2009 at 02:25:07. See the history of this page for a list of all contributions to it.