isoModSerre_iff_of_mono — Mathlib

English

For a mono morphism f, the Serre-mod Serre property is equivalent to the epi-mod Serre property: P.isoModSerre f ↔ P.epiModSerre f.

Русский

Для моно-морфизма f верно, что свойство P.isoModSerre f эквивалентно P.epiModSerre f.

LaTeX

$$$\forall X,Y\ f:X\to Y\,(\operatorname{Mono}(f)\Rightarrow (P\operatorname{isoModSerre}(f) \iff P\operatorname{epiModSerre}(f)))$$$

Lean4

theorem isoModSerre_iff_of_mono {X Y : C} (f : X ⟶ Y) [Mono f] : P.isoModSerre f ↔ P.epiModSerre f :=
  by
  have := P.monoModSerre_of_mono f
  rw [isoModSerre_iff]
  tauto

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