Rotating a cone triangle #
dg-enhancements-e6. The rotation axiom asks that Y → Z → X⟦1⟧ → Y⟦1⟧ be
distinguished whenever X → Y → Z → X⟦1⟧ is. Since a distinguished triangle is
one isomorphic to a cone triangle, what has to be produced is a comparison
between a cone on inr : Y → Z and the shift X⟦1⟧.
X⟦1⟧ is not a cone on inr, and cannot be made one #
IsConeOf is a representability condition on the nose: maps into the cone split
bijectively in every degree. For a cone W on inr, that reads
Hom(V, Y)⟨1⟩ × Hom(V, Z) ≅ Hom(V, W), and Z itself already splits as
Hom(V, X)⟨1⟩ × Hom(V, Y). So W is three summands wide and X⟦1⟧ is one; they
are not isomorphic as graded objects, and no choice of structure will make them so.
They are homotopy equivalent, which is all H⁰ sees, and that is what this file
constructs: a pair of closed degree-zero maps between W and X⟦1⟧. The two
extra summands of W cancel in H⁰ rather than being absent.
The maps #
fwd = snd_W ≫ toShift. Closed because δ snd_W = -(fst_W ≫ inr) — the cone's
one differential correction — and inr ≫ toShift = 0, which is the triangle
composing to zero at its second vertex. The correction is killed by the
orthogonality rather than by a choice.
bwd has to be assembled against the splitting, and its inl_W-component is
forced. Take s.inv ≫ inl for the inr_W-component: it is not closed, its
differential is s.inv ≫ f ≫ inr. The inl_W-component -(s.inv ≫ f)
contributes exactly -(s.inv ≫ f ≫ inr) through δ inl_W = inr ≫ inr_W, and its
own differential vanishes because s.inv and f are both closed. So the sum is
closed, and the sign is solved for rather than guessed.
The comparison Cone(inr) ⟶ X⟦1⟧: project to Z, then take the connecting
morphism of the original cone.
Equations
- hc.rotateFwd hd s = ((CategoryTheory.DGCategoryStruct.dgComp 0 0 0 CategoryTheory.IsConeOf.rotateFwd._proof_3) hd.snd) (hc.toShift s)
Instances For
It is closed. δ snd_W is the cone's correction term -(fst_W ≫ inr), and
inr ≫ toShift = 0 kills it.
The comparison X⟦1⟧ ⟶ Cone(inr), assembled against the splitting of maps
into the cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inl_W-component's own differential vanishes: s.inv is closed by
IsShiftBy.inv_closed, and f is closed by IsConeOf.delta_f.
The inr_W-component is not closed, and this is its differential.
The backward comparison is closed. The two components' differentials are
the same element of Hom(X⟦1⟧, W) with opposite signs: the inl_W-component
contributes through δ inl_W = inr ≫ inr_W, the inr_W-component through its
own failure to be closed. The sign in rotateBwd is what makes them cancel.
inl_W followed by the forward comparison vanishes: inl_W ≫ snd_W = 0.
inr_W followed by the forward comparison is the connecting morphism:
inr_W ≫ snd_W = dgId.
One composite is the identity on the nose. No homotopy is needed in this
direction: the inl_W-component of rotateBwd dies against snd_W, and what
survives is s.inv ≫ (inl ≫ fst) ≫ s.hom, which is s.inv ≫ s.hom.
The connecting morphism absorbs the shift out of rotateBwd's
inl_W-component: s.hom ≫ s.inv = dgId.
And out of its inr_W-component.
The homotopy's core computation. snd_W ≫ snd is not closed, and its
differential is exactly the inl_W-coefficient the composite has to correct:
both cones contribute their own failure, and inr ≫ snd = dgId turns the second
contribution into fst_W on the nose.
The composite in the other order, split along the cone's two inclusions.
The other composite is the identity up to homotopy. The primitive is
-(snd_W ≫ snd) ≫ inl_W, and delta_sndComp is why: its differential is the
inl_W-coefficient the composite has to correct, while the inr_W-coefficient
is corrected by the original cone's splitting of dgId.
The rotated triangle's third map, on the nose. rotateBwd followed by the
cone-on-inr's connecting morphism is -f⟦1⟧, with no homotopy: the
inr_W-component dies against fst_W, the inl_W-component survives through
inl_W ≫ fst_W = dgId, and what is left is literally mapShift's definition.
This is the third commuting square of the rotation isomorphism, and that it holds
strictly is why the sign of rotateBwd had to be what it is.
The rotated triangle's second map, split along the cone's two inclusions.
The rotated triangle's second square, up to homotopy. The primitive is
-(snd ≫ inl_W): its differential supplies the inl_W-coefficient through the
original cone's δ snd = -(fst ≫ f), and the inr_W-coefficient through the
cone's splitting of dgId Z.