glueDataObjCarrierIso — Mathlib

English

The underlying topological space of Spec(𝒪ₓ(U)/I(U)) is homeomorphic to its image inside X.

Русский

Общая топологическая структура Spec(𝒪ₓ(U)/I(U)) гомеоморфна его образу внутри X.

LaTeX

$$$ I.glueDataObjCarrierIso U : (I.glueDataObj U).carrier \\cong TopCat.of ∗(X.zeroLocus (I.ideal U) ∩ U) $$$

Lean4

/-- The underlying space of `Spec (𝒪ₓ(U)/I(U))` is homeomorphic to its image in `X`. -/
noncomputable def glueDataObjCarrierIso (U : X.affineOpens) :
    (I.glueDataObj U).carrier ≅ TopCat.of ↑(X.zeroLocus (U := U) (I.ideal U) ∩ U) :=
  TopCat.isoOfHomeo ((I.glueDataObjι U ≫ U.1.ι).isEmbedding.toHomeomorph.trans (.setCongr (I.range_glueDataObjι_ι U)))

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