instSplitEpiCategory — Mathlib

English

If φ.hom1 is an isomorphism, then T.obj3 is zero.

Русский

Если φ.hom1 изоморфизм, то T.obj3 нулевой.

LaTeX

$$$(T \\in \\mathrm{distTriang} \\, C) \\Rightarrow \\mathrm{IsIso}(T.mor_1) \\Rightarrow \\mathrm{IsZero}(T.obj_3)$$$

Lean4

instance : SplitEpiCategory C where
  isSplitEpi_of_epi f
    hf := by
    obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f
    obtain ⟨r, hr⟩ := Triangle.coyoneda_exact₂ _ hT (𝟙 _) (by rw [Triangle.mor₂_eq_zero_of_epi₁ _ hT hf, comp_zero])
    exact ⟨r, hr.symm⟩

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