LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Flags lift uniquely through a quotient in an abelian category

Statement

Let $W \leq L$ be a subobject in an abelian category, and let $q : L \to L / W$ be the quotient map. Inverse image along $q$ is an order isomorphism from the subobjects of $L / W$ to the interval of subobjects $U \leq L$ with $W \leq U$ . Its inverse sends $U$ to the image $q_{*} U$ , canonically isomorphic to $U / W$ . Under this correspondence, $(L / W) / (U / W) ≅ L / U .$

Facts & Assumptions

Given: An abelian category, subobjects $W \leq L$ , and the quotient map $q : L \to L / W$ .

[F1]

A subobject is a mutual-factorisation class of monomorphisms; its quotient is the cokernel of a representing monomorphism (Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms, The quotient of an object by a subobject).

[F2]

Direct image is the image of the composite with the given map, and inverse image is its pullback (Direct and inverse image of a subobject).

[F3]

Direct and inverse image form the Galois connection $f_{*} B \leq C ⟺ B \leq f^{*} C$ (Direct and inverse image of subobjects form a Galois connection).

[F4]

Pulling back an epimorphism in an abelian category gives an epimorphism (The pullback of an epimorphism is an epimorphism).

[F5]

For every morphism $f$ , $coker (\ker f)$ is canonically isomorphic to $im (f)$ (First isomorphism theorem in an abelian category).

[F6]

For nested subobjects $W \leq U \leq L$ , $(L / W) / (U / W) ≅ L / U$ (Third isomorphism theorem in an abelian category).

[F7]

Every monomorphism is the kernel of its cokernel (Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel).

Proof

technique · direct

1.1F1F2F3F4F5F7

Given a subobject $B \leq L / W$ , let $U = q^{*} B$ be its inverse image. Since $q_{*} W = 0 \leq B$ , [F3] gives $W \leq U$ . The pullback square defining $U$ has a projection $p : U \to B$ that is epic by [F4]; its kernel is the kernel $W$ of $q$ . By [F5], its image is canonically $U / W$ . Since $p$ is epic, any cokernel $c$ satisfies $c p = 0 = 0 p$ , so $c = 0$ by cancellation. Its universal property makes its codomain initial, because the only morphism out of $B$ annihilating $p$ is zero; hence the cokernel object is zero. By the image definition, $im (p) = \ker (coker p) = B$ . Thus $U / W ≅ B$ and $q_{*} U = B$ .

1.2F1F2F5F6F7

Conversely let $W \leq U \leq L$ . The restriction $q ∣_{U} : U \to L / W$ has kernel $W$ , so [F5] identifies its image $q_{*} U$ with $U / W$ . By [F6], the quotient map $L / W \to (L / W) / (U / W)$ , composed with $q$ , is the quotient map $L \to L / U$ . Its kernel is $U$ by [F1] and [F7], hence the inverse image of $U / W$ along $q$ is exactly $U$ .

2.1F3F6step 1.1step 1.2∎

Steps 1.1 and 1.2 show that the two assignments are inverse on subobject classes. Both assignments preserve inclusion by the Galois connection [F3], and [F6] gives the stated quotient identification. Thus inverse image along $q$ is the claimed order isomorphism.

Diagram

The quotient correspondence is represented by the following exact rows and the induced inclusion:

The vertical middle map is the subobject inclusion, and the right-hand map is the map induced by $U ↪ L$ . The diagram explains the correspondence; the proof above uses the categorical universal properties and the third isomorphism theorem, not the picture.

Depends on

Used by

Dependency tree · two levels

27 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

Saunders Mac Lane, Categories for the Working Mathematician, VIII.3 (standard reference, not scraped)
Olivier Schiffmann, Lectures on Hall Algebras, arXiv:math/0611617v2, §1.3 (standard reference, not scraped)