mono

Mathlib.Geometry.RingedSpace.OpenImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.mono

English

Open immersions are monomorphisms.

Русский

Открытые погружения являются монообразованиями.

LaTeX

$$$ \mathrm{Mono}(f) $$$

Lean4

instance mono : Mono f :=
  LocallyRingedSpace.forgetToSheafedSpace.mono_of_mono_map (show Mono f.toShHom by infer_instance)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru