mono_of_injective — Mathlib

English

If for a morphism f, each component f.app X is injective, then f is mono.

Русский

Если каждый компонент f.app X инъективен, то f является монообразом.

LaTeX

$$$\\forall X,\\, \\mathrm{Injective}(f.app X) \\Rightarrow \\mathrm{Mono}(f)$$$

Lean4

theorem mono_of_injective (hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Injective (f.app X)) : Mono f where
  right_cancellation {M} g₁ g₂
    hg := by
    ext X m
    exact hf (congr_fun ((evaluation R X ⋙ forget _).congr_map hg) m)

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