Module

LocalEtaleDVR.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.LocalEtaleDVR

5 declarations indexed from sourceView source ↗

Module documentation

The local rings of étale neighborhoods of a DVR

In a Noetherian local ring with principal maximal ideal (π), Krull intersection shows that every nonzero element is a unit times a power of π. If π is also a non-zero-divisor, these factorizations imply that the ring is a domain and then a DVR.

For a local, flat, essentially finite type, formally unramified algebra over a DVR, the maximal ideal is generated by the image of a base uniformizer and flatness makes that image a non-zero-divisor. This proves the DVR assertion for the local rings of pointed affine étale neighborhoods. Passing these factorizations through their localized germ maps is a separate step.

Imports7

Mathlib.Algebra.GroupWithZero.Regular
Mathlib.Algebra.Ring.Basic
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.Filtration
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.RingTheory.Localization.Submodule
Mathlib.RingTheory.Unramified.LocalRing

Imported by2

theorem

exists_unit_mul_pow_of_principal_maximalIdeal

L38 ↗

EtaleFundamentalGroups.StrictHenselian.exists_unit_mul_pow_of_principal_maximalIdeal

Documentation

Krull intersection supplies the exact power of a generator of the maximal ideal dividing any nonzero element, even before the ring is known to be a domain.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups.StrictHenselian

Lean source · statement

theorem exists_unit_mul_pow_of_principal_maximalIdeal
    {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (π : A) (hπ : maximalIdeal A = Ideal.span {π})
    (x : A) (hx : x ≠ 0) : ∃ (n : ℕ) (u : Aˣ), (u : A) * π ^ n = x

theorem

isDomain_of_principal_maximalIdeal_of_regular

L83 ↗

EtaleFundamentalGroups.StrictHenselian.isDomain_of_principal_maximalIdeal_of_regular

Documentation

A regular generator of the maximal ideal makes a Noetherian local ring an integral domain, by the unit--power factorizations just constructed.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups.StrictHenselian

Lean source · statement

theorem isDomain_of_principal_maximalIdeal_of_regular
    {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (π : A) (hπ : maximalIdeal A = Ideal.span {π}) (hreg : IsRegular π) :
    IsDomain A

theorem

localUnramifiedOverDVR_maximalIdeal

L105 ↗

EtaleFundamentalGroups.StrictHenselian.localUnramifiedOverDVR_maximalIdeal

Documentation

The image of a base uniformizer generates the maximal ideal of a local essentially finite type unramified algebra over a DVR.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups.StrictHenselian
variable (R B : Type*) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
  [CommRing B] [Algebra R B] [IsLocalRing B] [IsLocalHom (algebraMap R B)]
  [Algebra.EssFiniteType R B] [Algebra.FormallyUnramified R B] [Module.Flat R B]
omit [Module.Flat R B] in

Lean source · statement

theorem localUnramifiedOverDVR_maximalIdeal (π : R) (hπ : Irreducible π) :
    maximalIdeal B = Ideal.span {algebraMap R B π}

theorem

localUnramifiedOverDVR_isDomain

L113 ↗

EtaleFundamentalGroups.StrictHenselian.localUnramifiedOverDVR_isDomain

Documentation

A local, flat, essentially finite type, formally unramified algebra over a DVR is a domain; the uniformizer is regular by flatness.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups.StrictHenselian
variable (R B : Type*) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
  [CommRing B] [Algebra R B] [IsLocalRing B] [IsLocalHom (algebraMap R B)]
  [Algebra.EssFiniteType R B] [Algebra.FormallyUnramified R B] [Module.Flat R B]
include R in

Lean source · statement

theorem localUnramifiedOverDVR_isDomain : IsDomain B

theorem

localUnramifiedOverDVR_isDiscreteValuationRing

L128 ↗

EtaleFundamentalGroups.StrictHenselian.localUnramifiedOverDVR_isDiscreteValuationRing

Documentation

With the domain structure supplied by localUnramifiedOverDVR_isDomain, the same algebra is a DVR. This uses actual unit--power factorizations.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups.StrictHenselian
variable (R B : Type*) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
  [CommRing B] [Algebra R B] [IsLocalRing B] [IsLocalHom (algebraMap R B)]
  [Algebra.EssFiniteType R B] [Algebra.FormallyUnramified R B] [Module.Flat R B]
include R in

Lean source · statement

theorem localUnramifiedOverDVR_isDiscreteValuationRing [IsDomain B] :
    IsDiscreteValuationRing B

Module documentation

The local rings of étale neighborhoods of a DVR

Declarations

exists_unit_mul_pow_of_principal_maximalIdeal

isDomain_of_principal_maximalIdeal_of_regular

localUnramifiedOverDVR_maximalIdeal

localUnramifiedOverDVR_isDomain

localUnramifiedOverDVR_isDiscreteValuationRing