PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal
theorem PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal :
∀ {R : Type u} [inst : CommSemiring R] (t : Set (PrimeSpectrum R)) (I : Ideal R),
t ⊆ PrimeSpectrum.zeroLocus ↑I ↔ I ≤ PrimeSpectrum.vanishingIdeal t
This theorem states that for any given commutative semiring `R`, a set `t` of its prime spectrum, and an ideal `I` of `R`, the set `t` is a subset of the zero locus of `I` if and only if `I` is less than or equal to the vanishing ideal of `t`. Here, `PrimeSpectrum.zeroLocus` refers to the set of points in the prime spectrum where a given ideal vanishes and `PrimeSpectrum.vanishingIdeal` is the ideal associated with a set in the prime spectrum. The symbols `⊆` and `≤` denote subset and less than or equal to, respectively. This theorem is essentially describing a relationship between the algebraic and geometric notions in terms of ideals and the prime spectrum of a ring.
More concisely: For any commutative semiring R, set t of its prime spectrum, and ideal I, t is a subset of the zero locus of I if and only if I is less than or equal to the vanishing ideal of t.
|
PrimeSpectrum.zeroLocus_iUnion
theorem PrimeSpectrum.zeroLocus_iUnion :
∀ {R : Type u} [inst : CommSemiring R] {ι : Sort u_1} (s : ι → Set R),
PrimeSpectrum.zeroLocus (⋃ i, s i) = ⋂ i, PrimeSpectrum.zeroLocus (s i)
The theorem `PrimeSpectrum.zeroLocus_iUnion` states that for any commutative semiring `R` and any indexed collection of sets `s` of type `R` (indexed by some index type `ι`), the zero locus of the union of these sets is equal to the intersection of their zero loci. In mathematical terms, it says that for all indexed families of sets $(s_i)_{i\in\mathcal{I}}$, we have that the zero locus of the union (i.e., $\bigcup_{i\in\mathcal{I}} s_i$) equals the intersection of their zero loci (i.e., $\bigcap_{i\in\mathcal{I}} \text{ZeroLocus}(s_i)$). This theorem essentially encapsulates the property that the zero locus commutes with indexed unions.
More concisely: For any commutative semiring `R` and indexed collection `(s_i)` of sets over `R` (indexed by `ι`), the zero locus of their union equals the intersection of their zero loci: `ZeroLocus(⋃i∈I si) = ∩i∈I ZeroLocus(si)`.
|
PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical
theorem PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical :
∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R),
PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑I) = I.radical
The theorem `PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical` states that for any commutative semiring `R` and any ideal `I` of `R`, the vanishing ideal of the zero locus of `I` is equal to the radical of `I`. In other words, the ideals consisting of all elements that vanish on the set of prime ideals where `I` becomes zero, is the same as the ideal formed by those elements in `I` whose some power belongs to `I`.
More concisely: The theorem asserts that for any commutative semiring `R` and ideal `I`, the vanishing ideal of `I`'s zero locus equals the radical of `I`.
|
PrimeSpectrum.isClosed_iff_zeroLocus
theorem PrimeSpectrum.isClosed_iff_zeroLocus :
∀ {R : Type u} [inst : CommSemiring R] (Z : Set (PrimeSpectrum R)),
IsClosed Z ↔ ∃ s, Z = PrimeSpectrum.zeroLocus s
This theorem states that for any type `R` that is a commutative semiring, and any set `Z` of prime spectrums of `R`, `Z` is closed if and only if there exists some `s` such that `Z` is equal to the zero locus of `s` in the prime spectrum of `R`. In terms of algebraic geometry, it relates the topological property of being closed with the algebraic property of being the set of prime ideals that contain a given subset of the ring.
More concisely: For a commutative semiring `R` and a set `Z` of its prime spectrum, `Z` is closed if and only if it is the zero locus of some element in the prime spectrum of `R`.
|
PrimeSpectrum.gc
theorem PrimeSpectrum.gc :
∀ (R : Type u) [inst : CommSemiring R],
GaloisConnection (fun I => PrimeSpectrum.zeroLocus ↑I) fun t => PrimeSpectrum.vanishingIdeal t
The theorem `PrimeSpectrum.gc` states that for any commutative semiring `R`, the functions `zeroLocus` and `vanishingIdeal` form a Galois connection. Here, the `zeroLocus` function takes as input an ideal `I` of the ring `R` and returns the set of all prime ideals of `R` where `I` vanishes. The `vanishingIdeal` function takes as input a set `t` of prime ideals of `R` and returns the ideal of `R` that vanishes exactly on `t`. The Galois connection between these two functions means that for any ideal `I` and any set of prime ideals `t`, `I` vanishes on `t` if and only if `t` is contained in the zero locus of `I`.
More concisely: For any commutative semiring R, the functions zeroLocus and vanishingIdeal form a Galois connection, where zeroLocus(I) is the set of prime ideals where I vanishes, and vanishingIdeal(t) is the ideal that vanishes exactly on t, such that I is contained in the vanishing ideal of t if and only if t is contained in the zero locus of I.
|
PrimeSpectrum.isClosed_zeroLocus
theorem PrimeSpectrum.isClosed_zeroLocus :
∀ {R : Type u} [inst : CommSemiring R] (s : Set R), IsClosed (PrimeSpectrum.zeroLocus s)
This theorem states that for any set `s` of elements from a commutative semiring `R`, the zero locus of `s` in the prime spectrum of `R` is a closed set. Here, the zero locus of a set in the prime spectrum is the set of all prime ideals in which all elements of the set become zero when mapped under the ring homomorphism. The notion of "closed" is in the sense of the Zariski topology, a topology commonly used in algebraic geometry.
More concisely: The zero locus of any set in the prime spectrum of a commutative semiring is a closed set under the Zariski topology.
|
PrimeSpectrum.mem_vanishingIdeal
theorem PrimeSpectrum.mem_vanishingIdeal :
∀ {R : Type u} [inst : CommSemiring R] (t : Set (PrimeSpectrum R)) (f : R),
f ∈ PrimeSpectrum.vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asIdeal
This theorem states that for any commutative semiring `R`, a set `t` of prime spectra of `R`, and an element `f` of `R`, `f` is a member of the vanishing ideal of `t` if and only if for every prime spectrum `x` in `t`, `f` is an element of the ideal associated with `x`. In simpler terms, it provides a criterion for an element to belong to the vanishing ideal of a set of prime spectra: it must belong to the ideal of each prime spectrum in the set.
More concisely: For any commutative semiring R, an element f of R belongs to the vanishing ideal of a set T of its prime spectra if and only if it is contained in the ideal associated with each prime spectrum x in T.
|
Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic._auxLemma.31
theorem Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic._auxLemma.31 :
∀ {α : Type u} {a : α} {s : Set α}, ({a} ⊆ s) = (a ∈ s)
This theorem states that for any type 'α', any element 'a' of that type, and any set 's' of elements of type 'α', the single-element set containing 'a' is a subset of 's' if and only if 'a' is an element of 's'. Essentially, this is saying that a set is a subset of another set if its elements are also elements of the other set.
More concisely: For any type 'α' and any set 's' of elements from 'α', the set containing only one element 'a' of 'α' is a subset of 's' if and only if 'a' is an element of 's'.
|
PrimeSpectrum.vanishingIdeal_closure
theorem PrimeSpectrum.vanishingIdeal_closure :
∀ {R : Type u} [inst : CommSemiring R] (t : Set (PrimeSpectrum R)),
PrimeSpectrum.vanishingIdeal (closure t) = PrimeSpectrum.vanishingIdeal t
This theorem states that for any commutative semiring 'R' and any set 't' of elements from the prime spectrum of 'R', the vanishing ideal of the closure of 't' is equal to the vanishing ideal of 't' itself. In simpler terms, the set of all prime ideals that vanish on the closure of 't' is the same as the set of all prime ideals that vanish on 't'. This result connects important concepts in commutative algebra and topology, specifically the notions of closure and vanishing ideals in the context of prime spectrums.
More concisely: For any commutative semiring 'R' and subset 't' of its prime spectrum, the vanishing ideal of the closure of 't' equals the vanishing ideal of 't'.
|
PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical
theorem PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical :
∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R),
I.IsRadical → (IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ I.IsPrime)
This theorem states that for any set `R` of commutative semiring structure, and any ideal `I` in `R`, if `I` is a radical ideal, then the set of all prime ideal points where `I` becomes zero, denoted as `PrimeSpectrum.zeroLocus ↑I`, is irreducible if and only if `I` is a prime ideal. In other words, it establishes a correspondence between the irreducibility of the zero locus of a radical ideal in the prime spectrum and the primality of the ideal itself.
More concisely: For any commutative semiring `R` and radical ideal `I` in `R`, the zero locus of `I` in the prime spectrum is irreducible if and only if `I` is a prime ideal.
|
PrimeSpectrum.isOpen_basicOpen
theorem PrimeSpectrum.isOpen_basicOpen :
∀ {R : Type u} [inst : CommSemiring R] {a : R}, IsOpen ↑(PrimeSpectrum.basicOpen a)
This theorem states that for any given type `R` that is a commutative semiring, and any element `a` from `R`, the set generated by the function `PrimeSpectrum.basicOpen a` is an open set in the topological space of the prime spectrum of `R`. In other words, the basic open set containing all prime ideals of `R` that do not contain the element `a` is an open set in the topology of the prime spectrum of `R`.
More concisely: For any commutative semiring `R` and element `a` in `R`, the set of prime ideals not containing `a` forms an open set in the prime spectrum of `R`.
|
PrimeSpectrum.le_iff_specializes
theorem PrimeSpectrum.le_iff_specializes :
∀ {R : Type u} [inst : CommSemiring R] (x y : PrimeSpectrum R), x ≤ y ↔ x ⤳ y
This theorem states that for any commutative semiring `R` and any two elements `x` and `y` in the prime spectrum of `R`, `x` is less than or equal to `y` if and only if `x` specializes to `y`. The specialization relation, denoted `x ⤳ y`, is a binary relation often used in the theory of topological spaces, and specifically in the Zariski topology of the prime spectrum of a ring. In this context, it denotes that the prime ideal `x` is contained in the prime ideal `y` or, equivalently, that `y` is a generalization of `x`.
More concisely: In the prime spectrum of a commutative semiring, two elements are order-isomorphic, i.e., one is a specialization of the other, if and only if one is contained in the other as prime ideals.
|
PrimeSpectrum.vanishingIdeal_anti_mono_iff
theorem PrimeSpectrum.vanishingIdeal_anti_mono_iff :
∀ {R : Type u} [inst : CommSemiring R] {s t : Set (PrimeSpectrum R)},
IsClosed t → (s ⊆ t ↔ PrimeSpectrum.vanishingIdeal t ≤ PrimeSpectrum.vanishingIdeal s)
The theorem `PrimeSpectrum.vanishingIdeal_anti_mono_iff` states that for any type `R` with a commutative semiring structure and any two sets `s` and `t` of prime spectrums of `R`, if `t` is a closed set, then `s` is a subset of `t` if and only if the vanishing ideal of `t` is less than or equal to the vanishing ideal of `s`. Here, "less than or equal to" refers to the subset relation in the lattice structure of ideals in the ring, and the "prime spectrum" of a ring is the set of all prime ideals of the ring. The "vanishing ideal" of a set of prime ideals is the intersection of those ideals.
More concisely: A set of prime ideals in a commutative semiring is a subset of another if and only if the vanishing ideal of the second set is less than or equal to the vanishing ideal of the first.
|
PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
theorem PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure :
∀ {R : Type u} [inst : CommSemiring R] (t : Set (PrimeSpectrum R)),
PrimeSpectrum.zeroLocus ↑(PrimeSpectrum.vanishingIdeal t) = closure t
This theorem states that for any commutative semiring `R` and any set `t` of its prime spectrum, the zero locus of the vanishing ideal of `t` is equal to the closure of `t`. In other words, the set of all points where the functions given by the vanishing ideal of `t` vanish is exactly the closure of `t` itself. Here, the closure of a set is defined as the smallest closed set containing it, and the vanishing ideal of a set in the prime spectrum is the set of all ring elements that vanish on that set.
More concisely: The zero locus of a set of points in the prime spectrum of a commutative semiring equals the closure of that set, where the zero locus is the set of points where the vanishing ideal vanishes.
|
PrimeSpectrum.mem_zeroLocus
theorem PrimeSpectrum.mem_zeroLocus :
∀ {R : Type u} [inst : CommSemiring R] (x : PrimeSpectrum R) (s : Set R),
x ∈ PrimeSpectrum.zeroLocus s ↔ s ⊆ ↑x.asIdeal
This theorem states that for a given type `R` that is a commutative semiring, a point `x` in the prime spectrum of `R`, and a set `s` of `R`, `x` is in the zero locus of `s` if and only if `s` is a subset of the elements of `x` interpreted as an ideal. In the context of algebraic geometry, this is saying that a point on a scheme is in the zero locus of a set of functions if and only if those functions vanish on the corresponding prime ideal.
More concisely: A point in the prime spectrum of a commutative semiring is in the zero locus of a subset if and only if the subset is contained in the ideal generated by that point.
|
PrimeSpectrum.isClosed_singleton_iff_isMaximal
theorem PrimeSpectrum.isClosed_singleton_iff_isMaximal :
∀ {R : Type u} [inst : CommSemiring R] (x : PrimeSpectrum R), IsClosed {x} ↔ x.asIdeal.IsMaximal
This theorem states that for any given ring `R`, which is a commutative semiring, and a point `x` in the prime spectrum of `R`, the set containing only `x` is closed if and only if `x` is a maximal ideal in the ring `R`. In other words, the closure of a single point in the prime spectrum of a ring corresponds to maximal ideals of the ring.
More concisely: A point in the prime spectrum of a commutative semiring is a closed set if and only if it is a maximal ideal.
|
PrimeSpectrum.ext
theorem PrimeSpectrum.ext :
∀ {R : Type u} {inst : CommSemiring R} (x y : PrimeSpectrum R), x.asIdeal = y.asIdeal → x = y
This theorem states that for any commutative semiring `R`, if two elements `x` and `y` of the prime spectrum of `R` have equivalent ideals (i.e., `x.asIdeal = y.asIdeal`), then `x` and `y` are the same element. In other words, in the context of a commutative semiring, the prime spectrum mapping is injective with respect to the ideals of the elements.
More concisely: In a commutative semiring, two elements have equal prime spectra if and only if they are equal as elements.
|
PrimeSpectrum.basicOpen_eq_zeroLocus_compl
theorem PrimeSpectrum.basicOpen_eq_zeroLocus_compl :
∀ {R : Type u} [inst : CommSemiring R] (r : R), ↑(PrimeSpectrum.basicOpen r) = (PrimeSpectrum.zeroLocus {r})ᶜ := by
sorry
This theorem states that for any commutative semiring `R` and any element `r` of `R`, the set of all prime ideals that do not contain `r` (denoted as `PrimeSpectrum.basicOpen r`) is equal to the complement of the set of all prime ideals that annihilate `r` (denoted as `PrimeSpectrum.zeroLocus {r}`). In mathematical terms, the open subset of the prime spectrum consisting of ideals excluding `r` is the same as the set of ideals that do not annihilate `r`.
More concisely: The set of prime ideals not containing an element `r` in a commutative semiring `R` equals the complement of the set of prime ideals annihilating `r`.
|
Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic._auxLemma.2
theorem Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic._auxLemma.2 :
∀ {R : Type u} [inst : CommSemiring R] (x : PrimeSpectrum R) (s : Set R),
(x ∈ PrimeSpectrum.zeroLocus s) = (s ⊆ ↑x.asIdeal)
The theorem, `Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic._auxLemma.2`, states that for any commutative semiring `R`, given a prime spectrum `x` of `R` and a set `s` of elements of `R`, `x` is in the zero locus of `s` if and only if `s` is a subset of the ideal associated with `x`. In other words, a prime spectrum `x` is among the zero points of all the elements in `s` exactly when every element of `s` belongs to the ideal represented by `x`.
More concisely: A prime spectrum is in the zero locus of a set of elements if and only if that set is contained in the ideal represented by the spectrum.
|
PrimeSpectrum.zeroLocus_radical
theorem PrimeSpectrum.zeroLocus_radical :
∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R),
PrimeSpectrum.zeroLocus ↑I.radical = PrimeSpectrum.zeroLocus ↑I
This theorem states that for any ideal `I` in a commutative semiring `R`, the set of points in the prime spectrum where the radical of `I` vanishes (denoted by `PrimeSpectrum.zeroLocus ↑(Ideal.radical I)`) is equal to the set of points in the prime spectrum where `I` itself vanishes (denoted by `PrimeSpectrum.zeroLocus ↑I`). In other words, the zero locus of the radical of an ideal is the same as the zero locus of the ideal itself.
More concisely: The zero locus of an ideal and its radical in the prime spectrum of a commutative semiring are equal.
|
PrimeSpectrum.zeroLocus_empty_of_one_mem
theorem PrimeSpectrum.zeroLocus_empty_of_one_mem :
∀ {R : Type u} [inst : CommSemiring R] {s : Set R}, 1 ∈ s → PrimeSpectrum.zeroLocus s = ∅
The theorem `PrimeSpectrum.zeroLocus_empty_of_one_mem` states that for any type `R` that has the structure of a commutative semiring, and any set `s` of elements of `R`, if the number 1 is an element of `s`, then the zero locus of `s` in the prime spectrum is empty. In other words, there are no prime ideals of `R` that vanish on all elements of `s` when 1 is included in `s`.
More concisely: If `R` is a commutative semiring and `s` is a non-empty subset of `R` containing 1, then the zero locus of `s` in the prime spectrum of `R` is empty.
|
Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic._auxLemma.29
theorem Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic._auxLemma.29 :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {x : B}, (x ∈ ↑p) = (x ∈ p)
This theorem, under the namespace `Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic._auxLemma.29`, states that for any two types `A` and `B`, given a `SetLike` instance `i` between `A` and `B`, and for any element `p` of type `A` and `x` of type `B`, the proposition that `x` is in the coersion of `p` to a set (notated as `x ∈ ↑p`) is equivalent to the proposition that `x` is in `p` (notated as `x ∈ p`). Essentially, this theorem asserts that the membership of an element in a set remains unchanged even under coersion.
More concisely: For any `SetLike` instances `i` between types `A` and `B`, and for all `p` in `A` and `x` in `B`, `x ∈ ↑p` if and only if `x ∈ p`.
|
PrimeSpectrum.gc_set
theorem PrimeSpectrum.gc_set :
∀ (R : Type u) [inst : CommSemiring R],
GaloisConnection (fun s => PrimeSpectrum.zeroLocus s) fun t => ↑(PrimeSpectrum.vanishingIdeal t)
The theorem `PrimeSpectrum.gc_set` states that for any commutative semiring `R`, the functions `PrimeSpectrum.zeroLocus` and the coercion of `PrimeSpectrum.vanishingIdeal` form a Galois connection. In other words, for every set `s` and every topological space `t` in the prime spectrum of `R`, `PrimeSpectrum.zeroLocus s` is less than or equal to `t` if and only if `s` is less than or equal to the vanishing ideal of `t`.
More concisely: The functions `PrimeSpectrum.zeroLocus` and the coercion of `PrimeSpectrum.vanishingIdeal` form a Galois connection in the prime spectrum of any commutative semiring `R`. That is, for all sets `s` and topological spaces `t`, `PrimeSpectrum.zeroLocus s ⇐ t` if and only if `s ⊆ vanishingIdeal t`.
|
PrimeSpectrum.zeroLocus_span
theorem PrimeSpectrum.zeroLocus_span :
∀ {R : Type u} [inst : CommSemiring R] (s : Set R),
PrimeSpectrum.zeroLocus ↑(Ideal.span s) = PrimeSpectrum.zeroLocus s
This theorem, named `PrimeSpectrum.zeroLocus_span`, states that for any type `R` which is a commutative semiring and any set `s` of type `R`, the zero locus of the ideal generated by `s` is equal to the zero locus of `s` itself. In mathematical terms, if we think of `s` as a subset of a ring `R`, the set of all prime ideals that contain the ideal generated by `s` is exactly the same as the set of all prime ideals that contain `s`. The `zeroLocus` function maps a set to the set of prime ideals of the ring that contain all elements of the given set. The theorem thus relates the properties of an ideal and the subset of the ring which generates it in terms of the prime spectrum of the ring.
More concisely: For any commutative semiring R and set s of R, the ideal generated by s and the set s have equal zero locus in the prime spectrum of R.
|
PrimeSpectrum.vanishingIdeal_singleton
theorem PrimeSpectrum.vanishingIdeal_singleton :
∀ {R : Type u} [inst : CommSemiring R] (x : PrimeSpectrum R), PrimeSpectrum.vanishingIdeal {x} = x.asIdeal := by
sorry
This theorem, named "PrimeSpectrum.vanishingIdeal_singleton", states that for any given type `R` which is a commutative semiring, and for any 'x' in the prime spectrum of `R`, the vanishing ideal of the set containing only 'x' is equal to the ideal generated by 'x'. In other words, the ideal of all elements in `R` that vanish on the singleton set `{x}` is just the ideal defined by `x` itself.
More concisely: For any commutative semiring `R` and its prime spectrum element `x`, the vanishing ideal of the singleton set `{x}` equals the ideal generated by `x`.
|