opensRange_glueDataObjMap — Mathlib

English

The opensRange under glueDataObjMap composed with glueDataObjι matches the opens described by preimages through isomorphisms.

Русский

opensRange под glueDataObjMap после glueDataObjι совпадает с открытыми, заданными предобразами через изоморфизмы.

LaTeX

$$$ (I.glueDataObjMap ⋯).opensRange = (TopologicalSpace.Opens.map (I.glueDataObjι ⋯).base).obj (X.basicOpen f) $$$

Lean4

theorem opensRange_glueDataObjMap {V : X.affineOpens} (f : Γ(X, V.1)) :
    (I.glueDataObjMap (X.affineBasicOpen_le f)).opensRange = (I.glueDataObjι V) ⁻¹ᵁ (V.1.ι ⁻¹ᵁ X.basicOpen f) :=
  by
  letI := (Ideal.quotientMap _ _ (I.ideal_le_comap_ideal (X.affineBasicOpen_le f))).toAlgebra
  let f' : Γ(X, V) ⧸ I.ideal V := Ideal.Quotient.mk _ f
  have := I.isLocalization_away (X.affineBasicOpen_le f) f rfl
  ext1
  refine (localization_away_comap_range _ f').trans ?_
  rw [← comap_basicOpen, ← V.2.fromSpec_preimage_basicOpen, ← Scheme.preimage_comp, glueDataObjι_ι]
  rfl

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