injective_of_mono — Mathlib

English

If f is mono in PresheafOfModules, then for every X the map f.app X is injective.

Русский

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

LaTeX

$$$[Mono\\ f] \\Rightarrow \\forall X, \\ Function.Injective (f.app X)$$$

Lean4

theorem injective_of_mono [Mono f] (X : Cᵒᵖ) : Function.Injective (f.app X) :=
  by
  rw [← ModuleCat.mono_iff_injective]
  infer_instance

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