stalk_iso — Mathlib

English

Open immersion criterion via stalk iso: if all stalk maps are isomorphisms, then the morphism is an open immersion.

Русский

Критерий открытого вложения через изоморфизмы stalk: если все stalkMap изоморфны, то морфизм — открытое вложение.

LaTeX

$$$$ \forall x, \ IsIso( f.stalkMap x ) \Rightarrow IsOpenImmersion f $$$$

Lean4

instance stalk_iso {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (x : X) : IsIso (f.stalkMap x) :=
  inferInstanceAs <| IsIso (f.toLRSHom.stalkMap x)

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