# mathlib3documentation

algebraic_geometry.structure_sheaf

# The structure sheaf on `prime_spectrum R`. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
theorem algebraic_geometry.structure_sheaf.is_fraction.eq_mk' {R : Type u} [comm_ring R] {f : Π (x : U), }  :
(r s : R), (x : U), (hs : s x.val.as_ideal), f x = s, hs⟩

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), s y.val.as_ideal 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]

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 x.as_ideal.prime_compl) :
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 g x.as_ideal.prime_compl), 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 g₁ x.as_ideal.prime_compl) (hu₂ : (x : , x U g₂ x.as_ideal.prime_compl) :
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 g₁ x.as_ideal.prime_compl) (hu₂ : (x : , x U g₂ x.as_ideal.prime_compl) :
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 g₁ x.as_ideal.prime_compl} {hu₂ : (x : , x U g₂ x.as_ideal.prime_compl} (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 g₁ x.as_ideal.prime_compl} (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 g₁ x.as_ideal.prime_compl) (hu₂ : (x : , x U g₂ x.as_ideal.prime_compl) :
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 g₁ x.as_ideal.prime_compl) (hu₂ : (x : , x U g₂ x.as_ideal.prime_compl) :
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]
@[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`

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⟩

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]
@[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]
@[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]
@[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 (i : ι) (H : i t), ) (hs : (i : ι), (h i) (prime_spectrum.basic_open (h i)) _ = (iDh i).op) s) :
(a' h' : ι R) (iDh' : Π (i : ι), U), (U (i : ι) (H : i t), prime_spectrum.basic_open (h' i)) ( (i : ι), i t (j : ι), j t a' 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]
Equations
@[protected, instance]

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

@[protected, instance]
Equations
@[simp]
@[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]
@[simp]
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.carrier ) (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.carrier ) (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.carrier ) :

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.carrier ) (s : ) (p : V) :
( hUV) s).val p = rfl) (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.carrier ) (a b : R) (hb : (x : , x U ) :
hUV) hb) = (f b) V _

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_assoc {R : Type u} [comm_ring R] {S : Type u} [comm_ring S] (f : R →+* S) {X' : CommRing} (f' : X') :