to_stalk — Mathlib

English

The composed map equals the open map to the basicOpen on the spectrum.

Русский

Сложенная карта равна открытой карте к basicOpen на спектре.

LaTeX

$$$toBasicOpen_surjective\\_compat := toBasicOpen\\_toMap$$$

Lean4

/-- Stalk of the structure sheaf at a prime p as localization of R -/
instance to_stalk (p : PrimeSpectrum R) : IsLocalization.AtPrime ((structureSheaf R).presheaf.stalk p) p.asIdeal :=
  by
  convert
    (IsLocalization.isLocalization_iff_of_ringEquiv (S := Localization.AtPrime p.asIdeal) _
          (stalkIso R p).symm.commRingCatIsoToRingEquiv).mp
      Localization.isLocalization
  apply Algebra.algebra_ext
  intro
  rw [stalkAlgebra_map]
  congr 2
  change toStalk R p = _ ≫ (stalkIso R p).inv
  rw [Iso.eq_comp_inv]
  exact toStalk_comp_stalkToFiberRingHom R p

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