NYLL
Module

NestedDiagonalUnramified.lean

Nyll.EtaleFundamentalGroups.Kummer.Laurent.NestedDiagonalUnramified
7 declarations indexed from sourceView source ↗

Module documentation

Formal unramifiedness of a diagonal Laurent radical

The radical presentation of a finite lattice cover is dependent: at each stage the new radicand is the new Laurent monomial over the preceding radical, rather than an element of the original coefficient ring. This file proves that formal unramifiedness of that presentation forces every Smith exponent to be a unit in the original coefficient ring.

Coefficient extension for additive monoid algebras is handled by its canonical pushout square. Faithful flatness is preserved by this base change, and formal unramifiedness is reflected by faithfully-flat descent.

Imports6
Imported by2

Declarations

theorem

mapRingHom_faithfullyFlat

L37 ↗
EtaleFundamentalGroups.Kummer.mapRingHom_faithfullyFlat
Documentation

Faithful flatness survives coefficient extension in an additive monoid 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
theorem mapRingHom_faithfullyFlat
    {A B : Type u} {M : Type}
    [CommRing A] [CommRing B] [AddCommMonoid M]
    (f : A →+* B) (hf : f.FaithfullyFlat) :
    (AddMonoidAlgebra.mapRingHom M f).FaithfullyFlat
theorem

formallyUnramified_of_mapRingHom

L64 ↗
EtaleFundamentalGroups.Kummer.formallyUnramified_of_mapRingHom
Documentation

Formal unramifiedness of a coefficient extension reflects to the coefficient 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 formallyUnramified_of_mapRingHom
    {A B : Type u} {M : Type} [CommRing A] [Nontrivial A]
    [CommRing B] [AddCommMonoid M]
    (f : A →+* B)
    (hg : (AddMonoidAlgebra.mapRingHom M f).FormallyUnramified) :
    f.FormallyUnramified
def

nestedLaurentAugmentation

L99 ↗
EtaleFundamentalGroups.Kummer.nestedLaurentAugmentation
Documentation

Evaluation of every Laurent coordinate at one.

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 nestedLaurentAugmentation
    (R : Type u) [CommRing R] :
    (r : ℕ) → nestedLaurent R r →+* R
  | 0 => RingHom.id R
  | r + 1 =>
      AddMonoidAlgebra.liftNCRingHom
        (nestedLaurentAugmentation R r)
        (1 : Multiplicative ℤ →* R)
        (fun _ _ ↦ Commute.all _ _)
theorem

nestedLaurent_nontrivial

L109 ↗
EtaleFundamentalGroups.Kummer.nestedLaurent_nontrivial
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 nestedLaurent_nontrivial
    (R : Type u) [CommRing R] [Nontrivial R] :
    ∀ r : ℕ, Nontrivial (nestedLaurent R r)
  | 0 => by
      change Nontrivial R
      infer_instance
  | r + 1 => by
      let : Nontrivial (nestedLaurent R r) :=
        nestedLaurent_nontrivial R r
      change Nontrivial (AddMonoidAlgebra (nestedLaurent R r) ℤ)
      infer_instance
theorem

nestedDiagonalRadicalBase_faithfullyFlat

L122 ↗
EtaleFundamentalGroups.Kummer.nestedDiagonalRadicalBase_faithfullyFlat
Documentation

The canonical radical base map is faithfully flat.

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 nestedDiagonalRadicalBase_faithfullyFlat
    {R : Type u} [CommRing R] [Nontrivial R] :
    ∀ {r : ℕ} (n : Fin r → ℕ), (∀ i, 0 < n i) →
      (nestedDiagonalRadicalBase R r n).FaithfullyFlat
  | 0, _, _ => RingHom.FaithfullyFlat.of_bijective Function.bijective_id
  | r + 1, n, hn => by
      let nInit : Fin r → ℕ := Fin.init n
      let nLast : ℕ := n (Fin.last r)
      let T₀ := nestedDiagonalRadical R r nInit
      let B₀ := AddMonoidAlgebra (nestedLaurent R r) ℤ
      let A := AddMonoidAlgebra T₀ ℤ
      let uA : A := AddMonoidAlgebra.single (1 : ℤ) (1 : T₀)
      let pA : A[X] := X ^ nLast - C uA
      let f := nestedDiagonalRadicalBase R r nInit
      let g := AddMonoidAlgebra.mapRingHom ℤ f
      have hf : f.FaithfullyFlat :=
        nestedDiagonalRadicalBase_faithfullyFlat nInit
          (fun i ↦ hn i.castSucc)
      have hg : g.FaithfullyFlat :=
        mapRingHom_faithfullyFlat (M := ℤ) f hf
      let : Nontrivial (nestedLaurent R r) :=
        nestedLaurent_nontrivial R r
      let : Algebra B₀ A := g.toAlgebra
      let : Module.FaithfullyFlat B₀ A := by
        rw [← RingHom.faithfullyFlat_algebraMap_iff]
        simpa [g, RingHom.algebraMap_toAlgebra] using hg
      let : Nontrivial A := hg.injective.nontrivial
      let : Module.FaithfullyFlat A (AdjoinRoot pA) :=
        faithfullyFlat_adjoinRoot_X_pow_sub_C
          (hn (Fin.last r)) uA
      have hroot : (AdjoinRoot.of pA).FaithfullyFlat := by
        rw [← AdjoinRoot.algebraMap_eq,
          RingHom.faithfullyFlat_algebraMap_iff]
        infer_instance
      have hcomp : ((AdjoinRoot.of pA).comp g).FaithfullyFlat :=
        RingHom.FaithfullyFlat.stableUnderComposition _ _ hg hroot
      change ((AdjoinRoot.of pA).comp g).FaithfullyFlat
      exact hcomp
theorem

all_exponents_isUnit_of_formallyUnramified_nestedDiagonalRadical

L163 ↗
EtaleFundamentalGroups.Kummer.all_exponents_isUnit_of_formallyUnramified_nestedDiagonalRadical
Documentation

Formal unramifiedness of the dependent diagonal radical presentation forces every positive diagonal exponent to be a unit in the coefficient ring.

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_nestedDiagonalRadical
    {R : Type u} [CommRing R] [Nontrivial R]
    {r : ℕ} (n : Fin r → ℕ) (hn : ∀ i, 0 < n i)
    (hFU : (nestedDiagonalRadicalBase R r n).FormallyUnramified) :
    ∀ i, IsUnit (n i : R)
theorem

exists_smithCyclicCoordinates_isUnit_of_formallyUnramified_latticeCover

L229 ↗
EtaleFundamentalGroups.Kummer.exists_smithCyclicCoordinates_isUnit_of_formallyUnramified_latticeCover
Documentation

A formally unramified finite-index lattice cover has synchronized cyclic quotient coordinates whose orders are units in the coefficient ring. Both the coordinates and their unit property are produced from the lattice inclusion and the formal-unramifiedness of its actual monoid-algebra 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_smithCyclicCoordinates_isUnit_of_formallyUnramified_latticeCover
    {R L : Type u} [CommRing R] [Nontrivial R]
    [AddCommGroup L] [Module.Free ℤ L] [Module.Finite ℤ L]
    (H : Submodule ℤ L) [Finite (L ⧸ H)]
    (hFU : (AddMonoidAlgebra.mapDomainRingHom R
      H.subtype.toAddMonoidHom).FormallyUnramified) :
    ∃ (r : ℕ) (n : Fin r → ℕ),
      (∀ i, 0 < n i) ∧
        ∃ _eQ : (L ⧸ H) ≃+ ∀ i, ZMod (n i),
          ∀ i, IsUnit (n i : R)

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