ModuleGeometricStalkDVR.lean
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkDVR
3 declarations indexed from sourceView source ↗ Module documentation
The actual geometric étale stalk of a DVR is a DVR
Represent a nonzero germ on an affine étale neighborhood and localize its sections at the prime selected by the geometric point. The resulting ring is Noetherian, and unramifiedness identifies its maximal ideal with the ideal generated by the base uniformizer. Krull intersection on that actual local ring gives a unit times a power of the uniformizer. The localized germ map transfers this factorization to the geometric stalk.
The domain property comes from the general normal-domain geometric-stalk theorem. The unit--power factorizations identify its maximal ideal and give the DVR structure. This argument does not presume Noetherianity of a filtered colimit or the general theorem that every regular local ring is a domain.
Declarations
EtaleFundamentalGroups.StrictHenselian.geometricStalk_exists_unit_mul_uniformizer_pow
DocumentationEvery nonzero germ is a unit times a power of the image of any chosen base uniformizer. The factorization is constructed on a localized affine étale neighborhood.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
[Field Ω] [IsSepClosed Ω] (φ : R →+* Ω) [IsLocalHom φ]
EtaleFundamentalGroups.StrictHenselian.geometricStalk_maximalIdeal_eq_span_uniformizer
DocumentationA base uniformizer generates the maximal ideal of the actual geometric étale stalk.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
[Field Ω] [IsSepClosed Ω] (φ : R →+* Ω) [IsLocalHom φ]
EtaleFundamentalGroups.StrictHenselian.geometricStalk_isDiscreteValuationRing
DocumentationThe actual geometric étale stalk over a closed geometric point of a DVR is itself a DVR.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
[Field Ω] [IsSepClosed Ω] (φ : R →+* Ω) [IsLocalHom φ]