Module

ExactRootTargetAction.lean

Nyll.EtaleFundamentalGroups.Kummer.IteratedRadical.ExactRootTargetAction

4 declarations indexed from sourceView source ↗

Module documentation

A full iterated-radical action from one exact final root

The roots already adjoined in an iterated-radical prefix have canonical images in every algebra over that prefix. Thus the only new coordinate needed for one further stage is its final root. At the exact ramification index, that root is produced inside a fixed generic tensor component and is pulled back to the target field by the exact-unit-factor component comparison.

Appending these coordinates gives one action of the entire root cover on a single target field. Exponent-one stages need no separate branch: their canonical prefix coordinates satisfy the same power equation.

This is a conditional assembly leaf. In the selected-prefix application, the raw localized DVR theorem supplies the prefix map and valued extension, but not the finite valuation-ring extension or the strict-Henselian exact root input used below. Those data must come from the later chosen-factor or filtered-descent bridge; they are not consequences of completion alone.

Imports3

Imported by2

theorem

exists_iteratedRadicalTargetAction_of_prefix_and_lastRoot

L52 ↗

EtaleFundamentalGroups.Kummer.exists_iteratedRadicalTargetAction_of_prefix_and_lastRoot

Documentation

One new target root extends all canonical prefix roots to a simultaneous action of the Fin.snoc cover on the same target.

This is the finite-stage consumer for a descended exact-root factor. It is independent of how the last root was produced: a filtered finite-etale stage, a fixed tensor component, or any other source can supply z and hz. Exponent-one prefix stages are retained literally through their canonical distinguished roots.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uA uK uV uF uL uW

Lean source · full declaration

theorem exists_iteratedRadicalTargetAction_of_prefix_and_lastRoot
    {A : Type uA} {S : Type uL}
    [CommRing A] [IsDomain A]
    [CommRing S] [Algebra A S] [FaithfulSMul A S]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    [Algebra (iteratedRadical A r n a) S]
    [IsScalarTower A (iteratedRadical A r n a) S]
    (N : ℕ) (hN : 0 < N) (y : A)
    (z : S) (hz : z ^ N = algebraMap A S y)
    [IsDomain
      (iteratedRadical A (r + 1) (Fin.snoc n N) (Fin.snoc a y))] :
    let nFull : Fin (r + 1) → ℕ := Fin.snoc n N
    let aFull : Fin (r + 1) → A := Fin.snoc a y
    ∃ (x : Fin (r + 1) → S)
        (hx : ∀ i, x i ^ nFull i = algebraMap A S (aFull i)),
      Function.Injective
          (iteratedRadicalTargetAlgHom nFull aFull x hx) ∧
        (∀ i : Fin r,
          x i.castSucc =
            algebraMap (iteratedRadical A r n a) S
              (iteratedRadicalRoot A n a i)) ∧
        x (Fin.last r) = z := by
  dsimp only
  let nFull : Fin (r + 1) → ℕ := Fin.snoc n N
  let aFull : Fin (r + 1) → A := Fin.snoc a y
  let prefixRoot : Fin r → S := fun i ↦
    algebraMap (iteratedRadical A r n a) S
      (iteratedRadicalRoot A n a i)
  let xFull : Fin (r + 1) → S := Fin.snoc prefixRoot z
  have hnFull : ∀ i, 0 < nFull i := by
    intro i
    refine Fin.lastCases ?_ (fun j ↦ ?_) i
    · simpa [nFull] using hN
    · simpa [nFull] using hn j
  have hxFull : ∀ i,
      xFull i ^ nFull i = algebraMap A S (aFull i) := by
    intro i
    refine Fin.lastCases ?_ (fun j ↦ ?_) i
    · simpa [xFull, nFull, aFull] using hz
    · simp only [xFull, nFull, aFull, prefixRoot, Fin.snoc_castSucc]
      rw [← map_pow, iteratedRadicalRoot_pow]
      exact
        (IsScalarTower.algebraMap_apply A
          (iteratedRadical A r n a) S (a j)).symm
  refine ⟨xFull, hxFull, ?_, ?_, ?_⟩
  · exact
      iteratedRadicalTargetAlgHom_injective
        nFull aFull hnFull xFull hxFull
  · intro i
    simp [xFull, prefixRoot]
  · simp [xFull]

theorem

exists_iteratedRadicalTargetAction_of_prefix_and_lastRootAlgebra

L112 ↗

EtaleFundamentalGroups.Kummer.exists_iteratedRadicalTargetAction_of_prefix_and_lastRootAlgebra

Documentation

An algebra over the one-step exact root ring supplies the last coordinate needed by exists_iteratedRadicalTargetAction_of_prefix_and_lastRoot.

This is the application shape for a finite stage returned by filtered descent: the stage's structure map from the exact root ring produces the new root, while its already supplied prefix algebra retains every earlier coordinate in the same stage.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uA uK uV uF uL uW

Lean source · full declaration

theorem exists_iteratedRadicalTargetAction_of_prefix_and_lastRootAlgebra
    {A : Type uA} {S : Type uL}
    [CommRing A] [IsDomain A]
    [CommRing S] [Algebra A S] [FaithfulSMul A S]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    [Algebra (iteratedRadical A r n a) S]
    [IsScalarTower A (iteratedRadical A r n a) S]
    (N : ℕ) (hN : 0 < N) (y : A)
    [Algebra (AdjoinRoot (X ^ N - C y)) S]
    [IsScalarTower A (AdjoinRoot (X ^ N - C y)) S]
    [IsDomain
      (iteratedRadical A (r + 1) (Fin.snoc n N) (Fin.snoc a y))] :
    let nFull : Fin (r + 1) → ℕ := Fin.snoc n N
    let aFull : Fin (r + 1) → A := Fin.snoc a y
    ∃ (x : Fin (r + 1) → S)
        (hx : ∀ i, x i ^ nFull i = algebraMap A S (aFull i)),
      Function.Injective
          (iteratedRadicalTargetAlgHom nFull aFull x hx) ∧
        (∀ i : Fin r,
          x i.castSucc =
            algebraMap (iteratedRadical A r n a) S
              (iteratedRadicalRoot A n a i)) := by
  let Rn := AdjoinRoot (X ^ N - C y)
  let z : S := algebraMap Rn S (AdjoinRoot.root (X ^ N - C y))
  have hz : z ^ N = algebraMap A S y := by
    calc
      z ^ N = algebraMap Rn S
          (AdjoinRoot.root (X ^ N - C y) ^ N) :=
        (map_pow (algebraMap Rn S)
          (AdjoinRoot.root (X ^ N - C y)) N).symm
      _ = algebraMap Rn S (algebraMap A Rn y) := by
        rw [adjoinRoot_root_pow, AdjoinRoot.algebraMap_eq]
      _ = algebraMap A S y :=
        (IsScalarTower.algebraMap_apply A Rn S y).symm
  obtain ⟨x, hx, hinjective, hprefix, -⟩ :=
    exists_iteratedRadicalTargetAction_of_prefix_and_lastRoot
      n a hn N hN y z hz
  exact ⟨x, hx, hinjective, hprefix⟩

theorem

exists_targetRoot_of_exactRamificationIndex

L159 ↗

EtaleFundamentalGroups.Kummer.exists_targetRoot_of_exactRamificationIndex

Documentation

The exact ramification-index radical has a root in the target field.

The distinguished root is first taken in a canonical component of Froot ⊗[K] L. A target uniformizer and its unit decomposition produce HigherRadicalUnitFactorData; the exact-root comparison then makes the canonical right map L → component surjective, so the component root can be pulled back to L itself.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uA uK uV uF uL uW

Lean source · statement

theorem exists_targetRoot_of_exactRamificationIndex
    {K : Type uK} {Froot : Type uF} {L : Type uL}
    [Field K] [Field Froot] [Field L]
    [Algebra K Froot] [Algebra K L]
    (base : DVF.{uK, uV} K) (target : DVF.{uL, uW} L)
    [base.valuation.HasExtension target.valuation]
    [CharZero base.residueField]
    [Module.Finite base.valuationSubring target.valuationSubring]
    (varpi : base.valuationSubring)
    (hvarpi : base.valuation.IsUniformizer (varpi : K))
    (N : ℕ) (hExact : ramificationIndex base target = N)
    [Algebra (AdjoinRoot (X ^ N - C varpi)) Froot]
    [IsFractionRing (AdjoinRoot (X ^ N - C varpi)) Froot]
    [Algebra base.valuationSubring Froot]
    [IsScalarTower base.valuationSubring
      (AdjoinRoot (X ^ N - C varpi)) Froot]
    [IsScalarTower base.valuationSubring K Froot]
    [HenselianLocalRing (AdjoinRoot (X ^ N - C varpi))]
    [IsSepClosed
      (IsLocalRing.ResidueField (AdjoinRoot (X ^ N - C varpi)))] :
    ∃ x : L, x ^ N = algebraMap K L (varpi : K)

theorem

exists_iteratedRadicalTargetAction_of_prefix_and_exactLastRoot

L249 ↗

EtaleFundamentalGroups.Kummer.exists_iteratedRadicalTargetAction_of_prefix_and_exactLastRoot

Documentation

A supplied prefix algebra and one exact final root produce the simultaneous action of the full Fin.snoc root cover on one target field.

Every prefix coordinate is the image of its distinguished root. This includes inactive exponent-one stages without a case split. The final coordinate is sourced by exists_targetRoot_of_exactRamificationIndex, and domainhood of the full root ring makes the resulting action injective.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uA uK uV uF uL uW

Lean source · full declaration

theorem exists_iteratedRadicalTargetAction_of_prefix_and_exactLastRoot
    {A : Type uA} {K : Type uK} {Froot : Type uF} {L : Type uL}
    [CommRing A] [IsDomain A]
    [Field K] [Field Froot] [Field L]
    [Algebra A K] [Algebra K Froot] [Algebra K L] [Algebra A L]
    [IsScalarTower A K L] [FaithfulSMul A L]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    [Algebra (iteratedRadical A r n a) L]
    [IsScalarTower A (iteratedRadical A r n a) L]
    (base : DVF.{uK, uV} K) (target : DVF.{uL, uW} L)
    [base.valuation.HasExtension target.valuation]
    [CharZero base.residueField]
    [Module.Finite base.valuationSubring target.valuationSubring]
    (varpi : base.valuationSubring)
    (hvarpi : base.valuation.IsUniformizer (varpi : K))
    (N : ℕ) (hExact : ramificationIndex base target = N)
    (y : A)
    (hy : algebraMap A L y = algebraMap K L (varpi : K))
    [Algebra (AdjoinRoot (X ^ N - C varpi)) Froot]
    [IsFractionRing (AdjoinRoot (X ^ N - C varpi)) Froot]
    [Algebra base.valuationSubring Froot]
    [IsScalarTower base.valuationSubring
      (AdjoinRoot (X ^ N - C varpi)) Froot]
    [IsScalarTower base.valuationSubring K Froot]
    [HenselianLocalRing (AdjoinRoot (X ^ N - C varpi))]
    [IsSepClosed
      (IsLocalRing.ResidueField (AdjoinRoot (X ^ N - C varpi)))]
    [IsDomain
      (iteratedRadical A (r + 1) (Fin.snoc n N) (Fin.snoc a y))] :
    let nFull : Fin (r + 1) → ℕ := Fin.snoc n N
    let aFull : Fin (r + 1) → A := Fin.snoc a y
    ∃ (x : Fin (r + 1) → L)
        (hx : ∀ i, x i ^ nFull i = algebraMap A L (aFull i)),
      Function.Injective
          (iteratedRadicalTargetAlgHom nFull aFull x hx) ∧
        (∀ i : Fin r,
          x i.castSucc =
            algebraMap (iteratedRadical A r n a) L
              (iteratedRadicalRoot A n a i)) := by
  dsimp only
  let nFull : Fin (r + 1) → ℕ := Fin.snoc n N
  let aFull : Fin (r + 1) → A := Fin.snoc a y
  have hN : 0 < N := by
    rw [← hExact]
    exact ramificationIndex_pos_of_moduleFinite base target
  obtain ⟨z, hz⟩ :=
    exists_targetRoot_of_exactRamificationIndex
      (K := K) (Froot := Froot) (L := L)
      base target varpi hvarpi N hExact
  let prefixRoot : Fin r → L := fun i ↦
    algebraMap (iteratedRadical A r n a) L
      (iteratedRadicalRoot A n a i)
  let xFull : Fin (r + 1) → L := Fin.snoc prefixRoot z
  have hnFull : ∀ i, 0 < nFull i := by
    intro i
    refine Fin.lastCases ?_ (fun j ↦ ?_) i
    · simpa [nFull] using hN
    · simpa [nFull] using hn j
  have hxFull : ∀ i,
      xFull i ^ nFull i = algebraMap A L (aFull i) := by
    intro i
    refine Fin.lastCases ?_ (fun j ↦ ?_) i
    · simpa [xFull, nFull, aFull] using hz.trans hy.symm
    · simp only [xFull, nFull, aFull, prefixRoot, Fin.snoc_castSucc]
      rw [← map_pow, iteratedRadicalRoot_pow]
      exact
        (IsScalarTower.algebraMap_apply A
          (iteratedRadical A r n a) L (a j)).symm
  refine ⟨xFull, hxFull, ?_, ?_⟩
  · exact
      iteratedRadicalTargetAlgHom_injective
        nFull aFull hnFull xFull hxFull
  · intro i
    simp [xFull, prefixRoot]

Module documentation

A full iterated-radical action from one exact final root

Declarations

exists_iteratedRadicalTargetAction_of_prefix_and_lastRoot

exists_iteratedRadicalTargetAction_of_prefix_and_lastRootAlgebra

exists_targetRoot_of_exactRamificationIndex

exists_iteratedRadicalTargetAction_of_prefix_and_exactLastRoot