ProjectiveSpectrum.mem_zeroLocus
theorem ProjectiveSpectrum.mem_zeroLocus :
โ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
(๐ : โ โ Submodule R A) [inst_3 : GradedAlgebra ๐] (x : ProjectiveSpectrum ๐) (s : Set A),
x โ ProjectiveSpectrum.zeroLocus ๐ s โ s โ โx.asHomogeneousIdeal
The `ProjectiveSpectrum.mem_zeroLocus` theorem states that for any commutative semiring `R`, a commutative ring `A`, an `R`-algebra structure on `A`, a grading on `A` by the natural numbers, a point `x` in the projective spectrum of this graded algebra, and a set `s` of elements in `A`, `x` is in the zero locus of `s` if and only if `s` is a subset of the homogeneous ideal of `x` (that is, every element of `s` is in the homogeneous ideal of `x`). This theorem bridges the geometric concept of the zero locus (the set of all points where a given set of functions vanish) with the algebraic concept of homogeneous ideals in graded algebras.
More concisely: A point in the projective spectrum of a graded algebra belongs to the zero locus of a set of elements if and only if the set is contained in the homogeneous ideal of that point.
|
ProjectiveSpectrum.gc_homogeneousIdeal
theorem ProjectiveSpectrum.gc_homogeneousIdeal :
โ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
(๐ : โ โ Submodule R A) [inst_3 : GradedAlgebra ๐],
GaloisConnection (fun I => ProjectiveSpectrum.zeroLocus ๐ โI) fun t => ProjectiveSpectrum.vanishingIdeal t
This theorem, `ProjectiveSpectrum.gc_homogeneousIdeal`, establishes a Galois connection between the function mapping an ideal `I` to the zero locus in the projective spectrum of a graded algebra `๐`, and the function mapping a set `t` to its vanishing ideal in the same projective spectrum. Here, the graded algebra `๐` is a function from natural numbers `โ` to submodules of an algebra `A` over a commutative semiring `R`. The zero locus of an ideal is the set of all points where the functions in the ideal vanish, and the vanishing ideal of a set is the ideal of all functions that vanish on that set. A Galois connection between two functions `l` and `u` means that for all `a` and `b`, `l a` is less than or equal to `b` if and only if `a` is less than or equal to `u b`.
More concisely: The function mapping an ideal to its zero locus in the projective spectrum and the function mapping a set to its vanishing ideal form a Galois connection.
|
ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl
theorem ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl :
โ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
(๐ : โ โ Submodule R A) [inst_3 : GradedAlgebra ๐] (r : A),
โ(ProjectiveSpectrum.basicOpen ๐ r) = (ProjectiveSpectrum.zeroLocus ๐ {r})แถ
The theorem `ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl` states that for any commutative semiring `R`, any commutative ring `A`, any algebra `A` over `R`, any natural number-indexed collection `๐` of submodules of `A`, and any element `r` of `A`, the set of prime ideals not containing `r`, which is the basic open set of the projective spectrum of `๐`, is equal to the complement of the zero locus of `{r}` in the projective spectrum of `๐`. The zero locus of `{r}` is the set of all points in the projective spectrum where `r` vanishes.
More concisely: In the projective spectrum of any commutative ring `A` over a commutative semiring `R`, with a natural number-indexed collection `๐` of submodules, the set of prime ideals not containing an element `r` in `A` equals the complement of the zero locus of `{r}` in the projective spectrum of `๐`.
|
ProjectiveSpectrum.gc_set
theorem ProjectiveSpectrum.gc_set :
โ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
(๐ : โ โ Submodule R A) [inst_3 : GradedAlgebra ๐],
GaloisConnection (fun s => ProjectiveSpectrum.zeroLocus ๐ s) fun t => โ(ProjectiveSpectrum.vanishingIdeal t)
The theorem `ProjectiveSpectrum.gc_set` states that for any type `R` with commutative semiring structure, type `A` with commutative ring structure, an algebra structure on `R` and `A`, a function `๐` from natural numbers to the submodule of `R` and `A`, and a graded algebra on `๐`, the functions `ProjectiveSpectrum.zeroLocus ๐` and `fun t => โ(ProjectiveSpectrum.vanishingIdeal t)` form a Galois connection. In other words, for any set `s` and target `t`, `ProjectiveSpectrum.zeroLocus ๐ s` is less than or equal to `t` if and only if `s` is less than or equal to `ProjectiveSpectrum.vanishingIdeal t`. This relationship is commonly encountered in the study of projective spectrums in algebraic geometry.
More concisely: The theorem `ProjectiveSpectrum.gc_set` asserts that the mappings `ProjectiveSpectrum.zeroLocus` and `ProjectiveSpectrum.vanishingIdeal` form a Galois connection on subsets of natural numbers with respect to a given type `R` with commutative semiring structure, type `A` with commutative ring structure, an algebra structure on `R` and `A`, a function `๐` from natural numbers to the submodules of `R` and `A`, and a graded algebra on `๐`.
|
ProjectiveSpectrum.gc_ideal
theorem ProjectiveSpectrum.gc_ideal :
โ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
(๐ : โ โ Submodule R A) [inst_3 : GradedAlgebra ๐],
GaloisConnection (fun I => ProjectiveSpectrum.zeroLocus ๐ โI) fun t =>
(ProjectiveSpectrum.vanishingIdeal t).toIdeal
The theorem `ProjectiveSpectrum.gc_ideal` states that for any commutative semiring `R`, commutative ring `A`, and an algebra `A` over `R`, given a function `๐` that maps natural numbers to submodules of `A` over `R` (under the condition that `๐` forms a `GradedAlgebra`), the functions `zeroLocus` and `vanishingIdeal` form a Galois connection. In this context, `zeroLocus` takes a homogeneous ideal and produces its zero locus in the projective spectrum, and `vanishingIdeal` takes a subset of the projective spectrum and produces the homogeneous ideal of functions that vanish on it. The Galois connection property ensures a specific kind of correspondence between the set of homogeneous ideals and the subsets of the projective spectrum: for a homogeneous ideal `I` and a subset `t` of the projective spectrum, the zero locus of `I` is contained in `t` if and only if `I` is contained in the vanishing ideal of `t`.
More concisely: The `ProjectiveSpectrum.gc_ideal` theorem in Lean 4 states that the functions `zeroLocus` and `vanishingIdeal` form a Galois connection between graded submodules of a commutative ring `A` over a commutative semiring `R` and subsets of the projective spectrum of `A`, such that the zero locus of a homogeneous ideal is contained in a subset if and only if the ideal is contained in the vanishing ideal of the subset.
|
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology._auxLemma.1
theorem Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology._auxLemma.1 :
โ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
(๐ : โ โ Submodule R A) [inst_3 : GradedAlgebra ๐] (x : ProjectiveSpectrum ๐) (s : Set A),
(x โ ProjectiveSpectrum.zeroLocus ๐ s) = (s โ โx.asHomogeneousIdeal)
The theorem `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology._auxLemma.1` states that for any commutative semiring `R`, commutative ring `A`, and an algebra structure `A` over `R`, for a graded algebra structure `๐` : โ โ Submodule R A, each point `x` in the Projective Spectrum of `๐`, and a set `s` of `A`, the point `x` belongs to the zero locus of `๐` over `s` if and only if the set `s` is a subset of the inverse image of `x` under the map to the homogeneous ideal. In other words, the theorem establishes a correspondence between the zero locus of a set in the projective spectrum and the containment of the set in the homogeneous ideal associated with a point in the projective spectrum.
More concisely: For any commutative semiring `R`, commutative ring `A` with an algebra structure over `R`, graded algebra structure `๐` : โ โ Submodule R A, point `x` in the Projective Spectrum of `๐`, and set `s` in `A`, `x` lies in the zero locus of `๐` over `s` if and only if `s` is a subset of the inverse image of `x` under the map to the homogeneous ideal.
|