AlgebraicGeometry.localRingHom_comp_stalkIso
theorem AlgebraicGeometry.localRingHom_comp_stalkIso :
∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S),
CategoryTheory.CategoryStruct.comp
(AlgebraicGeometry.StructureSheaf.stalkIso (↑R) ((PrimeSpectrum.comap f) p)).hom
(CategoryTheory.CategoryStruct.comp
(Localization.localRingHom ((PrimeSpectrum.comap f) p).asIdeal p.asIdeal f ⋯)
(AlgebraicGeometry.StructureSheaf.stalkIso (↑S) p).inv) =
AlgebraicGeometry.PresheafedSpace.stalkMap (AlgebraicGeometry.Spec.sheafedSpaceMap f) p
This theorem states that for any two commutative rings `R` and `S` in the category of commutative rings, and a morphism `f` from `R` to `S`, and a prime spectrum `p` of the co-domain ring `S`, the composition of the isomorphism from the stalk of the structure sheaf of `R` at the point `p` preimage under `f` and the composition of the induced local ring homomorphism and the inverse of the isomorphism from the stalk of the structure sheaf of `S` at `p`, is equivalent to the stalk map of the induced map of the ring homomorphism on the ring spectra at `p`. This basically shows the compatibility of the local ring homomorphism induced by `f` with the isomorphisms from the stalks of the structure sheaves of the rings at the corresponding points.
More concisely: The isomorphism between the stalks of the structure sheaves of commutative rings at a prime spectrum point, under a morphism between the rings, equals the stalk map of the induced ring homomorphism.
|
AlgebraicGeometry.Spec_map_localization_isIso
theorem AlgebraicGeometry.Spec_map_localization_isIso :
∀ (R : CommRingCat) (M : Submonoid ↑R) (x : PrimeSpectrum (Localization M)),
CategoryTheory.IsIso
(AlgebraicGeometry.PresheafedSpace.stalkMap
(AlgebraicGeometry.Spec.toPresheafedSpace.map (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op) x)
This theorem states that for any commutative ring 'R', any of its submonoids 'M', and any point 'p' in the spectrum of the localization of 'R' at 'M' ('Spec M⁻¹R'), the stalk map of the morphism from 'Spec M⁻¹R' to 'Spec R' is an isomorphism. In algebraic geometry, the concept of 'stalk' is used to take a local view around a given point on a space. The 'stalk map' is a function associated with a continuous map between topological spaces. This result is important in the study of localization in commutative algebra and algebraic geometry, demonstrating how local properties at a point can reflect global properties of the space.
More concisely: For any commutative ring 'R', its submonoid 'M', and a point 'p' in the spectrum of 'M' inverse image of 'R', the stalk map of the morphism from the spectrum of 'M' inverse image of 'R' to 'Spec R' is an isomorphism at 'p'.
|