isIso_toSpec — Mathlib

English

The morphism toSpec 𝒜 f is an isomorphism of schemes; in particular, the base morphism is an open immersion that is an isomorphism onto its image.

Русский

Гранина toSpec 𝒜 f является изоморфизмом схем; в частности, основание отображения является открытым внедрением, изоморфным на образ.

LaTeX

$$$$\text{IsIso}(toSpec\ 𝒜 f)$$$$

Lean4

theorem isIso_toSpec (f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : IsIso (toSpec 𝒜 f) :=
  by
  haveI : IsIso (toSpec 𝒜 f).base := toSpec_base_isIso 𝒜 f_deg hm
  haveI _ (x) : IsIso ((toSpec 𝒜 f).stalkMap x) := by rw [stalkMap_toSpec 𝒜 f x f_deg hm]; infer_instance
  haveI : LocallyRingedSpace.IsOpenImmersion (toSpec 𝒜 f) :=
    LocallyRingedSpace.IsOpenImmersion.of_stalk_iso (toSpec 𝒜 f)
      (TopCat.homeoOfIso (asIso <| (toSpec 𝒜 f).base)).isOpenEmbedding
  exact LocallyRingedSpace.IsOpenImmersion.to_iso _

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