The structure sheaf on PrimeSpectrum R.

We define the structure sheaf on TopCat.of (PrimeSpectrum R), for an R-module M and prove basic properties about it. We define this as a subsheaf of the sheaf of dependent functions into the localizations, cut out by the condition that the function must be locally equal to a quotient of an element of M by an element of R.

Because the condition "is equal to a fraction" passes to smaller open subsets, the subset of functions satisfying this condition is automatically a subpresheaf. Because the condition "is locally equal to a fraction" is local, it is also a subsheaf.

(It may be helpful to refer back to Mathlib/Topology/Sheaves/SheafOfFunctions.lean, where we show that dependent functions into any type family form a sheaf, and also Mathlib/Topology/Sheaves/LocalPredicate.lean, where we characterise the predicates which pick out sub-presheaves and sub-sheaves of these sheaves.)

When M = R, the structure sheaf is furthermore a sheaf of commutative rings, which we bundle as structureSheaf : Sheaf CommRingCat (PrimeSpectrum.Top R).

We then obtain two key descriptions of the structure sheaf. We show that the stalks Mₓ is the localization of M at the prime corresponding to x, and we show that the sections Γ(M, D(f)) is the localization of M away from f.

Note that the results of this file are packaged into schemes and sheaf of modules in later files, and one usually should not directly use the results in this file to respect the abstraction boundaries.

References

• [Robin Hartshorne, Algebraic Geometry][Har77]

def AlgebraicGeometry.PrimeSpectrum.Top (R : Type u) [CommRing R] : TopCat

The prime spectrum as an object of TopCat.

Equations

• AlgebraicGeometry.PrimeSpectrum.Top R = { carrier := PrimeSpectrum R, str := PrimeSpectrum.zariskiTopology }

@[reducible, inline]

abbrev AlgebraicGeometry.StructureSheaf.Localizations {R : Type u} (M : Type u) [CommRing R] [AddCommGroup M] [Module R M] (P : ↑(PrimeSpectrum.Top R)) : Type u

The type family over PrimeSpectrum R consisting of the localization over each point.

Equations

• AlgebraicGeometry.StructureSheaf.Localizations M P = LocalizedModule P.asIdeal.primeCompl M

def AlgebraicGeometry.StructureSheaf.IsFraction {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)} (f : (x : ↥U) → Localizations M ↑x) : Prop

The predicate saying that a dependent function on an open U is realised as a fixed fraction r / s in each of the stalks (which are localizations at various prime ideals).

Equations

• AlgebraicGeometry.StructureSheaf.IsFraction f = ∃ (r : M) (s : R), ∀ (x : ↥U), ∃ (hs : s ∉ (↑x).asIdeal), f x = LocalizedModule.mk r ⟨s, hs⟩

def AlgebraicGeometry.StructureSheaf.isFractionPrelocal (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] : TopCat.PrelocalPredicate (Localizations M)

The predicate IsFraction is "prelocal", in the sense that if it holds on U it holds on any open subset V of U.

Equations

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

def AlgebraicGeometry.StructureSheaf.isLocallyFraction (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] : TopCat.LocalPredicate (Localizations M)

We will define the structure sheaf as the subsheaf of all dependent functions in Π x : U, Localizations R x consisting of those functions which can locally be expressed as a ratio of (the images in the localization of) elements of R.

Quoting Hartshorne:

For an open set $U ⊆ Spec A$, we define $𝒪(U)$ to be the set of functions $s : U → ⨆_{𝔭 ∈ U} A_𝔭$, such that $s(𝔭) ∈ A_𝔭$ for each $𝔭$, and such that $s$ is locally a quotient of elements of $A$: to be precise, we require that for each $𝔭 ∈ U$, there is a neighborhood $V$ of $𝔭$, contained in $U$, and elements $a, f ∈ A$, such that for each $𝔮 ∈ V, f ∉ 𝔮$, and $s(𝔮) = a/f$ in $A_𝔮$.

Now Hartshorne had the disadvantage of not knowing about dependent functions, so we replace his circumlocution about functions into a disjoint union with Π x : U, Localizations x.

Equations

• AlgebraicGeometry.StructureSheaf.isLocallyFraction R M = (AlgebraicGeometry.StructureSheaf.isFractionPrelocal R M).sheafify

def AlgebraicGeometry.StructureSheaf.sectionsSubmodule {R : Type u} (M : Type u) [CommRing R] [AddCommGroup M] [Module R M] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) : Submodule R ((x : ↥U) → Localizations M ↑x)

The functions satisfying isLocallyFraction form a submodule.

Equations

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

def AlgebraicGeometry.StructureSheaf.sectionsSubalgebra {R : Type u} (A : Type u) [CommRing R] [CommRing A] [Algebra R A] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) : Subalgebra R ((x : ↥U) → Localizations A ↑x)

The functions satisfying isLocallyFraction form a subalgebra.

Equations

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

def AlgebraicGeometry.StructureSheaf.sectionsSubalgebraSubmodule {R : Type u} (M : Type u) [CommRing R] [AddCommGroup M] [Module R M] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) : Submodule (↥(sectionsSubalgebra R U)) ((x : ↥U) → Localizations M ↑x)

The functions satisfying isLocallyFraction form a submodule.

Equations

• AlgebraicGeometry.StructureSheaf.sectionsSubalgebraSubmodule M U = { toAddSubmonoid := (AlgebraicGeometry.StructureSheaf.sectionsSubmodule M U).toAddSubmonoid, smul_mem' := ⋯ }

def AlgebraicGeometry.structureSheafInType (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] : TopCat.Sheaf (Type u) (PrimeSpectrum.Top R)

The structure sheaf (valued in Type, not yet CommRingCat) is the subsheaf consisting of functions satisfying isLocallyFraction.

Equations

• AlgebraicGeometry.structureSheafInType R M = TopCat.subsheafToTypes (AlgebraicGeometry.StructureSheaf.isLocallyFraction R M)

instance AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (U : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) : AddCommGroup ((structureSheafInType R M).val.obj U)

Equations

• AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType U = (AlgebraicGeometry.StructureSheaf.sectionsSubmodule M (Opposite.unop U)).toAddSubgroup.toAddCommGroup

instance AlgebraicGeometry.instModuleObjOppositeOpensCarrierTopValStructureSheafInType {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (U : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) : Module R ((structureSheafInType R M).val.obj U)

Equations

• AlgebraicGeometry.instModuleObjOppositeOpensCarrierTopValStructureSheafInType U = (AlgebraicGeometry.StructureSheaf.sectionsSubmodule M (Opposite.unop U)).module

instance AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (U : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) : CommRing ((structureSheafInType R A).val.obj U)

Equations

• AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType U = (AlgebraicGeometry.StructureSheaf.sectionsSubalgebra A (Opposite.unop U)).toCommRing

instance AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (U : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) : Algebra R ((structureSheafInType R A).val.obj U)

Equations

• AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType U = (AlgebraicGeometry.StructureSheaf.sectionsSubalgebra A (Opposite.unop U)).algebra

@[simp]

theorem AlgebraicGeometry.structureSheafInType.add_apply {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)} (s t : (structureSheafInType R M).val.obj (Opposite.op U)) (x : ↥U) : ↑(s + t) x = ↑s x + ↑t x

@[simp]

theorem AlgebraicGeometry.structureSheafInType.mul_apply {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)} (s t : (structureSheafInType R A).val.obj (Opposite.op U)) (x : ↥U) : ↑(s * t) x = ↑s x * ↑t x

@[simp]

theorem AlgebraicGeometry.structureSheafInType.smul_apply {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)} (r : R) (s : (structureSheafInType R M).val.obj (Opposite.op U)) (x : ↥U) : ↑(r • s) x = r • ↑s x

def AlgebraicGeometry.structurePresheafInModuleCat (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] : TopCat.Presheaf (ModuleCat R) (PrimeSpectrum.Top R)

The structure presheaf, valued in ModuleCat, constructed by dressing up the Type-valued structure presheaf.

Equations

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

@[simp]

theorem AlgebraicGeometry.structurePresheafInModuleCat_obj_carrier (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] (U : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) : ↑((structurePresheafInModuleCat R M).obj U) = (structureSheafInType R M).val.obj U

def AlgebraicGeometry.structurePresheafInCommRingCat (R : Type u) [CommRing R] : TopCat.Presheaf CommRingCat (PrimeSpectrum.Top R)

The structure presheaf, valued in CommRingCat, constructed by dressing up the Type-valued structure presheaf.

Equations

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

@[simp]

theorem AlgebraicGeometry.structurePresheafInCommRingCat_obj_carrier (R : Type u) [CommRing R] (U : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) : ↑((structurePresheafInCommRingCat R).obj U) = (structureSheafInType R R).val.obj U

instance AlgebraicGeometry.instModuleObjOppositeOpensCarrierTopValStructureSheafInType_1 {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (U : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) : Module ((structureSheafInType R R).val.obj U) ((structureSheafInType R M).val.obj U)

Equations

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

instance AlgebraicGeometry.instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (U : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) : IsScalarTower R ((structureSheafInType R R).val.obj U) ((structureSheafInType R M).val.obj U)

def AlgebraicGeometry.moduleStructurePresheaf (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] : PresheafOfModules (CategoryTheory.Functor.comp (structurePresheafInCommRingCat R) (CategoryTheory.forget₂ CommRingCat RingCat))

The structure sheaf of a module as a presheaf of modules on Spec R. We will later package this into a Scheme.Modules in Tilde.lean.

Equations

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

def AlgebraicGeometry.structurePresheafCompForget (R : Type u) [CommRing R] : CategoryTheory.Functor.comp (structurePresheafInCommRingCat R) (CategoryTheory.forget CommRingCat) ≅ (structureSheafInType R R).val

Some glue, verifying that the structure presheaf valued in CommRingCat agrees with the Type-valued structure presheaf.

Equations

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

@[simp]

theorem AlgebraicGeometry.StructureSheaf.res_apply {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (U V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (i : V ⟶ U) (s : (structureSheafInType R M).val.obj (Opposite.op U)) (x : ↥V) : ↑((structureSheafInType R M).val.map i.op s) x = ↑s (i x)

def AlgebraicGeometry.StructureSheaf.const {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (f : M) (g : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : U ≤ PrimeSpectrum.basicOpen g) : (structureSheafInType R M).val.obj (Opposite.op U)

The section of structureSheaf R on an open U sending each x ∈ U to the element f/g in the localization of R at x.

Equations

• AlgebraicGeometry.StructureSheaf.const f g U hu = ⟨fun (x : ↥(Opposite.unop (Opposite.op U))) => LocalizedModule.mk f ⟨g, ⋯⟩, ⋯⟩

@[simp]

theorem AlgebraicGeometry.StructureSheaf.const_apply {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (f : M) (g : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl) (x : ↥U) : ↑(const f g U hu) x = LocalizedModule.mk f ⟨g, ⋯⟩

theorem AlgebraicGeometry.StructureSheaf.exists_const {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (s : (structureSheafInType R M).val.obj (Opposite.op U)) (x : ↑(PrimeSpectrum.Top R)) (hx : x ∈ U) : ∃ (g : R) (_ : x ∈ PrimeSpectrum.basicOpen g) (i : PrimeSpectrum.basicOpen g ≤ U) (f : M), const f g (PrimeSpectrum.basicOpen g) ⋯ = (structureSheafInType R M).val.map i.hom.op s

@[simp]

theorem AlgebraicGeometry.StructureSheaf.res_const {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (f : M) (g : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : U ≤ PrimeSpectrum.basicOpen g) (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hv : V ≤ PrimeSpectrum.basicOpen g) (i : Opposite.op U ⟶ Opposite.op V) : (structureSheafInType R M).val.map i (const f g U hu) = const f g V hv

@[simp]

theorem AlgebraicGeometry.StructureSheaf.const_zero {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (f : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : U ≤ PrimeSpectrum.basicOpen f) : const 0 f U hu = 0

@[simp]

theorem AlgebraicGeometry.StructureSheaf.const_algebraMap {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (f : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : U ≤ PrimeSpectrum.basicOpen f) : const ((algebraMap R A) f) f U hu = 1

@[simp]

theorem AlgebraicGeometry.StructureSheaf.const_self {R : Type u} [CommRing R] (f : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : U ≤ PrimeSpectrum.basicOpen f) : const f f U hu = 1

@[simp]

theorem AlgebraicGeometry.StructureSheaf.const_one {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) : const 1 1 U ⋯ = 1

theorem AlgebraicGeometry.StructureSheaf.const_add {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (f₁ f₂ : M) (g₁ g₂ : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu₁ : U ≤ PrimeSpectrum.basicOpen g₁) (hu₂ : U ≤ PrimeSpectrum.basicOpen g₂) : const f₁ g₁ U hu₁ + const f₂ g₂ U hu₂ = const (g₂ • f₁ + g₁ • f₂) (g₁ * g₂) U ⋯

theorem AlgebraicGeometry.StructureSheaf.smul_const {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (f : M) (r g : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : U ≤ PrimeSpectrum.basicOpen g) : r • const f g U hu = const (r • f) g U hu

theorem AlgebraicGeometry.StructureSheaf.const_mul {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (f₁ f₂ : A) (g₁ g₂ : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu₁ : U ≤ PrimeSpectrum.basicOpen g₁) (hu₂ : U ≤ PrimeSpectrum.basicOpen g₂) : const f₁ g₁ U hu₁ * const f₂ g₂ U hu₂ = const (f₁ * f₂) (g₁ * g₂) U ⋯

theorem AlgebraicGeometry.StructureSheaf.const_ext {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {f₁ f₂ : M} {g₁ g₂ : R} {U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)} {hu₁ : U ≤ PrimeSpectrum.basicOpen g₁} {hu₂ : U ≤ PrimeSpectrum.basicOpen g₂} (h : g₂ • f₁ = g₁ • f₂) : const f₁ g₁ U hu₁ = const f₂ g₂ U hu₂

theorem AlgebraicGeometry.StructureSheaf.const_congr {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {f₁ f₂ : M} {g₁ g₂ : R} {U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)} {hu : U ≤ PrimeSpectrum.basicOpen g₁} (hf : f₁ = f₂) (hg : g₁ = g₂) : const f₁ g₁ U hu = const f₂ g₂ U ⋯

theorem AlgebraicGeometry.StructureSheaf.const_mul_rev {R : Type u} [CommRing R] (f g : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu₁ : U ≤ PrimeSpectrum.basicOpen g) (hu₂ : U ≤ PrimeSpectrum.basicOpen f) : const f g U hu₁ * const g f U hu₂ = 1

theorem AlgebraicGeometry.StructureSheaf.const_mul_cancel {R : Type u} [CommRing R] (f g₁ g₂ : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu₁ : U ≤ PrimeSpectrum.basicOpen g₁) (hu₂ : U ≤ PrimeSpectrum.basicOpen g₂) : const f g₁ U hu₁ * const g₁ g₂ U hu₂ = const f g₂ U hu₂

theorem AlgebraicGeometry.StructureSheaf.const_mul_cancel' {R : Type u} [CommRing R] (f g₁ g₂ : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu₁ : U ≤ PrimeSpectrum.basicOpen g₁) (hu₂ : U ≤ PrimeSpectrum.basicOpen g₂) : const g₁ g₂ U hu₂ * const f g₁ U hu₁ = const f g₂ U hu₂

theorem AlgebraicGeometry.StructureSheaf.const_eq_const_of_smul_eq_smul {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (f₁ f₂ : M) (g₁ g₂ : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu₁ : U ≤ PrimeSpectrum.basicOpen g₁) (hu₂ : U ≤ PrimeSpectrum.basicOpen g₂) (H : g₁ • f₂ = g₂ • f₁) : const f₁ g₁ U hu₁ = const f₂ g₂ U hu₂

def AlgebraicGeometry.StructureSheaf.toOpenₗ (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) : M →ₗ[R] (structureSheafInType R M).val.obj (Opposite.op U)

The canonical linear map interpreting an element of M as a section of the structure sheaf.

Equations

• AlgebraicGeometry.StructureSheaf.toOpenₗ R M U = { toFun := fun (m : M) => AlgebraicGeometry.StructureSheaf.const m 1 U ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem AlgebraicGeometry.StructureSheaf.toOpenₗ_eq_const {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (f : M) : (toOpenₗ R M U) f = const f 1 U ⋯

instance AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (f : R) : IsLocalizedModule (Submonoid.powers f) (toOpenₗ R M (PrimeSpectrum.basicOpen f))

theorem AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] : Function.Bijective ⇑(toOpenₗ R M ⊤)

theorem AlgebraicGeometry.StructureSheaf.algebraMap_obj_top_bijective {R : Type u} [CommRing R] : Function.Bijective ⇑(algebraMap R ((structureSheafInType R R).val.obj (Opposite.op ⊤)))

instance AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen {R : Type u} [CommRing R] (f : R) : IsLocalization.Away f ((structureSheafInType R R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))

def AlgebraicGeometry.StructureSheaf.toStalk (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : { carrier := R, commRing := inst✝ } ⟶ (structurePresheafInCommRingCat R).stalk x

The canonical ring homomorphism interpreting an element of R as an element of the stalk of structureSheaf R at x.

Equations

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

theorem AlgebraicGeometry.StructureSheaf.algebraMap_germ {R : Type u} [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↑(PrimeSpectrum.Top R)) (hxU : x ∈ U) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).val.obj (Opposite.op U)))) ((structurePresheafInCommRingCat R).germ U x hxU) = toStalk R x

theorem AlgebraicGeometry.StructureSheaf.algebraMap_germ_apply {R : Type u} [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↑(PrimeSpectrum.Top R)) (hxU : x ∈ U) (x✝ : R) : (CategoryTheory.ConcreteCategory.hom ((structurePresheafInCommRingCat R).germ U x hxU)) ((algebraMap R ((structureSheafInType R R).val.obj (Opposite.op U))) x✝) = (CategoryTheory.ConcreteCategory.hom (toStalk R x)) x✝

theorem AlgebraicGeometry.StructureSheaf.algebraMap_germ_assoc {R : Type u} [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↑(PrimeSpectrum.Top R)) (hxU : x ∈ U) {Z : CommRingCat} (h : (structurePresheafInCommRingCat R).stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).val.obj (Opposite.op U)))) (CategoryTheory.CategoryStruct.comp ((structurePresheafInCommRingCat R).germ U x hxU) h) = CategoryTheory.CategoryStruct.comp (toStalk R x) h

@[deprecated AlgebraicGeometry.StructureSheaf.algebraMap_germ (since := "2026-02-10")]

theorem AlgebraicGeometry.StructureSheaf.toOpen_germ {R : Type u} [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↑(PrimeSpectrum.Top R)) (hxU : x ∈ U) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).val.obj (Opposite.op U)))) ((structurePresheafInCommRingCat R).germ U x hxU) = toStalk R x

Alias of AlgebraicGeometry.StructureSheaf.algebraMap_germ.

instance AlgebraicGeometry.StructureSheaf.instAlgebraCarrierStalkCommRingCatStructurePresheafInCommRingCat {R : Type u} [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : Algebra R ↑((structurePresheafInCommRingCat R).stalk x)

Equations

• AlgebraicGeometry.StructureSheaf.instAlgebraCarrierStalkCommRingCatStructurePresheafInCommRingCat x = (CommRingCat.Hom.hom (AlgebraicGeometry.StructureSheaf.toStalk R x)).toAlgebra

instance AlgebraicGeometry.StructureSheaf.instModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheaf {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (x : ↑(PrimeSpectrum.Top R)) : Module R ↑(TopCat.Presheaf.stalk (moduleStructurePresheaf R M).presheaf x)

Equations

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

instance AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (x : ↑(PrimeSpectrum.Top R)) : IsScalarTower R ↑((structurePresheafInCommRingCat R).stalk x) ↑(TopCat.Presheaf.stalk (moduleStructurePresheaf R M).presheaf x)

def AlgebraicGeometry.StructureSheaf.toStalkₗ (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] (x : ↑(PrimeSpectrum.Top R)) : M →ₗ[R] ↑(TopCat.Presheaf.stalk (moduleStructurePresheaf R M).presheaf x)

The canonical ring homomorphism interpreting an element of R as an element of the stalk of structureSheaf R at x.

Equations

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

instance AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (x : ↑(PrimeSpectrum.Top R)) : IsLocalizedModule x.asIdeal.primeCompl (toStalkₗ R M x)

def AlgebraicGeometry.StructureSheaf.commRingCatStalkEquivModuleStalk (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : ↑(TopCat.Presheaf.stalk (moduleStructurePresheaf R R).presheaf x) ≃ₗ[R] ↑((structurePresheafInCommRingCat R).stalk x)

The stalk of Spec R at x is isomorphic to the stalk of R^~ at x.

Equations

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

instance AlgebraicGeometry.StructureSheaf.instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal {R : Type u} [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : IsLocalization.AtPrime (↑((structurePresheafInCommRingCat R).stalk x)) x.asIdeal

@[reducible, inline]

abbrev AlgebraicGeometry.StructureSheaf.stalkIso (R : Type u) [CommRing R] (x : PrimeSpectrum R) : Localization.AtPrime x.asIdeal ≃ₐ[R] ↑((structurePresheafInCommRingCat R).stalk x)

The stalk of Spec R at x is isomorphic to Rₚ, where p is the prime corresponding to x.

Equations

• AlgebraicGeometry.StructureSheaf.stalkIso R x = IsLocalization.algEquiv x.asIdeal.primeCompl (Localization.AtPrime x.asIdeal) ↑((AlgebraicGeometry.structurePresheafInCommRingCat R).stalk x)

def AlgebraicGeometry.Spec.structureSheaf (R : Type u) [CommRing R] : TopCat.Sheaf CommRingCat (PrimeSpectrum.Top R)

The structure sheaf on $Spec R$, valued in CommRingCat.

This is provided as a bundled SheafedSpace as Spec.SheafedSpace R later.

Equations

• AlgebraicGeometry.Spec.structureSheaf R = { val := AlgebraicGeometry.structurePresheafInCommRingCat R, cond := ⋯ }

@[deprecated "algebraMap" (since := "2026-02-10")]

def AlgebraicGeometry.StructureSheaf.toOpen (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) : { carrier := R, commRing := inst✝ } ⟶ (Spec.structureSheaf R).val.obj (Opposite.op U)

The canonical ring homomorphism interpreting an element of R as a section of the structure sheaf.

Equations

• AlgebraicGeometry.StructureSheaf.toOpen R U = CommRingCat.ofHom (algebraMap R ((AlgebraicGeometry.structureSheafInType R R).val.obj (Opposite.op U)))

@[simp]

theorem AlgebraicGeometry.StructureSheaf.algebraMap_self_map (R : Type u) [CommRing R] (U V : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) (i : V ⟶ U) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).val.obj V))) ((Spec.structureSheaf R).val.map i) = CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).val.obj U))

@[deprecated AlgebraicGeometry.StructureSheaf.algebraMap_self_map (since := "2026-02-10")]

theorem AlgebraicGeometry.StructureSheaf.toOpen_res (R : Type u) [CommRing R] (U V : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) (i : V ⟶ U) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).val.obj V))) ((Spec.structureSheaf R).val.map i) = CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).val.obj U))

Alias of AlgebraicGeometry.StructureSheaf.algebraMap_self_map.

instance AlgebraicGeometry.StructureSheaf.stalkAlgebra (R : Type u) [CommRing R] (p : PrimeSpectrum R) : Algebra R ↑((Spec.structureSheaf R).presheaf.stalk p)

Equations

• AlgebraicGeometry.StructureSheaf.stalkAlgebra R p = (CommRingCat.Hom.hom (AlgebraicGeometry.StructureSheaf.toStalk R p)).toAlgebra

@[simp]

theorem AlgebraicGeometry.StructureSheaf.stalkAlgebra_map (R : Type u) [CommRing R] (p : PrimeSpectrum R) (r : R) : (algebraMap R ↑((Spec.structureSheaf R).presheaf.stalk p)) r = (CategoryTheory.ConcreteCategory.hom (toStalk R p)) r

instance AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk (R : Type u) [CommRing R] (p : PrimeSpectrum R) : IsLocalization.AtPrime (↑((Spec.structureSheaf R).presheaf.stalk p)) p.asIdeal

Stalk of the structure sheaf at a prime p as localization of R

instance AlgebraicGeometry.StructureSheaf.openAlgebra (R : Type u) [CommRing R] (U : (TopologicalSpace.Opens (PrimeSpectrum R))ᵒᵖ) : Algebra R ↑((Spec.structureSheaf R).val.obj U)

Equations

• AlgebraicGeometry.StructureSheaf.openAlgebra R U = inferInstanceAs (Algebra R ((AlgebraicGeometry.structureSheafInType R R).presheaf.obj U))

instance AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen (R : Type u) [CommRing R] (r : R) : IsLocalization.Away r ↑((Spec.structureSheaf R).val.obj (Opposite.op (PrimeSpectrum.basicOpen r)))

Sections of the structure sheaf of Spec R on a basic open as localization of R

instance AlgebraicGeometry.StructureSheaf.to_basicOpen_epi (R : Type u) [CommRing R] (r : R) : CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R ↑((Spec.structureSheaf R).val.obj (Opposite.op (PrimeSpectrum.basicOpen r)))))

def AlgebraicGeometry.StructureSheaf.globalSectionsIso (R : Type u) [CommRing R] : { carrier := R, commRing := inst✝ } ≅ (Spec.structureSheaf R).val.obj (Opposite.op ⊤)

The ring isomorphism between the ring R and the global sections Γ(X, 𝒪ₓ).

Equations

• AlgebraicGeometry.StructureSheaf.globalSectionsIso R = (RingEquiv.ofBijective (algebraMap R ((AlgebraicGeometry.structureSheafInType R R).val.obj (Opposite.op ⊤))) ⋯).toCommRingCatIso

@[simp]

theorem AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv (R : Type u) [CommRing R] : (globalSectionsIso R).inv = CommRingCat.ofHom ↑(RingEquiv.ofBijective (algebraMap R ((structureSheafInType R R).val.obj (Opposite.op ⊤))) ⋯).symm

theorem AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom (R : CommRingCat) : (globalSectionsIso ↑R).hom = CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).val.obj (Opposite.op ⊤)))

@[simp]

theorem AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes {R : Type u_1} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (toStalk R y) ((Spec.structureSheaf R).presheaf.stalkSpecializes h) = toStalk R x

theorem AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_assoc {R : Type u_1} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) {Z : CommRingCat} (h✝ : (Spec.structureSheaf R).presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (toStalk R y) (CategoryTheory.CategoryStruct.comp ((Spec.structureSheaf R).presheaf.stalkSpecializes h) h✝) = CategoryTheory.CategoryStruct.comp (toStalk R x) h✝

theorem AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_apply {R : Type u_1} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) (x✝ : R) : (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).presheaf.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (toStalk R y)) x✝) = (CategoryTheory.ConcreteCategory.hom (toStalk R x)) x✝

def AlgebraicGeometry.StructureSheaf.Localizations.comapFun {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {S : Type u} [CommRing S] {N : Type u} [AddCommGroup N] [Module S N] {σ : R →+* S} (f : M →ₛₗ[σ] N) (y : ↑(PrimeSpectrum.Top S)) : Localizations M (PrimeSpectrum.comap σ y) →ₛₗ[σ] Localizations N y

The map M_{f y} ⟶ N_{y} used to build maps between structure sheaves.

Equations

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

@[simp]

theorem AlgebraicGeometry.StructureSheaf.Localizations.comapFun_mk {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {S : Type u} [CommRing S] {N : Type u} [AddCommGroup N] [Module S N] {σ : R →+* S} (f : M →ₛₗ[σ] N) (y : ↑(PrimeSpectrum.Top S)) (a : M) (b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl) : (comapFun f y) (LocalizedModule.mk a b) = LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩

def AlgebraicGeometry.StructureSheaf.comapFun {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {S : Type u} [CommRing S] {N : Type u} [AddCommGroup N] [Module S N] {σ : R →+* S} (f : M →ₛₗ[σ] N) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top S)) (hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier) (s : (x : ↥U) → Localizations M ↑x) (y : ↥V) : Localizations N ↑y

Given a ring homomorphism f : R →+* S, an open set U of the prime spectrum of R and an open set V of the prime spectrum of S, such that V ⊆ (comap f) ⁻¹' U, we can push a section s on U to a section on V, by composing with Localization.localRingHom _ _ f from the left and comap f from the right. Explicitly, if s evaluates on comap f p to a / b, its image on V evaluates on p to f(a) / f(b).

At the moment, we work with arbitrary dependent functions s : Π x : U, Localizations R x. Below, we prove the predicate isLocallyFraction is preserved by this map, hence it can be extended to a morphism between the structure sheaves of R and S.

Equations

• AlgebraicGeometry.StructureSheaf.comapFun f U V hUV s y = (AlgebraicGeometry.StructureSheaf.Localizations.comapFun f ↑y) (s ⟨PrimeSpectrum.comap σ ↑y, ⋯⟩)

theorem AlgebraicGeometry.StructureSheaf.isLocallyFraction_comapFun {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {S : Type u} [CommRing S] {N : Type u} [AddCommGroup N] [Module S N] {σ : R →+* S} (f : M →ₛₗ[σ] N) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top S)) (hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier) (s : (x : ↥U) → Localizations M ↑x) (hs : (isLocallyFraction R M).pred s) : (isLocallyFraction S N).pred (comapFun f U V hUV s)

def AlgebraicGeometry.StructureSheaf.comapₗ {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {S : Type u} [CommRing S] {N : Type u} [AddCommGroup N] [Module S N] {σ : R →+* S} (f : M →ₛₗ[σ] N) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top S)) (hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier) : (structureSheafInType R M).val.obj (Opposite.op U) →ₛₗ[σ] (structureSheafInType S N).val.obj (Opposite.op V)

For a ring homomorphism f : R →+* S and open sets U and V of the prime spectra of R and S such that V ⊆ (comap f) ⁻¹ U, the induced ring homomorphism from the structure sheaf of R at U to the structure sheaf of S at V.

Explicitly, this map is given as follows: For a point p : V, if the section s evaluates on p to the fraction a / b, its image on V evaluates on p to the fraction f(a) / f(b).

Equations

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

theorem AlgebraicGeometry.StructureSheaf.comapₗ_const {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {S : Type u} [CommRing S] {N : Type u} [AddCommGroup N] [Module S N] {σ : R →+* S} (f : M →ₛₗ[σ] N) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top S)) (hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier) (a : M) (b : R) (hb : U ≤ PrimeSpectrum.basicOpen b) : (comapₗ f U V hUV) (const a b U hb) = const (f a) (σ b) V ⋯

@[simp]

theorem AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top S)) (hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier) (s : ↑((Spec.structureSheaf R).val.obj (Opposite.op U))) (p : ↥V) : ↑((comapₗ f.toSemilinearMap U V hUV) s) p = (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (↑s ⟨PrimeSpectrum.comap f ↑p, ⋯⟩)

def AlgebraicGeometry.StructureSheaf.comap {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top S)) (hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier) : ↑((Spec.structureSheaf R).val.obj (Opposite.op U)) →+* ↑((Spec.structureSheaf S).val.obj (Opposite.op V))

For a ring homomorphism f : R →+* S and open sets U and V of the prime spectra of R and S such that V ⊆ (comap f) ⁻¹ U, the induced ring homomorphism from the structure sheaf of R at U to the structure sheaf of S at V.

Explicitly, this map is given as follows: For a point p : V, if the section s evaluates on p to the fraction a / b, its image on V evaluates on p to the fraction f(a) / f(b).

Equations

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

@[simp]

theorem AlgebraicGeometry.StructureSheaf.comap_apply {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top S)) (hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier) (s : ↑((Spec.structureSheaf R).val.obj (Opposite.op U))) (p : ↥V) : ↑((comap f U V hUV) s) p = (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (↑s ⟨PrimeSpectrum.comap f ↑p, ⋯⟩)

theorem AlgebraicGeometry.StructureSheaf.comap_const {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top S)) (hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier) (a b : R) (hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl) : (comap f U V hUV) (const a b U hb) = const (f a) (f b) V ⋯

theorem AlgebraicGeometry.StructureSheaf.comap_id_eq_map {R : Type u} [CommRing R] (U V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (iVU : V ⟶ U) : comap (RingHom.id R) U V ⋯ = CommRingCat.Hom.hom ((Spec.structureSheaf R).val.map iVU.op)

For an inclusion i : V ⟶ U between open sets of the prime spectrum of R, the comap of the identity from OO_X(U) to OO_X(V) equals as the restriction map of the structure sheaf.

This is a generalization of the fact that, for fixed U, the comap of the identity from OO_X(U) to OO_X(U) is the identity.

theorem AlgebraicGeometry.StructureSheaf.comap_id {R : Type u} [CommRing R] {U V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)} (hUV : U = V) : comap (RingHom.id R) U V ⋯ = CommRingCat.Hom.hom (CategoryTheory.eqToHom ⋯)

The comap of the identity is the identity. In this variant of the lemma, two open subsets U and V are given as arguments, together with a proof that U = V. This is useful when U and V are not definitionally equal.

@[simp]

theorem AlgebraicGeometry.StructureSheaf.comap_id' {R : Type u} [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) : comap (RingHom.id R) U U ⋯ = RingHom.id ↑((Spec.structureSheaf R).val.obj (Opposite.op U))

theorem AlgebraicGeometry.StructureSheaf.comap_comp {R : Type u} [CommRing R] {S : Type u} [CommRing S] {P : Type u} [CommRing P] (f : R →+* S) (g : S →+* P) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top S)) (W : TopologicalSpace.Opens ↑(PrimeSpectrum.Top P)) (hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U) (hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V) : comap (g.comp f) U W ⋯ = (comap g V W hVW).comp (comap f U V hUV)

theorem AlgebraicGeometry.StructureSheaf.toOpen_comp_comap {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R ↑((Spec.structureSheaf R).val.obj (Opposite.op U)))) (CommRingCat.ofHom (comap f U ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U) ⋯)) = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom f) (CommRingCat.ofHom (algebraMap S ↑((Spec.structureSheaf S).val.obj (Opposite.op ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))))

theorem AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : R) : (comap f U ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U) ⋯) ((algebraMap R ↑((Spec.structureSheaf R).val.obj (Opposite.op U))) x) = (algebraMap S ↑((Spec.structureSheaf S).val.obj (Opposite.op ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))) (f x)

theorem AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) {Z : CommRingCat} (h : { carrier := ↑((Spec.structureSheaf S).val.obj (Opposite.op ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))), commRing := ((Spec.structureSheaf S).val.obj (Opposite.op ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))).commRing } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R ↑((Spec.structureSheaf R).val.obj (Opposite.op U)))) (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (comap f U ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U) ⋯)) h) = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom f) (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap S ↑((Spec.structureSheaf S).val.obj (Opposite.op ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))))) h)

theorem AlgebraicGeometry.StructureSheaf.comap_basicOpen {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (x : R) : comap f (PrimeSpectrum.basicOpen x) (PrimeSpectrum.basicOpen (f x)) ⋯ = IsLocalization.map (↑((Spec.structureSheaf S).val.obj (Opposite.op (PrimeSpectrum.basicOpen (f x))))) f ⋯