mathlib documentation

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

def algebraic_geometry.Spec.Top (R : Type u) [comm_ring R] :

$Spec R$, just as a topological space.

Equations

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

Equations

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

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

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

Equations

The stalk_to_fiber map for the structure sheaf is surjective. (In fact, an isomorphism, as constructed below in stalk_iso_Type.)

The stalk_to_fiber map for the structure sheaf is injective. (In fact, an isomorphism, as constructed below in stalk_iso_Type.)

The proof here follows the argument in Hartshorne's Algebraic Geometry, Proposition II.2.2.

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
theorem algebraic_geometry.const_add (R : Type u) [comm_ring R] (f₁ f₂ g₁ g₂ : R) (U : topological_space.opens (algebraic_geometry.Spec.Top R)) (hu₁ : ∀ (x : (algebraic_geometry.Spec.Top R)), x Ug₁ (prime_spectrum.as_ideal x).prime_compl) (hu₂ : ∀ (x : (algebraic_geometry.Spec.Top R)), x Ug₂ (prime_spectrum.as_ideal x).prime_compl) :
algebraic_geometry.const R f₁ g₁ U hu₁ + algebraic_geometry.const R f₂ g₂ U hu₂ = algebraic_geometry.const R (f₁ * g₂ + f₂ * g₁) (g₁ * g₂) U _

theorem algebraic_geometry.const_mul (R : Type u) [comm_ring R] (f₁ f₂ g₁ g₂ : R) (U : topological_space.opens (algebraic_geometry.Spec.Top R)) (hu₁ : ∀ (x : (algebraic_geometry.Spec.Top R)), x Ug₁ (prime_spectrum.as_ideal x).prime_compl) (hu₂ : ∀ (x : (algebraic_geometry.Spec.Top R)), x Ug₂ (prime_spectrum.as_ideal x).prime_compl) :
(algebraic_geometry.const R f₁ g₁ U hu₁) * algebraic_geometry.const R f₂ g₂ U hu₂ = algebraic_geometry.const R (f₁ * f₂) (g₁ * g₂) U _

theorem algebraic_geometry.const_ext (R : Type u) [comm_ring R] {f₁ f₂ g₁ g₂ : R} {U : topological_space.opens (algebraic_geometry.Spec.Top R)} {hu₁ : ∀ (x : (algebraic_geometry.Spec.Top R)), x Ug₁ (prime_spectrum.as_ideal x).prime_compl} {hu₂ : ∀ (x : (algebraic_geometry.Spec.Top R)), x Ug₂ (prime_spectrum.as_ideal x).prime_compl} :
f₁ * g₂ = f₂ * g₁algebraic_geometry.const R f₁ g₁ U hu₁ = algebraic_geometry.const R f₂ g₂ U hu₂

theorem algebraic_geometry.const_congr (R : Type u) [comm_ring R] {f₁ f₂ g₁ g₂ : R} {U : topological_space.opens (algebraic_geometry.Spec.Top R)} {hu : ∀ (x : (algebraic_geometry.Spec.Top R)), x Ug₁ (prime_spectrum.as_ideal x).prime_compl} (hf : f₁ = f₂) (hg : g₁ = g₂) :
algebraic_geometry.const R f₁ g₁ U hu = algebraic_geometry.const R f₂ g₂ U _

theorem algebraic_geometry.const_mul_cancel (R : Type u) [comm_ring R] (f g₁ g₂ : R) (U : topological_space.opens (algebraic_geometry.Spec.Top R)) (hu₁ : ∀ (x : (algebraic_geometry.Spec.Top R)), x Ug₁ (prime_spectrum.as_ideal x).prime_compl) (hu₂ : ∀ (x : (algebraic_geometry.Spec.Top R)), x Ug₂ (prime_spectrum.as_ideal x).prime_compl) :
(algebraic_geometry.const R f g₁ U hu₁) * algebraic_geometry.const R g₁ g₂ U hu₂ = algebraic_geometry.const R f g₂ U hu₂

theorem algebraic_geometry.const_mul_cancel' (R : Type u) [comm_ring R] (f g₁ g₂ : R) (U : topological_space.opens (algebraic_geometry.Spec.Top R)) (hu₁ : ∀ (x : (algebraic_geometry.Spec.Top R)), x Ug₁ (prime_spectrum.as_ideal x).prime_compl) (hu₂ : ∀ (x : (algebraic_geometry.Spec.Top R)), x Ug₂ (prime_spectrum.as_ideal x).prime_compl) :
(algebraic_geometry.const R g₁ g₂ U hu₂) * algebraic_geometry.const R f g₁ U hu₁ = algebraic_geometry.const R f g₂ U hu₂

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

Equations

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

Equations

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

Equations

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

Equations

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

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