NYLL
Module

DiagonalRadical.lean

Nyll.EtaleFundamentalGroups.Kummer.Laurent.DiagonalRadical
18 declarations indexed from sourceView source ↗

Module documentation

Finite diagonal Laurent covers as iterated radicals

This file builds a finite diagonal Laurent cover one coordinate at a time. At each successor step, the preceding radical is extended by one Laurent coordinate and the one-variable cyclic Laurent equivalence removes the new diagonal exponent. All maps are explicit ring homomorphisms; no noncanonical algebra structures or scalar towers are installed.

Imports3
Imported by5

Declarations

def

nestedLaurent

L30 ↗
EtaleFundamentalGroups.Kummer.nestedLaurent
Documentation

The Laurent algebra obtained by adjoining r independent Laurent coordinates.

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 nestedLaurent (R : Type u) [CommRing R] : ℕ → CommRingCat.{u}
  | 0 => CommRingCat.of R
  | r + 1 => CommRingCat.of (AddMonoidAlgebra (nestedLaurent R r) ℤ)
def

nestedDiagonalRadical

L38 ↗
EtaleFundamentalGroups.Kummer.nestedDiagonalRadical
Documentation

The radical presentation built in parallel with nestedLaurent. At each successor step a root of the new degree-one Laurent monomial is adjoined.

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 nestedDiagonalRadical (R : Type u) [CommRing R] :
    (r : ℕ) → (Fin r → ℕ) → CommRingCat.{u}
  | 0, _ => CommRingCat.of R
  | r + 1, n =>
      CommRingCat.of (AdjoinRoot
        (X ^ n (Fin.last r) -
          C (AddMonoidAlgebra.single (1 : ℤ) (1 :
            nestedDiagonalRadical R r (Fin.init n)))))
def

nestedDiagonalRadicalBase

L48 ↗
EtaleFundamentalGroups.Kummer.nestedDiagonalRadicalBase
Documentation

The canonical base map from the nested Laurent algebra into its radical 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 · full declaration
def nestedDiagonalRadicalBase (R : Type u) [CommRing R] :
    (r : ℕ) → (n : Fin r → ℕ) →
      nestedLaurent R r →+* nestedDiagonalRadical R r n
  | 0, _ => RingHom.id R
  | r + 1, n =>
      let p := X ^ n (Fin.last r) -
        C (AddMonoidAlgebra.single (1 : ℤ) (1 :
          nestedDiagonalRadical R r (Fin.init n)))
      (AdjoinRoot.of p).comp
        (AddMonoidAlgebra.mapRingHom ℤ
          (nestedDiagonalRadicalBase R r (Fin.init n)))
def

nestedLaurentDiagonalMap

L61 ↗
EtaleFundamentalGroups.Kummer.nestedLaurentDiagonalMap
Documentation

The coordinatewise diagonal endomorphism of the nested Laurent algebra.

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 nestedLaurentDiagonalMap (R : Type u) [CommRing R] :
    (r : ℕ) → (n : Fin r → ℕ) → nestedLaurent R r →+* nestedLaurent R r
  | 0, _ => RingHom.id R
  | r + 1, n =>
      (AddMonoidAlgebra.mapDomainRingHom (nestedLaurent R r)
        (nsmulAddMonoidHom (n (Fin.last r)))).comp
        (AddMonoidAlgebra.mapRingHom ℤ
          (nestedLaurentDiagonalMap R r (Fin.init n)))
def

finLastInitAddEquiv

L71 ↗
EtaleFundamentalGroups.Kummer.finLastInitAddEquiv
Documentation

Split a tuple into its last coordinate and its initial tuple.

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
def finLastInitAddEquiv (r : ℕ) :
    (Fin (r + 1) → ℤ) ≃+ (ℤ × (Fin r → ℤ))
def

nestedLaurentMonomial

L79 ↗
EtaleFundamentalGroups.Kummer.nestedLaurentMonomial
Documentation

A monomial in the nested Laurent 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 · full declaration
def nestedLaurentMonomial (R : Type u) [CommRing R] :
    (r : ℕ) → (Fin r → ℤ) → R → nestedLaurent R r
  | 0, _, a => a
  | r + 1, x, a =>
      AddMonoidAlgebra.single (x (Fin.last r))
        (nestedLaurentMonomial R r (Fin.init x) a)
def

finLaurentRingEquiv

L87 ↗
EtaleFundamentalGroups.Kummer.finLaurentRingEquiv
Documentation

The ordinary Fin r Laurent algebra as the nested Laurent 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 · full declaration
def finLaurentRingEquiv (R : Type u) [CommRing R] :
    (r : ℕ) → AddMonoidAlgebra R (Fin r → ℤ) ≃+* nestedLaurent R r
  | 0 => (AddMonoidAlgebra.uniqueAlgEquiv R (Fin 0 → ℤ)).toRingEquiv
  | r + 1 =>
      (((AddMonoidAlgebra.domCongr R R (finLastInitAddEquiv r)).trans
        (AddMonoidAlgebra.curryAlgEquiv R)).toRingEquiv).trans
          (AddMonoidAlgebra.mapRingEquiv ℤ (finLaurentRingEquiv R r))
theorem

finLaurentRingEquiv_single

L95 ↗
EtaleFundamentalGroups.Kummer.finLaurentRingEquiv_single
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
theorem finLaurentRingEquiv_single
    {R : Type u} [CommRing R] :
    ∀ {r : ℕ} (x : Fin r → ℤ) (a : R),
      finLaurentRingEquiv R r (AddMonoidAlgebra.single x a) =
        nestedLaurentMonomial R r x a
  | 0, x, a => by
      have hx : x = 0 := Subsingleton.elim _ _
      subst x
      change
        (AddMonoidAlgebra.uniqueAlgEquiv R (Fin 0 → ℤ)).toRingEquiv
            (AddMonoidAlgebra.single 0 a) = a
      apply (AddMonoidAlgebra.uniqueAlgEquiv R (Fin 0 → ℤ)).symm.injective
      simp
  | r + 1, x, a => by
      change
        AddMonoidAlgebra.mapRingEquiv ℤ (finLaurentRingEquiv R r)
          (AddMonoidAlgebra.curryAlgEquiv R
            (AddMonoidAlgebra.domCongr R R (finLastInitAddEquiv r)
              (AddMonoidAlgebra.single x a))) =
          AddMonoidAlgebra.single (x (Fin.last r))
            (nestedLaurentMonomial R r (Fin.init x) a)
      rw [AddMonoidAlgebra.domCongr_single]
      change
        AddMonoidAlgebra.mapRingEquiv ℤ (finLaurentRingEquiv R r)
          (AddMonoidAlgebra.curryAlgEquiv R
            (AddMonoidAlgebra.single
              (x (Fin.last r), Fin.init x) a)) = _
      rw [AddMonoidAlgebra.curryAlgEquiv_single,
        AddMonoidAlgebra.mapRingEquiv_single,
        finLaurentRingEquiv_single]
def

finDiagonalAddMonoidHom

L127 ↗
EtaleFundamentalGroups.Kummer.finDiagonalAddMonoidHom
Documentation

Coordinatewise multiplication by the positive diagonal entries.

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 finDiagonalAddMonoidHom {r : ℕ} (n : Fin r → ℕ) :
    (Fin r → ℤ) →+ (Fin r → ℤ) where
  toFun x i := (n i : ℤ) * x i
  map_zero' := by ext; simp
  map_add' x y := by ext; simp [mul_add]
theorem

nestedLaurentDiagonalMap_monomial

L133 ↗
EtaleFundamentalGroups.Kummer.nestedLaurentDiagonalMap_monomial
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
theorem nestedLaurentDiagonalMap_monomial
    {R : Type u} [CommRing R] :
    ∀ {r : ℕ} (n : Fin r → ℕ) (x : Fin r → ℤ) (a : R),
      nestedLaurentDiagonalMap R r n (nestedLaurentMonomial R r x a) =
        nestedLaurentMonomial R r (finDiagonalAddMonoidHom n x) a
  | 0, _, _, _ => rfl
  | r + 1, n, x, a => by
      change
        AddMonoidAlgebra.mapDomainRingHom (nestedLaurent R r)
            (nsmulAddMonoidHom (n (Fin.last r)))
            (AddMonoidAlgebra.mapRingHom ℤ
              (nestedLaurentDiagonalMap R r (Fin.init n))
              (AddMonoidAlgebra.single (x (Fin.last r))
                (nestedLaurentMonomial R r (Fin.init x) a))) =
          AddMonoidAlgebra.single
            ((n (Fin.last r) : ℤ) * x (Fin.last r))
            (nestedLaurentMonomial R r
              (finDiagonalAddMonoidHom (Fin.init n) (Fin.init x)) a)
      rw [AddMonoidAlgebra.mapRingHom_single,
        nestedLaurentDiagonalMap_monomial]
      change
        AddMonoidAlgebra.mapDomain (nsmulAddMonoidHom (n (Fin.last r)))
            (AddMonoidAlgebra.single (x (Fin.last r))
              (nestedLaurentMonomial R r
                (finDiagonalAddMonoidHom (Fin.init n) (Fin.init x)) a)) = _
      rw [AddMonoidAlgebra.mapDomain_single]
      rfl
theorem

finLaurentRingEquiv_comp_diagonal

L162 ↗
EtaleFundamentalGroups.Kummer.finLaurentRingEquiv_comp_diagonal
Documentation

The finite-coordinate Laurent equivalence conjugates the two diagonal maps.

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 finLaurentRingEquiv_comp_diagonal
    {R : Type u} [CommRing R] {r : ℕ} (n : Fin r → ℕ) :
    (finLaurentRingEquiv R r).toRingHom.comp
        (AddMonoidAlgebra.mapDomainRingHom R (finDiagonalAddMonoidHom n)) =
      (nestedLaurentDiagonalMap R r n).comp
        (finLaurentRingEquiv R r).toRingHom
theorem

exists_nestedDiagonalRadicalRingEquiv

L183 ↗
EtaleFundamentalGroups.Kummer.exists_nestedDiagonalRadicalRingEquiv
Documentation

Positive diagonal exponents give an iterated radical ring equivalent to the nested Laurent algebra, with the equivalence restricting to the full diagonal endomorphism on the original 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 · full declaration
theorem exists_nestedDiagonalRadicalRingEquiv
    {R : Type u} [CommRing R] :
    ∀ {r : ℕ} (n : Fin r → ℕ), (∀ i, 0 < n i) →
      ∃ e : nestedDiagonalRadical R r n ≃+* nestedLaurent R r,
        e.toRingHom.comp (nestedDiagonalRadicalBase R r n) =
          nestedLaurentDiagonalMap R r n
  | 0, _, _ => ⟨RingEquiv.refl R, rfl⟩
  | r + 1, n, hn => by
      let nInit : Fin r → ℕ := Fin.init n
      let nLast : ℕ := n (Fin.last r)
      let L₀ := nestedLaurent R r
      let T₀ := nestedDiagonalRadical R r nInit
      let A := AddMonoidAlgebra T₀ ℤ
      let B := AddMonoidAlgebra L₀ ℤ
      let uA : A := AddMonoidAlgebra.single (1 : ℤ) (1 : T₀)
      let uB : B := AddMonoidAlgebra.single (1 : ℤ) (1 : L₀)
      let pA : A[X] := X ^ nLast - C uA
      let pB : B[X] := X ^ nLast - C uB
      obtain ⟨e₀, he₀⟩ :=
        exists_nestedDiagonalRadicalRingEquiv (R := R) (r := r)
          nInit (fun i ↦ hn i.castSucc)
      let c : A ≃+* B := AddMonoidAlgebra.mapRingEquiv ℤ e₀
      have hc :
          (AddMonoidAlgebra.mapRingHom ℤ e₀.toRingHom).comp
              (AddMonoidAlgebra.mapRingHom ℤ
                (nestedDiagonalRadicalBase R r nInit)) =
            AddMonoidAlgebra.mapRingHom ℤ
              (nestedLaurentDiagonalMap R r nInit) := by
        rw [← AddMonoidAlgebra.mapRingHom_comp, he₀]
      have hcu : c uA = uB := by
        simpa [c, uA, uB] using
          (AddMonoidAlgebra.mapRingEquiv_single (M := ℤ)
            e₀ (1 : T₀) (1 : ℤ))
      have hp : Associated (pA.map c) pB := by
        have h : pA.map c = pB := by
          simp [pA, pB, hcu]
        rw [h]
      let transport : AdjoinRoot pA ≃+* AdjoinRoot pB :=
        AdjoinRoot.mapRingEquiv c pA pB hp
      obtain ⟨eLast, _, heLast⟩ :=
        exists_cyclicLaurentRingEquiv (R := L₀) nLast (hn (Fin.last r))
      let e : AdjoinRoot pA ≃+* B := transport.trans eLast
      refine ⟨e, ?_⟩
      apply RingHom.ext
      intro x
      change eLast (transport
        (AdjoinRoot.of pA
          (AddMonoidAlgebra.mapRingHom ℤ
            (nestedDiagonalRadicalBase R r nInit) x))) = _
      rw [show transport (AdjoinRoot.of pA
          (AddMonoidAlgebra.mapRingHom ℤ
            (nestedDiagonalRadicalBase R r nInit) x)) =
          AdjoinRoot.of pB
            (c (AddMonoidAlgebra.mapRingHom ℤ
              (nestedDiagonalRadicalBase R r nInit) x)) by
        simp [transport]]
      rw [show eLast (AdjoinRoot.of pB
          (c (AddMonoidAlgebra.mapRingHom ℤ
            (nestedDiagonalRadicalBase R r nInit) x))) =
          AddMonoidAlgebra.mapDomainRingHom L₀
            (nsmulAddMonoidHom nLast)
            (c (AddMonoidAlgebra.mapRingHom ℤ
              (nestedDiagonalRadicalBase R r nInit) x)) by
        exact RingHom.congr_fun heLast _]
      change
        AddMonoidAlgebra.mapDomainRingHom L₀
            (nsmulAddMonoidHom nLast)
            (AddMonoidAlgebra.mapRingHom ℤ e₀
              (AddMonoidAlgebra.mapRingHom ℤ
                (nestedDiagonalRadicalBase R r nInit) x)) =
          AddMonoidAlgebra.mapDomainRingHom L₀
            (nsmulAddMonoidHom nLast)
            (AddMonoidAlgebra.mapRingHom ℤ
              (nestedLaurentDiagonalMap R r nInit) x)
      congr 1
      exact RingHom.congr_fun hc x
def

finDiagonalRadicalBase

L262 ↗
EtaleFundamentalGroups.Kummer.finDiagonalRadicalBase
Documentation

The base map from the ordinary finite-coordinate Laurent algebra to the corresponding nested radical 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
def finDiagonalRadicalBase
    (R : Type u) [CommRing R] {r : ℕ} (n : Fin r → ℕ) :
    AddMonoidAlgebra R (Fin r → ℤ) →+* nestedDiagonalRadical R r n
def

finLaurentDiagonalMap

L269 ↗
EtaleFundamentalGroups.Kummer.finLaurentDiagonalMap
Documentation

The diagonal endomorphism on the ordinary finite-coordinate Laurent algebra.

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
def finLaurentDiagonalMap
    (R : Type u) [CommRing R] {r : ℕ} (n : Fin r → ℕ) :
    AddMonoidAlgebra R (Fin r → ℤ) →+* AddMonoidAlgebra R (Fin r → ℤ)
theorem

exists_finDiagonalRadicalRingEquiv

L278 ↗
EtaleFundamentalGroups.Kummer.exists_finDiagonalRadicalRingEquiv
Documentation

The nested radical presentation is a finite-coordinate Laurent algebra, and its base map is exactly the coordinatewise positive diagonal map.

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 exists_finDiagonalRadicalRingEquiv
    {R : Type u} [CommRing R] {r : ℕ} (n : Fin r → ℕ)
    (hn : ∀ i, 0 < n i) :
    ∃ e : nestedDiagonalRadical R r n ≃+*
        AddMonoidAlgebra R (Fin r → ℤ),
      e.toRingHom.comp (finDiagonalRadicalBase R n) =
        finLaurentDiagonalMap R n
def

fintypeReindexAddEquiv

L307 ↗
EtaleFundamentalGroups.Kummer.fintypeReindexAddEquiv
Documentation

Reindex a finite family by its canonical equivalence with Fin.

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 fintypeReindexAddEquiv (ι : Type u) [Fintype ι] :
    (ι → ℤ) ≃+ (Fin (Fintype.card ι) → ℤ) where
  toFun x j := x ((Fintype.equivFin ι).symm j)
  invFun y i := y (Fintype.equivFin ι i)
  left_inv x := by
    ext i
    simp
  right_inv y := by
    ext j
    simp
  map_add' x y := by
    ext j
    rfl
def

fintypeReindexZModAddEquiv

L322 ↗
EtaleFundamentalGroups.Kummer.fintypeReindexZModAddEquiv
Documentation

Reindex the cyclic Smith quotient coordinates by Fintype.equivFin.

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
def fintypeReindexZModAddEquiv (ι : Type u) [Fintype ι]
    (n : ι → ℕ) :
    (∀ i, ZMod (n i)) ≃+
      (∀ j : Fin (Fintype.card ι),
        ZMod (n ((Fintype.equivFin ι).symm j)))
theorem

exists_smithDiagonalRadicalPresentation

L337 ↗
EtaleFundamentalGroups.Kummer.exists_smithDiagonalRadicalPresentation
Documentation

A finite-index free integer sublattice gives an explicit finite iterated radical presentation of its monoid-algebra map. The positive diagonal entries, the quotient coordinates, the monoid-algebra coordinate changes, and the commutative square are all produced from the same Smith choice for the lattice inclusion.

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 exists_smithDiagonalRadicalPresentation
    {R L : Type u} [CommRing R] [AddCommGroup L]
    [Module.Free ℤ L] [Module.Finite ℤ L]
    (H : Submodule ℤ L) [Finite (L ⧸ H)] :
    ∃ (r : ℕ) (n : Fin r → ℕ),
      (∀ i, 0 < n i) ∧
        ∃ (_eQ : (L ⧸ H) ≃+ ∀ i, ZMod (n i))
          (eH : AddMonoidAlgebra R H ≃+*
              AddMonoidAlgebra R (Fin r → ℤ))
          (eL : AddMonoidAlgebra R L ≃+*
              AddMonoidAlgebra R (Fin r → ℤ))
          (eRad : nestedDiagonalRadical R r n ≃+*
              AddMonoidAlgebra R (Fin r → ℤ)),
          eL.toRingHom.comp
              (AddMonoidAlgebra.mapDomainRingHom R
                H.subtype.toAddMonoidHom) =
            eRad.toRingHom.comp
              ((finDiagonalRadicalBase R n).comp eH.toRingHom)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.