English
Given two triangles T1,T2 in essImageDistTriang and arrows a,b satisfying a relation, there exists a mediating morphism c making the relevant square commute and extend the distinguished triangles appropriately.
Русский
Для треугольников T1,T2 из essImageDistTriang и стрелок a,b удовлетворяющих условию, существует медиатор c, делающий соответствующую диагональ выполнимой и корректно продолжающей тяготение треугольников.
LaTeX
$$$\exists c:\; T_1.mor_2 \to T_2.mor_2 \;\land\; T_1.mor_3 \; a\; =\; c \; T_2.mor_3$$$
Lean4
theorem complete_distinguished_essImageDistTriang_morphism
(H :
∀ (T₁' T₂' : Triangle C) (_ : T₁' ∈ distTriang C) (_ : T₂' ∈ distTriang C)
(a : L.obj (T₁'.obj₁) ⟶ L.obj (T₂'.obj₁)) (b : L.obj (T₁'.obj₂) ⟶ L.obj (T₂'.obj₂))
(_ : L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁),
∃ (φ : L.mapTriangle.obj T₁' ⟶ L.mapTriangle.obj T₂'), φ.hom₁ = a ∧ φ.hom₂ = b)
(T₁ T₂ : Triangle D) (hT₁ : T₁ ∈ Functor.essImageDistTriang L) (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
obtain ⟨T₁', e₁, hT₁'⟩ := hT₁
obtain ⟨T₂', e₂, hT₂'⟩ := hT₂
have comm₁ := e₁.inv.comm₁
have comm₁' := e₂.hom.comm₁
have comm₂ := e₁.hom.comm₂
have comm₂' := e₂.hom.comm₂
have comm₃ := e₁.inv.comm₃
have comm₃' := e₂.hom.comm₃
dsimp at comm₁ comm₁' comm₂ comm₂' comm₃ comm₃'
simp only [assoc] at comm₃
obtain ⟨φ, hφ₁, hφ₂⟩ :=
H T₁' T₂' hT₁' hT₂' (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂)
(by simp only [assoc, ← comm₁', ← reassoc_of% fac, ← reassoc_of% comm₁])
have h₂ := φ.comm₂
have h₃ := φ.comm₃
dsimp at h₂ h₃
simp only [assoc] at h₃
refine ⟨e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃, ?_, ?_⟩
·
rw [reassoc_of% comm₂, reassoc_of% h₂, hφ₂, assoc, assoc, Iso.hom_inv_id_triangle_hom₂_assoc, ← reassoc_of% comm₂',
Iso.hom_inv_id_triangle_hom₃, comp_id]
·
rw [assoc, assoc, ← cancel_epi e₁.inv.hom₃, ← reassoc_of% comm₃, Iso.inv_hom_id_triangle_hom₃_assoc, ←
cancel_mono (e₂.hom.hom₁⟦(1 : ℤ)⟧'), assoc, assoc, assoc, assoc, assoc, ← Functor.map_comp, ← Functor.map_comp, ←
hφ₁, h₃, comm₃', Iso.inv_hom_id_triangle_hom₃_assoc]
