Module

IteratedRegularity.lean

Nyll.EtaleFundamentalGroups.Kummer.RootCovers.Local.IteratedRegularity

15 declarations indexed from sourceView source ↗

Module documentation

Regularity of finite iterated local Kummer root covers

This file treats a finite diagonal root cover all at once. Starting from a regular parameter list consisting of the radicands followed by the remaining parameters, it tracks the images of all adjoined roots and remaining parameters in the final ring. That list generates the final maximal ideal and has unchanged length. Finite faithful integrality then supplies the dimension lower bound needed for the embedding-dimension criterion for a regular local ring.

The recursive local-ring and module structures are installed only inside proofs.

Imports2

Imported by3

def

iteratedLocalRootCoverRoots

L35 ↗

EtaleFundamentalGroups.Kummer.iteratedLocalRootCoverRoots

Documentation

The roots adjoined so far, mapped into the final iterated radical.

Source context 5 commands

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

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

Lean source · full declaration

def iteratedLocalRootCoverRoots
    (A : Type u) [CommRing A] :
    (r : ℕ) → (n : Fin r → ℕ) → (a : Fin r → A) →
      List (iteratedRadical A r n a)
  | 0, _, _ => []
  | r + 1, n, a =>
      let T : CommAlgCat.{u} A :=
        iteratedRadical A r (Fin.init n) (Fin.init a)
      let f : T[X] :=
        X ^ n (Fin.last r) - C (algebraMap A T (a (Fin.last r)))
      (iteratedLocalRootCoverRoots A r (Fin.init n) (Fin.init a)).map
          (AdjoinRoot.of f) ++
        [AdjoinRoot.root f]

def

iteratedLocalRootCoverConstructionList

L53 ↗

EtaleFundamentalGroups.Kummer.iteratedLocalRootCoverConstructionList

Documentation

The construction-order list: remaining parameters first, followed by roots in the order in which they were adjoined.

Source context 5 commands

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

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

Lean source · full declaration

def iteratedLocalRootCoverConstructionList
    (A : Type u) [CommRing A] :
    {r : ℕ} → (n : Fin r → ℕ) → (a : Fin r → A) →
      List A → List (iteratedRadical A r n a)
  | 0, _, _, rs => rs
  | r + 1, n, a, rs =>
      let T : CommAlgCat.{u} A :=
        iteratedRadical A r (Fin.init n) (Fin.init a)
      let f : T[X] :=
        X ^ n (Fin.last r) - C (algebraMap A T (a (Fin.last r)))
      (iteratedLocalRootCoverConstructionList A (Fin.init n) (Fin.init a) rs).map
          (AdjoinRoot.of f) ++
        [AdjoinRoot.root f]

def

iteratedLocalRootCoverParameterList

L72 ↗

EtaleFundamentalGroups.Kummer.iteratedLocalRootCoverParameterList

Documentation

The final parameter list. Reversing construction order puts every adjoined root first (newest to oldest), followed by the images of the remaining parameters.

Source context 5 commands

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

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

Lean source · statement

def iteratedLocalRootCoverParameterList
    (A : Type u) [CommRing A] {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (rs : List A) : List (iteratedRadical A r n a)

theorem

iteratedLocalRootCoverRoots_length

L78 ↗

EtaleFundamentalGroups.Kummer.iteratedLocalRootCoverRoots_length

Source context 5 commands

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

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

Lean source · statement

theorem iteratedLocalRootCoverRoots_length
    (A : Type u) [CommRing A] {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) :
    (iteratedLocalRootCoverRoots A r n a).length = r

theorem

iteratedLocalRootCoverParameterList_length

L95 ↗

EtaleFundamentalGroups.Kummer.iteratedLocalRootCoverParameterList_length

Source context 5 commands

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

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

Lean source · statement

theorem iteratedLocalRootCoverParameterList_length
    (A : Type u) [CommRing A] {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (rs : List A) :
    (iteratedLocalRootCoverParameterList A n a rs).length =
      (List.ofFn a ++ rs).length

theorem

ideal_ofList_move_middle_to_front

L119 ↗

EtaleFundamentalGroups.Kummer.ideal_ofList_move_middle_to_front

Source context 5 commands

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

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

Lean source · statement

theorem ideal_ofList_move_middle_to_front
    {R : Type u} [CommRing R] (xs ys : List R) (x : R) :
    Ideal.ofList (xs ++ x :: ys) = Ideal.ofList (x :: xs ++ ys)

theorem

radicands_mem_maximalIdeal

L125 ↗

EtaleFundamentalGroups.Kummer.radicands_mem_maximalIdeal

Source context 5 commands

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

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

Lean source · statement

theorem radicands_mem_maximalIdeal
    {A : Type u} [CommRing A] [IsLocalRing A]
    {r : ℕ} {a : Fin r → A} {rs : List A}
    (hgen : Ideal.ofList (List.ofFn a ++ rs) = maximalIdeal A) :
    ∀ i, a i ∈ maximalIdeal A

theorem

ideal_ofList_eq_of_perm

L134 ↗

EtaleFundamentalGroups.Kummer.ideal_ofList_eq_of_perm

Source context 5 commands

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

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

Lean source · statement

theorem ideal_ofList_eq_of_perm
    {R : Type u} [CommRing R] {xs ys : List R} (h : xs.Perm ys) :
    Ideal.ofList xs = Ideal.ofList ys

theorem

iteratedLocalRootCoverConstructionList_cons

L141 ↗

EtaleFundamentalGroups.Kummer.iteratedLocalRootCoverConstructionList_cons

Source context 5 commands

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

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

Lean source · statement

theorem iteratedLocalRootCoverConstructionList_cons
    {A : Type u} [CommRing A] {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (x : A) (rs : List A) :
    iteratedLocalRootCoverConstructionList A n a (x :: rs) =
      algebraMap A (iteratedRadical A r n a) x ::
        iteratedLocalRootCoverConstructionList A n a rs

theorem

ideal_ofList_iteratedLocalRootCoverConstructionList_eq_maximalIdeal

L170 ↗

EtaleFundamentalGroups.Kummer.ideal_ofList_iteratedLocalRootCoverConstructionList_eq_maximalIdeal

Documentation

The construction-order list generates the maximal ideal of the final cover.

Source context 5 commands

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

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

Lean source · statement

theorem ideal_ofList_iteratedLocalRootCoverConstructionList_eq_maximalIdeal
    {A : Type u} [CommRing A] [IsLocalRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) (rs : List A)
    [IsLocalRing (iteratedRadical A r n a)]
    (hn : ∀ i, 0 < n i)
    (hgen : Ideal.ofList (List.ofFn a ++ rs) = maximalIdeal A) :
    Ideal.ofList (iteratedLocalRootCoverConstructionList A n a rs) =
      maximalIdeal (iteratedRadical A r n a)

theorem

ideal_ofList_iteratedLocalRootCoverParameterList_eq_maximalIdeal

L272 ↗

EtaleFundamentalGroups.Kummer.ideal_ofList_iteratedLocalRootCoverParameterList_eq_maximalIdeal

Documentation

The images of all adjoined roots, followed by the remaining parameters, generate the maximal ideal of the final iterated local root cover.

Source context 5 commands

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

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

Lean source · statement

theorem ideal_ofList_iteratedLocalRootCoverParameterList_eq_maximalIdeal
    {A : Type u} [CommRing A] [IsLocalRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) (rs : List A)
    [IsLocalRing (iteratedRadical A r n a)]
    (hn : ∀ i, 0 < n i)
    (hgen : Ideal.ofList (List.ofFn a ++ rs) = maximalIdeal A) :
    Ideal.ofList (iteratedLocalRootCoverParameterList A n a rs) =
      maximalIdeal (iteratedRadical A r n a)

theorem

spanFinrank_ofList_le_length

L286 ↗

EtaleFundamentalGroups.Kummer.spanFinrank_ofList_le_length

Source context 5 commands

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

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

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

L295 ↗

EtaleFundamentalGroups.Kummer.parameter_length_eq_ringKrullDim

Source context 5 commands

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

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

Lean source · statement

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

theorem

isRegularLocalRing_iteratedRadical_of_regular_parameters

L315 ↗

EtaleFundamentalGroups.Kummer.isRegularLocalRing_iteratedRadical_of_regular_parameters

Documentation

A finite positive iterated Kummer root cover is regular local when the radicands followed by the remaining parameters form a regular sequence generating the base maximal ideal.

Source context 5 commands

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

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

Lean source · statement

theorem isRegularLocalRing_iteratedRadical_of_regular_parameters
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) (rs : List A)
    (hn : ∀ i, 0 < n i)
    (hreg : RingTheory.Sequence.IsRegular A (List.ofFn a ++ rs))
    (hgen : Ideal.ofList (List.ofFn a ++ rs) = maximalIdeal A) :
    IsRegularLocalRing (iteratedRadical A r n a)

theorem

iteratedLocalRootCoverParameterList_length_eq_ringKrullDim

L358 ↗

EtaleFundamentalGroups.Kummer.iteratedLocalRootCoverParameterList_length_eq_ringKrullDim

Documentation

The final root-and-parameter list is dimension-sized. Together with its maximal-ideal generation theorem, this is the parameter-system statement needed by downstream finite-cover consumers.

Source context 5 commands

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

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

Lean source · statement

theorem iteratedLocalRootCoverParameterList_length_eq_ringKrullDim
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) (rs : List A)
    (hn : ∀ i, 0 < n i)
    (hreg : RingTheory.Sequence.IsRegular A (List.ofFn a ++ rs))
    (hgen : Ideal.ofList (List.ofFn a ++ rs) = maximalIdeal A) :
    ringKrullDim (iteratedRadical A r n a) =
      ((iteratedLocalRootCoverParameterList A n a rs).length : WithBot ℕ∞)

Module documentation

Regularity of finite iterated local Kummer root covers

Declarations