instIsSplitMonoApp — Mathlib

English

If f: F → G is split mono, then each component f.app X is split mono.

Русский

Если f: F → G разложимо по диагонали (split mono), тогда каждый компонент f.app X разложим по диагонали.

LaTeX

$$IsSplitMono f ⇒ ∀ X, IsSplitMono (f.app X)$$

Lean4

instance {F G : C ⥤ D} (f : F ⟶ G) [IsSplitMono f] (X : C) : IsSplitMono (f.app X) :=
  inferInstanceAs (IsSplitMono (((evaluation C D).obj X).map f))

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