Theorems · Definition · algebraic geometry

AlgebraicGeometry.StructureSheaf.toPushforwardStalk

{R S : CommRingCat} →
  (f : R ⟶ S) →
    (p : PrimeSpectrum ↑R) →
      S ⟶
        ((TopCat.Presheaf.pushforward CommRingCat (AlgebraicGeometry.Spec.topMap f)).obj
              (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).stalk
          p

For an algebra f : R →+* S, this is the ring homomorphism S →+* (f∗ 𝒪ₛ)ₚ for a p : Spec R. This is shown to be the localization at p in isLocalizedModule_toPushforwardStalkAlgHom.

Defined in

Mathlib.AlgebraicGeometry.Spec

Cited by

3 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound