English
The relation of being homotopic on morphisms of a homological complex induces a congruence on the morphisms, i.e., it respects identity, composition, and is compatible with the category structure.
Русский
Отношение гомотопии на морфизмах гомологического комплекса порождает конгруэнцию: сохраняет тождественные и композиционные операции и согласуется со структурой категории.
LaTeX
$$$\text{Congruence}(\text{homotopic } V c)$$$
Lean4
noncomputable instance : IsTriangulated (HomotopyCategory C (ComplexShape.up ℤ)) :=
IsTriangulated.mk'
(by
rintro ⟨X₁ : CochainComplex C ℤ⟩ ⟨X₂ : CochainComplex C ℤ⟩ ⟨X₃ : CochainComplex C ℤ⟩ u₁₂' u₂₃'
obtain ⟨u₁₂, rfl⟩ := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map_surjective u₁₂'
obtain ⟨u₂₃, rfl⟩ := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map_surjective u₂₃'
refine
⟨_, _, _, _, _, _, _, _, Iso.refl _, Iso.refl _, Iso.refl _, by simp, by simp, _, _,
mappingCone_triangleh_distinguished u₁₂, _, _, mappingCone_triangleh_distinguished u₂₃, _, _,
mappingCone_triangleh_distinguished (u₁₂ ≫ u₂₃), ⟨?_⟩⟩
let α := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ (by rw [id_comp])
let β := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) (by rw [comp_id])
refine
Triangulated.Octahedron.mk ((HomotopyCategory.quotient _ _).map α.hom₃)
((HomotopyCategory.quotient _ _).map β.hom₃) ?_ ?_ ?_ ?_ ?_
· exact ((quotient _ _).mapTriangle.map α).comm₂
· exact ((quotient _ _).mapTriangle.map α).comm₃.symm.trans (by dsimp [α]; simp)
· exact ((quotient _ _).mapTriangle.map β).comm₂.trans (by dsimp [β]; simp)
· exact ((quotient _ _).mapTriangle.map β).comm₃
· refine isomorphic_distinguished _ (mappingConeCompTriangleh_distinguished u₁₂ u₂₃) _ ?_
exact
Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by dsimp [α, mappingConeCompTriangleh]; simp)
(by dsimp [β, mappingConeCompTriangleh]; simp) (by dsimp [mappingConeCompTriangleh]; simp))
