Module

Basic.lean

Nyll.EtaleFundamentalGroups.Kummer.IteratedRadical.Basic

5 declarations indexed from sourceView source ↗

Module documentation

Finite iterated Kummer radicals

This file adjoins finitely many roots of equations X ^ n i - a i, in the order indexed by Fin r. Every radicand comes from the original base ring; this is the diagonal presentation used after decomposing a finite abelian Kummer group into cyclic factors.

The intermediate rings are bundled only in the existing CommAlgCat A. Their algebra structures and all scalar towers are the canonical structures provided by CommAlgCat and AdjoinRoot. No recursive instances are installed globally.

Imports4

Mathlib.Algebra.Category.CommAlgCat.Basic
Mathlib.Data.Fin.Tuple.Basic
Nyll.EtaleFundamentalGroups.Kummer.Radicals.Relative
Nyll.EtaleFundamentalGroups.Kummer.Descent.RelativeRadical

Imported by7

def

iteratedRadical

L38 ↗

EtaleFundamentalGroups.Kummer.iteratedRadical

Documentation

The algebra obtained by successively adjoining roots of X ^ n i - algebraMap A _ (a i).

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · full declaration

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

theorem

finite_iteratedRadical

L52 ↗

EtaleFundamentalGroups.Kummer.finite_iteratedRadical

Documentation

A finite positive iterated radical is finite over its original base. The finite-module structures are installed only along the induction, so consumers do not ask typeclass search to unfold the recursive presentation.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem finite_iteratedRadical
    {A : Type u} [CommRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i) :
    Module.Finite A (iteratedRadical A r n a)

theorem

free_iteratedRadical

L80 ↗

EtaleFundamentalGroups.Kummer.free_iteratedRadical

Documentation

A positive iterated radical is free over its original base.

The proof composes the canonical monic AdjoinRoot bases one stage at a time. Keeping this as a named producer prevents completion consumers from asking typeclass search to unfold the recursive ring presentation.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem free_iteratedRadical
    {A : Type u} [CommRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i) :
    Module.Free A (iteratedRadical A r n a)

theorem

faithfullyFlat_iteratedRadical

L108 ↗

EtaleFundamentalGroups.Kummer.faithfullyFlat_iteratedRadical

Documentation

A positive-degree finite iterated radical is faithfully flat over its original base. At each step, monicity gives a free extension; faithful flatness is then composed through the canonical scalar tower.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem faithfullyFlat_iteratedRadical
    {A : Type u} [CommRing A] [Nontrivial A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i) :
    Module.FaithfullyFlat A (iteratedRadical A r n a)

theorem

all_exponents_isUnit_of_formallyUnramified_iteratedRadical

L136 ↗

EtaleFundamentalGroups.Kummer.all_exponents_isUnit_of_formallyUnramified_iteratedRadical

Documentation

If a finite diagonal iterated Kummer radical is formally unramified over its base, then every exponent is a unit in that base.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem all_exponents_isUnit_of_formallyUnramified_iteratedRadical
    {A : Type u} [CommRing A] [Nontrivial A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    [hFU : Algebra.FormallyUnramified A (iteratedRadical A r n a)] :
    ∀ i, IsUnit (n i : A)

Module documentation

Finite iterated Kummer radicals

Declarations

iteratedRadical

finite_iteratedRadical

free_iteratedRadical

faithfullyFlat_iteratedRadical

all_exponents_isUnit_of_formallyUnramified_iteratedRadical