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.
The effacement extension commutes with connecting morphisms
Statement
The next-degree components supplied by A partial morphism of delta functors extends through one dimension shift can be chosen so that they commute with the connecting morphisms of every short exact sequence. Equivalently, once the lower-degree components form a partial morphism of delta functors, the one-step extension may be chosen to preserve that compatibility in the next degree as well.
Facts & Assumptions
Given: A short exact sequence and lower-degree components already compatible with its connecting maps.
Item 19 defines the next-degree components from chosen effacements and proves naturality when the chosen effacement sequences fit into a ladder (A partial morphism of delta functors extends through one dimension shift).
Item 20 makes those next-degree components independent of which effacing morphisms are used (The effacement extension is independent of the effacing morphism).
The dimension-shift lemmas give the monicity or epicity used to define the one-step components from the connecting morphisms of the chosen effacement sequences (Dimension shift for a homological delta functor effaced in the middle, Dimension shift for a cohomological delta functor effaced in the middle).
Proof
In the homological case, write the given sequence as and choose the projective effacement used by [L1] to define . Projectivity of lifts through the epimorphism ; the lift restricts to a map , producing a morphism from the effacement sequence to the given sequence. By [L2], using this ladder-compatible effacement does not change . Naturality of the two connecting morphisms, the defining equation from [L1], and naturality of the already constructed give . This is the required homological connecting square.
In the cohomological case, choose the injective effacement used by [L1] to define . Injectivity of extends across the monomorphism and induces a map , producing a morphism from the given sequence to the effacement sequence. Again [L2] permits this compatible choice. Naturality of the connectors, the defining cokernel equation from [L1], and naturality of then give . This is the required cohomological connecting square.
The two cases show that the one-step extension preserves every connecting morphism, independently of the effacement choices by [L2].
Depends on
Used by
Dependency tree · two levels
10 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
- Alexandre Grothendieck, Some aspects of homological algebra (Barr translation) (standard reference, not scraped)
- The Stacks Project, Section 12.12: Cohomological delta-functors (standard reference, not scraped)