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.
Special adjoint functor theorem, data-supplied functor form
Statement
Under either hypothesis branch of Special adjoint functor theorem, objectwise form with explicit intersection smallness or preservation data, suppose an initial object of is supplied for every . Then these data determine a left adjoint to .
Facts & Assumptions
Given: The SAFT hypotheses and a supplied initial object in every comma category.
The objectwise SAFT gives an initial object of each fixed comma category under either explicit intersection branch (Special adjoint functor theorem, objectwise form with explicit intersection smallness or preservation data).
A supplied family of initial comma objects determines a left adjoint and its adjunction uniquely (A left adjoint exists exactly when chosen initial objects are supplied in every comma category).
Proof
Apply [L2] to the supplied initial comma objects. They assemble into a functor and an adjunction .
The supplied family is essential data: [L1] is objectwise and does not itself choose one initial object over a proper class. With the family supplied, [L2] completes the construction.
Depends on
Used by
- A category satisfying the explicit SAFT intersection hypotheses is cocomplete Corollary
- With the objectwise SAFT universal arrows supplied, a continuous Set-valued functor from a chosen-well-powered SAFT category is representable Corollary
- Choice and smallness ledger for the initial-object lemma, GAFT, and SAFT Remark
- With the SAFT initial comma objects supplied for all spaces, they assemble into the compact-Hausdorff reflection and agree on Tychonoff spaces with the constructed Stone-Cech adjunction Theorem
Dependency tree · two levels
13 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
- S. Mac Lane, Categories for the Working Mathematician, theorem V.8.2 and corollary (standard reference, not scraped)