NYLL
Module

HigherRadical.lean

Nyll.EtaleFundamentalGroups.Kummer.UnitAbsorption.HigherRadical
5 declarations indexed from sourceView source ↗

Module documentation

Finite-etale unit absorption after a higher radical base change

If e ∣ N, the pure e-th root cover of an element maps canonically to the pure N-th root cover by sending the first root to the (N / e)-th power of the second. This is the integral map needed to base change the finite-etale unit factor supplied by the DVR Abhyankar calculation from the ramification-index root to a prescribed larger root cover.

Imports2
Imported by5

Declarations

def

adjoinRootPowerMapOfDvd

L33 ↗
EtaleFundamentalGroups.Kummer.adjoinRootPowerMapOfDvd
Documentation

The canonical map from an e-th pure root cover to an N-th pure root cover when e ∣ N.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open scoped TensorProduct
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v w x
Lean source · statement
def adjoinRootPowerMapOfDvd
    {A : Type u} [CommRing A] {e N : ℕ} (hdiv : e ∣ N) (a : A) :
    AdjoinRoot (X ^ e - C a) →ₐ[A] AdjoinRoot (X ^ N - C a)
theorem

adjoinRootPowerMapOfDvd_root

L45 ↗
EtaleFundamentalGroups.Kummer.adjoinRootPowerMapOfDvd_root
Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open scoped TensorProduct
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v w x
Lean source · statement
theorem adjoinRootPowerMapOfDvd_root
    {A : Type u} [CommRing A] {e N : ℕ} (hdiv : e ∣ N) (a : A) :
    adjoinRootPowerMapOfDvd hdiv a
        (AdjoinRoot.root (X ^ e - C a)) =
      AdjoinRoot.root (X ^ N - C a) ^ (N / e)
theorem

isDomain_adjoinRoot_X_pow_sub_C_of_prime

L54 ↗
EtaleFundamentalGroups.Kummer.isDomain_adjoinRoot_X_pow_sub_C_of_prime
Documentation

The pure positive root polynomial of a prime element over a DVR is prime, hence its adjoin-root algebra is a domain.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open scoped TensorProduct
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v w x
Lean source · statement
theorem isDomain_adjoinRoot_X_pow_sub_C_of_prime
    {V : Type u} [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    {N : ℕ} (hN : 0 < N) (varpi : V) (hvarpi : Prime varpi) :
    IsDomain (AdjoinRoot (X ^ N - C varpi))
theorem

isDiscreteValuationRing_adjoinRoot_X_pow_sub_C_of_prime

L73 ↗
EtaleFundamentalGroups.Kummer.isDiscreteValuationRing_adjoinRoot_X_pow_sub_C_of_prime
Documentation

Adjoining a positive root of a prime element to a DVR again gives a DVR. Its maximal ideal is generated by the adjoined root.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open scoped TensorProduct
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v w x
Lean source · full declaration
theorem isDiscreteValuationRing_adjoinRoot_X_pow_sub_C_of_prime
    {V : Type u} [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    {N : ℕ} (hN : 0 < N) (varpi : V) (hvarpi : Prime varpi) :
    letI : IsDomain (AdjoinRoot (X ^ N - C varpi)) :=
      isDomain_adjoinRoot_X_pow_sub_C_of_prime hN varpi hvarpi
    IsDiscreteValuationRing (AdjoinRoot (X ^ N - C varpi)) := by
  let p : V[X] := X ^ N - C varpi
  have hNne : N ≠ 0 := hN.ne'
  let : IsDomain (AdjoinRoot p) :=
    isDomain_adjoinRoot_X_pow_sub_C_of_prime hN varpi hvarpi
  have hvarpi_mem : varpi ∈ IsLocalRing.maximalIdeal V :=
    (IsLocalRing.mem_maximalIdeal _).2 hvarpi.not_isUnit
  let : IsLocalRing (AdjoinRoot p) :=
    isLocalRing_adjoinRoot_X_pow_sub_C hN hvarpi_mem
  let : Module.FaithfullyFlat V (AdjoinRoot p) :=
    faithfullyFlat_adjoinRoot_X_pow_sub_C hN varpi
  have hmaxV :
      IsLocalRing.maximalIdeal V = Ideal.span {varpi} :=
    hvarpi.irreducible.maximalIdeal_eq
  have hmaxR :
      IsLocalRing.maximalIdeal (AdjoinRoot p) =
        Ideal.span {AdjoinRoot.root p} := by
    rw [maximalIdeal_adjoinRoot_X_pow_sub_C hN hvarpi_mem]
    apply le_antisymm
    · apply sup_le
      · rw [hmaxV, Ideal.map_span]
        simp only [Set.image_singleton]
        rw [show AdjoinRoot.of p varpi =
            AdjoinRoot.root p ^ N by
          simpa [p] using (adjoinRoot_root_pow N varpi).symm]
        rw [Ideal.span_le]
        rintro _ (rfl : _ = AdjoinRoot.root p ^ N)
        exact Ideal.pow_mem_of_mem (Ideal.span {AdjoinRoot.root p})
          (Ideal.mem_span_singleton_self _) N hN
      · exact le_rfl
    · exact le_sup_right
  have hroot_ne : AdjoinRoot.root p ≠ 0 := by
    intro hroot
    apply hvarpi.ne_zero
    apply FaithfulSMul.algebraMap_injective V (AdjoinRoot p)
    rw [AdjoinRoot.algebraMap_eq]
    rw [show AdjoinRoot.of p varpi =
        AdjoinRoot.root p ^ N by
      simpa [p] using (adjoinRoot_root_pow N varpi).symm]
    simp [hroot, hNne]
  have hR_notField : ¬ IsField (AdjoinRoot p) := by
    intro hfield
    have hbot : IsLocalRing.maximalIdeal (AdjoinRoot p) = ⊥ :=
      IsLocalRing.isField_iff_maximalIdeal_eq.mp hfield
    have : AdjoinRoot.root p ∈ (⊥ : Ideal (AdjoinRoot p)) := by
      rw [← hbot, hmaxR]
      exact Ideal.mem_span_singleton_self _
    exact hroot_ne (by simpa using this)
  have hprincipal :
      Submodule.IsPrincipal
        (IsLocalRing.maximalIdeal (AdjoinRoot p)) :=
    ⟨AdjoinRoot.root p, hmaxR⟩
  exact ((IsDiscreteValuationRing.TFAE
    (AdjoinRoot p) hR_notField).out 5 1).mp
    hprincipal
theorem

exists_finiteEtale_unitFactor_etale_over_higherUniformizerRoot

L141 ↗
EtaleFundamentalGroups.Kummer.exists_finiteEtale_unitFactor_etale_over_higherUniformizerRoot
Documentation

The actual finite-etale unit factor at ramification index e remains finite etale after base change to any prescribed N-th uniformizer root with e ∣ N.

The prescribed e-th root fed to unit absorption is constructed as the (N / e)-th power of the given N-th root. Thus neither this compatibility nor the finite-etale conclusion is a hypothesis.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open scoped TensorProduct
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v w x
Lean source · full declaration
theorem exists_finiteEtale_unitFactor_etale_over_higherUniformizerRoot
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (base : DVF.{u, w} K) (target : DVF.{v, x} L)
    [base.valuation.HasExtension target.valuation]
    [CharZero base.residueField]
    [Module.Finite base.valuationSubring target.valuationSubring]
    (varpi : base.valuationSubring)
    (hvarpi : base.valuation.IsUniformizer (varpi : K))
    (pi : target.valuationSubring)
    (unit : target.valuationSubringˣ)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (hdecomp :
      integerMap base target varpi =
        (unit : target.valuationSubring) *
          pi ^ ramificationIndex base target)
    (N : ℕ) (hdiv : ramificationIndex base target ∣ N)
    (beta : AlgebraicClosure L)
    (hbetaPow :
      beta ^ N = algebraMap K (AlgebraicClosure L) (varpi : K)) :
    ∃ (delta : AlgebraicClosure L) (q : target.valuationSubring[X])
      (unitFactorEquiv :
        AdjoinRoot (q.map (algebraMap target.valuationSubring L)) ≃ₐ[L]
          IntermediateField.adjoin L ({delta} : Set (AlgebraicClosure L)))
      (radicalToUnitFactor :
        AdjoinRoot
            (X ^ ramificationIndex base target - C varpi) →ₐ[base.valuationSubring]
          AdjoinRoot q),
      delta ^ ramificationIndex base target =
          algebraMap L (AlgebraicClosure L) (unit : L) ∧
        beta ^ (N / ramificationIndex base target) =
          delta * algebraMap L (AlgebraicClosure L) (pi : L) ∧
          q.Monic ∧
            q.map (algebraMap target.valuationSubring L) = minpoly L delta ∧
              Algebra.Etale target.valuationSubring (AdjoinRoot q) ∧
                Module.Finite target.valuationSubring (AdjoinRoot q) ∧
                  (IntermediateField.adjoin L
                      ({delta} : Set (AlgebraicClosure L))).restrictScalars K =
                    (IsScalarTower.toAlgHom K L
                        (AlgebraicClosure L)).fieldRange ⊔
                      IntermediateField.adjoin K
                        ({beta ^ (N / ramificationIndex base target)} :
                          Set (AlgebraicClosure L)) ∧
                    unitFactorEquiv
                        (AdjoinRoot.root
                          (q.map (algebraMap target.valuationSubring L))) =
                      IntermediateField.AdjoinSimple.gen L delta ∧
                      radicalToUnitFactor
                          (AdjoinRoot.root
                            (X ^ ramificationIndex base target - C varpi)) =
                        AdjoinRoot.root q *
                          algebraMap target.valuationSubring
                            (AdjoinRoot q) pi ∧
                        (letI : Algebra
                            (AdjoinRoot
                              (X ^ ramificationIndex base target - C varpi))
                            (AdjoinRoot q) :=
                          radicalToUnitFactor.toRingHom.toAlgebra
                         Algebra.Etale
                            (AdjoinRoot
                              (X ^ ramificationIndex base target - C varpi))
                            (AdjoinRoot q)) ∧
                        (let Rₑ := AdjoinRoot
                            (X ^ ramificationIndex base target - C varpi)
                         let Rₙ := AdjoinRoot (X ^ N - C varpi)
                         let Cq := AdjoinRoot q
                         let higherRootMap : Rₑ →ₐ[base.valuationSubring] Rₙ :=
                           adjoinRootPowerMapOfDvd hdiv varpi
                         letI : Algebra Rₑ Rₙ :=
                           higherRootMap.toRingHom.toAlgebra
                         letI : Algebra Rₑ Cq :=
                           radicalToUnitFactor.toRingHom.toAlgebra
                         let Tₙ := Rₙ ⊗[Rₑ] Cq
                         (Algebra.Etale Rₙ Tₙ ∧
                           Module.Finite Rₙ Tₙ)) := by
  let e := ramificationIndex base target
  have he_ne : e ≠ 0 := by
    simpa [e, ramificationIndex] using
      (Ideal.IsDedekindDomain.ramificationIdx'_ne_zero
        (maximalIdeal_map_integerMap_ne_bot base target)
        (IsLocalRing.maximalIdeal.isMaximal
          target.valuationSubring).isPrime
        (maximalIdeal_map_integerMap_le base target))
  let alpha : AlgebraicClosure L := beta ^ (N / e)
  have halphaPow :
      alpha ^ e = algebraMap K (AlgebraicClosure L) (varpi : K) := by
    rw [show alpha ^ e = beta ^ ((N / e) * e) by
      simp only [alpha, pow_mul]]
    rw [Nat.div_mul_cancel hdiv, hbetaPow]
  obtain ⟨delta, q, unitFactorEquiv, radicalToUnitFactor,
      hdeltaPow, halpha, hqMonic, hqMap, _hqDvd, hqEtale, hqFinite,
      hCompositum, hUnitFactorRoot, hRadicalToUnitFactorRoot,
      hPureEtale⟩ :=
    exists_finiteEtale_unitFactor_etale_over_prescribed_uniformizerRoot
      base target varpi hvarpi pi unit hpi hdecomp alpha halphaPow
  let Rₑ := AdjoinRoot (X ^ e - C varpi)
  let Rₙ := AdjoinRoot (X ^ N - C varpi)
  let Cq := AdjoinRoot q
  let higherRootMap : Rₑ →ₐ[base.valuationSubring] Rₙ :=
    adjoinRootPowerMapOfDvd hdiv varpi
  let : Algebra Rₑ Rₙ := higherRootMap.toRingHom.toAlgebra
  let : Algebra Rₑ Cq := radicalToUnitFactor.toRingHom.toAlgebra
  let : IsScalarTower base.valuationSubring Rₑ Cq :=
    IsScalarTower.of_algebraMap_eq fun z =>
      (radicalToUnitFactor.commutes z).symm
  let : Module.Finite base.valuationSubring Rₑ :=
    (monic_X_pow_sub_C varpi he_ne).finite_adjoinRoot
  let : Module.Finite target.valuationSubring Cq := hqFinite
  let : Module.Finite base.valuationSubring Cq :=
    Module.Finite.trans target.valuationSubring Cq
  let : Module.Finite Rₑ Cq :=
    Module.Finite.of_restrictScalars_finite
      base.valuationSubring Rₑ Cq
  let : Algebra.Etale Rₑ Cq := hPureEtale
  have hHigherEtale : Algebra.Etale Rₙ (Rₙ ⊗[Rₑ] Cq) := by
    infer_instance
  have hHigherFinite : Module.Finite Rₙ (Rₙ ⊗[Rₑ] Cq) := by
    exact Module.Finite.base_change Rₑ Rₙ Cq
  exact ⟨delta, q, unitFactorEquiv, radicalToUnitFactor,
    hdeltaPow, halpha, hqMonic, hqMap, hqEtale, hqFinite,
    hCompositum, hUnitFactorRoot, hRadicalToUnitFactorRoot,
    hPureEtale, hHigherEtale, hHigherFinite⟩

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