The distinguished triangles of H⁰ #
dg-enhancements-e6. Pretriangulated carries its distinguished triangles as a
field, so transporting a triangulated structure to H⁰ starts by saying which
triangles those are. This file says it, and discharges the two axioms that follow
from the saying rather than from any computation.
The definition #
A triangle of H⁰ C is distinguished when it is isomorphic to one built from a
dg cone: X → Y → Z → X⟦1⟧ with the second map IsConeOf.inr and the third
IsConeOf.toShift, the connecting morphism DGCategory/Cone.lean extracts.
Two choices in that sentence are worth naming.
The shift is the chosen one. toShift accepts any IsShiftBy X 1 X', but the
triangle must land in X⟦1⟧ — the shift HasShift (H0 C) ℤ actually uses, which
is IsPretriangulated.shiftWitness's. Using it here rather than an arbitrary
witness keeps a comparison isomorphism out of every subsequent proof; the price is
paid once, in H0Shift.lean, where the choice was made.
The cone is of a representative, not of the morphism. A morphism of H⁰ is a
homotopy class, and a cone is built from an actual cocycle. Different
representatives give different cones — isomorphic ones, but not equal — so the
definition quantifies over a cocycle and a cone on it, and closes under
isomorphism at the end. That is also why distinguished_cocone_triangle needs
Quotient.ind rather than a direct construction.
What this file does not do #
Three of the six Pretriangulated fields. contractible_distinguished needs the
cone on an identity to be a zero object of H⁰; rotate_distinguished_triangle
and complete_distinguished_triangle_morphism are the two theorems the axiom
system exists for. No Pretriangulated instance is claimed here, and the three
lemmas below are stated in the shape those fields want so that the instance is
assembly when they land.
The shift functors of H⁰ are additive. HasShift unfolds to
H0.shiftFunctor only through hasShiftMk, which is not reducible, so instance
search needs to be told.
The triangle a cone determines: the morphism, the cone's inclusion of the target, and minus the connecting morphism into the chosen shift.
The sign is not decoration #
IsConeOf.toShift is fst followed by the shift, with no sign; the triangle's
third map is its negative. That is the convention Mathlib fixes for the model:
CochainComplex.mappingCone.triangle is built from -mappingCone.fst, and
Cdg.triangle_mor₃_eq records that this repository's toShift is +fst
followed by the shift on the nose. Without the sign here the two structures
would differ in the third map, and dg-enhancements-e7's agreement theorem
would be false rather than hard: the sign patterns an isomorphism of triangles
can produce are exactly those whose product over the three vertices is +1, and
negating the third map alone is not one of them.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cone triangle's first map. Stated so that the rotation proofs can rewrite
with it instead of unfolding coneTriangle, whose dsimp normal form breaks
type-correctness at instances transparency: H0 C reduces to C, and the
Triangle.mk in the unfolded term then reads its objects at the wrong type.
The distinguished triangles of H⁰: those isomorphic to a cone triangle.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A cone triangle is distinguished, by the identity isomorphism.
isomorphic_distinguished. Immediate from the definition: the class is
defined as an isomorphism-closure, so this is transitivity.
distinguished_cocone_triangle. Every morphism of H⁰ fits into a
distinguished triangle: pick a cocycle representing it, take a dg cone on that,
and the triangle is a cone triangle on the nose.
A cone on an identity is a zero object of H⁰: its identity is a
coboundary, so it is zero in the quotient. Enhancement.lean proves the same
for an object whose dg identity vanishes on the nose; this is the version the
contractible triangle needs, where the identity is only null-homotopic.
contractible_distinguished. The triangle X → X → 0 is distinguished:
a cone on dgId X is a zero object of H⁰, so it is isomorphic to the chosen
zero object, and every square in sight commutes because it factors through one.
The content is IsConeOf.dgId_mem_coboundaries_of_dgId; everything here is the
bookkeeping that turns a null-homotopy into an isomorphism of triangles.
The comparison of dg-enhancements-e6's rotation, as an isomorphism of H⁰.
Both composites were proved in DGCategory/Rotate.lean: one on the nose, one up
to the primitive exhibited there. In H⁰ that difference disappears, which is
the whole reason the rotation axiom is a statement about H⁰ and not about the
dg category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
rotateIso, negated.
The cone triangle's third map carries a sign (coneTriangle), so the rotation
comparison has to carry one too: the second and third squares of
rotateConeTriangleIso each acquire the sign twice, once from the source
triangle and once from the target, and only the negated isomorphism cancels
both.
Equations
- CategoryTheory.H0.rotateIsoNeg hc hd = { hom := -(CategoryTheory.H0.rotateIso hc hd).hom, inv := -(CategoryTheory.H0.rotateIso hc hd).inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
The rotation of a cone triangle is the cone triangle on its second map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
rotate_distinguished_triangle, forward direction. The rotation of a
distinguished triangle is distinguished.
The lifting axiom, for cone triangles. A square commuting in H⁰ extends
to the cones, and both of the extension's squares hold on the nose.
The hypothesis is an equation in H⁰, so it says only that f₁ ≫ b - a ≫ f₂ is a
coboundary. Extracting the primitive is the first step, and folding it into the
lift is what IsConeOf.lift does; lift_closed is where it is consumed.
Dg cone morphisms as morphisms of H⁰ cone triangles #
The adapter below is a construction on IsConeOf.Morphism, so it lives in that
namespace rather than in H0; the H0 names it uses are opened locally.
A dg cone morphism descends to a morphism of the associated H⁰ cone
triangles. The retained degree-minus-one homotopy supplies the first square;
the two strict cone squares supply the other two.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The H⁰ adapter sends the canonical identity cone morphism to the
identity triangle morphism.
The H⁰ adapter preserves composition of dg cone morphisms.
complete_distinguished_triangle_morphism. A square commuting between
the first two vertices of two distinguished triangles extends to the third.
Both triangles are isomorphic to cone triangles, and exists_lift_of_comm is
this statement for those; Pretriangulated.exists_lift_of_iso conjugates the
square into them and the lift back. The two Quotient.inds are what turn the
H⁰-morphisms a and b into the cocycles the dg construction needs -- a
different representative gives a different lift, which is why the axiom asks
only for existence.
The five axioms H⁰ proves. Isomorphism-closure, the contractible
triangles, a cone on every morphism, the forward rotation, and the completion
of a square. The rotation axiom's reverse direction is not among them: it is a
theorem about these five, proved once and generically in
Triangulated/PretriangulatedAxioms.lean.
H⁰ of a pretriangulated dg category is pretriangulated
(dg-enhancements-e6). The distinguished triangles are distinguishedTriangles C
-- those isomorphic to a dg cone triangle -- and every field is one of the five
lemmas above, with the reverse rotation supplied by Axioms.mem_of_rotate_mem.
Equations
The instance's distinguished triangles are the ones this file defined, and
Iff.rfl is the proof: Axioms.pretriangulated is reducible, so
distTriang (H0 C) and distinguishedTriangles C are the same set rather than
two sets with a comparison between them. Downstream code can therefore reach a
cone triangle through coneTriangle_mem.