English
From the octahedron axiom, one can choose a concrete octahedron for a given distinguished triangle data.
Русский
Из аксиомы октaэдра можно выбрать конкретный октaэдр для данных выделенного треугольника.
LaTeX
$$$\\text{someOctahedron} : \\text{Octahedron comm h_1 h_2 h_3$ for given data}$$
Lean4
/-- When two diagrams are isomorphic, an octahedron for one gives an octahedron for the other. -/
def ofIso {X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C} (u₁₂' : X₁' ⟶ X₂') (u₂₃' : X₂' ⟶ X₃') (u₁₃' : X₁' ⟶ X₃')
(comm' : u₁₂' ≫ u₂₃' = u₁₃') (e₁ : X₁ ≅ X₁') (e₂ : X₂ ≅ X₂') (e₃ : X₃ ≅ X₃') (comm₁₂ : u₁₂ ≫ e₂.hom = e₁.hom ≫ u₁₂')
(comm₂₃ : u₂₃ ≫ e₃.hom = e₂.hom ≫ u₂₃') (v₁₂' : X₂' ⟶ Z₁₂') (w₁₂' : Z₁₂' ⟶ X₁'⟦(1 : ℤ)⟧)
(h₁₂' : Triangle.mk u₁₂' v₁₂' w₁₂' ∈ distTriang C) (v₂₃' : X₃' ⟶ Z₂₃') (w₂₃' : Z₂₃' ⟶ X₂'⟦(1 : ℤ)⟧)
(h₂₃' : Triangle.mk u₂₃' v₂₃' w₂₃' ∈ distTriang C) (v₁₃' : X₃' ⟶ Z₁₃') (w₁₃' : Z₁₃' ⟶ X₁'⟦(1 : ℤ)⟧)
(h₁₃' : Triangle.mk (u₁₃') v₁₃' w₁₃' ∈ distTriang C) (H : Octahedron comm' h₁₂' h₂₃' h₁₃') :
Octahedron comm h₁₂ h₂₃ h₁₃ :=
by
let iso₁₂ := isoTriangleOfIso₁₂ _ _ h₁₂ h₁₂' e₁ e₂ comm₁₂
let iso₂₃ := isoTriangleOfIso₁₂ _ _ h₂₃ h₂₃' e₂ e₃ comm₂₃
let iso₁₃ :=
isoTriangleOfIso₁₂ _ _ h₁₃ h₁₃' e₁ e₃ (by dsimp; rw [← comm, assoc, ← comm', ← reassoc_of% comm₁₂, comm₂₃])
have eq₁₂ := iso₁₂.hom.comm₂
have eq₁₂' := iso₁₂.hom.comm₃
have eq₁₃ := iso₁₃.hom.comm₂
have eq₁₃' := iso₁₃.hom.comm₃
have eq₂₃ := iso₂₃.hom.comm₂
have eq₂₃' := iso₂₃.hom.comm₃
have rel₁₂ := H.triangleMorphism₁.comm₂
have rel₁₃ := H.triangleMorphism₁.comm₃
have rel₂₂ := H.triangleMorphism₂.comm₂
have rel₂₃ := H.triangleMorphism₂.comm₃
dsimp [iso₁₂, iso₂₃, iso₁₃] at eq₁₂ eq₁₂' eq₁₃ eq₁₃' eq₂₃ eq₂₃' rel₁₂ rel₁₃ rel₂₂ rel₂₃
rw [Functor.map_id, comp_id] at rel₁₃
rw [id_comp] at rel₂₂
refine ⟨iso₁₂.hom.hom₃ ≫ H.m₁ ≫ iso₁₃.inv.hom₃, iso₁₃.hom.hom₃ ≫ H.m₃ ≫ iso₂₃.inv.hom₃, ?_, ?_, ?_, ?_, ?_⟩
· rw [reassoc_of% eq₁₂, ← cancel_mono iso₁₃.hom.hom₃, assoc, assoc, assoc, assoc, iso₁₃.inv_hom_id_triangle_hom₃,
eq₁₃, reassoc_of% comm₂₃, ← rel₁₂]
dsimp
rw [comp_id]
·
rw [← cancel_mono (e₁.hom⟦(1 : ℤ)⟧'), eq₁₂', assoc, assoc, assoc, eq₁₃', iso₁₃.inv_hom_id_triangle_hom₃_assoc, ←
rel₁₃]
· rw [reassoc_of% eq₁₃, reassoc_of% rel₂₂, ← cancel_mono iso₂₃.hom.hom₃, assoc, assoc, iso₂₃.inv_hom_id_triangle_hom₃,
eq₂₃]
dsimp
rw [comp_id]
·
rw [← cancel_mono (e₂.hom⟦(1 : ℤ)⟧'), assoc, assoc, assoc, assoc, eq₂₃', iso₂₃.inv_hom_id_triangle_hom₃_assoc, ←
rel₂₃, ← Functor.map_comp, comm₁₂, Functor.map_comp, reassoc_of% eq₁₃']
· refine isomorphic_distinguished _ H.mem _ ?_
refine
Triangle.isoMk _ _ (Triangle.π₃.mapIso iso₁₂) (Triangle.π₃.mapIso iso₁₃) (Triangle.π₃.mapIso iso₂₃) (by simp)
(by simp) ?_
dsimp
rw [assoc, ← Functor.map_comp, eq₁₂, Functor.map_comp, reassoc_of% eq₂₃']
