In mathematics, William Lawvere's elementary theory of abstract categories or ETAC provides an axiomatic construction of the theory of categories and functors in first-order logic.

Axioms

ETAC axioms,

0. For any letters x , y , u , A , B {\displaystyle x,y,u,A,B}, and unary function symbols Δ 0 {\displaystyle \Delta _{0}} and Δ 1 {\displaystyle \Delta _{1}}, and composition law Γ {\displaystyle \Gamma }, the following are defined as formulas: Δ 0 ( x ) = A {\displaystyle \Delta _{0}(x)=A}, Δ 1 ( x ) = B {\displaystyle \Delta _{1}(x)=B}, Γ ( x , y ; u ) {\displaystyle \Gamma (x,y;u)}, and x = y {\displaystyle x=y}; These formulas are to be, respectively, interpreted as “A {\displaystyle A} is the domain of x {\displaystyle x}", “B {\displaystyle B} is the codomain, or range, of x {\displaystyle x}", “u {\displaystyle u} is the composition x {\displaystyle x} followed by y {\displaystyle y}", and “x {\displaystyle x} equals y {\displaystyle y}".

1. If Φ {\displaystyle \Phi } and Ψ {\displaystyle \Psi } are formulas, then “[ Φ ] {\displaystyle [\Phi ]} and [ Ψ ] {\displaystyle [\Psi ]}”, “[ Φ ] {\displaystyle [\Phi ]} or [ Ψ ] {\displaystyle [\Psi ]}”, “[ Φ ] ⇒ [ Ψ ] {\displaystyle [\Phi ]\Rightarrow [\Psi ]}”, and “[ n o t Φ ] {\displaystyle [not\Phi ]}” are also formulas.

2. If Φ {\displaystyle \Phi } is a formula and x {\displaystyle x} is a letter, then “∀ x [ Φ ] {\displaystyle \forall x[\Phi ]}”, “∃ x [ Φ ] {\displaystyle \exists x[\Phi ]}” are also formulas.

3. A string of symbols is a formula in ETAC iff it follows from the above axioms 0 to 2.

A sentence is then defined as any formula in which every occurrence of each letter x {\displaystyle x} is within the scope of a quantifier, such as ∀ x {\displaystyle \forall x} or ∃ x {\displaystyle \exists x}. The theorems of ETAC are defined as all those sentences which can be derived through logical inference from the following ETAC axioms:

4. Δ i ( Δ j ( x ) ) = Δ j ( x ) {\displaystyle \Delta _{i}(\Delta _{j}(x))=\Delta _{j}(x)} for i , j = 0 , 1 {\displaystyle i,j=0,1}.

5a. Γ ( x , y ; u ) {\displaystyle \Gamma (x,y;u)} and Γ ( x , y ; u ′ ) {\displaystyle \Gamma (x,y;u')} ⇒ u = u ′ {\displaystyle \Rightarrow u=u'}.

5b. ∃ u [ Γ ( x , y ; u ) ] ⇒ Δ 1 ( x ) = Δ 0 ( y ) {\displaystyle \exists u[\Gamma (x,y;u)]\Rightarrow \Delta _{1}(x)=\Delta _{0}(y)}.

5c. Γ ( x , y ; u ) ⇒ Δ 0 ( u ) = Δ 0 ( x ) {\displaystyle \Gamma (x,y;u)\Rightarrow \Delta _{0}(u)=\Delta _{0}(x)} and Δ 1 ( u ) = Δ 1 ( y ) {\displaystyle \Delta _{1}(u)=\Delta _{1}(y)}.

6. Identity axiom: Γ ( Δ 0 ( x ) , x ; x ) {\displaystyle \Gamma (\Delta _{0}(x),x;x)} and Γ ( x , Δ 1 ( x ) ; x ) {\displaystyle \Gamma (x,\Delta _{1}(x);x)} yield always the same result.

7. Associativity axiom: Γ ( x , y ; u ) {\displaystyle \Gamma (x,y;u)} and Γ ( y , z ; w ) {\displaystyle \Gamma (y,z;w)} and Γ ( x , w ; f ) {\displaystyle \Gamma (x,w;f)} and Γ ( u , z ; g ) ⇒ f = g {\displaystyle \Gamma (u,z;g)\Rightarrow f=g}.

With these axioms in mind, one can see that commutative diagrams can be now regarded as certain abbreviated formulas corresponding to systems of equations such as: Δ 0 ( f ) = Δ 0 ( h ) = A {\displaystyle \Delta _{0}(f)=\Delta _{0}(h)=A}, Δ 1 ( f ) = Δ 0 ( g ) = B {\displaystyle \Delta _{1}(f)=\Delta _{0}(g)=B}, Δ 1 ( g ) = Δ 1 ( h ) = C {\displaystyle \Delta _{1}(g)=\Delta _{1}(h)=C} and Γ ( f , g ; h ) {\displaystyle \Gamma (f,g;h)}, instead of g ∘ f = h {\displaystyle g\circ f=h} for the arrows f, g, and h, drawn respectively between the `objects' A, B and C, thus forming a `triangular commutative diagram' in the usual sense of category theory. Compared with the ETAC formulas such diagrams have the advantage of a geometric–intuitive image of their equivalent underlying equations.

The common property of A of being an object is written in shorthand as the abbreviated formula Obj(A) standing for the following three equations:

8a. A = Δ 0 ( A ) = Δ 1 ( A ) {\displaystyle A=\Delta _{0}(A)=\Delta _{1}(A)},

8b. ∃ x [ A = Δ 0 ( x ) ] ∃ y [ A = Δ 1 ( y ) ] {\displaystyle \exists x[A=\Delta _{0}(x)]\exists y[A=\Delta _{1}(y)]},

8c. ∀ x ∀ u [ Γ ( x , A ; u ) ⇒ x = u ] {\displaystyle \forall x\forall u[\Gamma (x,A;u)\Rightarrow x=u]} and ∀ y ∀ v [ Γ ( A , y ; v ) ] ⇒ y = v {\displaystyle \forall y\forall v[\Gamma (A,y;v)]\Rightarrow y=v}.

Intuitively, with this terminology and axioms a category is meant to be any structure which is a direct interpretation of ETAC.

A functor is then understood to be a triple consisting of two such categories and of a rule F (`the functor') which assigns to each arrow or morphism x {\displaystyle x} of the first category, a unique morphism, written as `F ( x ) {\displaystyle F(x)}' of the second category, in such a way that the usual two conditions on both objects and arrows in the standard functor definition are fulfilled (see for example [])– the functor is well behaved, it carries object identities to image object identities, and commutative diagrams to image commmutative diagrams of the corresponding image objects and image morphisms.

At the next level, one then defines natural transformations or functorial morphisms between functors as metalevel abbreviated formulas and equations pertaining to commutative diagrams of the distinct images of two functors acting on both objects and morphisms. As the name indicates natural transformations are also well–behaved in terms of the ETAC equations satisfied.

See also

Notes

This article incorporates text from this source, which is available under the CC BY-SA 4.0 license. The original text was imported from The conversion to a wikitext was done by ChatGPT under a supervision; except the formatting, there is no change made by ChatGPT.

  • Brown, Ronald; Spencer, Christopher B. (1976). (PDF). Cahiers de Topologie et Géométrie Différentielle Catégoriques. 17 (4): 343–362 – via numdam.
  • Lawvere, F. William (November 1963). . Proceedings of the National Academy of Sciences. 50 (5): 869–872. doi:. PMID . Lawvere, F. William (2004). (PDF). Reprints in Theory and Applications of Categories. 5: 1–121.
  • Lawvere, F. William (1966). "The Category of Categories as a Foundation for Mathematics". (PDF). pp. 1–20. doi:. ISBN 978-3-642-99904-8 – via lawverearchives.com.

Further reading

  • Elaine Landry, Categories for the Working Philosopher,