ofRetract — Mathlib

English

Let F: C → D be a functor that preserves monomorphisms. If G is a retract of F in the functor category, then G also preserves monomorphisms.

Русский

Пусть F: C → D — функтор, сохраняющий мономорфизмы. Если G является ретрактом F в категории функторов, то и G сохраняет мономорфизмы.

LaTeX

$$$$ \\mathrm{PMon}(F) \\land \\mathrm{Retr}(G,F) \\Rightarrow \\mathrm{PMon}(G). $$$$

Lean4

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

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