exists_iso_binaryBiproduct_of_distTriang

English

There exists a canonical isomorphism between two distinguished triangles given an isomorphism between their ends.

Русский

Существует каноническое изоморфическое отображение между двумя распознаваемыми треугольниками, если их концы изоморфны.

LaTeX

$$$\\exists e' : T \\cong T' \\text{ such that } e'.hom_1 = \\text{given}, e'.hom_2 = \\text{given}$$$

Lean4

theorem exists_iso_binaryBiproduct_of_distTriang (T : Triangle C) (hT : T ∈ distTriang C) (zero : T.mor₃ = 0) :
    ∃ (e : T.obj₂ ≅ T.obj₁ ⊞ T.obj₃), T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd :=
  by
  have := T.epi₂ hT zero
  have := isSplitEpi_of_epi T.mor₂
  obtain ⟨fst, hfst⟩ := T.coyoneda_exact₂ hT (𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂) (by simp)
  let d := binaryBiproductData _ hT zero (section_ T.mor₂) (by simp) fst (by simp only [← hfst, sub_add_cancel])
  refine ⟨biprod.uniqueUpToIso _ _ d.isBilimit, ⟨?_, by simp [d]⟩⟩
  ext
  · simpa [d] using d.bicone.inl_fst
  · simpa [d] using d.bicone.inl_snd

Похожие утверждения