AlgebraicGeometry.StructureSheaf.isUnit_to_basicOpen_self
theorem AlgebraicGeometry.StructureSheaf.isUnit_to_basicOpen_self :
∀ (R : Type u) [inst : CommRing R] (f : R),
IsUnit ((AlgebraicGeometry.StructureSheaf.toOpen R (PrimeSpectrum.basicOpen f)) f)
The theorem `AlgebraicGeometry.StructureSheaf.isUnit_to_basicOpen_self` asserts that for any commutative ring `R` and any element `f` from `R`, the element `f` is a unit in the structure sheaf of the basic open subset of the prime spectrum of `R` not containing `f`. In other words, for each `f` in a commutative ring `R`, `f` has a multiplicative inverse in the algebraic geometry structure sheaf over the open subset of prime ideals not containing `f`.
More concisely: For every commutative ring R and element f, the function field of the basic open subset of the prime spectrum of R not containing f contains the multiplicative inverse of f.
|
AlgebraicGeometry.StructureSheaf.toOpen_eq_const
theorem AlgebraicGeometry.StructureSheaf.toOpen_eq_const :
∀ (R : Type u) [inst : CommRing R] (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (f : R),
(AlgebraicGeometry.StructureSheaf.toOpen R U) f = AlgebraicGeometry.StructureSheaf.const R f 1 U ⋯
This theorem states that for any commutative ring `R`, for any open set `U` in the topological space of the prime spectrum of `R`, and for any element `f` of `R`, the operation of applying the structure sheaf of `R` to `f` over the open set `U` is equivalent to taking the constant sheaf associated to `R` with the section `f` and the trivial section 1, restricted to `U`. In other words, the structure sheaf and the constant sheaf give the same result when applied to the same element of `R` over the same open set in the prime spectrum of `R`.
More concisely: For any commutative ring `R`, any open set `U` in the prime spectrum of `R`, and any element `f` in `R`, the application of the structure sheaf of `R` to `f` over `U` is equal to the restriction of the constant sheaf associated to `R` with section `f` and trivial section 1 to `U`.
|
AlgebraicGeometry.StructureSheaf.toOpen_res
theorem AlgebraicGeometry.StructureSheaf.toOpen_res :
∀ (R : Type u) [inst : CommRing R] (U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
(i : V ⟶ U),
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen R U)
((AlgebraicGeometry.Spec.structureSheaf R).val.map i.op) =
AlgebraicGeometry.StructureSheaf.toOpen R V
The theorem `AlgebraicGeometry.StructureSheaf.toOpen_res` states that for any type `R` that is a commutative ring, and any two open subsets `U` and `V` of the prime spectrum of `R` (seen as a topological space), if there is a morphism `i` from `V` to `U`, then the composition of the morphism `toOpen` from the structure sheaf of `R` at `U` and the map induced by `i` on the structure sheaf of `R` (seen as a presheaf of commutative rings) is equal to the morphism `toOpen` from the structure sheaf of `R` at `V`. This can be interpreted as a compatibility condition between the restriction of functions to open sets and the structure sheaf on the prime spectrum, in the context of algebraic geometry.
More concisely: For any commutative ring `R`, if `i` is a morphism from an open subset `V` to another open subset `U` in the prime spectrum of `R`, then the restriction of the structure sheaf morphism `toOpen` from `U` to the composition of `i` with the structure sheaf morphism `toOpen` from `V` is the identity.
|
AlgebraicGeometry.StructureSheaf.localizationToStalk_stalkSpecializes
theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_stalkSpecializes :
∀ {R : Type u_1} [inst : CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y),
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.localizationToStalk R y)
((AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalkSpecializes h) =
CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h))
(AlgebraicGeometry.StructureSheaf.localizationToStalk R x)
The theorem `AlgebraicGeometry.StructureSheaf.localizationToStalk_stalkSpecializes` states that for a commutative ring `R` and two points `x` and `y` in the spectrum of `R` such that `x` specializes to `y`, the composition of the canonical ring homomorphism from the localization of `R` at `y` to the stalk of the structure sheaf at `y` and the natural transformation from the stalk at `y` to the stalk at `x` is equal to the composition of the ring homomorphism from the localization at `y` to the localization at `x` and the canonical ring homomorphism from the localization of `R` at `x` to the stalk of the structure sheaf at `x`. In essence, this is saying that the diagram involving the localization-to-stalk maps and the specialization-induced localizations is commutative in the category of commutative rings.
More concisely: Given a commutative ring R and points x and y in its spectrum with x specializing to y, the diagram commutes in the category of commutative rings, where the maps are given by the localization-to-stalk homomorphisms and specialization-induced localizations.
|
AlgebraicGeometry.StructureSheaf.comap_id
theorem AlgebraicGeometry.StructureSheaf.comap_id :
∀ {R : Type u} [inst : CommRing R] (U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
(hUV : U = V), AlgebraicGeometry.StructureSheaf.comap (RingHom.id R) U V ⋯ = CategoryTheory.eqToHom ⋯
This theorem states that the comap (a function that transforms the target of a function given an original function and a function on the source) of the identity is the identity. More specifically, in the context of algebraic geometry, for any commutative ring `R` and any two open subsets `U` and `V` of the prime spectrum (the set of all prime ideals) of `R`, if `U` is equal to `V`, then the comap of the identity ring homomorphism (which maps each element of the ring to itself) from `U` to `V` is equal to the morphism from `U` to `V` induced by their equality, as provided by the `CategoryTheory.eqToHom` function. This result is particularly useful when the two open subsets `U` and `V` are not definitionally equal but are proven to be equal.
More concisely: In algebraic geometry, if two open subsets of the prime spectrum of a commutative ring are equal, then the comap of the identity ring homomorphism is equal to the induced morphism between them.
|
AlgebraicGeometry.StructureSheaf.comap_id_eq_map
theorem AlgebraicGeometry.StructureSheaf.comap_id_eq_map :
∀ {R : Type u} [inst : CommRing R] (U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
(iVU : V ⟶ U),
AlgebraicGeometry.StructureSheaf.comap (RingHom.id R) U V ⋯ =
(AlgebraicGeometry.Spec.structureSheaf R).val.map iVU.op
The theorem `AlgebraicGeometry.StructureSheaf.comap_id_eq_map` states that for an arbitrary commutative ring `R` and for an inclusion `i : V ⟶ U` between open sets `U` and `V` of the prime spectrum of `R`, the comap (co-domain mapping) of the identity from the structure sheaf over `U` to the structure sheaf over `V` is equal to the corresponding restriction map of the structure sheaf. This is an extension of the principle that, for a fixed `U`, the comap of the identity from the structure sheaf over `U` to itself is the identity map. Here, `AlgebraicGeometry.StructureSheaf.comap (RingHom.id R) U V ...` represents the comap of the identity and `(AlgebraicGeometry.Spec.structureSheaf R).val.map iVU.op` represents the restriction map of the structure sheaf.
More concisely: For any commutative ring R and inclusions i : V ⟶ U between open sets of the prime spectrum of R, the comap of the identity from the structure sheaf over U to the structure sheaf over V equals the corresponding restriction map.
|
AlgebraicGeometry.StructureSheaf.const.proof_4
theorem AlgebraicGeometry.StructureSheaf.const.proof_4 :
∀ (R : Type u_1) [inst : CommRing R] (g : R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
(∀ x ∈ U, g ∈ x.asIdeal.primeCompl) → ∀ (x : ↥(Opposite.op U).unop), g ∈ (↑x).asIdeal.primeCompl
This theorem states that for any commutative ring `R` and any element `g` of `R`, if a topological space `U` is an open subset of the prime spectrum of `R` and `g` is in the complement of the prime ideal of every point of `U`, then for any point `x` in the opposite of `U`, `g` is in the complement of the prime ideal of `x`. In other words, if `g` is not in any of the prime ideals of the points of `U`, then `g` is not in the prime ideal of any point in `U` even when considering `U` in the opposite direction.
More concisely: If `g` is not in any prime ideal of points in an open subset `U` of the prime spectrum of a commutative ring `R`, then `g` is not in the prime ideal of any point in the opposite of `U`.
|