$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.

Equations

• AlgebraicGeometry.Spec.topObj R = TopCat.of (PrimeSpectrum ↑R)

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.

Equations

• AlgebraicGeometry.Spec.topMap f = PrimeSpectrum.comap f

@[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.toPrefunctor.map f = AlgebraicGeometry.Spec.topMap f.unop

@[simp]

theorem AlgebraicGeometry.Spec.toTop_obj (R : CommRingCatᵒᵖ) : AlgebraicGeometry.Spec.toTop.toPrefunctor.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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[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)).toPrefunctor.obj U.unop) (_ : ∀ x ∈ ((TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.topMap f)).toPrefunctor.obj U.unop).carrier, x ∈ ((TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.topMap f)).toPrefunctor.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.

Equations

• One or more equations did not get rendered due to their size.

@[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.toPrefunctor.obj R = AlgebraicGeometry.Spec.sheafedSpaceObj R.unop

@[simp]

theorem AlgebraicGeometry.Spec.toSheafedSpace_map : ∀ {X Y : CommRingCatᵒᵖ} (f : X ⟶ Y), AlgebraicGeometry.Spec.toSheafedSpace.toPrefunctor.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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• AlgebraicGeometry.Spec.toPresheafedSpace = CategoryTheory.Functor.comp AlgebraicGeometry.Spec.toSheafedSpace AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace

@[simp]

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

theorem AlgebraicGeometry.Spec.toPresheafedSpace_obj_op (R : CommRingCat) : AlgebraicGeometry.Spec.toPresheafedSpace.toPrefunctor.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.toPrefunctor.map f = AlgebraicGeometry.Spec.sheafedSpaceMap f.unop

theorem AlgebraicGeometry.Spec.toPresheafedSpace_map_op (R : CommRingCat) (S : CommRingCat) (f : R ⟶ S) : AlgebraicGeometry.Spec.toPresheafedSpace.toPrefunctor.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.toPrefunctor.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map α.base).op.toPrefunctor.obj (Opposite.op U) = (TopologicalSpace.Opens.map β.base).op.toPrefunctor.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.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.stalkMap_toStalk_apply {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) (x : (CategoryTheory.forget CommRingCat).toPrefunctor.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).toPrefunctor.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.

Equations

• One or more equations did not get rendered due to their size.

@[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.toPrefunctor.obj R = AlgebraicGeometry.Spec.locallyRingedSpaceObj R.unop

@[simp]

theorem AlgebraicGeometry.Spec.toLocallyRingedSpace_map : ∀ {X Y : CommRingCatᵒᵖ} (f : X ⟶ Y), AlgebraicGeometry.Spec.toLocallyRingedSpace.toPrefunctor.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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.toSpecΓ_apply_coe (R : CommRingCat) (f : ↑(CommRingCat.of ↑R)) (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.Γ.toPrefunctor.obj (Opposite.op (AlgebraicGeometry.Spec.toLocallyRingedSpace.toPrefunctor.obj (Opposite.op R)))

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

Equations

• AlgebraicGeometry.toSpecΓ R = AlgebraicGeometry.StructureSheaf.toOpen ↑R ⊤

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

Equations

• (_ : CategoryTheory.IsIso (AlgebraicGeometry.toSpecΓ R)) = (_ : CategoryTheory.IsIso (AlgebraicGeometry.toSpecΓ R))

theorem AlgebraicGeometry.Spec_Γ_naturality_assoc {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) {Z : CommRingCat} (h : AlgebraicGeometry.LocallyRingedSpace.Γ.toPrefunctor.obj (Opposite.op (AlgebraicGeometry.Spec.toLocallyRingedSpace.toPrefunctor.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.Γ.toPrefunctor.map (AlgebraicGeometry.Spec.toLocallyRingedSpace.toPrefunctor.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.Γ.toPrefunctor.map (AlgebraicGeometry.Spec.toLocallyRingedSpace.toPrefunctor.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.

Equations

• AlgebraicGeometry.SpecΓIdentity = (CategoryTheory.NatIso.ofComponents fun (R : CommRingCat) => CategoryTheory.asIso (AlgebraicGeometry.toSpecΓ R)).symm

theorem AlgebraicGeometry.Spec_map_localization_isIso (R : CommRingCat) (M : Submonoid ↑R) (x : PrimeSpectrum (Localization M)) : CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.stalkMap (AlgebraicGeometry.Spec.toPresheafedSpace.toPrefunctor.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.

Equations

• One or more equations did not get rendered due to their size.

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).toPrefunctor.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).toPrefunctor.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)

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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 : ↑S × ↥(Ideal.primeCompl p.asIdeal)), x.2 • y = (AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom R S p) x.1

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))

Equations

• One or more equations did not get rendered due to their size.