English
For T1,T2 in essImageDistTriang and arrows a,b with a compatibility condition, there exists c such that the distinguished triangle morphisms satisfy the expected equalities after localization.
Русский
Для T1,T2 в essImageDistTriang и стрелок a,b с условиями совместимости существует c такой, что полученные морфизмы треугольников удовлетворяют нужным равенствам в локализации.
LaTeX
$$$\exists c, T_1.mor_2 \;\rightarrow\; c = b \;\rightarrow\; c \;\rightarrow\; T_2.mor_2 \land T_1.mor_3 \; a \,\! 1 \, = c \; T_2.mor_3$$$
Lean4
theorem complete_distinguished_triangle_morphism (T₁ T₂ : Triangle D) (hT₁ : T₁ ∈ L.essImageDistTriang)
(hT₂ : T₂ ∈ L.essImageDistTriang) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂)
(fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁) : ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ a⟦1⟧' = c ≫ T₂.mor₃ :=
by
refine L.complete_distinguished_essImageDistTriang_morphism ?_ T₁ T₂ hT₁ hT₂ a b fac
clear a b fac hT₁ hT₂ T₁ T₂
intro T₁ T₂ hT₁ hT₂ a b fac
obtain ⟨α, hα⟩ := exists_leftFraction L W a
obtain ⟨β, hβ⟩ := (MorphismProperty.RightFraction.mk α.s α.hs T₂.mor₁).exists_leftFraction
obtain ⟨γ, hγ⟩ := exists_leftFraction L W (b ≫ L.map β.s)
have := inverts L W β.s β.hs
have := inverts L W γ.s γ.hs
dsimp at hβ
obtain ⟨Z₂, σ, hσ, fac⟩ :=
(MorphismProperty.map_eq_iff_postcomp L W (α.f ≫ β.f ≫ γ.s) (T₁.mor₁ ≫ γ.f)).1
(by
rw [← cancel_mono (L.map β.s), assoc, assoc, hγ, ← cancel_mono (L.map γ.s), assoc, assoc, assoc, hα,
MorphismProperty.LeftFraction.map_comp_map_s, ← Functor.map_comp] at fac
rw [fac, ← Functor.map_comp_assoc, hβ, Functor.map_comp, Functor.map_comp, Functor.map_comp, assoc,
MorphismProperty.LeftFraction.map_comp_map_s_assoc])
simp only [assoc] at fac
obtain ⟨Y₃, g, h, hT₃⟩ := Pretriangulated.distinguished_cocone_triangle (β.f ≫ γ.s ≫ σ)
let T₃ := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
change T₃ ∈ distTriang C at hT₃
have hβγσ : W (β.s ≫ γ.s ≫ σ) := W.comp_mem _ _ β.hs (W.comp_mem _ _ γ.hs hσ)
obtain ⟨ψ₃, hψ₃, hψ₁, hψ₂⟩ :=
MorphismProperty.compatible_with_triangulation T₂ T₃ hT₂ hT₃ α.s (β.s ≫ γ.s ≫ σ) α.hs hβγσ
(by dsimp [T₃]; rw [reassoc_of% hβ])
let ψ : T₂ ⟶ T₃ := Triangle.homMk _ _ α.s (β.s ≫ γ.s ≫ σ) ψ₃ (by dsimp [T₃]; rw [reassoc_of% hβ]) hψ₁ hψ₂
have : IsIso (L.mapTriangle.map ψ) :=
Triangle.isIso_of_isIsos _ (inverts L W α.s α.hs) (inverts L W _ hβγσ) (inverts L W ψ₃ hψ₃)
refine
⟨L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f (γ.f ≫ σ) fac.symm) ≫
inv (L.mapTriangle.map ψ),
?_, ?_⟩
· rw [← cancel_mono (L.mapTriangle.map ψ).hom₁, ← comp_hom₁, assoc, IsIso.inv_hom_id, comp_id]
dsimp [ψ]
rw [hα, MorphismProperty.LeftFraction.map_comp_map_s]
· rw [← cancel_mono (L.mapTriangle.map ψ).hom₂, ← comp_hom₂, assoc, IsIso.inv_hom_id, comp_id]
dsimp [ψ]
simp only [Functor.map_comp, reassoc_of% hγ, MorphismProperty.LeftFraction.map_comp_map_s_assoc]
