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 #

@[nolint]
def 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.

Equations
Instances for projective_spectrum
@[reducible]
def projective_spectrum.as_homogeneous_ideal {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 π’œ) :

A method to view a point in the projective spectrum of a graded ring as a homogeneous ideal of that ring.

theorem projective_spectrum.as_homogeneous_ideal_def {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 π’œ) :
@[protected, instance]
def projective_spectrum.is_prime {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 π’œ) :
@[ext]
theorem projective_spectrum.ext {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 π’œ} :
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
@[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) :
@[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 prime spectrum of a commutative ring R is the intersection of all the 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
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 π’œ)) :
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) :
@[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.gc_ideal {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :

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

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 π’œ] :
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.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 π’œ] :
@[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_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.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)) :
projective_spectrum.zero_locus π’œ (⋃ (s' : set A) (H : s' ∈ s), s') = β‹‚ (s' : set A) (H : s' ∈ s), projective_spectrum.zero_locus π’œ s'
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_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) :
@[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) :
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 π’œ} :
@[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 π’œ)) :
is_closed Z ↔ βˆƒ (s : set A), Z = projective_spectrum.zero_locus π’œ s
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) :
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
@[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 π’œ) :
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 π’œ) :
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) :
@[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) :
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 π’œ] :

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 π’œ] :
Equations
@[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 π’œ) :
@[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 π’œ) :
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 π’œ) :