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]
def
algebraic_geometry.structure_sheaf.localizations
(R : Type u)
[comm_ring R]
(P : ↥(algebraic_geometry.prime_spectrum.Top R)) :
Type u
The type family over prime_spectrum R consisting of the localization over each point.
Instances for algebraic_geometry.structure_sheaf.localizations
- algebraic_geometry.structure_sheaf.localizations.comm_ring
- algebraic_geometry.structure_sheaf.localizations.local_ring
- algebraic_geometry.structure_sheaf.localizations.inhabited
- algebraic_geometry.structure_sheaf.localizations.algebra
- algebraic_geometry.structure_sheaf.as_ideal.is_localization.at_prime
@[protected, instance]
def
algebraic_geometry.structure_sheaf.localizations.inhabited
(R : Type u)
[comm_ring R]
(P : ↥(algebraic_geometry.prime_spectrum.Top R)) :
Equations
@[protected, instance]
def
algebraic_geometry.structure_sheaf.localizations.algebra
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(x : ↥U) :
@[protected, instance]
def
algebraic_geometry.structure_sheaf.is_fraction
{R : Type u}
[comm_ring R]
{U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R)}
(f : Π (x : ↥U), algebraic_geometry.structure_sheaf.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
- algebraic_geometry.structure_sheaf.is_fraction f = ∃ (r s : R), ∀ (x : ↥U), s ∉ x.val.as_ideal ∧ f x * ⇑(algebra_map R (algebraic_geometry.structure_sheaf.localizations R ↑x)) s = ⇑(algebra_map R (algebraic_geometry.structure_sheaf.localizations R ↑x)) r
theorem
algebraic_geometry.structure_sheaf.is_fraction.eq_mk'
{R : Type u}
[comm_ring R]
{U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R)}
{f : Π (x : ↥U), algebraic_geometry.structure_sheaf.localizations R ↑x}
(hf : algebraic_geometry.structure_sheaf.is_fraction f) :
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.
@[simp]
theorem
algebraic_geometry.structure_sheaf.is_locally_fraction_pred
(R : Type u)
[comm_ring R]
{U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R)}
(f : Π (x : ↥U), algebraic_geometry.structure_sheaf.localizations R ↑x) :
(algebraic_geometry.structure_sheaf.is_locally_fraction R).to_prelocal_predicate.pred f = ∀ (x : ↥U), ∃ (V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R)) (m : x.val ∈ V) (i : V ⟶ U) (r s : R), ∀ (y : ↥V), s ∉ y.val.as_ideal ∧ f (⇑i y) * ⇑(algebra_map R (algebraic_geometry.structure_sheaf.localizations R ↑(⇑i y))) s = ⇑(algebra_map R (algebraic_geometry.structure_sheaf.localizations R ↑(⇑i y))) r
def
algebraic_geometry.structure_sheaf.sections_subring
(R : Type u)
[comm_ring R]
(U : (topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))ᵒᵖ) :
subring (Π (x : ↥(opposite.unop U)), algebraic_geometry.structure_sheaf.localizations R ↑x)
The functions satisfying is_locally_fraction form a subring.
Equations
- algebraic_geometry.structure_sheaf.sections_subring R U = {carrier := {f : Π (x : ↥(opposite.unop U)), algebraic_geometry.structure_sheaf.localizations R ↑x | (algebraic_geometry.structure_sheaf.is_locally_fraction R).to_prelocal_predicate.pred f}, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, neg_mem' := _}
The structure sheaf (valued in Type, not yet CommRing) is the subsheaf consisting of
functions satisfying is_locally_fraction.
@[protected, instance]
def
algebraic_geometry.comm_ring_structure_sheaf_in_Type_obj
(R : Type u)
[comm_ring R]
(U : (topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))ᵒᵖ) :
@[simp]
theorem
algebraic_geometry.structure_presheaf_in_CommRing_obj
(R : Type u)
[comm_ring R]
(U : (topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))ᵒᵖ) :
The structure presheaf, valued in CommRing, constructed by dressing up the Type valued
structure presheaf.
Equations
- algebraic_geometry.structure_presheaf_in_CommRing R = {obj := λ (U : (topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))ᵒᵖ), CommRing.of ((algebraic_geometry.structure_sheaf_in_Type R).val.obj U), map := λ (U V : (topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))ᵒᵖ) (i : U ⟶ V), {to_fun := (algebraic_geometry.structure_sheaf_in_Type R).val.map i, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
algebraic_geometry.structure_presheaf_in_CommRing_map_apply
(R : Type u)
[comm_ring R]
(U V : (topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))ᵒᵖ)
(i : U ⟶ V)
(ᾰ : (algebraic_geometry.structure_sheaf_in_Type R).val.obj 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
- algebraic_geometry.Spec.structure_sheaf R = {val := algebraic_geometry.structure_presheaf_in_CommRing R _inst_1, cond := _}
@[simp]
theorem
algebraic_geometry.structure_sheaf.res_apply
(R : Type u)
[comm_ring R]
(U V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(i : V ⟶ U)
(s : ↥((algebraic_geometry.Spec.structure_sheaf R).val.obj (opposite.op U)))
(x : ↥V) :
noncomputable
def
algebraic_geometry.structure_sheaf.const
(R : Type u)
[comm_ring R]
(f g : R)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hu : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g ∈ x.as_ideal.prime_compl) :
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
- algebraic_geometry.structure_sheaf.const R f g U hu = ⟨λ (x : ↥(opposite.unop (opposite.op U))), is_localization.mk' (algebraic_geometry.structure_sheaf.localizations R ↑x) f ⟨g, _⟩, _⟩
@[simp]
theorem
algebraic_geometry.structure_sheaf.const_apply
(R : Type u)
[comm_ring R]
(f g : R)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hu : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g ∈ x.as_ideal.prime_compl)
(x : ↥U) :
(algebraic_geometry.structure_sheaf.const R f g U hu).val x = is_localization.mk' (algebraic_geometry.structure_sheaf.localizations R ↑x) f ⟨g, _⟩
theorem
algebraic_geometry.structure_sheaf.const_apply'
(R : Type u)
[comm_ring R]
(f g : R)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hu : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g ∈ x.as_ideal.prime_compl)
(x : ↥U)
(hx : g ∈ ↑x.as_ideal.prime_compl) :
(algebraic_geometry.structure_sheaf.const R f g U hu).val x = is_localization.mk' (algebraic_geometry.structure_sheaf.localizations R ↑x) f ⟨g, hx⟩
theorem
algebraic_geometry.structure_sheaf.exists_const
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(s : ↥((algebraic_geometry.Spec.structure_sheaf R).val.obj (opposite.op U)))
(x : ↥(algebraic_geometry.prime_spectrum.Top R))
(hx : x ∈ U) :
∃ (V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R)) (hxV : x ∈ V) (i : V ⟶ U) (f g : R) (hg : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ V → g ∈ x.as_ideal.prime_compl), algebraic_geometry.structure_sheaf.const R f g V hg = ⇑((algebraic_geometry.Spec.structure_sheaf R).val.map i.op) s
@[simp]
theorem
algebraic_geometry.structure_sheaf.res_const
(R : Type u)
[comm_ring R]
(f g : R)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hu : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g ∈ x.as_ideal.prime_compl)
(V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hv : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ V → g ∈ x.as_ideal.prime_compl)
(i : opposite.op U ⟶ opposite.op V) :
⇑((algebraic_geometry.Spec.structure_sheaf R).val.map i) (algebraic_geometry.structure_sheaf.const R f g U hu) = algebraic_geometry.structure_sheaf.const R f g V hv
theorem
algebraic_geometry.structure_sheaf.res_const'
(R : Type u)
[comm_ring R]
(f g : R)
(V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hv : V ≤ prime_spectrum.basic_open g) :
theorem
algebraic_geometry.structure_sheaf.const_zero
(R : Type u)
[comm_ring R]
(f : R)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hu : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → f ∈ x.as_ideal.prime_compl) :
algebraic_geometry.structure_sheaf.const R 0 f U hu = 0
theorem
algebraic_geometry.structure_sheaf.const_self
(R : Type u)
[comm_ring R]
(f : R)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hu : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → f ∈ x.as_ideal.prime_compl) :
algebraic_geometry.structure_sheaf.const R f f U hu = 1
theorem
algebraic_geometry.structure_sheaf.const_one
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R)) :
algebraic_geometry.structure_sheaf.const R 1 1 U _ = 1
theorem
algebraic_geometry.structure_sheaf.const_add
(R : Type u)
[comm_ring R]
(f₁ f₂ g₁ g₂ : R)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hu₁ : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g₁ ∈ x.as_ideal.prime_compl)
(hu₂ : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g₂ ∈ x.as_ideal.prime_compl) :
algebraic_geometry.structure_sheaf.const R f₁ g₁ U hu₁ + algebraic_geometry.structure_sheaf.const R f₂ g₂ U hu₂ = algebraic_geometry.structure_sheaf.const R (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)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hu₁ : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g₁ ∈ x.as_ideal.prime_compl)
(hu₂ : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g₂ ∈ x.as_ideal.prime_compl) :
algebraic_geometry.structure_sheaf.const R f₁ g₁ U hu₁ * algebraic_geometry.structure_sheaf.const R f₂ g₂ U hu₂ = algebraic_geometry.structure_sheaf.const R (f₁ * f₂) (g₁ * g₂) U _
theorem
algebraic_geometry.structure_sheaf.const_ext
(R : Type u)
[comm_ring R]
{f₁ f₂ g₁ g₂ : R}
{U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R)}
{hu₁ : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g₁ ∈ x.as_ideal.prime_compl}
{hu₂ : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g₂ ∈ x.as_ideal.prime_compl}
(h : f₁ * g₂ = f₂ * g₁) :
algebraic_geometry.structure_sheaf.const R f₁ g₁ U hu₁ = algebraic_geometry.structure_sheaf.const R f₂ g₂ U hu₂
theorem
algebraic_geometry.structure_sheaf.const_congr
(R : Type u)
[comm_ring R]
{f₁ f₂ g₁ g₂ : R}
{U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R)}
{hu : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g₁ ∈ x.as_ideal.prime_compl}
(hf : f₁ = f₂)
(hg : g₁ = g₂) :
algebraic_geometry.structure_sheaf.const R f₁ g₁ U hu = algebraic_geometry.structure_sheaf.const R f₂ g₂ U _
theorem
algebraic_geometry.structure_sheaf.const_mul_rev
(R : Type u)
[comm_ring R]
(f g : R)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hu₁ : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g ∈ x.as_ideal.prime_compl)
(hu₂ : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → f ∈ x.as_ideal.prime_compl) :
algebraic_geometry.structure_sheaf.const R f g U hu₁ * algebraic_geometry.structure_sheaf.const R g f U hu₂ = 1
theorem
algebraic_geometry.structure_sheaf.const_mul_cancel
(R : Type u)
[comm_ring R]
(f g₁ g₂ : R)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hu₁ : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g₁ ∈ x.as_ideal.prime_compl)
(hu₂ : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g₂ ∈ x.as_ideal.prime_compl) :
algebraic_geometry.structure_sheaf.const R f g₁ U hu₁ * algebraic_geometry.structure_sheaf.const R g₁ g₂ U hu₂ = algebraic_geometry.structure_sheaf.const R f g₂ U hu₂
theorem
algebraic_geometry.structure_sheaf.const_mul_cancel'
(R : Type u)
[comm_ring R]
(f g₁ g₂ : R)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(hu₁ : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g₁ ∈ x.as_ideal.prime_compl)
(hu₂ : ∀ (x : ↥(algebraic_geometry.prime_spectrum.Top R)), x ∈ U → g₂ ∈ x.as_ideal.prime_compl) :
algebraic_geometry.structure_sheaf.const R g₁ g₂ U hu₂ * algebraic_geometry.structure_sheaf.const R f g₁ U hu₁ = algebraic_geometry.structure_sheaf.const R f g₂ U hu₂
def
algebraic_geometry.structure_sheaf.to_open
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R)) :
The canonical ring homomorphism interpreting an element of R as
a section of the structure sheaf.
Equations
- algebraic_geometry.structure_sheaf.to_open R U = {to_fun := λ (f : ↥(CommRing.of R)), ⟨λ (x : ↥(opposite.unop (opposite.op U))), ⇑(algebra_map R (algebraic_geometry.structure_sheaf.localizations R ↑x)) f, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
Instances for algebraic_geometry.structure_sheaf.to_open
@[simp]
theorem
algebraic_geometry.structure_sheaf.to_open_res
(R : Type u)
[comm_ring R]
(U V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(i : V ⟶ U) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.to_open_apply
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(f : R)
(x : ↥U) :
(⇑(algebraic_geometry.structure_sheaf.to_open R U) f).val x = ⇑(algebra_map R (algebraic_geometry.structure_sheaf.localizations R ↑x)) f
theorem
algebraic_geometry.structure_sheaf.to_open_eq_const
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(f : R) :
noncomputable
def
algebraic_geometry.structure_sheaf.to_stalk
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top R)) :
The canonical ring homomorphism interpreting an element of R as an element of
the stalk of structure_sheaf R at x.
Equations
@[simp]
theorem
algebraic_geometry.structure_sheaf.to_open_germ
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(x : ↥U) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.germ_to_open
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(x : ↥U)
(f : R) :
theorem
algebraic_geometry.structure_sheaf.germ_to_top
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top R))
(f : R) :
theorem
algebraic_geometry.structure_sheaf.is_unit_to_basic_open_self
(R : Type u)
[comm_ring R]
(f : R) :
theorem
algebraic_geometry.structure_sheaf.is_unit_to_stalk
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top R))
(f : ↥(x.as_ideal.prime_compl)) :
noncomputable
def
algebraic_geometry.structure_sheaf.localization_to_stalk
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top 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]
theorem
algebraic_geometry.structure_sheaf.localization_to_stalk_of
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top R))
(f : R) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.localization_to_stalk_mk'
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top R))
(f : R)
(s : ↥(x.as_ideal.prime_compl)) :
def
algebraic_geometry.structure_sheaf.open_to_localization
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(x : ↥(algebraic_geometry.prime_spectrum.Top R))
(hx : x ∈ U) :
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
- algebraic_geometry.structure_sheaf.open_to_localization R U x hx = {to_fun := λ (s : ↥((algebraic_geometry.Spec.structure_sheaf R).val.obj (opposite.op U))), s.val ⟨x, hx⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
algebraic_geometry.structure_sheaf.coe_open_to_localization
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(x : ↥(algebraic_geometry.prime_spectrum.Top R))
(hx : x ∈ U) :
⇑(algebraic_geometry.structure_sheaf.open_to_localization R U x hx) = λ (s : ↥((algebraic_geometry.Spec.structure_sheaf R).val.obj (opposite.op U))), s.val ⟨x, hx⟩
theorem
algebraic_geometry.structure_sheaf.open_to_localization_apply
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(x : ↥(algebraic_geometry.prime_spectrum.Top R))
(hx : x ∈ U)
(s : ↥((algebraic_geometry.Spec.structure_sheaf R).val.obj (opposite.op U))) :
⇑(algebraic_geometry.structure_sheaf.open_to_localization R U x hx) s = s.val ⟨x, hx⟩
noncomputable
def
algebraic_geometry.structure_sheaf.stalk_to_fiber_ring_hom
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top R)) :
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
- algebraic_geometry.structure_sheaf.stalk_to_fiber_ring_hom R x = category_theory.limits.colimit.desc ((topological_space.open_nhds.inclusion x).op ⋙ (algebraic_geometry.Spec.structure_sheaf R).val) {X := {α := localization.at_prime x.as_ideal _, str := localization.comm_ring x.as_ideal.prime_compl}, ι := {app := λ (U : (topological_space.open_nhds x)ᵒᵖ), algebraic_geometry.structure_sheaf.open_to_localization R ((topological_space.open_nhds.inclusion x).obj (opposite.unop U)) x _, naturality' := _}}
Instances for algebraic_geometry.structure_sheaf.stalk_to_fiber_ring_hom
@[simp]
theorem
algebraic_geometry.structure_sheaf.germ_comp_stalk_to_fiber_ring_hom
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(x : ↥U) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.stalk_to_fiber_ring_hom_germ'
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(x : ↥(algebraic_geometry.prime_spectrum.Top R))
(hx : x ∈ U)
(s : ↥((algebraic_geometry.Spec.structure_sheaf R).val.obj (opposite.op U))) :
⇑(algebraic_geometry.structure_sheaf.stalk_to_fiber_ring_hom R x) (⇑((algebraic_geometry.Spec.structure_sheaf R).presheaf.germ ⟨x, hx⟩) s) = s.val ⟨x, hx⟩
@[simp]
theorem
algebraic_geometry.structure_sheaf.stalk_to_fiber_ring_hom_germ
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(x : ↥U)
(s : ↥((algebraic_geometry.Spec.structure_sheaf R).val.obj (opposite.op U))) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.to_stalk_comp_stalk_to_fiber_ring_hom
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top R)) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.stalk_to_fiber_ring_hom_to_stalk
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top R))
(f : R) :
noncomputable
def
algebraic_geometry.structure_sheaf.stalk_iso
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top 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]
theorem
algebraic_geometry.structure_sheaf.stalk_to_fiber_ring_hom_localization_to_stalk_assoc
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top R))
{X' : CommRing}
(f' : (algebraic_geometry.Spec.structure_sheaf R).presheaf.stalk x ⟶ X') :
@[simp]
theorem
algebraic_geometry.structure_sheaf.stalk_to_fiber_ring_hom_localization_to_stalk
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top R)) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.localization_to_stalk_stalk_to_fiber_ring_hom_assoc
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top R))
{X' : CommRing}
(f' : CommRing.of (localization.at_prime x.as_ideal) ⟶ X') :
@[simp]
theorem
algebraic_geometry.structure_sheaf.localization_to_stalk_stalk_to_fiber_ring_hom
(R : Type u)
[comm_ring R]
(x : ↥(algebraic_geometry.prime_spectrum.Top R)) :
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 : ↥(submonoid.powers s)) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.localization_to_basic_open
(R : Type u)
[comm_ring R]
(f : R) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.to_basic_open_to_map
(R : Type u)
[comm_ring R]
(s f : R) :
theorem
algebraic_geometry.structure_sheaf.to_basic_open_injective
(R : Type u)
[comm_ring R]
(f : R) :
theorem
algebraic_geometry.structure_sheaf.locally_const_basic_open
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(s : ↥((algebraic_geometry.Spec.structure_sheaf R).val.obj (opposite.op U)))
(x : ↥U) :
∃ (f g : R) (i : prime_spectrum.basic_open g ⟶ U), x.val ∈ prime_spectrum.basic_open g ∧ algebraic_geometry.structure_sheaf.const R f g (prime_spectrum.basic_open g) _ = ⇑((algebraic_geometry.Spec.structure_sheaf R).val.map i.op) s
theorem
algebraic_geometry.structure_sheaf.normalize_finite_fraction_representation
(R : Type u)
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(s : ↥((algebraic_geometry.Spec.structure_sheaf R).val.obj (opposite.op U)))
{ι : Type u_1}
(t : finset ι)
(a h : ι → R)
(iDh : Π (i : ι), prime_spectrum.basic_open (h i) ⟶ U)
(h_cover : U ≤ ⨆ (i : ι) (H : i ∈ t), prime_spectrum.basic_open (h i))
(hs : ∀ (i : ι), algebraic_geometry.structure_sheaf.const R (a i) (h i) (prime_spectrum.basic_open (h i)) _ = ⇑((algebraic_geometry.Spec.structure_sheaf R).val.map (iDh i).op) s) :
∃ (a' h' : ι → R) (iDh' : Π (i : ι), prime_spectrum.basic_open (h' 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 → ⇑((algebraic_geometry.Spec.structure_sheaf R).val.map (iDh' i).op) s = algebraic_geometry.structure_sheaf.const R (a' i) (h' i) (prime_spectrum.basic_open (h' i)) _
theorem
algebraic_geometry.structure_sheaf.to_basic_open_surjective
(R : Type u)
[comm_ring R]
(f : R) :
@[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) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.stalk_algebra_map
(R : Type u)
[comm_ring R]
(p : prime_spectrum R)
(r : R) :
@[protected, instance]
def
algebraic_geometry.structure_sheaf.is_localization.to_stalk
(R : Type u)
[comm_ring R]
(p : prime_spectrum R) :
Stalk of the structure sheaf at a prime p as localization of R
@[protected, instance]
def
algebraic_geometry.structure_sheaf.open_algebra
(R : Type u)
[comm_ring R]
(U : (topological_space.opens (prime_spectrum R))ᵒᵖ) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.open_algebra_map
(R : Type u)
[comm_ring R]
(U : (topological_space.opens (prime_spectrum R))ᵒᵖ)
(r : R) :
⇑(algebra_map R ↥((algebraic_geometry.Spec.structure_sheaf R).val.obj U)) r = ⇑(algebraic_geometry.structure_sheaf.to_open R (opposite.unop U)) r
@[protected, instance]
def
algebraic_geometry.structure_sheaf.is_localization.to_basic_open
(R : Type u)
[comm_ring R]
(r : R) :
Sections of the structure sheaf of Spec R on a basic open as localization of R
@[protected, instance]
theorem
algebraic_geometry.structure_sheaf.to_global_factors_apply
(R : Type u)
[comm_ring R]
(x : ↥(CommRing.of R)) :
@[protected, instance]
@[simp]
theorem
algebraic_geometry.structure_sheaf.global_sections_iso_hom_apply_coe
(R : Type u)
[comm_ring R]
(f : ↥(CommRing.of R))
(x : ↥(opposite.unop (opposite.op ⊤))) :
noncomputable
def
algebraic_geometry.structure_sheaf.global_sections_iso
(R : Type u)
[comm_ring R] :
The ring isomorphism between the ring R and the global sections Γ(X, 𝒪ₓ).
@[simp]
theorem
algebraic_geometry.structure_sheaf.to_stalk_stalk_specializes
{R : Type u_1}
[comm_ring R]
{x y : prime_spectrum R}
(h : x ⤳ y) :
@[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' : (algebraic_geometry.Spec.structure_sheaf R).presheaf.stalk x ⟶ X') :
@[simp]
theorem
algebraic_geometry.structure_sheaf.to_stalk_stalk_specializes_apply
{R : Type u_1}
[comm_ring R]
{x y : prime_spectrum R}
(h : x ⤳ y)
(x_1 : ↥(CommRing.of R)) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.localization_to_stalk_stalk_specializes
{R : Type u_1}
[comm_ring R]
{x y : prime_spectrum R}
(h : x ⤳ y) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.localization_to_stalk_stalk_specializes_assoc
{R : Type u_1}
[comm_ring R]
{x y : prime_spectrum R}
(h : x ⤳ y)
{X' : CommRing}
(f' : (algebraic_geometry.Spec.structure_sheaf R).presheaf.stalk x ⟶ X') :
@[simp]
theorem
algebraic_geometry.structure_sheaf.localization_to_stalk_stalk_specializes_apply
{R : Type u_1}
[comm_ring R]
{x y : prime_spectrum R}
(h : x ⤳ y)
(x_1 : ↥(CommRing.of (localization.at_prime y.as_ideal))) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.stalk_specializes_stalk_to_fiber
{R : Type u_1}
[comm_ring R]
{x y : prime_spectrum R}
(h : x ⤳ y) :
@[simp]
theorem
algebraic_geometry.structure_sheaf.stalk_specializes_stalk_to_fiber_apply
{R : Type u_1}
[comm_ring R]
{x y : prime_spectrum R}
(h : x ⤳ y)
(x_1 : ↥((algebraic_geometry.Spec.structure_sheaf R).presheaf.stalk y)) :
@[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' : CommRing.of (localization.at_prime x.as_ideal) ⟶ X') :
noncomputable
def
algebraic_geometry.structure_sheaf.comap_fun
{R : Type u}
[comm_ring R]
{S : Type u}
[comm_ring S]
(f : R →+* S)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top S))
(hUV : V.carrier ⊆ ⇑(prime_spectrum.comap f) ⁻¹' U.carrier)
(s : Π (x : ↥U), algebraic_geometry.structure_sheaf.localizations R ↑x)
(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
- algebraic_geometry.structure_sheaf.comap_fun f U V hUV s y = ⇑(localization.local_ring_hom (⇑(prime_spectrum.comap f) y.val).as_ideal y.val.as_ideal f _) (s ⟨⇑(prime_spectrum.comap f) y.val, _⟩)
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)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top S))
(hUV : V.carrier ⊆ ⇑(prime_spectrum.comap f) ⁻¹' U.carrier)
(s : Π (x : ↥U), algebraic_geometry.structure_sheaf.localizations R ↑x)
(hs : (algebraic_geometry.structure_sheaf.is_locally_fraction R).to_prelocal_predicate.pred s) :
noncomputable
def
algebraic_geometry.structure_sheaf.comap
{R : Type u}
[comm_ring R]
{S : Type u}
[comm_ring S]
(f : R →+* S)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top S))
(hUV : V.carrier ⊆ ⇑(prime_spectrum.comap f) ⁻¹' U.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
- algebraic_geometry.structure_sheaf.comap f U V hUV = {to_fun := λ (s : ↥((algebraic_geometry.Spec.structure_sheaf R).val.obj (opposite.op U))), ⟨algebraic_geometry.structure_sheaf.comap_fun f U V hUV s.val, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
algebraic_geometry.structure_sheaf.comap_apply
{R : Type u}
[comm_ring R]
{S : Type u}
[comm_ring S]
(f : R →+* S)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top S))
(hUV : V.carrier ⊆ ⇑(prime_spectrum.comap f) ⁻¹' U.carrier)
(s : ↥((algebraic_geometry.Spec.structure_sheaf R).val.obj (opposite.op U)))
(p : ↥V) :
(⇑(algebraic_geometry.structure_sheaf.comap f U V hUV) s).val p = ⇑(localization.local_ring_hom (⇑(prime_spectrum.comap f) p.val).as_ideal p.val.as_ideal f rfl) (s.val ⟨⇑(prime_spectrum.comap f) p.val, _⟩)
theorem
algebraic_geometry.structure_sheaf.comap_const
{R : Type u}
[comm_ring R]
{S : Type u}
[comm_ring S]
(f : R →+* S)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top S))
(hUV : V.carrier ⊆ ⇑(prime_spectrum.comap f) ⁻¹' U.carrier)
(a b : R)
(hb : ∀ (x : prime_spectrum R), x ∈ U → b ∈ x.as_ideal.prime_compl) :
⇑(algebraic_geometry.structure_sheaf.comap f U V hUV) (algebraic_geometry.structure_sheaf.const R a b U hb) = algebraic_geometry.structure_sheaf.const S (⇑f a) (⇑f b) V _
theorem
algebraic_geometry.structure_sheaf.comap_id_eq_map
{R : Type u}
[comm_ring R]
(U V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top 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]
(U V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top 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_id'
{R : Type u}
[comm_ring R]
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R)) :
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)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(V : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top S))
(W : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top P))
(hUV : ∀ (p : prime_spectrum S), p ∈ V → ⇑(prime_spectrum.comap f) p ∈ U)
(hVW : ∀ (p : prime_spectrum P), p ∈ W → ⇑(prime_spectrum.comap g) p ∈ V) :
algebraic_geometry.structure_sheaf.comap (g.comp f) U W _ = (algebraic_geometry.structure_sheaf.comap g V W hVW).comp (algebraic_geometry.structure_sheaf.comap f U V 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)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
(x : ↥(CommRing.of R)) :
⇑(algebraic_geometry.structure_sheaf.comap f U (⇑(topological_space.opens.comap (prime_spectrum.comap f)) U) _) (⇑(algebraic_geometry.structure_sheaf.to_open R U) x) = ⇑(algebraic_geometry.structure_sheaf.to_open S (⇑(topological_space.opens.comap (prime_spectrum.comap f)) U)) (⇑(CommRing.of_hom f) x)
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)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R))
{X' : CommRing}
(f' : (algebraic_geometry.Spec.structure_sheaf S).val.obj (opposite.op (⇑(topological_space.opens.comap (prime_spectrum.comap f)) U)) ⟶ 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)
(U : topological_space.opens ↥(algebraic_geometry.prime_spectrum.Top R)) :