glueDataObjι — Mathlib

English

The kernel of the map on Top (the global sections over the open set U) of the glued data object corresponds to the contraction of the ideal by the top iso.

Русский

Ядро отображения на верхнем уровне (глобальные секции над открытым множеством U) у склейки соответствует сокращению идеала по верхнему изоморфизму.

LaTeX

$$$ \\ker( I.glueDataObjι U ).appTop.hom = (I.ideal U).comap U.1.topIso.hom.hom $$$

Lean4

/-- `Spec (𝒪ₓ(U)/I(U)) ⟶ Spec (𝒪ₓ(U)) = U`, the closed immersion into `U`. -/
noncomputable def glueDataObjι (U : X.affineOpens) : I.glueDataObj U ⟶ U.1 :=
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk _)) ≫ U.2.isoSpec.inv

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