Theorems · Definition · algebraic geometry

AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom

(R S : CommRingCat) →
  (p : PrimeSpectrum ↑R) →
    [inst : Algebra ↑R ↑S] →
      ↑S →ₐ[↑R]
        ↑(((TopCat.Presheaf.pushforward CommRingCat
                    (AlgebraicGeometry.Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).stalk
            p)

This is the AlgHom version of toPushforwardStalk, which is the map S ⟶ (f∗ 𝒪ₛ)ₚ for some algebra R ⟶ S and some p : Spec R.

Defined in

Mathlib.AlgebraicGeometry.Spec

Cited by

2 results in Mathlib

Foundations

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

Assumes

Algebra