isLocalization_stalk' — Mathlib

English

At the prime corresponding to a point in an affine open, the stalk localization along the base ring is isomorphic to the stalk over the corresponding affine localization.

Русский

Для прайма, соответствующего точке в аффинном открытом, локализация на уровне stalk совпадает с локализацией на уровне stalk по соответствующему аффинному локализованию.

LaTeX

$$$@IsLocalization.AtPrime (R := Γ(X,U)) (S := X.presheaf.stalk (h_U.fromSpec.base y)) _ _ ((TopCat.Presheaf.algebra_section_stalk X.presheaf _)) y.asIdeal _$$$

Lean4

theorem isLocalization_stalk' (y : PrimeSpectrum Γ(X, U)) (hy : hU.fromSpec.base y ∈ U) :
    @IsLocalization.AtPrime (R := Γ(X, U)) (S := X.presheaf.stalk <| hU.fromSpec.base y) _ _
      ((TopCat.Presheaf.algebra_section_stalk X.presheaf _)) y.asIdeal _ :=
  by
  apply
    (@IsLocalization.isLocalization_iff_of_ringEquiv (R := Γ(X, U)) (S := X.presheaf.stalk (hU.fromSpec.base y)) _
        y.asIdeal.primeCompl _ (TopCat.Presheaf.algebra_section_stalk X.presheaf ⟨hU.fromSpec.base y, hy⟩) _ _
        (asIso <| hU.fromSpec.stalkMap y).commRingCatIsoToRingEquiv).mpr
  convert StructureSheaf.IsLocalization.to_stalk Γ(X, U) y using 1
  delta IsLocalization.AtPrime StructureSheaf.stalkAlgebra
  rw [RingHom.algebraMap_toAlgebra, RingEquiv.toRingHom_eq_coe, CategoryTheory.Iso.commRingCatIsoToRingEquiv_toRingHom,
    asIso_hom, ← CommRingCat.hom_comp, Scheme.stalkMap_germ, IsAffineOpen.fromSpec_app_self, Category.assoc,
    TopCat.Presheaf.germ_res]
  rfl

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