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.
With a supplied well-powering, a subobject classifier represents the subobject functor
Statement
Assume is locally small, has a subobject classifier , and has a supplied well-powering . For each object , let be the quotient set of by mutual factorization. Then is a contravariant Set-valued functor, and the classifier induces a natural isomorphism
Thus represents the supplied representative-set form of the subobject functor.
Facts & Assumptions
Given: A locally small category with a subobject classifier and a supplied well-powering .
A subobject classifier assigns to each monomorphism a unique classifying map whose pullback of recovers the same subobject (Subobject classifier).
A supplied well-powering gives a set of monomorphisms into each object , containing a representative of every subobject class (Well-powered and co-well-powered categories, and supplied well-powerings).
Mutual factorization is an equivalence relation on monomorphisms into a fixed object, and subobjects are precisely those equivalence classes (Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms, Mutual factorisation is an equivalence relation on monomorphisms into an object and dually on epimorphisms out of it).
A contravariantly representable functor is a natural isomorphism for some presheaf (Presheaves, covariantly and contravariantly representable functors, and representations).
Proof
By [L3], the quotient by mutual factorization is a well-defined set for each , and its elements correspond exactly to subobject classes of represented inside the supplied set .
For a morphism and a class , pull back along . The resulting monomorphism into defines a subobject class of , and [L2] provides a representative of that class in ; step 1.1 shows that the resulting element of is independent of the chosen representative. Hence is a contravariant functor.
For each , define by sending to the class of the pullback of along . Conversely, define by sending the class of to its unique classifying map from [L1].
The composites are identities. If , then because the pullback subobject of along is classified by itself, and that classifying map is unique by [L1]. If , then the pullback of along represents the same subobject class as , so . Naturality follows because pullback commutes with composition of classifying maps.
Therefore is a natural isomorphism . By [L4], represents the supplied representative-set form of the subobject functor.
Depends on
- Subobject classifier
- Well-powered and co-well-powered categories, and supplied well-powerings
- Presheaves, covariantly and contravariantly representable functors, and representations
- Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms
- Mutual factorisation is an equivalence relation on monomorphisms into an object and dually on epimorphisms out of it
Used by
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
- Tom Leinster, Basic Category Theory, Exercise 6.3.26 (standard reference, not scraped)
- S. Mac Lane, Categories for the Working Mathematician, 2nd ed., IV.9 (standard reference, not scraped)