The projections off a dg cone #
IsConeOf states its universal property for maps into the cone: Hom(W, Z)
splits as a product of Hom(W, X) in degree +1 and Hom(W, Y). The maps out of the cone that a
triangle needs are not part of the data, and this file extracts them.
The extraction is the standard one and needs no new hypothesis: apply the
splitting to dgId Z itself. That gives fst : (dgHom Z X).X 1 and
snd : (dgHom Z Y).X 0 with fst ≫ inl + snd ≫ inr = dgId Z.
The projection is closed, and that is where the work is #
fst is not closed by construction — it is one half of a splitting of an
identity, and nothing in IsConeOf mentions its differential. What forces it is
uniqueness of the splitting: differentiate the splitting of dgId Z, use
δ (dgId Z) = 0 and δ inl = f ≫ inr, and the result is a second splitting of
0. Injectivity then reads off both δ fst = 0 and δ snd = -(fst ≫ f).
So the connecting map of the triangle is closed for a reason, rather than by
assumption, and the cone's snd fails to be closed by exactly the term that
makes the triangle rotate.
The splitting of dgId Z along the cone's two inclusions.
Instances For
The degree-1 projection of the cone onto the source.
Instances For
The degree-0 projection of the cone onto the target.
Instances For
The two projections split the identity.
The splitting of the identity is unique. fst and snd are
Classical.choice on a surjectivity, so the only handle on them is the equation
they satisfy; the cone's injectivity clause turns that equation into a
characterisation. Every identification of fst or snd with a concretely given
element goes through here.
Differentiating the splitting of the identity: the projection's differential
composed into the cone equals the two inr-terms it has to cancel against.
Everything below is read off this one equation, which is why it is stated in the raw form the Leibniz rule produces rather than in a tidied one.
The projection onto the source is closed. Nothing in IsConeOf says so;
what forces it is uniqueness of the splitting, applied to the differentiated
identity. fst and the correction term are the unique pair splitting 0, and
the pair of zeros splits it too.
The projection onto the source is closed.
The projection onto the target is not closed, and this is by how much. The term is what makes the triangle rotate.
inr followed by the two projections: the splitting of inr itself. Both
halves come from one application of uniqueness, so they are proved together.
inl followed by the two projections: the splitting of inl itself, and the
other half of the biproduct-like orthogonality.
The source's inclusion is a section of the cone's projection to it.
And it is orthogonal to the projection onto the target.
The cone's projection to the source is orthogonal to the target's inclusion.
This is the g ≫ h = 0 of the triangle, before the shift is applied.
And the target's inclusion is a section of the cone's projection to it.
The connecting morphism of the triangle: project to the source, then cross
the shift. Degree zero, because fst has degree 1 and s.hom degree -1.
Equations
- hc.toShift s = ((CategoryTheory.DGCategoryStruct.dgComp 1 (-1) 0 CategoryTheory.IsConeOf.splitId._proof_3) hc.fst) s.hom
Instances For
It is closed, because both factors are — delta_fst for the projection, and
IsShiftBy.hom_closed for the shift.
So the connecting morphism is a morphism of Z⁰, and hence of H⁰.
Changing the shift changes the connecting morphism by the comparison.
toShift reads its witness only through hom, and the comparison of two shifts
cancels the first witness against the second. This is what lets the cone triangle
be stated at the chosen shift and still be recognised in a model where a
different shift is the natural one.
The triangle composes to zero at the second vertex: inr followed by the
connecting morphism vanishes on the nose, not merely up to homotopy.
The morphism a cone is built on is automatically closed. IsConeOf does
not ask for it: what it asks is δ inl = f ≫ inr, and applying δ twice turns
that into (δ f) ≫ inr = 0. Uniqueness of the splitting then reads off δ f = 0.
So exists_cone's cocycle hypothesis is needed to produce a cone, not to use
one.
The cone on an identity is contractible. snd ≫ inl is a primitive for
the cone's identity, so the cone becomes a zero object in H⁰.
Both corrections conspire: δ inl = f ≫ inr contributes the snd ≫ inr half,
and δ snd = -(fst ≫ f) — the failure of snd to be closed — contributes the
fst ≫ inl half with the sign the Leibniz rule supplies. At f = dgId the two
halves are exactly the splitting of dgId Z.