The structure sheaf on PrimeSpectrum R.

We define the structure sheaf on TopCat.of (PrimeSpectrum R), for a commutative ring R 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 ratio of elements 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.)

We also set up the ring structure, obtaining structureSheaf : Sheaf CommRingCat (PrimeSpectrum.Top R).

We then construct two basic isomorphisms, relating the structure sheaf to the underlying ring R. First, StructureSheaf.stalkIso gives an isomorphism between the stalk of the structure sheaf at a point p and the localization of R at the prime ideal p. Second, StructureSheaf.basicOpenIso gives an isomorphism between the structure sheaf on basicOpen f and the localization of R at the submonoid of powers of f.

References

• [Robin Hartshorne, Algebraic Geometry][Har77]

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

The prime spectrum, just as a topological space.

Equations

• AlgebraicGeometry.PrimeSpectrum.Top R = TopCat.of (PrimeSpectrum R)

def AlgebraicGeometry.StructureSheaf.Localizations (R : Type u) [CommRing R] (P : ↑(PrimeSpectrum.Top R)) : Type u

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

Equations

• AlgebraicGeometry.StructureSheaf.Localizations R P = Localization.AtPrime P.asIdeal

instance AlgebraicGeometry.StructureSheaf.commRingLocalizations (R : Type u) [CommRing R] (P : ↑(PrimeSpectrum.Top R)) : CommRing (Localizations R P)

Equations

• AlgebraicGeometry.StructureSheaf.commRingLocalizations R P = inferInstanceAs (CommRing (Localization.AtPrime P.asIdeal))

instance AlgebraicGeometry.StructureSheaf.localRingLocalizations (R : Type u) [CommRing R] (P : ↑(PrimeSpectrum.Top R)) : IsLocalRing (Localizations R P)

instance AlgebraicGeometry.StructureSheaf.instInhabitedLocalizations (R : Type u) [CommRing R] (P : ↑(PrimeSpectrum.Top R)) : Inhabited (Localizations R P)

Equations

• AlgebraicGeometry.StructureSheaf.instInhabitedLocalizations R P = { default := 1 }

instance AlgebraicGeometry.StructureSheaf.instAlgebraLocalizationsValCarrierTopMemOpens (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↥U) : Algebra R (Localizations R ↑x)

Equations

• AlgebraicGeometry.StructureSheaf.instAlgebraLocalizationsValCarrierTopMemOpens R U x = inferInstanceAs (Algebra R (Localization.AtPrime (↑x).asIdeal))

instance AlgebraicGeometry.StructureSheaf.instAtPrimeLocalizationsValCarrierTopMemOpensAsIdeal (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↥U) : IsLocalization.AtPrime (Localizations R ↑x) (↑x).asIdeal

def AlgebraicGeometry.StructureSheaf.IsFraction {R : Type u} [CommRing R] {U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)} (f : (x : ↥U) → Localizations R ↑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

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

theorem AlgebraicGeometry.StructureSheaf.IsFraction.eq_mk' {R : Type u} [CommRing R] {U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)} {f : (x : ↥U) → Localizations R ↑x} (hf : IsFraction f) : ∃ (r : R) (s : R), ∀ (x : ↥U), ∃ (hs : s ∉ (↑x).asIdeal), f x = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) r ⟨s, hs⟩

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

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 : Type u) [CommRing R] : TopCat.LocalPredicate (Localizations R)

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\subseteq SpecA$, we define $𝒪(U)$ to be the set of functions $s:U\to {⨆}_{𝔭\in U}{A}_{𝔭}$, such that $s(𝔭)\in A_{𝔭}$ for each $𝔭$, and such that $s$ is locally a quotient of elements of $A$: to be precise, we require that for each $𝔭\in U$, there is a neighborhood $V$ of $𝔭$, contained in $U$, and elements $a,f\in A$, such that for each $𝔮\in V,f\notin 𝔮$, 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 = (AlgebraicGeometry.StructureSheaf.isFractionPrelocal R).sheafify

@[simp]

theorem AlgebraicGeometry.StructureSheaf.isLocallyFraction_pred (R : Type u) [CommRing R] {U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)} (f : (x : ↥U) → Localizations R ↑x) : (isLocallyFraction R).pred f = ∀ (x : ↥U), ∃ (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (_ : ↑x ∈ V) (i : V ⟶ U) (r : R) (s : R), ∀ (y : ↥V), s ∉ (↑y).asIdeal ∧ f ((fun (x : ↥V) => ⟨↑x, ⋯⟩) y) * (algebraMap R (Localizations R ↑((fun (x : ↥V) => ⟨↑x, ⋯⟩) y))) s = (algebraMap R (Localizations R ↑((fun (x : ↥V) => ⟨↑x, ⋯⟩) y))) r

def AlgebraicGeometry.StructureSheaf.sectionsSubring (R : Type u) [CommRing R] (U : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) : Subring ((x : ↥(Opposite.unop U)) → Localizations R ↑x)

The functions satisfying isLocallyFraction form a subring.

Equations

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

def AlgebraicGeometry.structureSheafInType (R : Type u) [CommRing R] : 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 = TopCat.subsheafToTypes (AlgebraicGeometry.StructureSheaf.isLocallyFraction R)

instance AlgebraicGeometry.commRingStructureSheafInTypeObj (R : Type u) [CommRing R] (U : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) : CommRing ((structureSheafInType R).val.obj U)

Equations

• AlgebraicGeometry.commRingStructureSheafInTypeObj R U = (AlgebraicGeometry.StructureSheaf.sectionsSubring R U).toCommRing

def AlgebraicGeometry.structurePresheafInCommRing (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.structurePresheafInCommRing_obj_carrier (R : Type u) [CommRing R] (U : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top R))ᵒᵖ) : ↑((structurePresheafInCommRing R).obj U) = (structureSheafInType R).val.obj U

def AlgebraicGeometry.structurePresheafCompForget (R : Type u) [CommRing R] : CategoryTheory.Functor.comp (structurePresheafInCommRing R) (CategoryTheory.forget CommRingCat) ≅ (structureSheafInType 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.

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

The structure sheaf on $SpecR$, valued in CommRingCat.

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

Equations

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

@[simp]

theorem AlgebraicGeometry.StructureSheaf.res_apply (R : Type u) [CommRing R] (U V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (i : V ⟶ U) (s : ↑((Spec.structureSheaf R).val.obj (Opposite.op U))) (x : ↥V) : ↑((CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).val.map i.op)) s) x = ↑s ((fun (x : ↥V) => ⟨↑x, ⋯⟩) x)

def AlgebraicGeometry.StructureSheaf.const (R : Type u) [CommRing R] (f g : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl) : ↑((Spec.structureSheaf R).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 R f g U hu = ⟨fun (x : ↥(Opposite.unop (Opposite.op U))) => IsLocalization.mk' (AlgebraicGeometry.StructureSheaf.Localizations R ↑x) f ⟨g, ⋯⟩, ⋯⟩

@[simp]

theorem AlgebraicGeometry.StructureSheaf.const_apply (R : Type u) [CommRing R] (f g : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl) (x : ↥U) : ↑(const R f g U hu) x = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) f ⟨g, ⋯⟩

theorem AlgebraicGeometry.StructureSheaf.const_apply' (R : Type u) [CommRing R] (f g : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl) (x : ↥U) (hx : g ∈ (↑x).asIdeal.primeCompl) : ↑(const R f g U hu) x = IsLocalization.mk' (Localizations R ↑x) f ⟨g, hx⟩

theorem AlgebraicGeometry.StructureSheaf.exists_const (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (s : ↑((Spec.structureSheaf R).val.obj (Opposite.op U))) (x : ↑(PrimeSpectrum.Top R)) (hx : x ∈ U) : ∃ (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (_ : x ∈ V) (i : V ⟶ U) (f : R) (g : R) (hg : ∀ x ∈ V, g ∈ x.asIdeal.primeCompl), const R f g V hg = (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).val.map i.op)) s

@[simp]

theorem AlgebraicGeometry.StructureSheaf.res_const (R : Type u) [CommRing R] (f g : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl) (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hv : ∀ x ∈ V, g ∈ x.asIdeal.primeCompl) (i : Opposite.op U ⟶ Opposite.op V) : (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).val.map i)) (const R f g U hu) = const R f g V hv

theorem AlgebraicGeometry.StructureSheaf.res_const' (R : Type u) [CommRing R] (f g : R) (V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hv : V ≤ PrimeSpectrum.basicOpen g) : (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).val.map (CategoryTheory.homOfLE hv).op)) (const R f g (PrimeSpectrum.basicOpen g) ⋯) = const R f g V hv

theorem AlgebraicGeometry.StructureSheaf.const_zero (R : Type u) [CommRing R] (f : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl) : const R 0 f U hu = 0

theorem AlgebraicGeometry.StructureSheaf.const_self (R : Type u) [CommRing R] (f : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl) : const R f f U hu = 1

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

theorem AlgebraicGeometry.StructureSheaf.const_add (R : Type u) [CommRing R] (f₁ f₂ g₁ g₂ : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl) (hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl) : const R f₁ g₁ U hu₁ + const R f₂ g₂ U hu₂ = const R (f₁ * g₂ + f₂ * g₁) (g₁ * g₂) U ⋯

theorem AlgebraicGeometry.StructureSheaf.const_mul (R : Type u) [CommRing R] (f₁ f₂ g₁ g₂ : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl) (hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl) : const R f₁ g₁ U hu₁ * const R f₂ g₂ U hu₂ = const R (f₁ * f₂) (g₁ * g₂) U ⋯

theorem AlgebraicGeometry.StructureSheaf.const_ext (R : Type u) [CommRing R] {f₁ f₂ g₁ g₂ : R} {U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)} {hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl} {hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl} (h : f₁ * g₂ = f₂ * g₁) : const R f₁ g₁ U hu₁ = const R f₂ g₂ U hu₂

theorem AlgebraicGeometry.StructureSheaf.const_congr (R : Type u) [CommRing R] {f₁ f₂ g₁ g₂ : R} {U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)} {hu : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl} (hf : f₁ = f₂) (hg : g₁ = g₂) : const R f₁ g₁ U hu = const R f₂ g₂ U ⋯

theorem AlgebraicGeometry.StructureSheaf.const_mul_rev (R : Type u) [CommRing R] (f g : R) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (hu₁ : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl) (hu₂ : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl) : const R f g U hu₁ * const R 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₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl) (hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl) : const R f g₁ U hu₁ * const R g₁ g₂ U hu₂ = const R 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₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl) (hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl) : const R g₁ g₂ U hu₂ * const R f g₁ U hu₁ = const R f g₂ U hu₂

def AlgebraicGeometry.StructureSheaf.toOpen (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) : CommRingCat.of R ⟶ (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

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

@[simp]

theorem AlgebraicGeometry.StructureSheaf.toOpen_res (R : Type u) [CommRing R] (U V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (i : V ⟶ U) : CategoryTheory.CategoryStruct.comp (toOpen R U) ((Spec.structureSheaf R).val.map i.op) = toOpen R V

@[simp]

theorem AlgebraicGeometry.StructureSheaf.toOpen_apply (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (f : R) (x : ↥U) : ↑((CategoryTheory.ConcreteCategory.hom (toOpen R U)) f) x = (algebraMap R (Localizations R ↑x)) f

theorem AlgebraicGeometry.StructureSheaf.toOpen_eq_const (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (f : R) : (CategoryTheory.ConcreteCategory.hom (toOpen R U)) f = const R f 1 U ⋯

def AlgebraicGeometry.StructureSheaf.toStalk (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : CommRingCat.of R ⟶ (Spec.structureSheaf R).presheaf.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.

@[simp]

theorem AlgebraicGeometry.StructureSheaf.toOpen_germ (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↑(PrimeSpectrum.Top R)) (hx : x ∈ U) : CategoryTheory.CategoryStruct.comp (toOpen R U) ((Spec.structureSheaf R).presheaf.germ U x hx) = toStalk R x

@[simp]

theorem AlgebraicGeometry.StructureSheaf.germ_toOpen (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↑(PrimeSpectrum.Top R)) (hx : x ∈ U) (f : R) : (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).presheaf.germ U x hx)) ((CategoryTheory.ConcreteCategory.hom (toOpen R U)) f) = (CategoryTheory.ConcreteCategory.hom (toStalk R x)) f

theorem AlgebraicGeometry.StructureSheaf.toOpen_Γgerm_apply (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) (f : R) : (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).presheaf.Γgerm x)) ((CategoryTheory.ConcreteCategory.hom (toOpen R ⊤)) f) = (CategoryTheory.ConcreteCategory.hom (toStalk R x)) f

theorem AlgebraicGeometry.StructureSheaf.isUnit_to_basicOpen_self (R : Type u) [CommRing R] (f : R) : IsUnit ((CategoryTheory.ConcreteCategory.hom (toOpen R (PrimeSpectrum.basicOpen f))) f)

theorem AlgebraicGeometry.StructureSheaf.isUnit_toStalk (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) (f : ↥x.asIdeal.primeCompl) : IsUnit ((CategoryTheory.ConcreteCategory.hom (toStalk R x)) ↑f)

def AlgebraicGeometry.StructureSheaf.localizationToStalk (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : CommRingCat.of (Localization.AtPrime x.asIdeal) ⟶ (Spec.structureSheaf R).presheaf.stalk x

The canonical ring homomorphism from the localization of R at p to the stalk of the structure sheaf at the point p.

Equations

• AlgebraicGeometry.StructureSheaf.localizationToStalk R x = CommRingCat.ofHom (let_fun this := IsLocalization.lift ⋯; this)

@[simp]

theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_of (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) (f : R) : (CategoryTheory.ConcreteCategory.hom (localizationToStalk R x)) ((algebraMap R (Localization x.asIdeal.primeCompl)) f) = (CategoryTheory.ConcreteCategory.hom (toStalk R x)) f

@[simp]

theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_mk' (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) (f : R) (s : ↥x.asIdeal.primeCompl) : (CategoryTheory.ConcreteCategory.hom (localizationToStalk R x)) (IsLocalization.mk' (Localization.AtPrime x.asIdeal) f s) = (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).presheaf.germ (PrimeSpectrum.basicOpen ↑s) x ⋯)) (const R f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)

def AlgebraicGeometry.StructureSheaf.openToLocalization (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↑(PrimeSpectrum.Top R)) (hx : x ∈ U) : (Spec.structureSheaf R).val.obj (Opposite.op U) ⟶ CommRingCat.of (Localization.AtPrime x.asIdeal)

The ring homomorphism that takes a section of the structure sheaf of R on the open set U, implemented as a subtype of dependent functions to localizations at prime ideals, and evaluates the section on the point corresponding to a given prime ideal.

Equations

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

@[simp]

theorem AlgebraicGeometry.StructureSheaf.coe_openToLocalization (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↑(PrimeSpectrum.Top R)) (hx : x ∈ U) : ⇑(CategoryTheory.ConcreteCategory.hom (openToLocalization R U x hx)) = fun (s : ↑((Spec.structureSheaf R).val.obj (Opposite.op U))) => ↑s ⟨x, hx⟩

theorem AlgebraicGeometry.StructureSheaf.openToLocalization_apply (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↑(PrimeSpectrum.Top R)) (hx : x ∈ U) (s : ↑((Spec.structureSheaf R).val.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (openToLocalization R U x hx)) s = ↑s ⟨x, hx⟩

def AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : (Spec.structureSheaf R).presheaf.stalk x ⟶ CommRingCat.of (Localization.AtPrime x.asIdeal)

The ring homomorphism from the stalk of the structure sheaf of R at a point corresponding to a prime ideal p to the localization of R at p, formed by gluing the openToLocalization maps.

Equations

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

@[simp]

theorem AlgebraicGeometry.StructureSheaf.germ_comp_stalkToFiberRingHom (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↑(PrimeSpectrum.Top R)) (hx : x ∈ U) : CategoryTheory.CategoryStruct.comp ((Spec.structureSheaf R).presheaf.germ U x hx) (stalkToFiberRingHom R x) = openToLocalization R U x hx

@[simp]

theorem AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_germ (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (x : ↑(PrimeSpectrum.Top R)) (hx : x ∈ U) (s : ↑((Spec.structureSheaf R).val.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (stalkToFiberRingHom R x)) ((CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).presheaf.germ U x hx)) s) = ↑s ⟨x, hx⟩

@[simp]

theorem AlgebraicGeometry.StructureSheaf.toStalk_comp_stalkToFiberRingHom (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : CategoryTheory.CategoryStruct.comp (toStalk R x) (stalkToFiberRingHom R x) = CommRingCat.ofHom (algebraMap R (Localization.AtPrime x.asIdeal))

@[simp]

theorem AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_toStalk (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) (f : R) : (CategoryTheory.ConcreteCategory.hom (stalkToFiberRingHom R x)) ((CategoryTheory.ConcreteCategory.hom (toStalk R x)) f) = (algebraMap R ↑(CommRingCat.of (Localization.AtPrime x.asIdeal))) f

def AlgebraicGeometry.StructureSheaf.stalkIso (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : (Spec.structureSheaf R).presheaf.stalk x ≅ CommRingCat.of (Localization.AtPrime x.asIdeal)

The ring isomorphism between the stalk of the structure sheaf of R at a point p corresponding to a prime ideal in R and the localization of R at p.

Equations

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

@[simp]

theorem AlgebraicGeometry.StructureSheaf.stalkIso_hom (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : (stalkIso R x).hom = stalkToFiberRingHom R x

@[simp]

theorem AlgebraicGeometry.StructureSheaf.stalkIso_inv (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : (stalkIso R x).inv = localizationToStalk R x

instance AlgebraicGeometry.StructureSheaf.instIsIsoCommRingCatStalkToFiberRingHom (R : Type u) [CommRing R] (x : PrimeSpectrum R) : CategoryTheory.IsIso (stalkToFiberRingHom R x)

instance AlgebraicGeometry.StructureSheaf.instIsLocalHomCarrierStalkCommRingCatPresheafStructureSheafOfAtPrimeAsIdealRingHomHomStalkToFiberRingHom (R : Type u) [CommRing R] (x : PrimeSpectrum R) : IsLocalHom (CommRingCat.Hom.hom (stalkToFiberRingHom R x))

instance AlgebraicGeometry.StructureSheaf.instIsIsoCommRingCatLocalizationToStalk (R : Type u) [CommRing R] (x : PrimeSpectrum R) : CategoryTheory.IsIso (localizationToStalk R x)

instance AlgebraicGeometry.StructureSheaf.instIsLocalHomCarrierOfAtPrimeAsIdealStalkCommRingCatPresheafStructureSheafRingHomHomLocalizationToStalk (R : Type u) [CommRing R] (x : PrimeSpectrum R) : IsLocalHom (CommRingCat.Hom.hom (localizationToStalk R x))

@[simp]

theorem AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_localizationToStalk (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : CategoryTheory.CategoryStruct.comp (stalkToFiberRingHom R x) (localizationToStalk R x) = CategoryTheory.CategoryStruct.id ((Spec.structureSheaf R).presheaf.stalk x)

theorem AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_localizationToStalk_assoc (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) {Z : CommRingCat} (h : (Spec.structureSheaf R).presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (stalkToFiberRingHom R x) (CategoryTheory.CategoryStruct.comp (localizationToStalk R x) h) = h

@[simp]

theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_stalkToFiberRingHom (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) : CategoryTheory.CategoryStruct.comp (localizationToStalk R x) (stalkToFiberRingHom R x) = CategoryTheory.CategoryStruct.id (CommRingCat.of (Localization.AtPrime x.asIdeal))

theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_stalkToFiberRingHom_assoc (R : Type u) [CommRing R] (x : ↑(PrimeSpectrum.Top R)) {Z : CommRingCat} (h : CommRingCat.of (Localization.AtPrime x.asIdeal) ⟶ Z) : CategoryTheory.CategoryStruct.comp (localizationToStalk R x) (CategoryTheory.CategoryStruct.comp (stalkToFiberRingHom R x) h) = h

def AlgebraicGeometry.StructureSheaf.toBasicOpen (R : Type u) [CommRing R] (f : R) : Localization.Away f →+* ↑((Spec.structureSheaf R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))

The canonical ring homomorphism interpreting s ∈ R_f as a section of the structure sheaf on the basic open defined by f ∈ R.

Equations

• AlgebraicGeometry.StructureSheaf.toBasicOpen R f = IsLocalization.Away.lift f ⋯

@[simp]

theorem AlgebraicGeometry.StructureSheaf.toBasicOpen_mk' (R : Type u) [CommRing R] (s f : R) (g : ↥(Submonoid.powers s)) : (toBasicOpen R s) (IsLocalization.mk' (Localization.Away s) f g) = const R f (↑g) (PrimeSpectrum.basicOpen s) ⋯

@[simp]

theorem AlgebraicGeometry.StructureSheaf.localization_toBasicOpen (R : Type u) [CommRing R] (f : R) : (toBasicOpen R f).comp (algebraMap R (Localization.Away f)) = CommRingCat.Hom.hom (toOpen R (PrimeSpectrum.basicOpen f))

@[simp]

theorem AlgebraicGeometry.StructureSheaf.toBasicOpen_to_map (R : Type u) [CommRing R] (s f : R) : (toBasicOpen R s) ((algebraMap R (Localization.Away s)) f) = const R f 1 (PrimeSpectrum.basicOpen s) ⋯

theorem AlgebraicGeometry.StructureSheaf.toBasicOpen_injective (R : Type u) [CommRing R] (f : R) : Function.Injective ⇑(toBasicOpen R f)

theorem AlgebraicGeometry.StructureSheaf.locally_const_basicOpen (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (s : ↑((Spec.structureSheaf R).val.obj (Opposite.op U))) (x : ↥U) : ∃ (f : R) (g : R) (i : PrimeSpectrum.basicOpen g ⟶ U), ↑x ∈ PrimeSpectrum.basicOpen g ∧ const R f g (PrimeSpectrum.basicOpen g) ⋯ = (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).val.map i.op)) s

theorem AlgebraicGeometry.StructureSheaf.normalize_finite_fraction_representation (R : Type u) [CommRing R] (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top R)) (s : ↑((Spec.structureSheaf R).val.obj (Opposite.op U))) {ι : Type u_1} (t : Finset ι) (a h : ι → R) (iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U) (h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)) (hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).val.map (iDh i).op)) s) : ∃ (a' : ι → R) (h' : ι → R) (iDh' : (i : ι) → PrimeSpectrum.basicOpen (h' i) ⟶ U), U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i) ∧ (∀ i ∈ t, ∀ j ∈ t, a' i * h' j = h' i * a' j) ∧ ∀ i ∈ t, (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).val.map (iDh' i).op)) s = const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) ⋯

theorem AlgebraicGeometry.StructureSheaf.toBasicOpen_surjective (R : Type u) [CommRing R] (f : R) : Function.Surjective ⇑(toBasicOpen R f)

instance AlgebraicGeometry.StructureSheaf.isIso_toBasicOpen (R : Type u) [CommRing R] (f : R) : CategoryTheory.IsIso (CommRingCat.ofHom (toBasicOpen R f))

def AlgebraicGeometry.StructureSheaf.basicOpenIso (R : Type u) [CommRing R] (f : R) : (Spec.structureSheaf R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)) ≅ CommRingCat.of (Localization.Away f)

The ring isomorphism between the structure sheaf on basicOpen f and the localization of R at the submonoid of powers of f.

Equations

• AlgebraicGeometry.StructureSheaf.basicOpenIso R f = (CategoryTheory.asIso (CommRingCat.ofHom (AlgebraicGeometry.StructureSheaf.toBasicOpen R f))).symm

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 = (CommRingCat.Hom.hom (AlgebraicGeometry.StructureSheaf.toOpen R (Opposite.unop U))).toAlgebra

@[simp]

theorem AlgebraicGeometry.StructureSheaf.openAlgebra_map (R : Type u) [CommRing R] (U : (TopologicalSpace.Opens (PrimeSpectrum R))ᵒᵖ) (r : R) : (algebraMap R ↑((Spec.structureSheaf R).val.obj U)) r = (CategoryTheory.ConcreteCategory.hom (toOpen R (Opposite.unop U))) r

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 (toOpen R (PrimeSpectrum.basicOpen r))

theorem AlgebraicGeometry.StructureSheaf.to_global_factors (R : Type u) [CommRing R] : toOpen R ⊤ = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R (Localization.Away 1))) (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (toBasicOpen R 1)) ((Spec.structureSheaf R).val.map (CategoryTheory.eqToHom ⋯).op))

theorem AlgebraicGeometry.StructureSheaf.to_global_factors_apply (R : Type u) [CommRing R] (x : CategoryTheory.ToType (CommRingCat.of R)) : (CategoryTheory.ConcreteCategory.hom (toOpen R ⊤)) x = (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).val.map (CategoryTheory.eqToHom ⋯))) (const R x 1 (PrimeSpectrum.basicOpen 1) ⋯)

instance AlgebraicGeometry.StructureSheaf.isIso_to_global (R : Type u) [CommRing R] : CategoryTheory.IsIso (toOpen R ⊤)

def AlgebraicGeometry.StructureSheaf.globalSectionsIso (R : Type u) [CommRing R] : CommRingCat.of R ≅ (Spec.structureSheaf R).val.obj (Opposite.op ⊤)

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

Equations

• AlgebraicGeometry.StructureSheaf.globalSectionsIso R = CategoryTheory.asIso (AlgebraicGeometry.StructureSheaf.toOpen R ⊤)

@[simp]

theorem AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv (R : Type u) [CommRing R] : (globalSectionsIso R).inv = CategoryTheory.inv (toOpen R ⊤)

@[simp]

theorem AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom (R : CommRingCat) : (globalSectionsIso ↑R).hom = toOpen ↑R ⊤

@[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✝ : CategoryTheory.ToType (CommRingCat.of R)) : (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).presheaf.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (toStalk R y)) x✝) = (CategoryTheory.ConcreteCategory.hom (toStalk R x)) x✝

@[simp]

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

theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_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 (localizationToStalk R y) (CategoryTheory.CategoryStruct.comp ((Spec.structureSheaf R).presheaf.stalkSpecializes h) h✝) = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h)) (CategoryTheory.CategoryStruct.comp (localizationToStalk R x) h✝)

theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_stalkSpecializes_apply {R : Type u_1} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) (x✝ : CategoryTheory.ToType (CommRingCat.of (Localization.AtPrime y.asIdeal))) : (CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).presheaf.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (localizationToStalk R y)) x✝) = (CategoryTheory.ConcreteCategory.hom (localizationToStalk R x)) ((CategoryTheory.ConcreteCategory.hom (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h))) x✝)

@[simp]

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

theorem AlgebraicGeometry.StructureSheaf.stalkSpecializes_stalk_to_fiber_assoc {R : Type u_1} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) {Z : CommRingCat} (h✝ : CommRingCat.of (Localization.AtPrime x.asIdeal) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((Spec.structureSheaf R).presheaf.stalkSpecializes h) (CategoryTheory.CategoryStruct.comp (stalkToFiberRingHom R x) h✝) = CategoryTheory.CategoryStruct.comp (stalkToFiberRingHom R y) (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h)) h✝)

theorem AlgebraicGeometry.StructureSheaf.stalkSpecializes_stalk_to_fiber_apply {R : Type u_1} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) (x✝ : CategoryTheory.ToType ((Spec.structureSheaf R).presheaf.stalk y)) : (CategoryTheory.ConcreteCategory.hom (stalkToFiberRingHom R x)) ((CategoryTheory.ConcreteCategory.hom ((Spec.structureSheaf R).presheaf.stalkSpecializes h)) x✝) = (CategoryTheory.ConcreteCategory.hom (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h))) ((CategoryTheory.ConcreteCategory.hom (stalkToFiberRingHom R y)) x✝)

def AlgebraicGeometry.StructureSheaf.comapFun {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 : (x : ↥U) → Localizations R ↑x) (y : ↥V) : Localizations S ↑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 = (Localization.localRingHom ((PrimeSpectrum.comap f) ↑y).asIdeal (↑y).asIdeal f ⋯) (s ⟨(PrimeSpectrum.comap f) ↑y, ⋯⟩)

theorem AlgebraicGeometry.StructureSheaf.comapFunIsLocallyFraction {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 : (x : ↥U) → Localizations R ↑x) (hs : (isLocallyFraction R).pred s) : (isLocallyFraction S).pred (comapFun f U V hUV s)

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 R a b U hb) = const S (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 (toOpen R U) (CommRingCat.ofHom (comap f U ((TopologicalSpace.Opens.comap (PrimeSpectrum.comap f)) U) ⋯)) = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom f) (toOpen S ((TopologicalSpace.Opens.comap (PrimeSpectrum.comap f)) 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 : CategoryTheory.ToType (CommRingCat.of R)) : (comap f U ((TopologicalSpace.Opens.comap (PrimeSpectrum.comap f)) U) ⋯) ((CategoryTheory.ConcreteCategory.hom (toOpen R U)) x) = (CategoryTheory.ConcreteCategory.hom (toOpen S ((TopologicalSpace.Opens.comap (PrimeSpectrum.comap f)) 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 : CommRingCat.of ↑((Spec.structureSheaf S).val.obj (Opposite.op ((TopologicalSpace.Opens.comap (PrimeSpectrum.comap f)) U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (toOpen R U) (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (comap f U ((TopologicalSpace.Opens.comap (PrimeSpectrum.comap f)) U) ⋯)) h) = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom f) (CategoryTheory.CategoryStruct.comp (toOpen S ((TopologicalSpace.Opens.comap (PrimeSpectrum.comap f)) 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 ⋯