nLab ETCS with elements

Contents

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

In usual presentations of categorical set theories such as ETCS, the set theory is usually a theory of sets and functions in an abstract category, with elements being defined as the global elements, the morphisms out of the terminal object. However, this approach poses a few conceptual and practical issues, namely that in ordinary mathematical practice, elements are not the same as functions out of the terminal set 𝟙\mathbb{1}, although AA is in bijection with the function set A 𝟙A^\mathbb{1}, and function evaluation of elements defined as function composition of functions out of the terminal set is an abuse of notation.

There are other structural set theories, such as SEAR, which explicitly put in the elements of a set as a primitive of the theory. In such a theory involving sets and functions, function evaluation would be a primitive of the theory, rather than derived from function composition of global elements, and the axiom of function extensionality is likewise defined directly on the elements. Such a theory reads more like a traditional presentation of set theory in terms of sets and elements, rather than category theory. However, in contrast to SEAR, this theory is essentially the same structurally as ETCS: as a theory of sets and functions.

In this presentation, we will be adapting Tom Leinster‘s presentation of ETCS.

Basic primitives

Our theory has the following primitives:

  • Some things called sets;

  • For every set AA, these things called elements in AA, with elements aa in AA written as aAa \in A;

  • For every set AA and BB, these things called functions from AA to BB, with functions ff from AA to BB written as f:ABf:A \to B;

  • For every set AA and BB, an operation called function evaluation assigning every element aAa \in A and function f:ABf:A \to B an element f(a)Bf(a) \in B;

  • For every set AA, a function id A:AAid_A:A \to A called the identity function of AA;

  • For every set AA, BB, and CC, an operation called function composition assigning every function f:ABf:A \to B and g:BCg:B \to C a function gf:ACg \circ f:A \to C;

Equality of elements and functions

For every set AA and elements aAa \in A and bAb \in A, there is a relation a=ba = b called equality of elements, such that

  • for every element aAa \in A, a=aa = a
  • for every element aAa \in A and bAb \in A, a=ba = b implies that b=ab = a
  • for every element aAa \in A, bAb \in A, and cAc \in A, a=ba = b and b=cb = c implies that a=ca = c.

For every set AA and BB and functions f:ABf:A \to B and g:ABg:A \to B, there is a relation f=gf = g called equality of functions, such that

  • for every function f:ABf:A \to B, f=ff = f
  • for every function f:ABf:A \to B and g:ABg:A \to B, f=gf = g implies that g=fg = f
  • for every function f:ABf:A \to B, g:ABg:A \to B, and h:ABh:A \to B, f=gf = g and g=hg = h implies that f=hf = h.

Basic axioms for functions

Axiom of identity functions. For every set AA and for every element aAa \in A, id A(a)=aid_A(a) = a.

Axiom of composition/evaluation equivalence. For every set AA, BB, and CC, and for every element aAa \in A, (gf)(a)=g(f(a))(g \circ f)(a) = g(f(a)).

Axiom of extensionality. For every set AA and BB and for every function f:ABf:A \to B and g:ABg:A \to B, if f(x)=g(x)f(x) = g(x) for all elements x:Ax \colon A, then f=gf = g.

The associativity and unit laws of function composition follow from the axioms:

  • For every set AA and BB, function f:ABf:A \to B, and element aAa \in A,

    (gid A)(a)=g(id A(a))=g(a)(g \circ id_A)(a) = g(id_A(a)) = g(a)

    and extensionality implies that gid A=gg \circ id_A = g.

  • For every set AA and BB, function f:ABf:A \to B, and element aAa \in A,

    (id Bg)(a)=id B(g(a))=g(a)(id_B \circ g)(a) = id_B(g(a)) = g(a)

    and extensionality implies that id Bg=gid_B \circ g = g.

  • For every set AA, BB, CC, and DD, function f:ABf:A \to B, g:BCg:B \to C, and h:CDh:C \to D, and element aAa \in A,

    (h(gf))(a)=h((gf)(a))=h(g(f(a))=(hg)(f(a))=((hg)f)(a)(h \circ (g \circ f))(a) = h((g \circ f)(a)) = h(g(f(a)) = (h \circ g)(f(a)) = ((h \circ g) \circ f)(a)

    and extensionality implies that h(gf)=(hg)fh \circ (g \circ f) = (h \circ g) \circ f.

Thus, these axioms imply that the collection of sets, functions, and elements form a category.

Other axioms

Axiom of singletons. There is a set 𝟙\mathbb{1}, called a singleton, with a unique element *𝟙* \in \mathbb{1}, called a point.

Axiom of Cartesian products. For every set AA and BB, there is a set A×BA \times B, called a Cartesian product of AA and BB, with a function p A:A×BAp_A:A \times B \to A called the projection onto AA and a function p B:A×BBp_B:A \times B \to B called the projection onto BB, such that given two elements aAa \in A and bBb \in B there is a unique element a,bA×Ba, b \in A \times B such that p A(a,b)=ap_A(a, b) = a and p B(a,b)=bp_B(a, b) = b.

Axiom of fibers. For every set AA and BB, element bBb \in B, and function f:ABf:A \to B, there is a set f 1(b)f^{-1}(b) called the fiber of ff over bb with a function i:f 1(b)Ai:f^{-1}(b) \to A, such that for every element af 1(b)a \in f^{-1}(b), f(i(a))=bf(i(a)) = b, and for every other set CC and function g:CAg:C \to A such that for every element cCc \in C, f(g(c))=bf(g(c)) = b, there is a unique function j:Cf 1(b)j:C \to f^{-1}(b) such that for every element cCc \in C, g(c)=i(j(c))g(c) = i(j(c)). A fiber of ff over bb is also called the solution set of the equation f(x)=bf(x) = b.

An injection is a function f:ABf:A \to B such that for every element aAa \in A and bAb \in A, if f(a)=f(b)f(a) = f(b), then a=ba = b.

Axiom of truth values. There is a set Ω\Omega called a set of truth values with an element Ω\bot \in \Omega called true such that for every set AA and BB and injection f:ABf:A \to B, there is a unique function χ A:BΩ\chi_A:B \to \Omega called the classifying function of AA such that AA is the fiber of χ A\chi_A over \bot.

Axiom of function sets. For every set AA and BB there is a set B AB^A called the function set with a function ()(()):B A×AB(-)((-)):B^A \times A \to B such that for every set CC and function f:C×ABf:C \times A \to B there is a unique function g:CB Ag:C \to B^A such that for all elements cCc \in C and aAa \in A, g(c)(a)=f(c,a)g(c)(a) = f(c, a).

Axiom of natural numbers. There exists a set \mathbb{N} called a set of natural numbers with an element 00 \in \mathbb{N} and a function s:s:\mathbb{N} \to \mathbb{N} such that for every other set AA with an element aAa \in A and a function g:AAg:A \to A, there is a unique function f:Af:\mathbb{N} \to A such that f(0)=af(0) = a and f(s(a))=g(f(a))f(s(a)) = g(f(a)).

A surjection is a function f:ABf:A \to B such that for every bBb \in B the fiber of ff at bb is inhabited. A right inverse of ff is a function g:BAg:B \to A such that for all elements aAa \in A, f(g(a))=af(g(a)) = a. A choice set is a set BB such that all surjections into BB have right inverses.

Axiom of choice. Every set is a choice set.

These axioms imply that the collection of sets, functions, and elements form a model of ETCS.

See also

References

Last revised on June 7, 2024 at 23:37:44. See the history of this page for a list of all contributions to it.