TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28

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.

Zassenhaus butterfly lemma in an abelian category

Statement

Let $A_{0} \leq A_{1}$ and $B_{0} \leq B_{1}$ be subobjects of an object $X$ in an abelian category. Then there is a canonical isomorphism

$\frac{A_{0} \lor (A_{1} \land B_{1})}{A_{0} \lor (A_{1} \land B_{0})} ≅ \frac{(A_{1} \land B_{1}) \lor B_{0}}{(A_{0} \land B_{1}) \lor B_{0}} .$

Facts & Assumptions

Given: Subobjects $A_{0} \leq A_{1}$ and $B_{0} \leq B_{1}$ of an object $X$ .

[L1]

The subobject lattice of $X$ is modular (The subobject lattice of an abelian category is modular).

[L2]

For subobjects $U, V$ of a common object, one has $(U \lor V) / V ≅ U / (U \land V)$ (Second isomorphism theorem in an abelian category).

[L3]

Nested quotients satisfy the third isomorphism theorem (Third isomorphism theorem in an abelian category).

Proof

technique · direct

1.1L1L2construct

Put $M : = A_{1} \land B_{1}$ , $U : = A_{1} \land B_{0}$ , and $V : = A_{0} \land B_{1}$ . Since $U \leq M$ , the second isomorphism theorem [L2] applied to $A_{0}$ and $M$ inside $A_{0} \lor M$ gives $\frac{A_{0} \lor M}{A_{0} \lor U} ≅ \frac{M}{M \land (A_{0} \lor U)} .$ By modularity [L1] inside the interval below $M$ , $M \land (A_{0} \lor U) = (M \land A_{0}) \lor U = V \lor U .$ So the left quotient is canonically isomorphic to $M / (V \lor U)$ .

1.2L1L2construct

Similarly, since $V \leq M$ , the second isomorphism theorem [L2] applied to $M$ and $B_{0}$ inside $M \lor B_{0}$ gives $\frac{M \lor B_{0}}{V \lor B_{0}} ≅ \frac{M}{M \land (V \lor B_{0})} .$ Again modularity yields $M \land (V \lor B_{0}) = V \lor (M \land B_{0}) = V \lor U .$ So the right quotient is also canonically isomorphic to $M / (V \lor U)$ .

2.1L3step 1.1step 1.2∎

The two quotients in steps 1.1 and 1.2 are canonically isomorphic to the same quotient of $M$ , hence to each other. The nested-quotient compatibility of [L3] identifies these isomorphisms with the displayed butterfly quotient comparison.

Depends on

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

Pavel Etingof, Shlomo Gelaki, Dmitri Nikshych, and Victor Ostrik, Tensor Categories, Section 1.5 (standard reference, not scraped)