mono_of_presheaf_mono — Mathlib

English

A morphism of sheaves is mono if its underlying presheaf morphism is mono (under suitable assumptions).

Русский

Морфизм шейфов моно тогда и только тогда, когда его базовый морфизм между прешейфами моно (при некоторых допущениях).

LaTeX

$$$\\text{Mono}(f) \\iff \\text{Mono}(f.1)$ under suitable assumptions.$$

Lean4

/-- This is stated as a lemma to prevent class search from forming a loop since a sheaf morphism is
monic if and only if it is monic as a presheaf morphism (under suitable assumption). -/
theorem mono_of_presheaf_mono {F G : Sheaf J A} (f : F ⟶ G) [h : Mono f.1] : Mono f :=
  (sheafToPresheaf J A).mono_of_mono_map h

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