Projective spectrum of a graded ring #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The projective spectrum of a graded commutative ring is the subtype of all homogenous ideals that are prime and do not contain the irrelevant ideal. It is naturally endowed with a topology: the Zariski topology.
Notation #
Ris a commutative semiring;Ais a commutative ring and anR-algebra;𝒜 : ℕ → submodule R Ais the grading ofA;
Main definitions #
projective_spectrum 𝒜: The projective spectrum of a graded ringA, or equivalently, the set of all homogeneous ideals ofAthat is both prime and relevant i.e. not containing irrelevant ideal. Henceforth, we call elements of projective spectrum relevant homogeneous prime ideals.projective_spectrum.zero_locus 𝒜 s: The zero locus of a subsetsofAis the subset ofprojective_spectrum 𝒜consisting of all relevant homogeneous prime ideals that contains.projective_spectrum.vanishing_ideal t: The vanishing ideal of a subsettofprojective_spectrum 𝒜is the intersection of points int(viewed as relevant homogeneous prime ideals).projective_spectrum.Top: the topological space ofprojective_spectrum 𝒜endowed with the Zariski topology.
theorem
projective_spectrum.ext_iff
{R : Type u_1}
{A : Type u_2}
{_inst_1 : comm_semiring R}
{_inst_2 : comm_ring A}
{_inst_3 : algebra R A}
{𝒜 : ℕ → submodule R A}
{_inst_4 : graded_algebra 𝒜}
(x y : projective_spectrum 𝒜) :
x = y ↔ x.as_homogeneous_ideal = y.as_homogeneous_ideal
@[nolint, ext]
structure
projective_spectrum
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
Type u_2
- as_homogeneous_ideal : homogeneous_ideal 𝒜
- is_prime : self.as_homogeneous_ideal.to_ideal.is_prime
- not_irrelevant_le : ¬homogeneous_ideal.irrelevant 𝒜 ≤ self.as_homogeneous_ideal
The projective spectrum of a graded commutative ring is the subtype of all homogenous ideals that are prime and do not contain the irrelevant ideal.
Instances for projective_spectrum
- projective_spectrum.has_sizeof_inst
- projective_spectrum.zariski_topology
- projective_spectrum.partial_order
theorem
projective_spectrum.ext
{R : Type u_1}
{A : Type u_2}
{_inst_1 : comm_semiring R}
{_inst_2 : comm_ring A}
{_inst_3 : algebra R A}
{𝒜 : ℕ → submodule R A}
{_inst_4 : graded_algebra 𝒜}
(x y : projective_spectrum 𝒜)
(h : x.as_homogeneous_ideal = y.as_homogeneous_ideal) :
x = y
def
projective_spectrum.zero_locus
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(s : set A) :
The zero locus of a set s of elements of a commutative ring A is the set of all relevant
homogeneous prime ideals of the ring that contain the set s.
An element f of A can be thought of as a dependent function on the projective spectrum of 𝒜.
At a point x (a homogeneous prime ideal) the function (i.e., element) f takes values in the
quotient ring A modulo the prime ideal x. In this manner, zero_locus s is exactly the subset
of projective_spectrum 𝒜 where all "functions" in s vanish simultaneously.
Equations
- projective_spectrum.zero_locus 𝒜 s = {x : projective_spectrum 𝒜 | s ⊆ ↑(x.as_homogeneous_ideal)}
@[simp]
theorem
projective_spectrum.mem_zero_locus
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(x : projective_spectrum 𝒜)
(s : set A) :
x ∈ projective_spectrum.zero_locus 𝒜 s ↔ s ⊆ ↑(x.as_homogeneous_ideal)
@[simp]
theorem
projective_spectrum.zero_locus_span
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(s : set A) :
def
projective_spectrum.vanishing_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
{𝒜 : ℕ → submodule R A}
[graded_algebra 𝒜]
(t : set (projective_spectrum 𝒜)) :
The vanishing ideal of a set t of points of the projective spectrum of a commutative ring R
is the intersection of all the relevant homogeneous prime ideals in the set t.
An element f of A can be thought of as a dependent function on the projective spectrum of 𝒜.
At a point x (a homogeneous prime ideal) the function (i.e., element) f takes values in the
quotient ring A modulo the prime ideal x. In this manner, vanishing_ideal t is exactly the
ideal of A consisting of all "functions" that vanish on all of t.
Equations
- projective_spectrum.vanishing_ideal t = ⨅ (x : projective_spectrum 𝒜) (h : x ∈ t), x.as_homogeneous_ideal
theorem
projective_spectrum.coe_vanishing_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
{𝒜 : ℕ → submodule R A}
[graded_algebra 𝒜]
(t : set (projective_spectrum 𝒜)) :
↑(projective_spectrum.vanishing_ideal t) = {f : A | ∀ (x : projective_spectrum 𝒜), x ∈ t → f ∈ x.as_homogeneous_ideal}
theorem
projective_spectrum.mem_vanishing_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
{𝒜 : ℕ → submodule R A}
[graded_algebra 𝒜]
(t : set (projective_spectrum 𝒜))
(f : A) :
f ∈ projective_spectrum.vanishing_ideal t ↔ ∀ (x : projective_spectrum 𝒜), x ∈ t → f ∈ x.as_homogeneous_ideal
@[simp]
theorem
projective_spectrum.vanishing_ideal_singleton
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
{𝒜 : ℕ → submodule R A}
[graded_algebra 𝒜]
(x : projective_spectrum 𝒜) :
theorem
projective_spectrum.subset_zero_locus_iff_le_vanishing_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
{𝒜 : ℕ → submodule R A}
[graded_algebra 𝒜]
(t : set (projective_spectrum 𝒜))
(I : ideal A) :
theorem
projective_spectrum.gc_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
galois_connection (λ (I : ideal A), projective_spectrum.zero_locus 𝒜 ↑I) (λ (t : (set (projective_spectrum 𝒜))ᵒᵈ), (projective_spectrum.vanishing_ideal t).to_ideal)
zero_locus and vanishing_ideal form a galois connection.
theorem
projective_spectrum.gc_set
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
galois_connection (λ (s : set A), projective_spectrum.zero_locus 𝒜 s) (λ (t : (set (projective_spectrum 𝒜))ᵒᵈ), ↑(projective_spectrum.vanishing_ideal t))
zero_locus and vanishing_ideal form a galois connection.
theorem
projective_spectrum.gc_homogeneous_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
galois_connection (λ (I : homogeneous_ideal 𝒜), projective_spectrum.zero_locus 𝒜 ↑I) (λ (t : (set (projective_spectrum 𝒜))ᵒᵈ), projective_spectrum.vanishing_ideal t)
theorem
projective_spectrum.subset_zero_locus_iff_subset_vanishing_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(t : set (projective_spectrum 𝒜))
(s : set A) :
theorem
projective_spectrum.subset_vanishing_ideal_zero_locus
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(s : set A) :
theorem
projective_spectrum.ideal_le_vanishing_ideal_zero_locus
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(I : ideal A) :
theorem
projective_spectrum.homogeneous_ideal_le_vanishing_ideal_zero_locus
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(I : homogeneous_ideal 𝒜) :
theorem
projective_spectrum.subset_zero_locus_vanishing_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(t : set (projective_spectrum 𝒜)) :
theorem
projective_spectrum.zero_locus_anti_mono
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
{s t : set A}
(h : s ⊆ t) :
theorem
projective_spectrum.zero_locus_anti_mono_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
{s t : ideal A}
(h : s ≤ t) :
theorem
projective_spectrum.zero_locus_anti_mono_homogeneous_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
{s t : homogeneous_ideal 𝒜}
(h : s ≤ t) :
theorem
projective_spectrum.vanishing_ideal_anti_mono
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
{s t : set (projective_spectrum 𝒜)}
(h : s ⊆ t) :
theorem
projective_spectrum.zero_locus_bot
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
@[simp]
theorem
projective_spectrum.zero_locus_singleton_zero
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
@[simp]
theorem
projective_spectrum.zero_locus_empty
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
@[simp]
theorem
projective_spectrum.vanishing_ideal_univ
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
theorem
projective_spectrum.zero_locus_empty_of_one_mem
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
{s : set A}
(h : 1 ∈ s) :
@[simp]
theorem
projective_spectrum.zero_locus_singleton_one
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
projective_spectrum.zero_locus 𝒜 {1} = ∅
@[simp]
theorem
projective_spectrum.zero_locus_univ
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
theorem
projective_spectrum.zero_locus_sup_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(I J : ideal A) :
theorem
projective_spectrum.zero_locus_sup_homogeneous_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(I J : homogeneous_ideal 𝒜) :
theorem
projective_spectrum.zero_locus_union
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(s s' : set A) :
theorem
projective_spectrum.vanishing_ideal_union
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(t t' : set (projective_spectrum 𝒜)) :
theorem
projective_spectrum.zero_locus_supr_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
{γ : Sort u_3}
(I : γ → ideal A) :
projective_spectrum.zero_locus 𝒜 (↑⨆ (i : γ), I i) = ⋂ (i : γ), projective_spectrum.zero_locus 𝒜 ↑(I i)
theorem
projective_spectrum.zero_locus_supr_homogeneous_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
{γ : Sort u_3}
(I : γ → homogeneous_ideal 𝒜) :
projective_spectrum.zero_locus 𝒜 (↑⨆ (i : γ), I i) = ⋂ (i : γ), projective_spectrum.zero_locus 𝒜 ↑(I i)
theorem
projective_spectrum.zero_locus_Union
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
{γ : Sort u_3}
(s : γ → set A) :
projective_spectrum.zero_locus 𝒜 (⋃ (i : γ), s i) = ⋂ (i : γ), projective_spectrum.zero_locus 𝒜 (s i)
theorem
projective_spectrum.zero_locus_bUnion
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(s : set (set A)) :
theorem
projective_spectrum.vanishing_ideal_Union
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
{γ : Sort u_3}
(t : γ → set (projective_spectrum 𝒜)) :
projective_spectrum.vanishing_ideal (⋃ (i : γ), t i) = ⨅ (i : γ), projective_spectrum.vanishing_ideal (t i)
theorem
projective_spectrum.zero_locus_inf
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(I J : ideal A) :
theorem
projective_spectrum.union_zero_locus
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(s s' : set A) :
theorem
projective_spectrum.zero_locus_mul_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(I J : ideal A) :
theorem
projective_spectrum.zero_locus_mul_homogeneous_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(I J : homogeneous_ideal 𝒜) :
theorem
projective_spectrum.zero_locus_singleton_mul
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(f g : A) :
projective_spectrum.zero_locus 𝒜 {f * g} = projective_spectrum.zero_locus 𝒜 {f} ∪ projective_spectrum.zero_locus 𝒜 {g}
@[simp]
theorem
projective_spectrum.zero_locus_singleton_pow
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(f : A)
(n : ℕ)
(hn : 0 < n) :
projective_spectrum.zero_locus 𝒜 {f ^ n} = projective_spectrum.zero_locus 𝒜 {f}
theorem
projective_spectrum.sup_vanishing_ideal_le
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(t t' : set (projective_spectrum 𝒜)) :
theorem
projective_spectrum.mem_compl_zero_locus_iff_not_mem
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
{f : A}
{I : projective_spectrum 𝒜} :
I ∈ (projective_spectrum.zero_locus 𝒜 {f})ᶜ ↔ f ∉ I.as_homogeneous_ideal
@[protected, instance]
def
projective_spectrum.zariski_topology
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
The Zariski topology on the prime spectrum of a commutative ring is defined via the closed sets of the topology: they are exactly those sets that are the zero locus of a subset of the ring.
Equations
def
projective_spectrum.Top
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
The underlying topology of Proj is the projective spectrum of graded ring A.
Equations
theorem
projective_spectrum.is_open_iff
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(U : set (projective_spectrum 𝒜)) :
theorem
projective_spectrum.is_closed_iff_zero_locus
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(Z : set (projective_spectrum 𝒜)) :
theorem
projective_spectrum.is_closed_zero_locus
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(s : set A) :
theorem
projective_spectrum.zero_locus_vanishing_ideal_eq_closure
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(t : set (projective_spectrum 𝒜)) :
theorem
projective_spectrum.vanishing_ideal_closure
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(t : set (projective_spectrum 𝒜)) :
def
projective_spectrum.basic_open
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(r : A) :
basic_open r is the open subset containing all prime ideals not containing r.
Equations
- projective_spectrum.basic_open 𝒜 r = {carrier := {x : projective_spectrum 𝒜 | r ∉ x.as_homogeneous_ideal}, is_open' := _}
@[simp]
theorem
projective_spectrum.mem_basic_open
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(f : A)
(x : projective_spectrum 𝒜) :
x ∈ projective_spectrum.basic_open 𝒜 f ↔ f ∉ x.as_homogeneous_ideal
theorem
projective_spectrum.mem_coe_basic_open
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(f : A)
(x : projective_spectrum 𝒜) :
x ∈ ↑(projective_spectrum.basic_open 𝒜 f) ↔ f ∉ x.as_homogeneous_ideal
theorem
projective_spectrum.is_open_basic_open
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
{a : A} :
@[simp]
theorem
projective_spectrum.basic_open_eq_zero_locus_compl
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(r : A) :
↑(projective_spectrum.basic_open 𝒜 r) = (projective_spectrum.zero_locus 𝒜 {r})ᶜ
@[simp]
theorem
projective_spectrum.basic_open_one
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
@[simp]
theorem
projective_spectrum.basic_open_zero
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
theorem
projective_spectrum.basic_open_mul
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(f g : A) :
theorem
projective_spectrum.basic_open_mul_le_left
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(f g : A) :
theorem
projective_spectrum.basic_open_mul_le_right
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(f g : A) :
@[simp]
theorem
projective_spectrum.basic_open_pow
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(f : A)
(n : ℕ)
(hn : 0 < n) :
theorem
projective_spectrum.basic_open_eq_union_of_projection
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(f : A) :
projective_spectrum.basic_open 𝒜 f = ⨆ (i : ℕ), projective_spectrum.basic_open 𝒜 (⇑(graded_algebra.proj 𝒜 i) f)
theorem
projective_spectrum.is_topological_basis_basic_opens
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
topological_space.is_topological_basis (set.range (λ (r : A), ↑(projective_spectrum.basic_open 𝒜 r)))
The specialization order #
We endow projective_spectrum 𝒜 with a partial order,
where x ≤ y if and only if y ∈ closure {x}.
@[protected, instance]
def
projective_spectrum.partial_order
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜] :
@[simp]
theorem
projective_spectrum.as_ideal_le_as_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(x y : projective_spectrum 𝒜) :
x.as_homogeneous_ideal ≤ y.as_homogeneous_ideal ↔ x ≤ y
@[simp]
theorem
projective_spectrum.as_ideal_lt_as_ideal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(x y : projective_spectrum 𝒜) :
x.as_homogeneous_ideal < y.as_homogeneous_ideal ↔ x < y
theorem
projective_spectrum.le_iff_mem_closure
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(𝒜 : ℕ → submodule R A)
[graded_algebra 𝒜]
(x y : projective_spectrum 𝒜) :