Alphabeta MathHow 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.
Groups and group homomorphisms form the large locally small category
Statement
Groups and group homomorphisms form a large locally small category .
Facts & Assumptions
Given: Groups and homomorphisms , .
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).
The functions between fixed sets form the set (The set of all functions ); 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
By [L1], identity maps and composites remain group homomorphisms; their associativity and unit equations are the corresponding equations for functions.
Thus the group objects and homomorphisms satisfy the category axioms, and each hom-collection is a set of functions between two fixed underlying sets.
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 is large and locally small.
Depends on
Used by
- GAFT recovers the published free-group adjunction, and the comma-initial criterion the abelianisation adjunction Corollary
- Presheaves and sheaves of groups, rings, and modules Definition
- A Kan extension computing the free-group functor Example
- For n≥ 1, determinant is a natural transformation det:GLₙ(-)⟹(-)^× from commutative rings to groups Example
- The equalizer of two group homomorphisms is their agreement subgroup Example
- The free group on X represents G mapstoSet(X,U(G)) Example
- The free-group functor F:Set toGrp and free-module functor R⁽⁻⁾:Set→ R-Mod Example
- The opposite-group functor is naturally isomorphic to the identity functor by inversion Example
- The singleton set and trivial group are terminal, while the empty set and trivial group are initial Example
- Underlying-set and structure-forgetting functors among Grp, Ring, Vect_F, R-Mod, Top, and Set Example
- FALSE: colimits in Grp are computed by taking the Set-colimit of the underlying diagram False statement
- The fundamental group is a functor π₁:Top_*toGrp Proposition
- Grp is complete and cocomplete Theorem
- The free-group functor is left adjoint to the underlying-set functor Theorem
Dependency tree · two levels
17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Emily Riehl, Category Theory in Context, Chapter 1 (standard reference, not scraped)