Alphabeta Math
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 35 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 35 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Categories, Functors and Natural Transformations

1 · Prerequisites

2 · Summary

Sets and functions, groups and homomorphisms, unital rings, vector spaces, modules, topological spaces, and posets provide the recurring examples. The development uses product topology and continuity, linear and module maps, group actions, the fundamental group, the Axiom of Choice, and Burali–Forti's size obstruction to keep large-category claims inside ZFC's definable-class convention.

A category packages identities and associative composition; opposite categories lead to duality, while isomorphisms, monomorphisms, epimorphisms, zero objects, and zero morphisms describe special arrows and objects. Functors preserve structure, natural transformations compose vertically and horizontally, and interchange organizes small categories into a strict 2-category. Natural isomorphisms then distinguish equivalence from strict isomorphism, with split essential surjectivity giving a choice-free criterion and Choice supplying skeletons and selected representatives.

3 · Logical flowchart

4 · Definitions, theorems and proofs

RemarkRemark: AI-adaptedProof: Not applicableaudited 2026-08-11Open item page →

Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why CAT is not formed

The word class in this development is an abbreviation for a formula in the language of set theory, as described by The first-order language of set theory: ∈, =, formulas with parameters, and class abbreviations. It is not an additional set. A category may therefore have a definable class of objects and a definable class of morphisms. Quantification over such a category is a schema: each use expands to an ordinary formula of ZFC.

A category is small when its objects and morphisms form sets, and locally small when each hom-collection is a set. The category Cat used below has small categories as objects; its hom-categories are sets or locally small categories as asserted in the relevant result. We do not form a category CAT of all large categories. Doing so as though all classes were members of a larger set would conflict with the same size obstruction exhibited for the ordinals by Burali-Forti: there is no set of all ordinals. Class recursion, when used, is only the definable schema licensed by Transfinite recursion.

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-11Open item page →

Category, object, morphism, domain, codomain, identity, composition, and hom-collection

Definition

Under the definable-class convention of Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why CAT is not formed, every class below is a formula and every function whose domain may be proper-class-sized is a definable class-function schema. When its domain is a set, it is an ordinary set-valued function.

A category C consists of a class Ob⁡(C) of objects, a class Mor⁡(C) of morphisms, functions dom⁡,cod⁡:Mor⁡(C)→Ob⁡(C), an identity morphism 1A:A→A for every object A, and a composite g∘f:A→C whenever f:A→B and g:B→C.

These data satisfy, whenever the composites are defined,

h∘(g∘f)=(h∘g)∘f,1B∘f=f=f∘1A.

We write C(A,B), or Hom⁡C(A,B), for the hom-collection of morphisms with domain A and codomain B. The object class is allowed to be empty; then the morphism class is empty and all axioms are vacuous.

Morphisms carry their domain and codomain. A category is often presented the other way round, by saying what the morphisms from A to B are for each pair of objects. When it is, Mor⁡(C) is the disjoint union of those hom-collections: a morphism is a triple (A,B,f) with f in the collection assigned to (A,B), and dom⁡ and cod⁡ are the first two projections, which are then functions in the required sense. This is not a technicality that can be dropped. In this library a function is a set of ordered pairs and does not determine a codomain (A function is a relation f with (a,b)∈f and (a,c)∈f implying b=c; f:A→B, the value f(a), domain and codomain), so the empty function is a function ∅→B for every B at once; reading the morphisms of Set as bare functions would give that one set two different codomains and leave cod⁡ undefined. Every concrete category below whose morphisms are described as structure-preserving maps is to be read with this tagging, and each hom-collection is then in canonical bijection with the corresponding collection of untagged maps, so no size or smallness claim is affected.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Small, locally small, and large categories

Definition

Let C be a category (Category, object, morphism, domain, codomain, identity, composition, and hom-collection) under the class convention of Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why CAT is not formed.

  • C is small when both Ob⁡(C) and Mor⁡(C) are sets.
  • C is locally small when every C(A,B) is a set.
  • C is large when it is not small.

A small category is locally small because each hom-collection is a subclass of the set of all morphisms. A large category may or may not be locally small.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Subcategory and full subcategory

Definition

A subcategory A of a category C (Category, object, morphism, domain, codomain, identity, composition, and hom-collection) has a subclass of the objects of C and, for each A,B∈A, a subclass A(A,B)⊆C(A,B). It contains the identities of its objects and is closed under the composition inherited from C.

The subcategory is full when A(A,B)=C(A,B) for every pair of its objects. Thus a full subcategory is determined entirely by its objects.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Sets and functions form the large locally small category Set

Statement

Sets as objects and functions as morphisms form a large locally small category Set.

Facts & Assumptions

Given: Sets A,B,C and functions f:A→B, g:B→C.

[L1]

A category has associative composition and an identity at every object, and when it is presented by its hom-collections a morphism is the triple (A,B,f), so that dom⁡ and cod⁡ are the projections (Category, object, morphism, domain, codomain, identity, composition, and hom-collection); a function is a set of ordered pairs with a set domain and a uniquely determined value at each point of it, and does not itself determine a codomain (A function is a relation f with (a,b)∈f and (a,c)∈f implying b=c; f:A→B, the value f(a), domain and codomain); the functions A→B form the set BA (The set BA of all functions A→B).

[L2]

Small, locally small, and large have the meanings in Small, locally small, and large categories, and the ordinals do not form a set (Burali-Forti: there is no set of all ordinals).

Proof

technique · direct
1.1

Identity functions are functions, composites of functions are functions, function composition is associative, and 1B∘f=f=f∘1A.

givenL1
2.1

Hence sets and functions satisfy every axiom of a category.

step 1.1L1
3.1

For fixed A,B, the hom-collection is {(A,B,f):f∈BA}, a set in bijection with the set BA from [L1]; the tagging is what gives each morphism a unique codomain, since the empty function alone would be a morphism into every set. The object class contains every ordinal and therefore is not a set, so Set is locally small and large.

step 2.1L1L2∎
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Groups and group homomorphisms form the large locally small category Grp

Statement

Groups and group homomorphisms form a large locally small category Grp.

Facts & Assumptions

Given: Groups G,H,K and homomorphisms f:G→H, g:H→K.

[L1]

Groups are sets with the group operations (Group and abelian group), and identity maps and composites of group homomorphisms are group homomorphisms (Monoid homomorphism and group homomorphism).

[L2]

The functions A→B between fixed sets form the set BA (The set BA of all functions A→B); the category and size conditions are Category, object, morphism, domain, codomain, identity, composition, and hom-collection and Small, locally small, and large categories, while the ordinals form a proper class (Burali-Forti: there is no set of all ordinals).

Proof

technique · direct
1.1

By [L1], identity maps and composites remain group homomorphisms; their associativity and unit equations are the corresponding equations for functions.

givenL1
2.1

Thus the group objects and homomorphisms satisfy the category axioms, and each hom-collection is a set of functions between two fixed underlying sets.

step 1.1L2
3.1

For every ordinal α, the singleton {α} carries a transported trivial group structure, and distinct ordinals give distinct group objects; [L2] therefore rules out a set of all group objects, so Grp is large and locally small.

step 2.1L2∎
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Unital rings and unit-preserving ring homomorphisms form the large locally small category Ring

Statement

Unital rings and unit-preserving ring homomorphisms form a large locally small category Ring.

Facts & Assumptions

Given: Unital rings R,S,T and unit-preserving homomorphisms f:R→S and g:S→T.

[L1]

A ring is an additive abelian group and multiplicative monoid with both distributive laws (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides); a ring homomorphism preserves addition, multiplication, zero, and one (Ring homomorphism: additive, multiplicative, and required to send 1 to 1).

[L2]

The functions A→B between fixed sets form the set BA (The set BA of all functions A→B); the category and size conditions are Category, object, morphism, domain, codomain, identity, composition, and hom-collection and Small, locally small, and large categories, and the ordinals form a proper class (Burali-Forti: there is no set of all ordinals).

Proof

technique · direct
1.1

The identity of a ring preserves both operations and the unit, and g∘f preserves them because f and g do; function composition supplies associativity and identity equations.

givenL1
2.1

These data form a category, and every hom-collection is a set because it is a subset of the functions between the two underlying sets.

step 1.1L2
3.1

For each ordinal α, the one-element set {α} carries the zero-ring structure with 0=1=α; these are distinct objects, so [L2] shows that Ring is large and locally small.

step 2.1L1L2∎
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Vector spaces over a fixed field and linear maps form the large locally small category VectF

Statement

For a fixed field F, vector spaces over F and linear maps form a large locally small category VectF.

Facts & Assumptions

Given: F-vector spaces U,V,W and linear maps S:U→V, T:V→W.

[L1]

The vector-space axioms are those of Vector space over a field, and a linear map preserves vector addition and scalar multiplication (Linear map between vector spaces over the same field).

[L2]

Proof

technique · direct
1.1

Identity maps preserve addition and scalar multiplication, and T∘S does so by applying linearity first to S and then to T; composition is associative and unital as function composition.

givenL1
2.1

Hence F-vector spaces and linear maps form a category, and every hom-collection is a set of functions.

step 1.1L2
3.1

Each singleton {α}, for an ordinal α, carries a transported zero-dimensional F-vector-space structure; these distinct objects and [L2] show that VectF is large and locally small.

step 2.1L1L2∎
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Left modules over a fixed ring and module homomorphisms form the large locally small category R-Mod

Statement

For a fixed ring R, left R-modules and module homomorphisms form a large locally small category R-Mod.

Facts & Assumptions

Given: Left R-modules M,N,P and module homomorphisms f:M→N, g:N→P.

[L1]

Left modules satisfy the axioms in Unital left and right modules over a ring; unqualified module means left module, and module homomorphisms preserve addition and scalar multiplication (Module homomorphism and isomorphism, kernel, image and cokernel).

[L2]

The functions A→B between fixed sets form the set BA (The set BA of all functions A→B); the category and size notions are Category, object, morphism, domain, codomain, identity, composition, and hom-collection and Small, locally small, and large categories, and the ordinals form a proper class (Burali-Forti: there is no set of all ordinals).

Proof

technique · direct
1.1

Identity maps are module homomorphisms, and g∘f preserves addition and scalar multiplication by the two homomorphism laws; function composition is associative and unital.

givenL1
2.1

Thus left R-modules and their homomorphisms form a category whose hom-collections are sets.

step 1.1L2
3.1

For every ordinal α, the singleton {α} carries a transported zero R-module structure, producing a proper class of distinct objects by [L2]; hence R-Mod is large and locally small.

step 2.1L1L2∎
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Topological spaces and continuous maps form the large locally small category Top

Statement

Topological spaces and continuous maps form a large locally small category Top.

Facts & Assumptions

Given: Topological spaces X,Y,Z and continuous maps f:X→Y, g:Y→Z.

[L1]

A topology is the structure in Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison, and identity maps and composites of continuous maps are continuous by the inverse-image definition in Continuity of a map of topological spaces at a point and globally.

Proof

technique · direct
1.1

Identity maps and g∘f are continuous by [L1], while associativity and unit equations are those of function composition.

givenL1
2.1

Consequently spaces and continuous maps form a category, and each hom-collection is a set of functions between fixed underlying sets.

step 1.1L2
3.1

Every singleton {α}, for an ordinal α, has its unique topology; these give distinct space objects, so [L2] makes Top large and locally small.

step 2.1L1L2∎
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Posets and monotone maps form the large locally small category Poset

Statement

Partially ordered sets and monotone maps form a large locally small category Poset.

Facts & Assumptions

Given: Posets P,Q,R and monotone maps f:P→Q, g:Q→R.

[L1]

Partial orders are reflexive, antisymmetric, and transitive (Partial order and partially ordered set); a composite of monotone maps is monotone by transitivity of implication.

Proof

technique · direct
1.1

Identity maps are monotone, and x≤y gives f(x)≤f(y) and then g(f(x))≤g(f(y)), so g∘f is monotone; composition is associative and unital as function composition.

givenL1
2.1

Hence posets and monotone maps form a category whose hom-collections are sets of functions.

step 1.1L2
3.1

Each singleton {α} has its equality order, and ordinals yield a proper class of distinct such posets by [L2]; therefore Poset is large and locally small.

step 2.1L1L2∎
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible

Statement

Every monoid is a one-object category. Under this identification, the monoid is a group exactly when every morphism is invertible.

Facts & Assumptions

Given: A monoid (M,⋅,e).

[L1]

A monoid has associative multiplication and a two-sided identity (Semigroup and monoid), exactly the composition and identity laws required by Category, object, morphism, domain, codomain, identity, composition, and hom-collection.

[L2]

A group is a monoid in which every element has a two-sided inverse (Group and abelian group).

Proof

technique · direct
1.1

Take one object ∗, put Hom⁡(∗,∗)=M, define composition by y∘x=y⋅x, and take 1∗=e; [L1] verifies the category axioms.

givenL1
2.1

A morphism x:∗→∗ is an isomorphism precisely when some y satisfies yx=e=xy.

step 1.1L1
3.1

By [L2], every morphism in this one-object category is invertible exactly when M is a group.

step 2.1L2∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Preorder and monotone map

Definition

A preorder on a set P is a relation ≤ that is reflexive and transitive. Unlike a partial order (Partial order and partially ordered set), it need not be antisymmetric.

A map f:P→Q between preorders is monotone when x≤Py implies f(x)≤Qf(y). Every partial order is a preorder, and the definition of monotone map agrees with the usual one for partially ordered sets.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

A preorder is a category with at most one morphism between any two objects, and its functors are exactly monotone maps

Statement

A preorder determines a category with at most one morphism between any two objects, and functors between such categories are exactly monotone maps.

Facts & Assumptions

Given: Preorders (P,≤P) and (Q,≤Q).

[L1]

A preorder is reflexive and transitive, and a monotone map preserves its relation (Preorder and monotone map).

[L2]

Category identities and composition have the meanings of Category, object, morphism, domain, codomain, identity, composition, and hom-collection. In this proposition, a functor is an assignment on objects and arrows that preserves identities and composition.

Proof

technique · direct
1.1

Make the elements of P objects and put one morphism x→y when x≤Py, and none otherwise; reflexivity supplies identities and transitivity supplies the unique possible composites, so [L1] gives a category.

givenL1L2
2.1

A function F:P→Q extends to a functor exactly when x≤Py guarantees a target morphism F(x)→F(y), which is exactly F(x)≤QF(y).

step 1.1L1L2
3.1

Thus the functors between the associated categories are precisely the monotone maps, with no extra arrow choices because every relevant hom-collection has at most one member.

step 2.1L1∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Opposite category Cop

Definition

For a category C (Category, object, morphism, domain, codomain, identity, composition, and hom-collection), the opposite category Cop has the same objects and reverses every morphism:

Cop(A,B)=C(B,A).

The identity at A remains 1A. If fop:B→A and gop:C→B correspond to f:A→B and g:B→C in C, define fop∘opgop=(g∘f)op. Associativity and the identity laws follow directly from those of C, so this prescription is a category. Moreover (Cop)op=C strictly.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Every theorem about categories has a formal dual obtained by reversing morphisms and composition

Statement

A formal theorem derivable solely from the category axioms has a formal dual: reverse every morphism, reverse the order of every composite, and exchange each defined notion with its opposite-category version.

Facts & Assumptions

Given: A derivation in the formal language of categories.

[L1]

Passing from C to Cop reverses arrows and composition, preserves identities, and is involutive (Opposite category Cop).

Proof

technique · direct
1.1

Translate every typed arrow f:A→B to fop:B→A, every g∘f to fop∘opgop, and leave equality and logical connectives unchanged.

givenL1
2.1

Under this translation, each category axiom becomes the corresponding category axiom in the opposite category, so every permitted inference in the original derivation remains a permitted inference after translation.

step 1.1L1
3.1

Translating the complete derivation therefore proves the translated conclusion; applying the translation twice returns the original theorem.

step 2.1L1∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Isomorphism, groupoid, and connected category

Definition

In a category C (Category, object, morphism, domain, codomain, identity, composition, and hom-collection), a morphism f:A→B is an isomorphism if there is a morphism g:B→A with g∘f=1A and f∘g=1B. Such a g is unique and is denoted f−1.

A groupoid is a category in which every morphism is an isomorphism. A category is connected when it is nonempty and any two objects can be joined by a finite zigzag of morphisms, with successive arrows allowed to point in either direction. In a groupoid this is equivalent to being nonempty and having an isomorphism between every ordered pair of objects. Nonemptiness cannot be dropped: the empty groupoid has an isomorphism between every ordered pair of its objects, vacuously, and is not connected.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

The isomorphisms in a category form its maximal subgroupoid

Statement

For every category C, the subcategory with all objects and exactly the isomorphisms as morphisms is a groupoid, and it contains every subgroupoid of C.

Facts & Assumptions

Given: A category C.

[L1]

Isomorphisms and groupoids are defined in Isomorphism, groupoid, and connected category, and category composition is associative and unital (Category, object, morphism, domain, codomain, identity, composition, and hom-collection).

Proof

technique · direct
1.1

Identities are isomorphisms, and if f and g are composable isomorphisms then g∘f has inverse f−1∘g−1, so the isomorphisms form a subcategory.

givenL1
2.1

Every morphism of this subcategory is invertible by construction, hence it is a groupoid.

step 1.1L1
3.1

If G is any subgroupoid contained in C, every morphism of G has its two-sided inverse in C and is therefore an isomorphism of C; thus G lies in this subgroupoid, proving maximality.

step 2.1L1∎
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

A morphism is an isomorphism exactly when postcomposition, equivalently precomposition, induces bijections on every hom-collection

Statement

For a morphism f:A→B, the following are equivalent: f is an isomorphism; for every object X, postcomposition f∘−:C(X,A)→C(X,B) is bijective; and for every X, precomposition −∘f:C(B,X)→C(A,X) is bijective.

Facts & Assumptions

Given: A morphism f:A→B in a category C.

[L1]

Isomorphisms have two-sided inverses (Isomorphism, groupoid, and connected category), and a map is bijective exactly when it has a two-sided inverse (Injection, surjection, bijection).

[L2]

Reversing arrows exchanges postcomposition with precomposition (Every theorem about categories has a formal dual obtained by reversing morphisms and composition).

Proof

technique · direct
1.1

If f has inverse f−1, postcomposition by f−1 is a two-sided inverse to postcomposition by f, and similarly precomposition by f−1 inverts precomposition by f; both maps are bijections.

givenL1
2.1

Conversely, suppose every postcomposition map is bijective. Surjectivity at X=B gives g:B→A with f∘g=1B; injectivity at X=A applied to f∘(g∘f)=f=f∘1A gives g∘f=1A, so f is an isomorphism.

step 1.1L1
3.1

The identical argument in Cop, using [L2], proves that bijectivity of every precomposition map also characterises isomorphisms.

step 2.1L2∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Monomorphism and epimorphism by left and right cancellation

Definition

Let f:A→B be a morphism in a category (Category, object, morphism, domain, codomain, identity, composition, and hom-collection).

  • f is a monomorphism, or monic, when f∘g=f∘h implies g=h for every parallel pair g,h:X→A.
  • f is an epimorphism, or epic, when g∘f=h∘f implies g=h for every parallel pair g,h:B→Y.

Thus monomorphisms are left-cancellable and epimorphisms are right-cancellable. The definitions are formally dual.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Split monomorphism, split epimorphism, retraction, and section

Definition

Let f:A→B be a morphism.

If there is r:B→A with r∘f=1A, then f is a split monomorphism and a section, while r is a retraction of f. If there is s:B→A with f∘s=1B, then f is a split epimorphism and a retraction, while s is a section of f.

When both identities hold, f and its splitting are inverse isomorphisms in the sense of Isomorphism, groupoid, and connected category.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Identities and composites of monomorphisms or epimorphisms retain cancellation; split monomorphisms are monic and split epimorphisms are epic

Statement

Identity morphisms are monic and epic; composites of monomorphisms are monic, composites of epimorphisms are epic; every split monomorphism is monic, and every split epimorphism is epic.

Facts & Assumptions

Given: Composable morphisms in a category.

[L1]

Monomorphisms and epimorphisms are defined by left and right cancellation (Monomorphism and epimorphism by left and right cancellation).

[L2]

A split monomorphism has a left inverse and a split epimorphism has a right inverse (Split monomorphism, split epimorphism, retraction, and section); the two halves are dual by Every theorem about categories has a formal dual obtained by reversing morphisms and composition.

Proof

technique · direct
1.1

Identities cancel trivially; if f and g are monic and (g∘f)u=(g∘f)v, cancellation by g and then by f gives u=v, so composites of monomorphisms are monic.

givenL1
2.1

Applying the dual argument of [L2] proves that identities and composites of epimorphisms are epic.

step 1.1L1L2
3.1

If r∘f=1, then fu=fv implies u=rfu=rfv=v, so a split monomorphism is monic; dually, f∘s=1 makes a split epimorphism epic.

step 2.1L1L2∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

In Set, monomorphisms are exactly injections and epimorphisms are exactly surjections

Statement

In Set, a function is monic exactly when it is injective, and it is epic exactly when it is surjective.

Facts & Assumptions

Given: A function f:A→B regarded as a morphism of Set.

[L1]

The morphisms of Set are functions (Sets and functions form the large locally small category Set), monic and epic mean cancellation (Monomorphism and epimorphism by left and right cancellation), and injective, surjective, and bijective have their usual fibrewise meanings (Injection, surjection, bijection).

Proof

technique · direct
1.1

If f is injective, f∘g=f∘h implies g=h pointwise, so f is monic; if f is not injective, choose a0≠a1 with f(a0)=f(a1), and the two maps from a singleton selecting a0,a1 show that f is not monic.

givenL1
2.1

If f is surjective and g∘f=h∘f, then for each b∈B choose an a only for this fixed b with f(a)=b, giving g(b)=h(b); hence g=h and f is epic.

step 1.1L1
3.1

If f is not surjective, let g:B→{0,1} be constantly 0 and let h be 0 on f[A] and 1 outside f[A]; then g≠h but g∘f=h∘f, so f is not epic.

step 2.1L1∎
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Under the Axiom of Choice, every epimorphism in Set is a split epimorphism

Statement

Assume the Axiom of Choice. Every epimorphism in Set is a split epimorphism.

Facts & Assumptions

Given: An epimorphism p:X→Y in Set.

[L2]

The Axiom of Choice selects an element from every member of a set-indexed family of nonempty sets (The Axiom of Choice), and a split epimorphism has a right inverse (Split monomorphism, split epimorphism, retraction, and section).

Proof

technique · direct
1.1

By [L1], every fibre p−1({y}) for y∈Y is nonempty.

givenL1
2.1

By [L2], choose s(y)∈p−1({y}) for every y∈Y; if Y is empty this is the unique empty function, so the same construction covers that boundary case.

step 1.1L2choose
3.1

Then p(s(y))=y for every y, so p∘s=1Y and p is split epic.

step 2.1L2∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

The inclusion Z↪Q is monic and epic but neither surjective nor an isomorphism in Ring

Statement

In Ring, the canonical inclusion i:Z↪Q is monic and epic, but its underlying function is not surjective and it is not an isomorphism.

Facts & Assumptions

Given: The canonical unital ring homomorphism i:Z→Q.

[L1]

The integers form a commutative ring (The integers form a commutative ring), the rationals form a field and hence a commutative ring (The rationals form a field, Every field is a commutative ring with 1≠0; it is an integral domain, and it is a commutative division ring), and The integers embed in the rationals identifies i as an injective embedding.

[L2]

Morphisms of Ring are unit-preserving ring homomorphisms (Unital rings and unit-preserving ring homomorphisms form the large locally small category Ring); monic, epic, and isomorphism mean cancellation and a two-sided inverse (Monomorphism and epimorphism by left and right cancellation, Isomorphism, groupoid, and connected category).

Proof

technique · direct
1.1

If i∘u=i∘v, injectivity of i gives u=v pointwise, so i is monic.

givenL1L2
2.1

If ring homomorphisms f,g:Q→R agree after i, then for q=a/b with b≠0 both send q to the common image of a times the inverse of the common image of b; hence f(q)=g(q) for every q, so i is epic.

step 1.1L1L2
3.1

The rational 1/2 is not an integer, so the underlying function of i is not surjective; a categorical inverse would be an inverse function and would force surjectivity, so i is not an isomorphism.

step 2.1L1L2∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Initial object, terminal object, and zero object

Definition

In a category C (Category, object, morphism, domain, codomain, identity, composition, and hom-collection), an object I is initial when for every object A there is exactly one morphism I→A. An object T is terminal when for every A there is exactly one morphism A→T. These notions are dual under Every theorem about categories has a formal dual obtained by reversing morphisms and composition.

A zero object is an object that is both initial and terminal. The definition does not choose a particular zero object when several distinct but isomorphic ones occur.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Category with zero morphisms

Definition

A category with zero morphisms is a category C (Category, object, morphism, domain, codomain, identity, composition, and hom-collection) equipped with a specified morphism 0A,B:A→B for every ordered pair of objects such that, for all f:A′→A and g:B→B′,

0A,B∘f=0A′,B,g∘0A,B=0A,B′.

The family is part of the structure. Merely naming an isolated morphism as zero does not supply zero morphisms.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

A zero object supplies a unique compatible system of zero morphisms

Statement

A chosen zero object 0 in a category supplies a unique compatible system of zero morphisms.

Facts & Assumptions

Given: A zero object 0 in a category C.

[L1]

A zero object is both initial and terminal, so there are unique arrows A→0 and 0→B for every A,B (Initial object, terminal object, and zero object).

[L2]

A system of zero morphisms must absorb composition on either side (Category with zero morphisms).

Proof

technique · direct
1.1

Define 0A,B as the composite of the unique arrows A→0 and 0→B supplied by [L1].

givenL1
2.1

For f:A′→A, both 0A,B∘f and 0A′,B factor through 0 using the unique arrow A′→0, so they are equal; the same uniqueness proves g∘0A,B=0A,B′.

step 1.1L1L2
3.1

Any compatible zero family must have 0A,B=00,B∘0A,0, and both factors are the unique arrows to and from 0, so the family of step 1.1 is unique.

step 2.1L1L2∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Covariant functor, identity functor, composite functor, and contravariant functor

Definition

For categories C,D (Category, object, morphism, domain, codomain, identity, composition, and hom-collection), a covariant functor F:C→D assigns an object FA to every object A and a morphism Ff:FA→FB to every f:A→B, satisfying

F(1A)=1FA,F(g∘f)=Fg∘Ff.

The identity functor acts identically on objects and morphisms. For F:C→D and G:D→E, the composite functor GF has (GF)A=G(FA) and (GF)f=G(Ff).

A contravariant functor from C to D means a covariant functor Cop→D, using Opposite category Cop.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Every functor preserves isomorphisms

Statement

Every functor sends isomorphisms to isomorphisms.

Facts & Assumptions

Given: A functor F:C→D and an isomorphism f:A→B.

[L1]

Functors preserve identities and composition (Covariant functor, identity functor, composite functor, and contravariant functor), and an isomorphism has a two-sided inverse (Isomorphism, groupoid, and connected category).

Proof

technique · direct
1.1

Let g:B→A satisfy g∘f=1A and f∘g=1B.

givenL1
2.1

Functoriality gives F(g)∘F(f)=F(1A)=1FA and F(f)∘F(g)=F(1B)=1FB.

step 1.1L1
3.1

Thus F(g) is a two-sided inverse of F(f), so F(f) is an isomorphism.

step 2.1L1∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors

Definition

Let F:C→D be a functor (Covariant functor, identity functor, composite functor, and contravariant functor). For each A,B, it induces

FA,B:C(A,B)→D(FA,FB),f↦Ff.

The functor is faithful when every FA,B is injective, full when every FA,B is surjective, and fully faithful when every FA,B is bijective (Injection, surjection, bijection).

It is essentially surjective when every object D of D is isomorphic to some FC (Isomorphism, groupoid, and connected category). It is split essentially surjective when the data include, for every D, a specified object CD and specified isomorphism εD:FCD→D. The word split records these witnesses and is strictly stronger as data than their mere existence.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Embedding and full embedding of categories

Definition

An embedding of categories is a functor that is faithful and injective on objects. A full embedding is an embedding that is also full. These terms use the notions of Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors.

Thus a fully faithful functor need not be an embedding: it may send distinct but isomorphic objects to the same object. Conversely, an embedding need not be full.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Every fully faithful functor reflects isomorphisms

Statement

If F:C→D is fully faithful and F(f) is an isomorphism, then f is an isomorphism.

Facts & Assumptions

Given: A fully faithful functor F and a morphism f:A→B such that F(f) is invertible.

[L1]

Fullness lifts every morphism between FA and FB, while faithfulness reflects equality between parallel morphisms (Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors).

[L2]

An isomorphism has a two-sided inverse (Isomorphism, groupoid, and connected category).

Proof

technique · direct
1.1

Let h:FB→FA be the inverse of F(f); fullness gives g:B→A with F(g)=h.

givenL1L2
2.1

Then F(g∘f)=h∘F(f)=1FA=F(1A) and F(f∘g)=F(f)∘h=1FB=F(1B).

step 1.1L1L2
3.1

Faithfulness gives g∘f=1A and f∘g=1B, so f is an isomorphism.

step 2.1L1L2∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Natural transformation and its components

Definition

Let F,G:C→D be functors (Covariant functor, identity functor, composite functor, and contravariant functor). A natural transformation α:F⇒G is a family of morphisms αA:FA→GA, one for each object A of C, such that every f:A→B satisfies the naturality equation

Gf∘αA=αB∘Ff.

The morphism αA is the component of α at A.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Identity natural transformation and vertical composition

Definition

For a functor F:C→D, the identity natural transformation 1F:F⇒F has component (1F)A=1FA.

For natural transformations α:F⇒G and β:G⇒H (Natural transformation and its components), their vertical composite β∘α:F⇒H is defined componentwise by

(β∘α)A=βA∘αA.

The fact that this componentwise family is natural is discharged by Vertical composites of natural transformations satisfy naturality ↗.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Vertical composites of natural transformations satisfy naturality

Statement

The vertical composite of two natural transformations satisfies the naturality equation.

Facts & Assumptions

Given: Natural transformations α:F⇒G and β:G⇒H, and a morphism f:A→B.

[L1]

Vertical composition is componentwise, and α,β satisfy their naturality equations (Identity natural transformation and vertical composition).

Proof

technique · direct
1.1

By naturality, Gf∘αA=αB∘Ff and Hf∘βA=βB∘Gf.

givenL1
2.1

Therefore Hf∘(βA∘αA)=(βB∘Gf)∘αA=βB∘(αB∘Ff)=(βB∘αB)∘Ff.

step 1.1L1
3.1

This is the naturality equation for the componentwise family β∘α.

step 2.1L1∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Whiskering and horizontal composition of natural transformations

Definition

Let α:F⇒G:C→D be a natural transformation (Natural transformation and its components), and let H:D→E and K:B→C be functors (Covariant functor, identity functor, composite functor, and contravariant functor). The left whiskering Hα:HF⇒HG has components H(αA), and the right whiskering αK:FK⇒GK has components αKB.

For β:H⇒L:D→E, the horizontal composite β∗α:HF⇒LG has either equal component formula

(β∗α)A=βGA∘H(αA)=L(αA)∘βFA.

Their equality is the naturality equation for β at αA. Naturality of the resulting family is proved in Horizontal composites of natural transformations satisfy naturality ↗.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Horizontal composites of natural transformations satisfy naturality

Statement

The horizontal composite of natural transformations satisfies the naturality equation.

Facts & Assumptions

Given: Natural transformations α:F⇒G:C→D and β:H⇒L:D→E, and f:A→B in C.

[L1]

Horizontal composition has component βGA∘H(αA)=L(αA)∘βFA, and functors preserve composition (Whiskering and horizontal composition of natural transformations).

Proof

technique · direct
1.1

Naturality of β at Gf gives L(Gf)∘βGA=βGB∘H(Gf), while functoriality sends the naturality equation Gf∘αA=αB∘Ff to H(Gf)∘H(αA)=H(αB)∘H(Ff).

givenL1
2.1

Combining these equations gives L(Gf)∘βGA∘H(αA)=βGB∘H(αB)∘H(Ff).

step 1.1L1
3.1

The two outer composites are exactly L(Gf)∘(β∗α)A and (β∗α)B∘H(Ff), which proves naturality.

step 2.1L1∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Horizontal and vertical composition of natural transformations satisfy the interchange law

Statement

Whenever the expressions are defined,

(β′∘β)∗(α′∘α)=(β′∗α′)∘(β∗α).

Thus horizontal and vertical composition of natural transformations satisfy the interchange law.

Facts & Assumptions

Given: Natural transformations α:F⇒G, α′:G⇒K:C→D and β:H⇒L, β′:L⇒M:D→E.

[L1]

Vertical composition is componentwise and its composites are natural (Identity natural transformation and vertical composition, Vertical composites of natural transformations satisfy naturality); horizontal composition has the standard component formula and its composites are natural (Whiskering and horizontal composition of natural transformations, Horizontal composites of natural transformations satisfy naturality).

Proof

technique · direct
1.1

At an object A, expand the left side by [L1] as βKA′∘βKA∘H(αA′)∘H(αA).

givenL1
2.1

Naturality of β at αA′:GA→KA gives βKA∘H(αA′)=L(αA′)∘βGA. Substitution turns step 1.1 into (βKA′∘L(αA′))∘(βGA∘H(αA)).

step 1.1L1
3.1

The two parenthesised factors are the A-components of β′∗α′ and β∗α, so every component agrees with the right side and the transformations are equal.

step 2.1L1∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Product category and its projection functors

Definition

For categories C and D (Category, object, morphism, domain, codomain, identity, composition, and hom-collection), their product category C×D has objects (C,D), morphisms (f,g):(C,D)→(C′,D′), componentwise identities, and componentwise composition

(f′,g′)∘(f,g)=(f′∘f,g′∘g).

The category axioms hold componentwise. The projection functors πC and πD send an object or morphism to its corresponding component, and satisfy the functor laws of Covariant functor, identity functor, composite functor, and contravariant functor componentwise.

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-11Open item page →

Functor category [C,D]

Definition

Within the definable-class convention of Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why CAT is not formed, the construction below is formed when the source category C is small. Then a functor out of C and a natural transformation between two such functors are set-coded data, so they can be objects and morphisms of a category in ZFC.

For categories C,D, the functor category [C,D] has functors C→D as objects and natural transformations as morphisms (Natural transformation and its components). Its identities and composition are the identity transformations and vertical composition. These are the operations of Identity natural transformation and vertical composition.

Closure under composition is Vertical composites of natural transformations satisfy naturality. Associativity and the identity laws hold at each component because they hold in D. Further smallness and local-smallness properties of this category are stated separately.

For an arbitrary large source C, the same notation may be used only as metatheoretic shorthand for functors and natural transformations; this definition does not form those proper-class-sized data into a category.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

If C is small and D is locally small then [C,D] is locally small; if both are small it is small

Statement

If C is small and D is locally small, then [C,D] is locally small. If both C and D are small, then [C,D] is small.

Facts & Assumptions

Given: Categories C,D with the stated size hypotheses.

[L1]

The objects and morphisms of [C,D] are functors and natural transformations (Functor category [C,D]).

[L2]

Smallness and local smallness mean set-sized object, morphism, and hom-collections as specified in Small, locally small, and large categories.

Proof

technique · direct
1.1

For fixed functors F,G, a natural transformation is a family in the set-indexed product ∏C∈Ob⁡CD(FC,GC) satisfying a set of naturality equations; smallness of C and local smallness of D make this a set.

givenL1L2
2.1

Hence every hom-collection of [C,D] is a set, so the functor category is locally small.

step 1.1L1L2
3.1

If D is also small, the possible object and morphism functions of a functor lie in set-sized function spaces, and the functor equations define a subset; the union of the set-sized natural-transformation sets is then a set, so [C,D] is small.

step 2.1L1L2∎
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-11Open item page →

Natural isomorphism

Definition

A natural isomorphism α:F⇒G is a natural transformation for which there is a natural transformation β:G⇒F with β∘α=1F and α∘β=1G. The compositions here are the vertical compositions of Identity natural transformation and vertical composition.

When the source category is small, so that Functor category [C,D] is formed, this says exactly that α is an isomorphism from F to G in that functor category. Thus the definition combines Natural transformation and its components with the categorical notion of isomorphism from Isomorphism, groupoid, and connected category without requiring a functor category for an arbitrary large source.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

A natural transformation is a natural isomorphism exactly when every component is an isomorphism

Statement

A natural transformation α:F⇒G is a natural isomorphism exactly when every component αA is an isomorphism.

Facts & Assumptions

Given: A natural transformation α:F⇒G.

[L1]

A natural isomorphism has a two-sided inverse natural transformation (Natural isomorphism), and vertical composition and identity transformations are componentwise (Identity natural transformation and vertical composition).

Proof

technique · direct
1.1

If α has a natural inverse β, then βAαA=1FA and αAβA=1GA at every object, so each αA is an isomorphism.

givenL1
2.1

Conversely, suppose every αA is invertible and put βA=αA−1; from GfαA=αBFf, composition with the two inverses gives FfβA=βBGf, so β:G⇒F is natural.

step 1.1L1
3.1

Componentwise, β∘α=1F and α∘β=1G, hence α is a natural isomorphism.

step 2.1L1∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Equivalence, quasi-inverse, and adjoint equivalence of categories

Definition

An equivalence of categories from C to D consists of functors F:C→D and G:D→C, called quasi-inverses, together with natural isomorphisms

η:1C⇒GF,ε:FG⇒1D.

The categories are then called equivalent. The notions of functor and natural isomorphism are those of Covariant functor, identity functor, composite functor, and contravariant functor and Natural isomorphism.

An adjoint equivalence is such data satisfying the triangle identities

Gε∘ηG=1G,εF∘Fη=1F.

Here Gε, ηG, εF, and Fη are the whiskerings of Whiskering and horizontal composition of natural transformations. No triangle identity is required of a bare equivalence.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Equivalence of categories is reflexive, symmetric, and transitive

Statement

Equivalence of categories is reflexive, symmetric, and transitive.

Facts & Assumptions

Given: Categories and equivalence data between them.

[L1]

An equivalence consists of quasi-inverse functors and natural isomorphisms in both composite directions (Equivalence, quasi-inverse, and adjoint equivalence of categories).

[L2]

Vertical composition is componentwise (Identity natural transformation and vertical composition); whiskering and horizontal composition produce natural transformations between composite functors (Whiskering and horizontal composition of natural transformations), and those horizontal composites are natural (Horizontal composites of natural transformations satisfy naturality).

Proof

technique · direct
1.1

The identity functor is its own quasi-inverse and the identity natural transformations supply an equivalence C≃C, proving reflexivity.

givenL1
2.1

If (F,G,η,ε) gives C≃D, then (G,F,ε−1,η−1) gives D≃C, proving symmetry.

step 1.1L1
3.1

If (F,G) gives C≃D and (H,K) gives D≃E, then HF and GK are quasi-inverses; whiskering and vertically composing the two units gives 1C⇒GKHF, and doing the same with the counits gives HFGK⇒1E, so [L2] proves transitivity.

step 2.1L1L2∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

A functor is an equivalence exactly when it is fully faithful and split essentially surjective, without Choice

Statement

A functor F:C→D is an equivalence exactly when it is fully faithful and split essentially surjective. No choice principle is needed because the splitting is part of the data.

Facts & Assumptions

Given: A functor F:C→D.

[L1]

Equivalence and quasi-inverse data are defined in Equivalence, quasi-inverse, and adjoint equivalence of categories.

[L2]

Fully faithful and split essentially surjective have the precise hom-bijection and specified-witness meanings in Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors.

[L3]

A fully faithful functor reflects isomorphisms (Every fully faithful functor reflects isomorphisms).

Proof

technique · direct
1.1

Suppose first that F has quasi-inverse G, unit η:1C⇒GF, and counit ε:FG⇒1D. Then D↦(GD,εD) explicitly splits essential surjectivity.

givenL1L2
1.2

Conversely, assume F is fully faithful and comes with objects CD and isomorphisms εD:FCD→D. Define GD=CD, and for u:D→E define G(u) as the unique morphism whose image under F is εE−1uεD; fullness gives existence and faithfulness gives uniqueness.

givenL2
2.1

Naturality and invertibility of η show faithfulness: if Ff=Fg, then GFf=GFg, so ηBf=GFf ηA=GFg ηA=ηBg and f=g.

step 1.1L1
2.2

The defining equation makes G(1D)=1GD and G(vu)=G(v)G(u) after applying faithful F, so G is a functor, and the same equation is precisely naturality of ε:FG⇒1D.

step 1.2L2
3.1

Put δA=εFA∘F(ηA), an automorphism of FA. For u:FA→FB, set v=δBuδA−1 and h=ηB−1G(v)ηA; naturality of ε gives Fh=δB−1vδA=u, so F is full.

step 1.1step 2.1L1L2
3.2

For each A, fullness gives a unique ηA:A→GFA with F(ηA)=εFA−1; faithfulness and naturality of ε make η natural, and [L3] makes each ηA an isomorphism because its image is.

step 2.2L2L3
4.1

Thus (F,G,η,ε) is equivalence data. The two constructions prove both directions without making any unrecorded selection.

step 1.1step 2.1step 3.1step 3.2L1∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

Under the Axiom of Choice, essential surjectivity onto a small category admits a splitting

Statement

Assume the Axiom of Choice. If F:C→D is essentially surjective and D is small, then its essential surjectivity admits a splitting.

Facts & Assumptions

Given: An essentially surjective functor F:C→D with small target D.

[L1]

Essential surjectivity asserts an object and isomorphism witness over every target object, while split essential surjectivity records one such witness for each object (Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors).

[L2]

A small category has a set of objects (Small, locally small, and large categories), and the Axiom of Choice selects from a set-indexed family of nonempty sets (The Axiom of Choice).

Proof

technique · direct
1.1

Since Ob⁡D is a set and each D has some pair (C,ε:FC→D), Collection bounds a witness for every D inside one set of candidate pairs.

givenL1L2
2.1

For each D, the candidates in that bounding set form a nonempty set, so [L2] chooses one pair (CD,εD).

step 1.1L2choose
3.1

The selected family is exactly a splitting of essential surjectivity as defined in [L1].

step 2.1L1∎
CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

Under the Axiom of Choice, a functor with small target is an equivalence exactly when it is fully faithful and essentially surjective

Statement

Assume the Axiom of Choice and let F:C→D have small target. Then F is an equivalence exactly when it is fully faithful and essentially surjective.

Facts & Assumptions

Given: A functor F:C→D with small D, under the Axiom of Choice.

[L1]

An equivalence is fully faithful and split essentially surjective, and the converse holds (A functor is an equivalence exactly when it is fully faithful and split essentially surjective, without Choice).

[L2]

Essential surjectivity over a small target can be split under Choice (Under the Axiom of Choice, essential surjectivity onto a small category admits a splitting).

Proof

technique · direct
1.1

If F is an equivalence, [L1] makes it fully faithful and split essentially surjective, hence essentially surjective.

givenL1
2.1

If F is fully faithful and essentially surjective, [L2] supplies a splitting.

step 1.1L2
3.1

The converse direction of [L1] now makes F an equivalence, proving the biconditional.

step 2.1L1∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Every equivalence of categories can be equipped as an adjoint equivalence

Statement

Every equivalence of categories admits a choice of unit and counit satisfying the triangle identities, and hence can be equipped as an adjoint equivalence.

Facts & Assumptions

Given: Equivalence data F:C⇄D:G with a natural isomorphism η:1C⇒GF.

[L1]

An adjoint equivalence is equivalence data satisfying two triangle identities (Equivalence, quasi-inverse, and adjoint equivalence of categories), and natural isomorphisms have invertible components (A natural transformation is a natural isomorphism exactly when every component is an isomorphism).

Proof

technique · direct
1.1

The quasi-inverse G is itself an equivalence, hence fully faithful by [L2]; for each D, fullness gives a unique εD′:FGD→D with G(εD′)=ηGD−1.

givenL1L2
2.1

Naturality of η and faithfulness of G show that the components εD′ are natural; since G(εD′) is an isomorphism, reflection in [L2] makes each εD′ an isomorphism.

step 1.1L1L2
3.1

The defining equation gives Gε′∘ηG=1G; applying G to ε′F∘Fη and using naturality of η at each ηA gives the identity, and faithfulness of G yields ε′F∘Fη=1F.

step 2.1L1L2
4.1

Thus (F,G,η,ε′) satisfies both triangle identities and is an adjoint equivalence.

step 3.1L1∎
PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

Under the Axiom of Choice, a connected small groupoid is equivalent to the automorphism group of any one of its objects

Statement

Assume the Axiom of Choice. If G is a connected small groupoid and A is any object, then G is equivalent to the one-object category Aut⁡G(A).

Facts & Assumptions

Given: A connected small groupoid G and an object A.

[L1]

In a connected groupoid, every object is isomorphic to A (Isomorphism, groupoid, and connected category), and smallness makes the object collection a set (Small, locally small, and large categories).

Proof

technique · direct
1.1

By [L1] and [L2], choose for every object X an isomorphism pX:A→X, taking pA=1A.

givenL1L2choose
2.1

Define F:G→Aut⁡(A) by sending every object to the sole object and f:X→Y to pY−1fpX; identities and composites are preserved by cancellation of pYpY−1.

step 1.1L2
3.1

For each X,Y, the inverse hom-map sends u∈Aut⁡(A) to pYupX−1, so F is fully faithful; it is split essentially surjective because its target has one object, and [L2] makes it an equivalence.

step 2.1L2∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Skeletal category and skeleton

Definition

A category is skeletal when isomorphic objects are equal (Isomorphism, groupoid, and connected category).

A skeleton of a category C is a full subcategory S⊆C (Subcategory and full subcategory) that is skeletal and contains an object isomorphic to every object of C. Thus a skeleton contains exactly one object from each isomorphism class, once the representative objects have been selected.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

Under the Axiom of Choice, every small category has a skeleton

Statement

Assume the Axiom of Choice. Every small category has a skeleton.

Facts & Assumptions

Given: A small category C.

[L1]

A skeleton is a full skeletal subcategory containing one representative of every isomorphism class (Skeletal category and skeleton).

[L2]

The object collection of a small category is a set (Small, locally small, and large categories), and Choice selects from a set-indexed family of nonempty sets (The Axiom of Choice).

Proof

technique · direct
1.1

Isomorphism defines an equivalence relation on the set Ob⁡C, so its quotient is a set whose members are nonempty isomorphism classes.

givenL1L2
2.1

By [L2], choose one object from each class and let S be the full subcategory on the selected objects.

step 1.1L1L2choose
3.1

Every object of C is isomorphic to its selected representative, while two selected isomorphic objects lie in the same class and are equal; hence S is a skeleton.

step 2.1L1∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Comma category, slice category, and coslice category

Definition

For functors S:A→C and T:B→C (Covariant functor, identity functor, composite functor, and contravariant functor), the comma category (S↓T) has objects (A,B,f) with f:SA→TB. A morphism (a,b):(A,B,f)→(A′,B′,f′) satisfies

T(b)∘f=f′∘S(a).

Identities and composites are componentwise. Functoriality of S,T shows that the displayed square remains commutative under composition, and the category axioms follow from Category, object, morphism, domain, codomain, identity, composition, and hom-collection.

For an object C∈C, let ΔC:1→C be the functor from the one-object, identity-only category that selects C. The slice category is C/C=(1C↓ΔC): its objects are arrows f:A→C, and a morphism from f:A→C to f′:A′→C is an arrow a:A→A′ with f′∘a=f. The coslice category is C/C=(ΔC↓1C): its objects are arrows f:C→A, and a morphism from f:C→A to f′:C→A′ is an arrow a:A→A′ with a∘f=f′.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Diagram as a functor from an indexing category

Definition

A diagram in a category C is a functor D:J→C (Covariant functor, identity functor, composite functor, and contravariant functor) from an indexing category J. The shape of the diagram is J. Thus objects and arrows of J name objects and commuting composites displayed in C. All relations in J are preserved by functoriality.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Strict 2-category

Definition

A strict 2-category consists of a class of objects and, for every ordered pair A,B, a hom-category K(A,B) (Category, object, morphism, domain, codomain, identity, composition, and hom-collection). Objects of a hom-category are 1-morphisms and its morphisms are 2-morphisms.

There are identity 1-morphisms and horizontal-composition functors

K(B,C)×K(A,B)⟶K(A,C)

where the product and functor notions are those of Product category and its projection functors and Covariant functor, identity functor, composite functor, and contravariant functor. They are associative and unital as literal equalities. Because horizontal composition is functorial, it satisfies the interchange law with the vertical composition inside each hom-category. The adjective strict refers to these equalities rather than coherent isomorphisms.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Small categories, functors, and natural transformations form the strict 2-category Cat

Statement

Small categories, functors, and natural transformations form a strict 2-category Cat.

Facts & Assumptions

Given: Small categories A,B,C.

[L1]

A strict 2-category has hom-categories, strictly associative and unital horizontal composition, and interchange (Strict 2-category).

[L2]

Proof

technique · direct
1.1

Take small categories as objects and [A,B] as each hom-category; its objects are functors and its morphisms are natural transformations.

givenL1L2
2.1

Functor composition gives horizontal composition, whiskering gives its action on natural transformations, and ordinary composition of functions makes associativity and units literal equalities.

step 1.1L1L2
3.1

The interchange theorem makes horizontal composition functorial with respect to vertical composition; the class convention of Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why CAT is not formed treats the object collection schematically and never forms CAT, so all strict 2-category axioms hold for Cat.

step 2.1L1L2∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Eckmann–Hilton: two unital operations satisfying interchange coincide and are commutative

Statement

Let a set X carry two unital binary operations ∘ and ∗ with the same unit e, and suppose

(a∘b)∗(c∘d)=(a∗c)∘(b∗d)

for all a,b,c,d. Then the operations coincide and their common operation is commutative.

Facts & Assumptions

Given: The two operations, common unit, and interchange identity in the Statement.

[L1]

A unital associative operation is a monoid operation (Semigroup and monoid); only the unit laws and interchange are needed for the calculation below.

Proof

technique · direct
1.1

For a,b∈X, interchange gives a∗b=(a∘e)∗(e∘b)=(a∗e)∘(e∗b)=a∘b, so the operations coincide.

givenL1
2.1

A second use gives a∘b=(e∗a)∘(b∗e)=(e∘b)∗(a∘e)=b∗a.

step 1.1L1
3.1

By step 1.1, b∗a=b∘a, so step 2.1 says a∘b=b∘a; the common operation is commutative.

step 1.1step 2.1∎
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

A functor is an isomorphism of categories exactly when its object and morphism maps are bijective

Statement

A functor is an isomorphism of categories, meaning that it has a two-sided inverse functor, exactly when its object map and its total morphism map are bijective.

For large categories, these are bijective definable class maps under Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why CAT is not formed.

Facts & Assumptions

Given: A functor F:C→D.

[L1]

Functors preserve domains, codomains, identities, and composition (Covariant functor, identity functor, composite functor, and contravariant functor), while the Statement defines a category isomorphism by a two-sided inverse functor.

[L2]

A set function is bijective exactly when it has a two-sided inverse (f:A→B is a bijection if and only if there is a function g:B→A with g∘f=ΔA and f∘g=ΔB; such a g is unique, equals the inverse relation f−1, and is itself a bijection). Under the Statement's definable-class convention, the same pointwise statement defines a bijective class map and its uniquely determined inverse class map.

Proof

technique · direct
1.1

If F has an inverse functor, the object maps and morphism maps are pointwise inverse maps and hence bijective by [L2].

givenL1L2
1.2

Conversely, use the uniquely determined inverse set functions or definable class maps on objects and morphisms supplied by [L2]. The inverse morphism map preserves domain and codomain because applying injective F reduces each assertion to the corresponding assertion for F.

givenL1L2
2.1

The same injectivity argument shows that the inverse sends identities to identities and preserves composition; it is therefore an inverse functor, so F is a category isomorphism.

step 1.2L1L2∎
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

The fundamental group is a functor π1:Top∗→Grp

Statement

Let Top∗ have pointed spaces (X,x0) as objects and basepoint-preserving continuous maps as morphisms. The assignment

π1:Top∗⟶Grp,(X,x0)⟼π1(X,x0)

and f↦f∗ is a functor.

Facts & Assumptions

Given: Pointed spaces and basepoint-preserving continuous maps.

[L2]

The induced map f∗ on fundamental groups is the homomorphism of The homomorphism on fundamental groups induced by a pointed continuous map, and induced maps satisfy (g∘f)∗=g∗∘f∗ and (1X)∗=1π1(X,x0) (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

[L3]

Proof

technique · direct
1.1

Basepoint-preserving continuous maps contain identities and are closed under composition, so they form the stated pointed category.

givenL1
2.1

By [L2], every morphism f is sent to a group homomorphism f∗, and the identity and composite equations required in [L3] hold.

step 1.1L2L3
3.1

Therefore the object and morphism assignments define a functor π1:Top∗→Grp.

step 2.1L1L3∎

5 · Examples, counterexamples and false statements

None yet.

Sources