instIsSplitEpiMap — Mathlib

English

If f is IsSplitEpi in C, then F.map f is IsSplitEpi for any functor F: C → D.

Русский

Если f является IsSplitEpi в C, то F.map f является IsSplitEpi для любого функторa F: C → D.

LaTeX

$$$ \forall X,Y\; (f: X \to Y) [\mathrm{IsSplitEpi}(f)] (F: C \to D),\; \mathrm{IsSplitEpi}(F.map(f)).$$$

Lean4

instance {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] (F : C ⥤ D) : IsSplitEpi (F.map f) :=
  IsSplitEpi.mk' (hf.exists_splitEpi.some.map F)

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