# mathlibdocumentation

algebraic_geometry.structure_sheaf

# The structure sheaf on prime_spectrum R. #

We define the structure sheaf on Top.of (prime_spectrum 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 topology.sheaves.sheaf_of_functions, where we show that dependent functions into any type family form a sheaf, and also topology.sheaves.local_predicate, where we characterise the predicates which pick out sub-presheaves and sub-sheaves of these sheaves.)

We also set up the ring structure, obtaining structure_sheaf R : sheaf CommRing (Top.of (prime_spectrum R)).

We then construct two basic isomorphisms, relating the structure sheaf to the underlying ring R. First, structure_sheaf.stalk_iso 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, structure_sheaf.basic_open_iso gives an isomorphism between the structure sheaf on basic_open f and the localization of R at the submonoid of powers of f.

## References #

The prime spectrum, just as a topological space.

Equations
@[protected, instance]
@[protected, instance]

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

Equations
Instances for algebraic_geometry.structure_sheaf.localizations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def algebraic_geometry.structure_sheaf.is_fraction {R : Type u} [comm_ring R] (f : Π (x : U), ) :
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
• = ∃ (r s : R), ∀ (x : U), f x * =
theorem algebraic_geometry.structure_sheaf.is_fraction.eq_mk' {R : Type u} [comm_ring R] {f : Π (x : U), }  :
∃ (r s : R), ∀ (x : U), ∃ (hs : , f x =

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

Equations

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
@[simp]
theorem algebraic_geometry.structure_sheaf.is_locally_fraction_pred (R : Type u) [comm_ring R] (f : Π (x : U), ) :
= ∀ (x : U), ∃ (V : (m : x.val V) (i : V U) (r s : R), ∀ (y : V), f (i y) * s = r

The functions satisfying is_locally_fraction form a subring.

Equations

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

Equations
@[protected, instance]
Equations
@[simp]

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

Equations
@[simp]
theorem algebraic_geometry.structure_presheaf_in_CommRing_map_apply (R : Type u) [comm_ring R] (i : U V) (ᾰ : U) :

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

Equations

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

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

Equations
@[simp]
theorem algebraic_geometry.structure_sheaf.res_apply (R : Type u) [comm_ring R] (i : V U) (s : ) (x : V) :
( s).val x = s.val (i x)
noncomputable def algebraic_geometry.structure_sheaf.const (R : Type u) [comm_ring R] (f g : R) (hu : ∀ (x : , x U) :

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

Equations
@[simp]
theorem algebraic_geometry.structure_sheaf.const_apply (R : Type u) [comm_ring R] (f g : R) (hu : ∀ (x : , x U) (x : U) :
hu).val x =
theorem algebraic_geometry.structure_sheaf.const_apply' (R : Type u) [comm_ring R] (f g : R) (hu : ∀ (x : , x U) (x : U) (hx : g ) :
hu).val x =
theorem algebraic_geometry.structure_sheaf.exists_const (R : Type u) [comm_ring R] (s : ) (hx : x U) :
∃ (V : (hxV : x V) (i : V U) (f g : R) (hg : ∀ (x : , x V, hg = s
@[simp]
theorem algebraic_geometry.structure_sheaf.res_const (R : Type u) [comm_ring R] (f g : R) (hu : ∀ (x : , x U) (hv : ∀ (x : , x V) (i : ) :
hu) = hv
theorem algebraic_geometry.structure_sheaf.res_const' (R : Type u) [comm_ring R] (f g : R) (hv : V ) :
theorem algebraic_geometry.structure_sheaf.const_zero (R : Type u) [comm_ring R] (f : R) (hu : ∀ (x : , x U) :
hu = 0
theorem algebraic_geometry.structure_sheaf.const_self (R : Type u) [comm_ring R] (f : R) (hu : ∀ (x : , x U) :
hu = 1
theorem algebraic_geometry.structure_sheaf.const_add (R : Type u) [comm_ring R] (f₁ f₂ g₁ g₂ : R) (hu₁ : ∀ (x : , x U) (hu₂ : ∀ (x : , x U) :
hu₁ + hu₂ = (f₁ * g₂ + f₂ * g₁) (g₁ * g₂) U _
theorem algebraic_geometry.structure_sheaf.const_mul (R : Type u) [comm_ring R] (f₁ f₂ g₁ g₂ : R) (hu₁ : ∀ (x : , x U) (hu₂ : ∀ (x : , x U) :
hu₁ * hu₂ = (g₁ * g₂) U _
theorem algebraic_geometry.structure_sheaf.const_ext (R : Type u) [comm_ring R] {f₁ f₂ g₁ g₂ : R} {hu₁ : ∀ (x : , x U} {hu₂ : ∀ (x : , x U} (h : f₁ * g₂ = f₂ * g₁) :
hu₁ = hu₂
theorem algebraic_geometry.structure_sheaf.const_congr (R : Type u) [comm_ring R] {f₁ f₂ g₁ g₂ : R} {hu : ∀ (x : , x U} (hf : f₁ = f₂) (hg : g₁ = g₂) :
hu = _
theorem algebraic_geometry.structure_sheaf.const_mul_rev (R : Type u) [comm_ring R] (f g : R) (hu₁ : ∀ (x : , x U) (hu₂ : ∀ (x : , x U) :
hu₁ * hu₂ = 1
theorem algebraic_geometry.structure_sheaf.const_mul_cancel (R : Type u) [comm_ring R] (f g₁ g₂ : R) (hu₁ : ∀ (x : , x U) (hu₂ : ∀ (x : , x U) :
hu₁ * hu₂ = hu₂
theorem algebraic_geometry.structure_sheaf.const_mul_cancel' (R : Type u) [comm_ring R] (f g₁ g₂ : R) (hu₁ : ∀ (x : , x U) (hu₂ : ∀ (x : , x U) :
hu₂ * hu₁ = hu₂

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

Equations
Instances for algebraic_geometry.structure_sheaf.to_open
@[simp]
theorem algebraic_geometry.structure_sheaf.to_open_res (R : Type u) [comm_ring R] (i : V U) :
@[simp]
theorem algebraic_geometry.structure_sheaf.to_open_apply (R : Type u) [comm_ring R] (f : R) (x : U) :
noncomputable def algebraic_geometry.structure_sheaf.to_stalk (R : Type u) [comm_ring R]  :

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

Equations
@[simp]
@[simp]
theorem algebraic_geometry.structure_sheaf.germ_to_open (R : Type u) [comm_ring R] (x : U) (f : R) :

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

Equations
Instances for algebraic_geometry.structure_sheaf.localization_to_stalk
@[simp]

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
@[simp]
theorem algebraic_geometry.structure_sheaf.coe_open_to_localization (R : Type u) [comm_ring R] (hx : x U) :
= λ (s : , s.val x, hx⟩
theorem algebraic_geometry.structure_sheaf.open_to_localization_apply (R : Type u) [comm_ring R] (hx : x U) (s : ) :
= s.val x, hx⟩

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 open_to_localization maps.

Equations
Instances for algebraic_geometry.structure_sheaf.stalk_to_fiber_ring_hom
@[simp]
@[simp]
theorem algebraic_geometry.structure_sheaf.stalk_to_fiber_ring_hom_germ' (R : Type u) [comm_ring R] (hx : x U) (s : ) :
= s.val x, hx⟩
@[simp]
noncomputable def algebraic_geometry.structure_sheaf.stalk_iso (R : Type u) [comm_ring R]  :

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
@[simp]
@[simp]
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
@[simp]
noncomputable def algebraic_geometry.structure_sheaf.to_basic_open (R : Type u) [comm_ring R] (f : R) :

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

Equations
Instances for algebraic_geometry.structure_sheaf.to_basic_open
@[simp]
theorem algebraic_geometry.structure_sheaf.to_basic_open_mk' (R : Type u) [comm_ring R] (s f : R) (g : ) :
@[simp]
theorem algebraic_geometry.structure_sheaf.locally_const_basic_open (R : Type u) [comm_ring R] (s : ) (x : U) :
∃ (f g : R) (i : ,
theorem algebraic_geometry.structure_sheaf.normalize_finite_fraction_representation (R : Type u) [comm_ring R] (s : ) {ι : Type u_1} (t : finset ι) (a h : ι → R) (iDh : Π (i : ι), U) (h_cover : U.val ⋃ (i : ι) (H : i t), (prime_spectrum.basic_open (h i)).val) (hs : ∀ (i : ι), (h i) (prime_spectrum.basic_open (h i)) _ = (iDh i).op) s) :
∃ (a' h' : ι → R) (iDh' : Π (i : ι), U), (U.val ⋃ (i : ι) (H : i t), (prime_spectrum.basic_open (h' i)).val) (∀ (i : ι), i t∀ (j : ι), j ta' i * h' j = h' i * a' j) ∀ (i : ι), i t (iDh' i).op) s = (h' i) (prime_spectrum.basic_open (h' i)) _
@[protected, instance]
noncomputable def algebraic_geometry.structure_sheaf.basic_open_iso (R : Type u) [comm_ring R] (f : R) :

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

Equations
@[protected, instance]
noncomputable def algebraic_geometry.structure_sheaf.stalk_algebra (R : Type u) [comm_ring R] (p : prime_spectrum R) :
Equations
@[simp]
@[protected, instance]

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

@[protected, instance]
Equations
@[simp]
theorem algebraic_geometry.structure_sheaf.open_algebra_map (R : Type u) [comm_ring R] (U : ᵒᵖ) (r : R) :
@[protected, instance]

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

@[protected, instance]
@[protected, instance]
@[simp]

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

Equations
@[simp]
@[simp]
theorem algebraic_geometry.structure_sheaf.to_stalk_stalk_specializes_assoc {R : Type u_1} [comm_ring R] {x y : prime_spectrum R} (h : x y) {X' : CommRing} (f' : X') :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem algebraic_geometry.structure_sheaf.stalk_specializes_stalk_to_fiber_assoc {R : Type u_1} [comm_ring R] {x y : prime_spectrum R} (h : x y) {X' : CommRing} (f' : X') :
noncomputable def algebraic_geometry.structure_sheaf.comap_fun {R : Type u} [comm_ring R] {S : Type u} [comm_ring S] (f : R →+* S) (hUV : V.val ) (s : Π (x : U), ) (y : V) :

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.local_ring_hom _ _ 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 is_locally_fraction is preserved by this map, hence it can be extended to a morphism between the structure sheaves of R and S.

Equations
theorem algebraic_geometry.structure_sheaf.comap_fun_is_locally_fraction {R : Type u} [comm_ring R] {S : Type u} [comm_ring S] (f : R →+* S) (hUV : V.val ) (s : Π (x : U), )  :
noncomputable def algebraic_geometry.structure_sheaf.comap {R : Type u} [comm_ring R] {S : Type u} [comm_ring S] (f : R →+* S) (hUV : V.val ) :

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
@[simp]
theorem algebraic_geometry.structure_sheaf.comap_apply {R : Type u} [comm_ring R] {S : Type u} [comm_ring S] (f : R →+* S) (hUV : V.val ) (s : ) (p : V) :
( hUV) s).val p = (s.val p.val, _⟩)
theorem algebraic_geometry.structure_sheaf.comap_const {R : Type u} [comm_ring R] {S : Type u} [comm_ring S] (f : R →+* S) (hUV : V.val ) (a b : R) (hb : ∀ (x : , x U) :
hUV) hb) = (f b) V _
theorem algebraic_geometry.structure_sheaf.comap_id_eq_map {R : Type u} [comm_ring R] (iVU : V U) :

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 algebraic_geometry.structure_sheaf.comap_id {R : Type u} [comm_ring R] (hUV : U = V) :

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 be useful when U and V are not definitionally equal.

@[simp]
theorem algebraic_geometry.structure_sheaf.comap_comp {R : Type u} [comm_ring R] {S : Type u} [comm_ring S] {P : Type u} [comm_ring P] (f : R →+* S) (g : S →+* P) (hUV : ∀ (p : , p V U) (hVW : ∀ (p : , p W V) :
_ = hVW).comp hUV)
theorem algebraic_geometry.structure_sheaf.to_open_comp_comap_apply {R : Type u} [comm_ring R] {S : Type u} [comm_ring S] (f : R →+* S) (x : (CommRing.of R)) :
theorem algebraic_geometry.structure_sheaf.to_open_comp_comap_assoc {R : Type u} [comm_ring R] {S : Type u} [comm_ring S] (f : R →+* S) {X' : CommRing} (f' : X') :
theorem algebraic_geometry.structure_sheaf.to_open_comp_comap {R : Type u} [comm_ring R] {S : Type u} [comm_ring S] (f : R →+* S)  :