instIsSplitMonoMap — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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