mono_of_injective — Mathlib

English

The property SurjectiveOnStalks is Zariski-local at the source as well.

Русский

Свойство SurjectiveOnStalks локально по зарику на источнике.

LaTeX

$$IsZariskiLocalAtSource @SurjectiveOnStalks$$

Lean4

theorem mono_of_injective [SurjectiveOnStalks f] (hf : Function.Injective f.base) : Mono f :=
  by
  refine (Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).mono_of_mono_map ?_
  apply SheafedSpace.mono_of_base_injective_of_stalk_epi
  · exact hf
  · exact fun x ↦ ConcreteCategory.epi_of_surjective _ (f.stalkMap_surjective x)

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