to_iso — Mathlib

English

If f is an open immersion and epi on the base, then f is an isomorphism; equivalently, the associated morphism to locally ringed spaces reflects isomorphisms.

Русский

Если f — открытое вложение и Эпихим на основание, то f является изоморфизмом; эквивалентно отображение изоморфизмов в локально кольцевых пространствах.

LaTeX

$$$$ IsOpenImmersion(f) \land Epimorphic(f.base) \Rightarrow IsIso(f) $$$$

Lean4

theorem to_iso {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsOpenImmersion f] [Epi f.base] : IsIso f :=
  @isIso_of_reflects_iso _ _ _ _ _ _ f
    (Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)
    (@PresheafedSpace.IsOpenImmersion.to_iso _ _ _ _ f.toPshHom h _) _

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