instSplitMonoCategory — Mathlib

English

In a diagram of distinguished triangles with φ, if φ.hom₂ is an isomorphism and φ.hom₃ isomorphism, then φ.hom₁ is an isomorphism.

Русский

В диаграмме распознаваемых треугольников с φ, если φ.hom2 и φ.hom3 изоморфизм, то φ.hom1 изоморфизм.

LaTeX

$$${(T,T',φ)\\;}{\\in distTriang }$$$

Lean4

instance : SplitMonoCategory C where
  isSplitMono_of_mono f
    hf := by
    obtain ⟨X, g, h, hT⟩ := distinguished_cocone_triangle₁ f
    obtain ⟨r, hr⟩ := Triangle.yoneda_exact₂ _ hT (𝟙 _) (by rw [Triangle.mor₁_eq_zero_of_mono₂ _ hT hf, zero_comp])
    exact ⟨r, hr.symm⟩

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