map_mono — Mathlib

English

Every functor preserves monomorphisms under the assumption of preserving monos, i.e., map of mono is mono.

Русский

Каждый функтор сохраняет моно-морфизмы при предположении сохранения моно, т.е. образ моно-морфизма — моно.

LaTeX

$$MonoMap := Mono (F.map f) if Mono f and F preserves monos$$

Lean4

instance map_mono (F : C ⥤ D) [PreservesMonomorphisms F] {X Y : C} (f : X ⟶ Y) [Mono f] : Mono (F.map f) :=
  PreservesMonomorphisms.preserves f

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