$Spec$ as a functor to locally ringed spaces.

We define the functor $Spec$ from commutative rings to locally ringed spaces.

Implementation notes

We define $Spec$ in three consecutive steps, each with more structure than the last:

1. Spec.toTop, valued in the category of topological spaces,
2. Spec.toSheafedSpace, valued in the category of sheafed spaces and
3. Spec.toLocallyRingedSpace, valued in the category of locally ringed spaces.

Additionally, we provide Spec.toPresheafedSpace as a composition of Spec.toSheafedSpace with a forgetful functor.

Related results

The adjunction Γ ⊣ Spec is constructed in Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean.

def AlgebraicGeometry.Spec.topObj (R : CommRingCat) : TopCat

The spectrum of a commutative ring, as a topological space.

def AlgebraicGeometry.Spec.topMap {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) : AlgebraicGeometry.Spec.topObj S ⟶ AlgebraicGeometry.Spec.topObj R

The induced map of a ring homomorphism on the ring spectra, as a morphism of topological spaces.

@[simp]

theorem AlgebraicGeometry.Spec.topMap_id (R : CommRingCat) : AlgebraicGeometry.Spec.topMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec.topObj R)

theorem AlgebraicGeometry.Spec.topMap_comp {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) : AlgebraicGeometry.Spec.topMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.topMap g) (AlgebraicGeometry.Spec.topMap f)

@[simp]

theorem AlgebraicGeometry.Spec.toTop_map {R : CommRingCatᵒᵖ} {S : CommRingCatᵒᵖ} (f : R ⟶ S) : AlgebraicGeometry.Spec.toTop.map f = AlgebraicGeometry.Spec.topMap f.unop

@[simp]

theorem AlgebraicGeometry.Spec.toTop_obj (R : CommRingCatᵒᵖ) : AlgebraicGeometry.Spec.toTop.obj R = AlgebraicGeometry.Spec.topObj R.unop

def AlgebraicGeometry.Spec.toTop : CategoryTheory.Functor CommRingCatᵒᵖ TopCat

The spectrum, as a contravariant functor from commutative rings to topological spaces.

@[simp]

theorem AlgebraicGeometry.Spec.sheafedSpaceObj_carrier (R : CommRingCat) : ↑(AlgebraicGeometry.Spec.sheafedSpaceObj R).toPresheafedSpace = AlgebraicGeometry.Spec.topObj R

@[simp]

theorem AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf (R : CommRingCat) : (AlgebraicGeometry.Spec.sheafedSpaceObj R).toPresheafedSpace.presheaf = (AlgebraicGeometry.Spec.structureSheaf ↑R).val

def AlgebraicGeometry.Spec.sheafedSpaceObj (R : CommRingCat) : AlgebraicGeometry.SheafedSpace CommRingCat

The spectrum of a commutative ring, as a SheafedSpace.

@[simp]

theorem AlgebraicGeometry.Spec.sheafedSpaceMap_base {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) : (AlgebraicGeometry.Spec.sheafedSpaceMap f).base = AlgebraicGeometry.Spec.topMap f

@[simp]

theorem AlgebraicGeometry.Spec.sheafedSpaceMap_c_app {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (U : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Spec.sheafedSpaceObj R).toPresheafedSpace)ᵒᵖ) : (AlgebraicGeometry.Spec.sheafedSpaceMap f).c.app U = AlgebraicGeometry.StructureSheaf.comap f U.unop ((TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.topMap f)).obj U.unop) (_ : ∀ (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑S)), x ∈ ((TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.topMap f)).obj U.unop).carrier → x ∈ ((TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.topMap f)).obj U.unop).carrier)

def AlgebraicGeometry.Spec.sheafedSpaceMap {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) : AlgebraicGeometry.Spec.sheafedSpaceObj S ⟶ AlgebraicGeometry.Spec.sheafedSpaceObj R

The induced map of a ring homomorphism on the ring spectra, as a morphism of sheafed spaces.

@[simp]

theorem AlgebraicGeometry.Spec.sheafedSpaceMap_id {R : CommRingCat} : AlgebraicGeometry.Spec.sheafedSpaceMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec.sheafedSpaceObj R)

theorem AlgebraicGeometry.Spec.sheafedSpaceMap_comp {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) : AlgebraicGeometry.Spec.sheafedSpaceMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.sheafedSpaceMap g) (AlgebraicGeometry.Spec.sheafedSpaceMap f)

@[simp]

theorem AlgebraicGeometry.Spec.toSheafedSpace_obj (R : CommRingCatᵒᵖ) : AlgebraicGeometry.Spec.toSheafedSpace.obj R = AlgebraicGeometry.Spec.sheafedSpaceObj R.unop

@[simp]

theorem AlgebraicGeometry.Spec.toSheafedSpace_map : ∀ {X Y : CommRingCatᵒᵖ} (f : X ⟶ Y), AlgebraicGeometry.Spec.toSheafedSpace.map f = AlgebraicGeometry.Spec.sheafedSpaceMap f.unop

def AlgebraicGeometry.Spec.toSheafedSpace : CategoryTheory.Functor CommRingCatᵒᵖ (AlgebraicGeometry.SheafedSpace CommRingCat)

Spec, as a contravariant functor from commutative rings to sheafed spaces.

def AlgebraicGeometry.Spec.toPresheafedSpace : CategoryTheory.Functor CommRingCatᵒᵖ (AlgebraicGeometry.PresheafedSpace CommRingCat)

Spec, as a contravariant functor from commutative rings to presheafed spaces.

@[simp]

theorem AlgebraicGeometry.Spec.toPresheafedSpace_obj (R : CommRingCatᵒᵖ) : AlgebraicGeometry.Spec.toPresheafedSpace.obj R = (AlgebraicGeometry.Spec.sheafedSpaceObj R.unop).toPresheafedSpace

theorem AlgebraicGeometry.Spec.toPresheafedSpace_obj_op (R : CommRingCat) : AlgebraicGeometry.Spec.toPresheafedSpace.obj (Opposite.op R) = (AlgebraicGeometry.Spec.sheafedSpaceObj R).toPresheafedSpace

@[simp]

theorem AlgebraicGeometry.Spec.toPresheafedSpace_map (R : CommRingCatᵒᵖ) (S : CommRingCatᵒᵖ) (f : R ⟶ S) : AlgebraicGeometry.Spec.toPresheafedSpace.map f = AlgebraicGeometry.Spec.sheafedSpaceMap f.unop

theorem AlgebraicGeometry.Spec.toPresheafedSpace_map_op (R : CommRingCat) (S : CommRingCat) (f : R ⟶ S) : AlgebraicGeometry.Spec.toPresheafedSpace.map f.op = AlgebraicGeometry.Spec.sheafedSpaceMap f

theorem AlgebraicGeometry.Spec.basicOpen_hom_ext {X : AlgebraicGeometry.RingedSpace} {R : CommRingCat} {α : X ⟶ AlgebraicGeometry.Spec.sheafedSpaceObj R} {β : X ⟶ AlgebraicGeometry.Spec.sheafedSpaceObj R} (w : α.base = β.base) (h : ∀ (r : ↑R), let U := PrimeSpectrum.basicOpen r; CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑R) U) (α.c.app (Opposite.op U))) (X.presheaf.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map α.base).op.obj (Opposite.op U) = (TopologicalSpace.Opens.map β.base).op.obj (Opposite.op U)))) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑R) U) (β.c.app (Opposite.op U))) : α = β

@[simp]

theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_toSheafedSpace (R : CommRingCat) : (AlgebraicGeometry.Spec.locallyRingedSpaceObj R).toSheafedSpace = AlgebraicGeometry.Spec.sheafedSpaceObj R

def AlgebraicGeometry.Spec.locallyRingedSpaceObj (R : CommRingCat) : AlgebraicGeometry.LocallyRingedSpace

The spectrum of a commutative ring, as a LocallyRingedSpace.

theorem AlgebraicGeometry.stalkMap_toStalk_apply {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) (x : (CategoryTheory.forget CommRingCat).obj (CommRingCat.of ↑R)) : ↑(AlgebraicGeometry.PresheafedSpace.stalkMap (AlgebraicGeometry.Spec.sheafedSpaceMap f) p) (↑(AlgebraicGeometry.StructureSheaf.toStalk (↑R) (↑(PrimeSpectrum.comap f) p)) x) = ↑(CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toStalk (↑S) p)) x

theorem AlgebraicGeometry.stalkMap_toStalk {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑R) (↑(PrimeSpectrum.comap f) p)) (AlgebraicGeometry.PresheafedSpace.stalkMap (AlgebraicGeometry.Spec.sheafedSpaceMap f) p) = CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toStalk (↑S) p)

theorem AlgebraicGeometry.localRingHom_comp_stalkIso_apply {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) (x : (CategoryTheory.forget CommRingCat).obj (TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (AlgebraicGeometry.Spec.structureSheaf ↑R)) (↑(PrimeSpectrum.comap f) p))) : ↑(AlgebraicGeometry.StructureSheaf.localizationToStalk (↑S) p) (↑(Localization.localRingHom (↑(PrimeSpectrum.comap f) p).asIdeal p.asIdeal f (_ : (↑(PrimeSpectrum.comap f) p).asIdeal = (↑(PrimeSpectrum.comap f) p).asIdeal)) (↑(AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom (↑R) (↑(PrimeSpectrum.comap f) p)) x)) = ↑(AlgebraicGeometry.PresheafedSpace.stalkMap (AlgebraicGeometry.Spec.sheafedSpaceMap f) p) x

theorem AlgebraicGeometry.localRingHom_comp_stalkIso {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.stalkIso (↑R) (↑(PrimeSpectrum.comap f) p)).hom (CategoryTheory.CategoryStruct.comp (Localization.localRingHom (↑(PrimeSpectrum.comap f) p).asIdeal p.asIdeal f (_ : (↑(PrimeSpectrum.comap f) p).asIdeal = (↑(PrimeSpectrum.comap f) p).asIdeal)) (AlgebraicGeometry.StructureSheaf.stalkIso (↑S) p).inv) = AlgebraicGeometry.PresheafedSpace.stalkMap (AlgebraicGeometry.Spec.sheafedSpaceMap f) p

Under the isomorphisms stalkIso, the map stalkMap (Spec.sheafedSpaceMap f) p corresponds to the induced local ring homomorphism Localization.localRingHom.

@[simp]

theorem AlgebraicGeometry.Spec.locallyRingedSpaceMap_val {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) : (AlgebraicGeometry.Spec.locallyRingedSpaceMap f).val = AlgebraicGeometry.Spec.sheafedSpaceMap f

def AlgebraicGeometry.Spec.locallyRingedSpaceMap {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) : AlgebraicGeometry.Spec.locallyRingedSpaceObj S ⟶ AlgebraicGeometry.Spec.locallyRingedSpaceObj R

The induced map of a ring homomorphism on the prime spectra, as a morphism of locally ringed spaces.

@[simp]

theorem AlgebraicGeometry.Spec.locallyRingedSpaceMap_id (R : CommRingCat) : AlgebraicGeometry.Spec.locallyRingedSpaceMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec.locallyRingedSpaceObj R)

theorem AlgebraicGeometry.Spec.locallyRingedSpaceMap_comp {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) : AlgebraicGeometry.Spec.locallyRingedSpaceMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.locallyRingedSpaceMap g) (AlgebraicGeometry.Spec.locallyRingedSpaceMap f)

@[simp]

theorem AlgebraicGeometry.Spec.toLocallyRingedSpace_obj (R : CommRingCatᵒᵖ) : AlgebraicGeometry.Spec.toLocallyRingedSpace.obj R = AlgebraicGeometry.Spec.locallyRingedSpaceObj R.unop

@[simp]

theorem AlgebraicGeometry.Spec.toLocallyRingedSpace_map : ∀ {X Y : CommRingCatᵒᵖ} (f : X ⟶ Y), AlgebraicGeometry.Spec.toLocallyRingedSpace.map f = AlgebraicGeometry.Spec.locallyRingedSpaceMap f.unop

def AlgebraicGeometry.Spec.toLocallyRingedSpace : CategoryTheory.Functor CommRingCatᵒᵖ AlgebraicGeometry.LocallyRingedSpace

Spec, as a contravariant functor from commutative rings to locally ringed spaces.

@[simp]

theorem AlgebraicGeometry.toSpecΓ_apply_coe (R : CommRingCat) (f : ↑(CommRingCat.of ↑R)) (x : { x // x ∈ (Opposite.op ⊤).unop }) : ↑(↑(AlgebraicGeometry.toSpecΓ R) f) x = ↑(algebraMap (↑R) (AlgebraicGeometry.StructureSheaf.Localizations ↑R ↑x)) f

def AlgebraicGeometry.toSpecΓ (R : CommRingCat) : R ⟶ AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op (AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R)))

The counit morphism R ⟶ Γ(Spec R) given by AlgebraicGeometry.StructureSheaf.toOpen.

instance AlgebraicGeometry.isIso_toSpecΓ (R : CommRingCat) : CategoryTheory.IsIso (AlgebraicGeometry.toSpecΓ R)

theorem AlgebraicGeometry.Spec_Γ_naturality_assoc {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) {Z : CommRingCat} (h : AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op (AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op S))) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.toSpecΓ S) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.toSpecΓ R) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Γ.map (AlgebraicGeometry.Spec.toLocallyRingedSpace.map f.op).op) h)

theorem AlgebraicGeometry.Spec_Γ_naturality {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) : CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.toSpecΓ S) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.toSpecΓ R) (AlgebraicGeometry.LocallyRingedSpace.Γ.map (AlgebraicGeometry.Spec.toLocallyRingedSpace.map f.op).op)

@[simp]

theorem AlgebraicGeometry.SpecΓIdentity_inv_app (X : CommRingCat) : AlgebraicGeometry.SpecΓIdentity.inv.app X = AlgebraicGeometry.toSpecΓ X

@[simp]

theorem AlgebraicGeometry.SpecΓIdentity_hom_app (X : CommRingCat) : AlgebraicGeometry.SpecΓIdentity.hom.app X = CategoryTheory.inv (AlgebraicGeometry.toSpecΓ X)

def AlgebraicGeometry.SpecΓIdentity : CategoryTheory.Functor.comp AlgebraicGeometry.Spec.toLocallyRingedSpace.rightOp AlgebraicGeometry.LocallyRingedSpace.Γ ≅ CategoryTheory.Functor.id CommRingCat

The counit (SpecΓIdentity.inv.op) of the adjunction Γ ⊣ Spec is an isomorphism.

theorem AlgebraicGeometry.Spec_map_localization_isIso (R : CommRingCat) (M : Submonoid ↑R) (x : PrimeSpectrum (Localization M)) : CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.stalkMap (AlgebraicGeometry.Spec.toPresheafedSpace.map (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op) x)

The stalk map of Spec M⁻¹R ⟶ Spec R is an iso for each p : Spec M⁻¹R.

def AlgebraicGeometry.StructureSheaf.toPushforwardStalk {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) : S ⟶ TopCat.Presheaf.stalk (AlgebraicGeometry.Spec.topMap f _* (AlgebraicGeometry.Spec.structureSheaf ↑S).val) 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.

theorem AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) {Z : CommRingCat} (h : TopCat.Presheaf.stalk (AlgebraicGeometry.Spec.topMap f _* (AlgebraicGeometry.Spec.structureSheaf ↑S).val) p ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toPushforwardStalk f p) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑R) p) (CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor CommRingCat p).map (AlgebraicGeometry.Spec.sheafedSpaceMap f).c) h)

theorem AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) : CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toPushforwardStalk f p) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑R) p) ((TopCat.Presheaf.stalkFunctor CommRingCat p).map (AlgebraicGeometry.Spec.sheafedSpaceMap f).c)

instance AlgebraicGeometry.StructureSheaf.instAlgebraαCommRingStalkCommRingCatInstCommRingCatLargeCategoryHasColimits_commRingCatTopObjPushforwardObjTopMapValOpensTopologicalSpaceTopInstCommRingαTopologicalSpace_coeSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensGrothendieckTopologyStructureSheafToCommSemiringToSemiring {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) : Algebra ↑R ↑(TopCat.Presheaf.stalk (AlgebraicGeometry.Spec.topMap f _* (AlgebraicGeometry.Spec.structureSheaf ↑S).val) p)

theorem AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) : algebraMap ↑R ↑(TopCat.Presheaf.stalk (AlgebraicGeometry.Spec.topMap f _* (AlgebraicGeometry.Spec.structureSheaf ↑S).val) p) = CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toPushforwardStalk f p)

@[simp]

theorem AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply (R : CommRingCat) (S : CommRingCat) (p : PrimeSpectrum ↑R) [Algebra ↑R ↑S] : ∀ (a : ↑S), ↑(AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom R S p) a = ↑(TopCat.Presheaf.germ (AlgebraicGeometry.Spec.topMap (algebraMap ↑R ↑S) _* (AlgebraicGeometry.Spec.structureSheaf ↑S).val) { val := p, property := trivial }) (↑(AlgebraicGeometry.StructureSheaf.toOpen ↑S ⊤) a)

def AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom (R : CommRingCat) (S : CommRingCat) (p : PrimeSpectrum ↑R) [Algebra ↑R ↑S] : ↑S →ₐ[↑R] ↑(TopCat.Presheaf.stalk (AlgebraicGeometry.Spec.topMap (algebraMap ↑R ↑S) _* (AlgebraicGeometry.Spec.structureSheaf ↑S).val) p)

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

theorem AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux (R : CommRingCat) (S : CommRingCat) (p : PrimeSpectrum ↑R) [Algebra ↑R ↑S] (y : ↑(TopCat.Presheaf.stalk (AlgebraicGeometry.Spec.topMap (algebraMap ↑R ↑S) _* (AlgebraicGeometry.Spec.structureSheaf ↑S).val) p)) : ∃ x, x.snd • y = ↑(AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom R S p) x.fst

instance AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom (R : CommRingCat) (S : CommRingCat) (p : PrimeSpectrum ↑R) [Algebra ↑R ↑S] : IsLocalizedModule (Ideal.primeCompl p.asIdeal) (AlgHom.toLinearMap (AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom R S p))