Module

IteratedHeightOne.lean

Nyll.EtaleFundamentalGroups.Kummer.RootCovers.Local.IteratedHeightOne

10 declarations indexed from sourceView source ↗

Module documentation

Height-one primes of an iterated local root cover

This file exposes the individual roots in a finite diagonal Kummer cover and uses their defining equations to classify the contractions of height-one primes meeting the boundary. It also extracts the corresponding divisibility of ramification indices directly from the length definition of Ideal.ramificationIdx.

No primality or uniformizer hypothesis is imposed on an adjoined root.

Imports5

Nyll.EtaleFundamentalGroups.Kummer.IteratedRadical.Basic
Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.RingTheory.OrderOfVanishing.Basic
Mathlib.RingTheory.RamificationInertia.Ramification

Imported by5

def

iteratedRadicalRoot

L36 ↗

EtaleFundamentalGroups.Kummer.iteratedRadicalRoot

Documentation

The i-th root in the final iterated radical, transported through all subsequent root adjunctions.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open scoped BigOperators
universe u

Lean source · full declaration

def iteratedRadicalRoot
    (A : Type u) [CommRing A] :
    {r : ℕ} → (n : Fin r → ℕ) → (a : Fin r → A) →
      Fin r → iteratedRadical A r n a
  | 0, _, _, i => Fin.elim0 i
  | r + 1, n, a, i =>
      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)))
      Fin.lastCases
        (AdjoinRoot.root f)
        (fun j ↦ AdjoinRoot.of f
          (iteratedRadicalRoot A (Fin.init n) (Fin.init a) j)) i

theorem

iteratedRadicalRoot_last

L52 ↗

EtaleFundamentalGroups.Kummer.iteratedRadicalRoot_last

Documentation

The last distinguished root is the root of the final adjunction.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open scoped BigOperators
universe u

Lean source · statement

theorem iteratedRadicalRoot_last {A : Type u} [CommRing A] {r : ℕ}
    (n : Fin (r + 1) → ℕ) (a : Fin (r + 1) → A) :
    iteratedRadicalRoot A n a (Fin.last r) =
      AdjoinRoot.root (X ^ n (Fin.last r) -
        C (algebraMap A (iteratedRadical A r (Fin.init n) (Fin.init a)) (a (Fin.last r))))

theorem

iteratedRadicalRoot_castSucc

L65 ↗

EtaleFundamentalGroups.Kummer.iteratedRadicalRoot_castSucc

Documentation

Earlier distinguished roots enter the final adjunction through its canonical map.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open scoped BigOperators
universe u

Lean source · statement

theorem iteratedRadicalRoot_castSucc {A : Type u} [CommRing A] {r : ℕ}
    (n : Fin (r + 1) → ℕ) (a : Fin (r + 1) → A) (j : Fin r) :
    iteratedRadicalRoot A n a j.castSucc =
      AdjoinRoot.of (X ^ n (Fin.last r) -
        C (algebraMap A (iteratedRadical A r (Fin.init n) (Fin.init a)) (a (Fin.last r))))
        (iteratedRadicalRoot A (Fin.init n) (Fin.init a) j)

theorem

iteratedRadicalRoot_pow

L81 ↗

EtaleFundamentalGroups.Kummer.iteratedRadicalRoot_pow

Documentation

Each indexed root satisfies its original diagonal Kummer equation in 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 scoped BigOperators
universe u

Lean source · statement

theorem iteratedRadicalRoot_pow
    {A : Type u} [CommRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) (i : Fin r) :
    iteratedRadicalRoot A n a i ^ n i =
      algebraMap A (iteratedRadical A r n a) (a i)

theorem

algebraMap_prod_radicands_eq_prod_iteratedRadicalRoot_pow

L112 ↗

EtaleFundamentalGroups.Kummer.algebraMap_prod_radicands_eq_prod_iteratedRadicalRoot_pow

Documentation

The product of the base radicands becomes the product of the corresponding root powers in the final iterated cover.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open scoped BigOperators
universe u

Lean source · statement

theorem algebraMap_prod_radicands_eq_prod_iteratedRadicalRoot_pow
    {A : Type u} [CommRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A) :
    algebraMap A (iteratedRadical A r n a) (∏ i, a i) =
      ∏ i, iteratedRadicalRoot A n a i ^ n i

theorem

disjoint_powers_prod_radicands_of_iteratedRadicalRoots_not_mem

L124 ↗

EtaleFundamentalGroups.Kummer.disjoint_powers_prod_radicands_of_iteratedRadicalRoots_not_mem

Documentation

A prime avoiding every adjoined root is disjoint from the powers of the full boundary product. Thus it defines a prime on the boundary-complement Away localization.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open scoped BigOperators
universe u

Lean source · statement

theorem disjoint_powers_prod_radicands_of_iteratedRadicalRoots_not_mem
    {A : Type u} [CommRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (q : Ideal (iteratedRadical A r n a)) [q.IsPrime]
    (havoid : ∀ i, iteratedRadicalRoot A n a i ∉ q) :
    Disjoint
      ((Submonoid.powers
        (algebraMap A (iteratedRadical A r n a) (∏ i, a i)) :
          Submonoid (iteratedRadical A r n a)) :
        Set (iteratedRadical A r n a))
      (q : Set (iteratedRadical A r n a))

theorem

map_to_away_prod_radicands_isPrime_of_iteratedRadicalRoots_not_mem

L144 ↗

EtaleFundamentalGroups.Kummer.map_to_away_prod_radicands_isPrime_of_iteratedRadicalRoots_not_mem

Documentation

The explicit prime on the Away localization supplied by a height-one prime which misses every root.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open scoped BigOperators
universe u

Lean source · statement

theorem map_to_away_prod_radicands_isPrime_of_iteratedRadicalRoots_not_mem
    {A : Type u} [CommRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (q : Ideal (iteratedRadical A r n a)) [q.IsPrime]
    (havoid : ∀ i, iteratedRadicalRoot A n a i ∉ q) :
    (q.map (algebraMap (iteratedRadical A r n a)
      (Localization.Away
        (algebraMap A (iteratedRadical A r n a) (∏ i, a i))))).IsPrime

theorem

under_eq_span_radicand_of_height_eq_one_of_iteratedRadicalRoot_mem

L164 ↗

EtaleFundamentalGroups.Kummer.under_eq_span_radicand_of_height_eq_one_of_iteratedRadicalRoot_mem

Documentation

A height-one prime meeting the i-th root contracts to the corresponding prime boundary branch in the base. The contraction equality is produced from faithful flatness and going down; it is not an input hypothesis.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open scoped BigOperators
universe u

Lean source · statement

theorem under_eq_span_radicand_of_height_eq_one_of_iteratedRadicalRoot_mem
    {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    (q : Ideal (iteratedRadical A r n a)) [q.IsPrime]
    (hqheight : q.height = 1) (i : Fin r)
    (hai : Prime (a i))
    (hroot : iteratedRadicalRoot A n a i ∈ q) :
    q.under A = Ideal.span {a i}

theorem

exponent_dvd_ramificationIdx_of_height_eq_one_of_iteratedRadicalRoot_mem

L207 ↗

EtaleFundamentalGroups.Kummer.exponent_dvd_ramificationIdx_of_height_eq_one_of_iteratedRadicalRoot_mem

Documentation

If a height-one prime of an iterated local root cover contains the i-th root, then the exponent n i divides its ramification index over the original base. Flatness makes the base radicand regular on the cover, hence its root is regular as well. Additivity of order of vanishing then computes the quotient length of the root power. In particular, the root is not assumed prime or a uniformizer.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open scoped BigOperators
universe u

Lean source · statement

theorem exponent_dvd_ramificationIdx_of_height_eq_one_of_iteratedRadicalRoot_mem
    {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    (q : Ideal (iteratedRadical A r n a)) [q.IsPrime]
    (hqheight : q.height = 1) (i : Fin r)
    (hai : Prime (a i))
    (hroot : iteratedRadicalRoot A n a i ∈ q) :
    n i ∣ q.ramificationIdx A

theorem

heightOnePrime_away_or_exists_branch_under_eq_and_exponent_dvd

L267 ↗

EtaleFundamentalGroups.Kummer.heightOnePrime_away_or_exists_branch_under_eq_and_exponent_dvd

Documentation

Every height-one prime of the positive iterated root cover either extends to the full boundary-complement Away localization, or meets a labelled root; in the latter case its base contraction and the resulting ramification-index divisibility are both produced by the construction.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open scoped BigOperators
universe u

Lean source · statement

theorem heightOnePrime_away_or_exists_branch_under_eq_and_exponent_dvd
    {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i) (ha : ∀ i, Prime (a i))
    (q : Ideal (iteratedRadical A r n a)) [q.IsPrime]
    (hqheight : q.height = 1) :
    Disjoint
        ((Submonoid.powers
          (algebraMap A (iteratedRadical A r n a) (∏ i, a i)) :
            Submonoid (iteratedRadical A r n a)) :
          Set (iteratedRadical A r n a))
        (q : Set (iteratedRadical A r n a)) ∨
      ∃ i,
        q.under A = Ideal.span {a i} ∧
          n i ∣ q.ramificationIdx A

Module documentation

Height-one primes of an iterated local root cover

Declarations