isoModSerre_iff_of_epi — Mathlib

English

For epi morphisms f, the isoModSerre property is equivalent to the monoModSerre property: P.isoModSerre f ↔ P.monoModSerre f.

Русский

Для эпиморфизмов f свойство P.isoModSerre f эквивалентно P.monoModSerre f.

LaTeX

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

Lean4

theorem isoModSerre_iff_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] : P.isoModSerre f ↔ P.monoModSerre f :=
  by
  have := P.epiModSerre_of_epi f
  rw [isoModSerre_iff]
  tauto

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