Lifting a square to a map of cones #
dg-enhancements-e6. complete_distinguished_triangle_morphism asks that a
commuting square between the first two vertices of two distinguished triangles
extend to the third. For cone triangles the extension is written down against the
splitting, and this file writes it down.
The homotopy is the whole difficulty #
If the square commuted on the nose the obvious candidate
fst₁ ≫ (a ≫ inl₂) + snd₁ ≫ (b ≫ inr₂) would already be closed. It does not:
the square commutes in H⁰, which means only that f₁ ≫ b - a ≫ f₂ is a
coboundary, and the candidate's differential is exactly that difference pushed
into the cone. So the homotopy k witnessing it is added to the map, as a
third term fst₁ ≫ (k ≫ inr₂), and the two contributions cancel.
That is the axiom's actual content, and it is why the lift is not unique: a
different k gives a different c, homotopic but not equal.
One owner for the lift #
Everything here is the degree-zero case of Pretriangulated.HomogeneousLift.
HomotopySquare is a HomogeneousSquare of degree zero whose vertical maps
are closed, lift is homogeneousLift 0, and closedness of the lift is
homogeneousLift_d read at degree zero. No sign is computed twice.
Both squares are strict #
Once c exists, neither square needs a homotopy. inr₁ ≫ c = b ≫ inr₂ because
inr₁ is orthogonal to fst₁ and a section of snd₁, so the k-term and the
a-term both vanish. And c ≫ fst₂ = fst₁ ≫ a because inl₂ ≫ fst₂ is the
identity while inr₂ ≫ fst₂ is zero, which kills the b- and k-terms.
The second square is stated on the cone projection fst, not on the
connecting morphism into a chosen shift: it needs no shift witness, so cone
morphisms compose without choosing one, and the connecting-morphism form
Morphism.toShift_comm is a consequence for every witness at once.
A degree-zero square between closed dg morphisms together with a chosen
degree-minus-one homotopy witnessing its commutativity in H⁰: a
HomogeneousSquare of degree zero whose vertical maps are closed.
This is the canonical input to cone functoriality. In particular, the homotopy is stored as data rather than merely asserted to exist, so cone maps can be constructed and composed without making a fresh choice.
- homotopy : ↑((DGCategoryStruct.dgHom X₁ Y₂).X (0 - 1))
- homotopy_boundary : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X₁ Y₂).d (0 - 1) 0)) self.homotopy = Int.negOnePow 0 • (((DGCategoryStruct.dgComp 0 0 0 ⋯) f₁) b - ((DGCategoryStruct.dgComp 0 0 0 ⋯) a) f₂)
The first vertical morphism is closed.
The second vertical morphism is closed.
Instances For
The boundary equation of a degree-zero homotopy, with the trivial Koszul
sign (-1)^0 removed: δ k = f₁ ≫ b - a ≫ f₂.
Build a homotopy square from closed vertical maps and the unsigned boundary equation.
Equations
- CategoryTheory.DGCategory.HomotopySquare.ofBoundary ha hb k hk = { homotopy := k, homotopy_boundary := ⋯, a_closed := ha, b_closed := hb }
Instances For
A strictly commuting square of closed degree-zero morphisms, regarded as a homotopy square with zero homotopy.
Equations
Instances For
Two homotopy squares with the same chosen homotopy are equal. Closedness and the boundary equation are propositions, so the degree-minus-one element is the only additional data once the four boundary morphisms are fixed.
The identity homotopy square.
Equations
Instances For
Composition of chosen homotopy squares. The composite homotopy is the
standard sum k₁ ≫ b₂ + a₁ ≫ k₂; unlike an existential commutativity proof,
this operation retains the witness needed by the induced cone map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A cone morphism keeps the dg representative and the strict identities
that make it useful downstream. In particular, this is stronger data than
a morphism between the corresponding triangles in H⁰: the representative
is closed before passing to the quotient, and both cone squares are retained
on the nose.
- square : DGCategory.HomotopySquare f₁ f₂ a b
The chosen homotopy-commutative square on the first two objects.
- hom : ↥(cocycles Z₁ Z₂)
The closed degree-zero dg morphism between the cone objects.
- inr_comm : ((DGCategoryStruct.dgComp 0 0 0 ⋯) hc₁.inr) ↑self.hom = ((DGCategoryStruct.dgComp 0 0 0 ⋯) b) hc₂.inr
The square on the cone inclusions.
- fst_comm : ((DGCategoryStruct.dgComp 0 1 1 ⋯) ↑self.hom) hc₂.fst = ((DGCategoryStruct.dgComp 1 0 1 ⋯) hc₁.fst) a
The square on the cone projections to the sources. Stated on
fst, so no shift witness is involved; seeMorphism.toShift_commfor the connecting-morphism form at any chosen shift.
Instances For
The closedness of the first component, projected from the canonical homotopy-square input.
The closedness of the second component, projected from the canonical homotopy-square input.
The chosen degree-minus-one homotopy underlying a cone morphism.
Instances For
The boundary equation for the chosen homotopy underlying a cone morphism.
A cone morphism is determined by its chosen homotopy square and its closed map between cone objects. The two strict compatibility fields are propositions.
The connecting-morphism square, at every chosen shift. toShift is
fst followed by the shift's element and mapShift is conjugation by the
two shift witnesses, so the fst square gives the connecting square once
s₁.hom ≫ s₁.inv cancels.
The lift of a square to the cones, with the homotopy folded in: the
degree-zero case of homogeneousLift.
Equations
- hc₁.lift hc₂ a b k = hc₁.homogeneousLift hc₂ 0 a b k
Instances For
The first square, strictly. inr₁ ≫ fst₁ = 0 kills the first and third
terms, and inr₁ ≫ snd₁ = dgId leaves the second.
The second square, strictly. inr₂ ≫ fst₂ = 0 kills the b- and
k-terms and inl₂ ≫ fst₂ = dgId collapses the a-term.
The lift is closed. homogeneousLift_d at degree zero: the
differential of the lift is the lift of δ a and δ b, which vanish.
The standard dg lift of a chosen homotopy square, packaged as a cone
morphism. lift_closed consumes the square's boundary equation, while the two
strict square lemmas retain the resulting naturality before passage to H⁰.
Equations
Instances For
The connecting-morphism square of the lift, for any two shift witnesses.
lift_comp_fst supplies the fst square; the rest is s₁.hom ≫ s₁.inv = 1.
The identity cone morphism.
Equations
- CategoryTheory.IsConeOf.Morphism.id hc = { square := CategoryTheory.DGCategory.HomotopySquare.id f, hom := ⟨CategoryTheory.DGCategoryStruct.dgId Z, ⋯⟩, inr_comm := ⋯, fst_comm := ⋯ }
Instances For
Composition of cone morphisms. The underlying degree-zero maps and the homotopies compose strictly, and both cone squares are chased through the middle cone; no shift witness is needed.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A strict square whose two vertical maps are isomorphisms induces an isomorphism between any chosen cones. The forward and inverse maps are the strict cone lifts of the two endpoint isomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cone isomorphism strictly commutes with the target inclusions.
The cone isomorphism strictly commutes with the source projections.