mathlib documentation

algebraic_geometry.projective_spectrum.topology

Projective spectrum of a graded ring #

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 #

Main definitions #

source
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
source
@[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

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
source
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
source
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) :
set (projective_spectrum π’œ)

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
source
@[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)
source
@[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) :
projective_spectrum.zero_locus π’œ ↑(ideal.span s) = projective_spectrum.zero_locus π’œ s
source
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 π’œ)) :
homogeneous_ideal π’œ

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
source
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}
source
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
source
@[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 π’œ) :
projective_spectrum.vanishing_ideal {x} = x.as_homogeneous_ideal
source
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) :
t βŠ† projective_spectrum.zero_locus π’œ ↑I ↔ I ≀ (projective_spectrum.vanishing_ideal t).to_ideal
source
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.

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

source
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)
source
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) :
t βŠ† projective_spectrum.zero_locus π’œ s ↔ s βŠ† ↑(projective_spectrum.vanishing_ideal t)
source
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) :
s βŠ† ↑(projective_spectrum.vanishing_ideal (projective_spectrum.zero_locus π’œ s))
source
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) :
I ≀ (projective_spectrum.vanishing_ideal (projective_spectrum.zero_locus π’œ ↑I)).to_ideal
source
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 π’œ) :
I ≀ projective_spectrum.vanishing_ideal (projective_spectrum.zero_locus π’œ ↑I)
source
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 π’œ)) :
t βŠ† projective_spectrum.zero_locus π’œ ↑(projective_spectrum.vanishing_ideal t)
source
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) :
projective_spectrum.zero_locus π’œ t βŠ† projective_spectrum.zero_locus π’œ s
source
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) :
projective_spectrum.zero_locus π’œ ↑t βŠ† projective_spectrum.zero_locus π’œ ↑s
source
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) :
projective_spectrum.zero_locus π’œ ↑t βŠ† projective_spectrum.zero_locus π’œ ↑s
source
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) :
projective_spectrum.vanishing_ideal t ≀ projective_spectrum.vanishing_ideal s
source
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 π’œ] :
projective_spectrum.zero_locus π’œ ↑βŠ₯ = set.univ
source
@[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 π’œ] :
projective_spectrum.zero_locus π’œ {0} = set.univ
source
@[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 π’œ] :
projective_spectrum.zero_locus π’œ βˆ… = set.univ
source
@[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 π’œ] :
projective_spectrum.vanishing_ideal βˆ… = ⊀
source
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) :
projective_spectrum.zero_locus π’œ s = βˆ…
source
@[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} = βˆ…
source
@[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 π’œ] :
projective_spectrum.zero_locus π’œ set.univ = βˆ…
source
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) :
projective_spectrum.zero_locus π’œ ↑(I βŠ” J) = projective_spectrum.zero_locus π’œ ↑I ∩ projective_spectrum.zero_locus π’œ ↑J
source
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 π’œ) :
projective_spectrum.zero_locus π’œ ↑(I βŠ” J) = projective_spectrum.zero_locus π’œ ↑I ∩ projective_spectrum.zero_locus π’œ ↑J
source
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) :
projective_spectrum.zero_locus π’œ (s βˆͺ s') = projective_spectrum.zero_locus π’œ s ∩ projective_spectrum.zero_locus π’œ s'
source
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 π’œ)) :
projective_spectrum.vanishing_ideal (t βˆͺ t') = projective_spectrum.vanishing_ideal t βŠ“ projective_spectrum.vanishing_ideal t'
source
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)
source
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)
source
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)
source
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)) :
projective_spectrum.zero_locus π’œ (⋃ (s' : set A) (H : s' ∈ s), s') = β‹‚ (s' : set A) (H : s' ∈ s), projective_spectrum.zero_locus π’œ s'
source
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)
source
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) :
projective_spectrum.zero_locus π’œ ↑(I βŠ“ J) = projective_spectrum.zero_locus π’œ ↑I βˆͺ projective_spectrum.zero_locus π’œ ↑J
source
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) :
projective_spectrum.zero_locus π’œ s βˆͺ projective_spectrum.zero_locus π’œ s' = projective_spectrum.zero_locus π’œ ↑(ideal.span s βŠ“ ideal.span s')
source
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) :
projective_spectrum.zero_locus π’œ ↑(I * J) = projective_spectrum.zero_locus π’œ ↑I βˆͺ projective_spectrum.zero_locus π’œ ↑J
source
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 π’œ) :
projective_spectrum.zero_locus π’œ ↑(I * J) = projective_spectrum.zero_locus π’œ ↑I βˆͺ projective_spectrum.zero_locus π’œ ↑J
source
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}
source
@[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}
source
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 π’œ)) :
projective_spectrum.vanishing_ideal t βŠ” projective_spectrum.vanishing_ideal t' ≀ projective_spectrum.vanishing_ideal (t ∩ t')
source
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
source
@[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 π’œ] :
topological_space (projective_spectrum π’œ)

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
source
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 π’œ] :
Top

The underlying topology of Proj is the projective spectrum of graded ring A.

Equations
source
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 π’œ)) :
is_open U ↔ βˆƒ (s : set A), Uᢜ = projective_spectrum.zero_locus π’œ s
source
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 π’œ)) :
is_closed Z ↔ βˆƒ (s : set A), Z = projective_spectrum.zero_locus π’œ s
source
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) :
is_closed (projective_spectrum.zero_locus π’œ s)
source
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 π’œ)) :
projective_spectrum.zero_locus π’œ ↑(projective_spectrum.vanishing_ideal t) = closure t
source
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 π’œ)) :
projective_spectrum.vanishing_ideal (closure t) = projective_spectrum.vanishing_ideal t
source
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) :
topological_space.opens (projective_spectrum π’œ)

basic_open r is the open subset containing all prime ideals not containing r.

Equations
source
@[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
source
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
source
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} :
is_open ↑(projective_spectrum.basic_open π’œ a)
source
@[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})ᢜ
source
@[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 π’œ] :
projective_spectrum.basic_open π’œ 1 = ⊀
source
@[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 π’œ] :
projective_spectrum.basic_open π’œ 0 = βŠ₯
source
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) :
projective_spectrum.basic_open π’œ (f * g) = projective_spectrum.basic_open π’œ f βŠ“ projective_spectrum.basic_open π’œ g
source
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) :
projective_spectrum.basic_open π’œ (f * g) ≀ projective_spectrum.basic_open π’œ f
source
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) :
projective_spectrum.basic_open π’œ (f * g) ≀ projective_spectrum.basic_open π’œ g
source
@[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) :
projective_spectrum.basic_open π’œ (f ^ n) = projective_spectrum.basic_open π’œ f
source
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)
source
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}.

source
@[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 π’œ] :
partial_order (projective_spectrum π’œ)
Equations
source
@[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
source
@[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
source
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 π’œ) :
x ≀ y ↔ y ∈ closure {x}