epiModSerre_of_epi — Mathlib

English

Let C be an abelian category and P an object property that forms a Serre class. If f: X → Y is an epimorphism, then f belongs to the Serre-modification associated to P, i.e. P.epiModSerre f holds.

Русский

Пусть C — абелева категория, P — свойство объектов, образующее класс Серре. Если f: X ⟶ Y — эпиморфизм, то он принадлежит к серр-обновлению, т.е. P.epiModSerre f.

LaTeX

$$$\forall X,Y\ f:X\to Y\,\big(\operatorname{Epi}(f)\Rightarrow P\operatorname{epiModSerre}(f)\big)$$$

Lean4

theorem epiModSerre_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] : P.epiModSerre f :=
  P.epimorphisms_le_epiModSerre f (epimorphisms.infer_property f)

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