ModuleDimensionOne.lean
Nyll.EtaleFundamentalGroups.Purity.Local.DimensionOne
3 declarations indexed from sourceView source ↗ Module documentation
Dimension-one local purity over a DVR
At every height-one point of the regular base used in the absolute Abhyankar argument, the local ring is a DVR. A finite torsion-free algebra over that DVR is finite free, hence flat. If the algebra is local, unramifiedness at its closed point therefore makes the morphism etale at that point. The etale locus is open and stable under generalization, while every prime of a local ring lies below its closed point, so the whole finite algebra is etale.
This is the dimension-one input to the higher-dimensional local-purity step; it does not assume flatness or etaleness separately.
Imports4
- Mathlib.RingTheory.DiscreteValuationRing.Basic
- Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
- Mathlib.RingTheory.Flat.TorsionFree
- Mathlib.RingTheory.Smooth.Fiber
Imported by6
Declarations
EtaleFundamentalGroups.etale_of_dedekind_of_finite_torsionFree_of_isUnramifiedAt_all_maximalIdeals
DocumentationDimension-one purity over a Dedekind domain: a finite torsion-free algebra that is unramified at every maximal ideal is finite etale.
Torsion-freeness produces flatness over the Dedekind base. At each prime of the target, choose a maximal ideal above it. Unramifiedness at that maximal ideal and flatness give etaleness there, and stability under generalization then gives etaleness at the original prime.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
universe u v
EtaleFundamentalGroups.etale_of_dvr_of_finite_torsionFree_of_isUnramifiedAt_all_maximalIdeals
DocumentationDimension-one purity over a DVR: a finite torsion-free algebra that is unramified at every maximal ideal is finite etale.
This formulation directly consumes the all-maximal-ideals output of the DVR Abhyankar theorem. Finite torsion-freeness over the PID underlying the DVR produces flatness; openness and generalization-stability of the etale locus then propagate etaleness from the maximal points to every prime.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
universe u v
EtaleFundamentalGroups.etale_of_dvr_of_finite_torsionFree_of_isUnramifiedAt_maximalIdeal
DocumentationDimension-one local purity: a finite torsion-free local algebra over a DVR that is unramified at its closed point is finite etale.
The torsion-free hypothesis is supplied by the normalization sitting inside its fraction field. Flatness is produced in the proof from finite torsion-freeness over the PID underlying the DVR.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
universe u v