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.
Left modules over a fixed ring and module homomorphisms form the large locally small category
Statement
For a fixed ring , left -modules and module homomorphisms form a large locally small category .
Facts & Assumptions
Given: Left -modules and module homomorphisms , .
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).
The functions between fixed sets form the set (The set of all functions ); 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
Identity maps are module homomorphisms, and preserves addition and scalar multiplication by the two homomorphism laws; function composition is associative and unital.
Thus left -modules and their homomorphisms form a category whose hom-collections are sets.
For every ordinal , the singleton carries a transported zero -module structure, producing a proper class of distinct objects by [L2]; hence is large and locally small.
Depends on
- Category, object, morphism, domain, codomain, identity, composition, and hom-collection
- Small, locally small, and large categories
- Unital left and right modules over a ring; unqualified module means left module
- Module homomorphism and isomorphism, kernel, image and cokernel
- The set $B^{A}$ of all functions $A \to B$
- Burali-Forti: there is no set of all ordinals
Used by
- Local systems and pullback Definition
- Presheaves and sheaves of groups, rings, and modules Definition
- A module-valued coend computed as a quotient of a direct sum Example
- A pullback of module maps is computed as a kernel of a difference map Example
- Abelian groups, modules, and vector spaces are additive Example
- The free-group functor F:Set toGrp and free-module functor R⁽⁻⁾:Set→ R-Mod Example
- Underlying-set and structure-forgetting functors among Grp, Ring, Vect_F, R-Mod, Top, and Set Example
- A module-valued coend is the direct sum of the diagonal values modulo the dinaturality submodule Theorem
- Abelian groups form an abelian category Theorem
- Coextension of scalars is right adjoint to restriction of scalars Theorem
- For every ring R, the category R-Mod is complete and cocomplete Theorem
- Modules over a commutative ring form a monoidal category Theorem
- Modules over a ring form an abelian category Theorem
- The free-module functor is left adjoint to the underlying-set functor Theorem
- The matrix category is fully faithful in modules and, with chosen bases, equivalent to finite free modules Theorem
Dependency tree · two levels
16 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)