instHasBinaryBiproducts — Mathlib

English

If mor1 and mor2 are isomorphisms, mor3 is an isomorphism.

Русский

Если mor1 и mor2 изоморфизмы, mor3 изоморфизм.

LaTeX

$$$(T,T' \\in \\mathrm{distTriang} \\, C) \\Rightarrow \\mathrm{IsIso}(\\phi.hom_1) \\Rightarrow \\mathrm{IsIso}(\\phi.hom_2) \\Rightarrow \\mathrm{IsIso}(\\phi.hom_3)$$$

Lean4

instance : HasBinaryBiproducts C :=
  ⟨fun X₁ X₃ => by
    obtain ⟨X₂, inl, snd, mem⟩ := distinguished_cocone_triangle₂ (0 : X₃ ⟶ X₁⟦(1 : ℤ)⟧)
    obtain ⟨inr : X₃ ⟶ X₂, inr_snd : 𝟙 _ = inr ≫ snd⟩ := Triangle.coyoneda_exact₃ _ mem (𝟙 X₃) (by simp)
    obtain ⟨fst : X₂ ⟶ X₁, hfst : 𝟙 X₂ - snd ≫ inr = fst ≫ inl⟩ :=
      Triangle.coyoneda_exact₂ _ mem (𝟙 X₂ - snd ≫ inr)
        (by
          dsimp
          simp only [sub_comp, assoc, id_comp, ← inr_snd, comp_id, sub_self])
    refine ⟨⟨binaryBiproductData _ mem rfl inr inr_snd.symm fst ?_⟩⟩
    dsimp
    simp only [← hfst, sub_add_cancel]⟩

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