ofRetract — Mathlib

English

If r : Retract G F, and F preserves epimorphisms, then G preserves epimorphisms.

Русский

Если r : Retract G F и F сохраняет эпиморфизмы, тогда G сохраняет эпиморфизмы.

LaTeX

$$Retract(G,F) ∧ PreservesEpimorphisms F ⇒ PreservesEpimorphisms G$$

Lean4

theorem ofRetract {F G : C ⥤ D} (r : Retract G F) [F.PreservesEpimorphisms] : G.PreservesEpimorphisms where
  preserves := (preservesEpimorphisms.of_natTrans r.r).preserves

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