Module

Regularity.lean

Nyll.EtaleFundamentalGroups.Kummer.RootCovers.Local.Regularity

9 declarations indexed from sourceView source ↗

Module documentation

Regularity of a local Kummer root cover

This file proves the regular-local part of the one-step Kummer root construction. The key dimension input is produced here from going-up: a faithfully integral extension cannot decrease Krull dimension.

For B = R[X] / (X ^ n - a), if a :: rs is a regular sequence generating the maximal ideal of R, then the maximal ideal of B is generated by the adjoined root followed by the images of rs. This generating family has the same length as the dimension of R; going-up supplies the required lower bound on the dimension of B, so B is regular local.

Imports3

Nyll.EtaleFundamentalGroups.Kummer.RootCovers.Local.Basic
Mathlib.RingTheory.KrullDimension.Regular
Mathlib.RingTheory.RegularLocalRing.Defs

Imported by4

theorem

exists_lift_ltSeries

L36 ↗

EtaleFundamentalGroups.Kummer.IntegralDimension.exists_lift_ltSeries

Source context 6 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
noncomputable section
namespace IntegralDimension

Lean source · statement

theorem exists_lift_ltSeries
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Nontrivial R] [Algebra R S] [Algebra.IsIntegral R S] [FaithfulSMul R S]
    (p : LTSeries (PrimeSpectrum R)) :
    ∃ q : LTSeries (PrimeSpectrum S),
      q.length = p.length ∧
        q.last.asIdeal.comap (algebraMap R S) = p.last.asIdeal

theorem

ringKrullDim_le_of_faithfully_integral

L79 ↗

EtaleFundamentalGroups.Kummer.IntegralDimension.ringKrullDim_le_of_faithfully_integral

Documentation

A faithfully integral extension cannot decrease Krull dimension.

Source context 6 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
noncomputable section
namespace IntegralDimension

Lean source · statement

theorem ringKrullDim_le_of_faithfully_integral
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Nontrivial R] [Algebra R S] [Algebra.IsIntegral R S] [FaithfulSMul R S] :
    ringKrullDim R ≤ ringKrullDim S

def

localRootCoverParameterList

L96 ↗

EtaleFundamentalGroups.Kummer.localRootCoverParameterList

Documentation

The parameter list on the root cover: the new root replaces a.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
noncomputable section

Lean source · statement

def localRootCoverParameterList
    (R : Type u) [CommRing R] (n : ℕ) (a : R) (rs : List R) :
    List (AdjoinRoot (X ^ n - C a))

theorem

localRootCoverParameterList_length

L103 ↗

EtaleFundamentalGroups.Kummer.localRootCoverParameterList_length

Source context 5 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
noncomputable section

Lean source · statement

theorem localRootCoverParameterList_length
    (R : Type u) [CommRing R] (n : ℕ) (a : R) (rs : List R) :
    (localRootCoverParameterList R n a rs).length = (a :: rs).length

theorem

ideal_ofList_localRootCoverParameterList_eq_maximalIdeal

L112 ↗

EtaleFundamentalGroups.Kummer.ideal_ofList_localRootCoverParameterList_eq_maximalIdeal

Documentation

If a :: rs generates the maximal ideal of R, then the root followed by the images of rs generates the maximal ideal of the local root cover.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
noncomputable section

Lean source · full declaration

theorem ideal_ofList_localRootCoverParameterList_eq_maximalIdeal
    {R : Type u} [CommRing R] [IsLocalRing R] {n : ℕ} (hn : 0 < n)
    {a : R} {rs : List R}
    (hgen : Ideal.ofList (a :: rs) = maximalIdeal R) :
    letI : IsLocalRing (AdjoinRoot (X ^ n - C a)) :=
      isLocalRing_adjoinRoot_X_pow_sub_C hn (by
        rw [← hgen, Ideal.ofList_cons]
        exact (show Ideal.span {a} ≤ Ideal.span {a} ⊔ Ideal.ofList rs from le_sup_left)
          (Ideal.mem_span_singleton_self a))
    Ideal.ofList (localRootCoverParameterList R n a rs) =
      maximalIdeal (AdjoinRoot (X ^ n - C a)) := by
  let f : R[X] := X ^ n - C a
  let B := AdjoinRoot f
  have ha : a ∈ maximalIdeal R := by
    rw [← hgen, Ideal.ofList_cons]
    exact (show Ideal.span {a} ≤ Ideal.span {a} ⊔ Ideal.ofList rs from le_sup_left)
      (Ideal.mem_span_singleton_self a)
  let : IsLocalRing B := isLocalRing_adjoinRoot_X_pow_sub_C hn ha
  rw [maximalIdeal_adjoinRoot_X_pow_sub_C hn ha]
  apply le_antisymm
  · rw [localRootCoverParameterList, Ideal.ofList_cons]
    apply sup_le
    · exact le_sup_right
    · refine le_trans ?_ le_sup_left
      rw [← Ideal.map_ofList]
      apply Ideal.map_mono
      rw [← hgen, Ideal.ofList_cons]
      exact le_sup_right
  · apply sup_le
    · rw [← hgen, Ideal.map_ofList, List.map_cons, Ideal.ofList_cons]
      apply sup_le
      · rw [Ideal.span_le]
        rintro x (rfl : x = AdjoinRoot.of f a)
        rw [← adjoinRoot_root_pow n a]
        exact Ideal.pow_mem_of_mem _ (by
          rw [localRootCoverParameterList, Ideal.ofList_cons]
          exact (show Ideal.span {AdjoinRoot.root (X ^ n - C a)} ≤
              Ideal.span {AdjoinRoot.root (X ^ n - C a)} ⊔
                Ideal.ofList (rs.map (AdjoinRoot.of (X ^ n - C a))) from le_sup_left)
            (Ideal.mem_span_singleton_self _)) n hn
      · rw [localRootCoverParameterList, Ideal.ofList_cons]
        exact le_sup_right
    · rw [localRootCoverParameterList, Ideal.ofList_cons]
      exact le_sup_left

theorem

spanFinrank_ofList_le_length

L157 ↗

EtaleFundamentalGroups.Kummer.spanFinrank_ofList_le_length

Source context 5 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
noncomputable section

Lean source · statement

theorem spanFinrank_ofList_le_length
    {R : Type u} [CommRing R] (l : List R) :
    (Ideal.ofList l).spanFinrank ≤ l.length

theorem

parameter_length_eq_ringKrullDim

L166 ↗

EtaleFundamentalGroups.Kummer.parameter_length_eq_ringKrullDim

Source context 5 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
noncomputable section

Lean source · statement

theorem parameter_length_eq_ringKrullDim
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {a : R} {rs : List R}
    (hreg : RingTheory.Sequence.IsRegular R (a :: rs))
    (hgen : Ideal.ofList (a :: rs) = maximalIdeal R) :
    ((a :: rs).length : WithBot ℕ∞) = ringKrullDim R

theorem

isRegularLocalRing_adjoinRoot_X_pow_sub_C_of_regular_parameters

L190 ↗

EtaleFundamentalGroups.Kummer.isRegularLocalRing_adjoinRoot_X_pow_sub_C_of_regular_parameters

Documentation

The positive local Kummer root cover is regular local when a occurs first in a regular sequence generating the base maximal ideal.

All hypotheses are supplied by an explicit strict-normal-crossings parameter chart: no regularity or dimension statement about the target is assumed.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
noncomputable section

Lean source · statement

theorem isRegularLocalRing_adjoinRoot_X_pow_sub_C_of_regular_parameters
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {n : ℕ} (hn : 0 < n) {a : R} {rs : List R}
    (hreg : RingTheory.Sequence.IsRegular R (a :: rs))
    (hgen : Ideal.ofList (a :: rs) = maximalIdeal R) :
    IsRegularLocalRing (AdjoinRoot (X ^ n - C a))

theorem

localRootCoverParameterList_length_eq_ringKrullDim

L235 ↗

EtaleFundamentalGroups.Kummer.localRootCoverParameterList_length_eq_ringKrullDim

Documentation

The replacement family on the root cover is a dimension-sized generating family of its maximal ideal. In particular, the adjoined root is the new first regular parameter in the embedding-dimension sense.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
noncomputable section

Lean source · statement

theorem localRootCoverParameterList_length_eq_ringKrullDim
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {n : ℕ} (hn : 0 < n) {a : R} {rs : List R}
    (hreg : RingTheory.Sequence.IsRegular R (a :: rs))
    (hgen : Ideal.ofList (a :: rs) = maximalIdeal R) :
    ringKrullDim (AdjoinRoot (X ^ n - C a)) =
      ((localRootCoverParameterList R n a rs).length : WithBot ℕ∞)

Module documentation

Regularity of a local Kummer root cover

Declarations