instHasTwoOutOfThreePropertyIsoModSerre

English

IsoModSerre has the two-out-of-three property: if two of f, g, and f∘g satisfy isoModSerre, then the third does as well.

Русский

Свойство HasTwoOutOfThreeProperty для isoModSerre: если два из f, g, f∘g удовлетворяют isoModSerre, то и третий тоже.

LaTeX

$$$P.isoModSerre.HasTwoOutOfThreeProperty$$$

Lean4

instance : P.isoModSerre.HasTwoOutOfThreeProperty
    where
  of_postcomp f g hg
    hfg :=
    ⟨P.prop_of_mono (kernel.map f (f ≫ g) (𝟙 _) g (by simp)) hfg.1,
      P.prop_X₂_of_exact ((kernelCokernelCompSequence_exact f g).exact 2) hg.1 hfg.2⟩
  of_precomp f g hf
    hfg :=
    ⟨P.prop_X₂_of_exact ((kernelCokernelCompSequence_exact f g).exact 1) hfg.1 hf.2,
      P.prop_of_epi (cokernel.map (f ≫ g) g f (𝟙 _) (by simp)) hfg.2⟩

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