NYLL
Module

FieldOverLowerFractionRing.lean

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

Module documentation

The higher radical field as a fraction field over the lower radical

The field generated by a prescribed higher root is already represented as higherRadicalFieldOverLower inside the chosen algebraic closure. This file identifies it with the fraction field of the literal higher root ring and records compatibility with the canonical map from the actual lower root.

Imports1
Imported by3

Declarations

def

higherRadicalFieldOverLowerGenericFiberAlgEquiv

L32 ↗
EtaleFundamentalGroups.Kummer.higherRadicalFieldOverLowerGenericFiberAlgEquiv
Documentation

The generic fibre of the literal N-th root ring is the higher radical field, regarded over the lower field generated by the appropriate power of the chosen root.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
universe uK uV uOmega uF
Lean source · full declaration
def higherRadicalFieldOverLowerGenericFiberAlgEquiv
    {K : Type uK} {Omega : Type uOmega}
    [Field K] [Field Omega] [Algebra K Omega]
    (base : DVF.{uK, uV} K)
    {e N : ℕ} (hN : 0 < N)
    (varpi : base.valuationSubring) (hvarpiPrime : Prime varpi)
    (beta : Omega)
    (hbetaPow : beta ^ N = algebraMap K Omega (varpi : K)) :
    let V := base.valuationSubring
    let Rₙ := AdjoinRoot (X ^ N - C varpi)
    let F := lowerRadicalField (K := K) e N beta
    let K' := higherRadicalFieldOverLower (K := K) e N beta
    letI : Algebra K K' :=
      ((algebraMap F K').comp (algebraMap K F)).toAlgebra
    (K ⊗[V] Rₙ) ≃ₐ[K] K' := by
  dsimp only
  let V := base.valuationSubring
  let Rₙ := AdjoinRoot (X ^ N - C varpi)
  let F := lowerRadicalField (K := K) e N beta
  let Kₙ : IntermediateField K Omega :=
    IntermediateField.adjoin K ({beta} : Set Omega)
  let K' := higherRadicalFieldOverLower (K := K) e N beta
  letI : Algebra K K' :=
    ((algebraMap F K').comp (algebraMap K F)).toAlgebra
  let eKₙ : Kₙ ≃ₐ[K] K' :=
    { toFun := fun z ↦ ⟨z.1, z.2⟩
      invFun := fun z ↦ ⟨z.1, z.2⟩
      left_inv := fun _ ↦ rfl
      right_inv := fun _ ↦ rfl
      map_mul' := fun _ _ ↦ rfl
      map_add' := fun _ _ ↦ rfl
      commutes' := fun _ ↦ rfl }
  exact
    (pureRadicalGenericFiberAlgEquiv hN varpi hvarpiPrime beta
      hbetaPow).trans eKₙ
def

higherRadicalFieldOverLowerRootAlgebra

L71 ↗
EtaleFundamentalGroups.Kummer.higherRadicalFieldOverLowerRootAlgebra
Documentation

The root-ring algebra structure on the higher radical field induced by its generic-fibre equivalence.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
universe uK uV uOmega uF
Lean source · full declaration
def higherRadicalFieldOverLowerRootAlgebra
    {K : Type uK} {Omega : Type uOmega}
    [Field K] [Field Omega] [Algebra K Omega]
    (base : DVF.{uK, uV} K)
    {e N : ℕ} (hN : 0 < N)
    (varpi : base.valuationSubring) (hvarpiPrime : Prime varpi)
    (beta : Omega)
    (hbetaPow : beta ^ N = algebraMap K Omega (varpi : K)) :
    let Rₙ := AdjoinRoot (X ^ N - C varpi)
    let F := lowerRadicalField (K := K) e N beta
    let K' := higherRadicalFieldOverLower (K := K) e N beta
    letI : Algebra K K' :=
      ((algebraMap F K').comp (algebraMap K F)).toAlgebra
    Algebra Rₙ K' := by
  dsimp only
  let V := base.valuationSubring
  let F := lowerRadicalField (K := K) e N beta
  let K' := higherRadicalFieldOverLower (K := K) e N beta
  letI : IsFractionRing V K := base.valuationSubring_isFractionRing
  letI : Algebra V F :=
    ((algebraMap K F).comp (algebraMap V K)).toAlgebra
  letI : IsScalarTower V K F := IsScalarTower.of_algebraMap_eq' rfl
  letI : Algebra K K' :=
    ((algebraMap F K').comp (algebraMap K F)).toAlgebra
  letI : IsScalarTower K F K' := IsScalarTower.of_algebraMap_eq' rfl
  letI : Algebra V K' :=
    ((algebraMap K K').comp (algebraMap V K)).toAlgebra
  letI : IsScalarTower V K K' := IsScalarTower.of_algebraMap_eq' rfl
  exact (genericFiberRightAlgHom
    (higherRadicalFieldOverLowerGenericFiberAlgEquiv
      (e := e) base hN varpi hvarpiPrime beta hbetaPow)).toRingHom.toAlgebra
theorem

higherRadicalFieldOverLower_isFractionRing

L105 ↗
EtaleFundamentalGroups.Kummer.higherRadicalFieldOverLower_isFractionRing
Documentation

With the canonical root-ring action, the higher radical field is a fraction field of the literal higher root ring.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
universe uK uV uOmega uF
Lean source · full declaration
theorem higherRadicalFieldOverLower_isFractionRing
    {K : Type uK} {Omega : Type uOmega}
    [Field K] [Field Omega] [Algebra K Omega]
    (base : DVF.{uK, uV} K)
    {e N : ℕ} (hN : 0 < N)
    (varpi : base.valuationSubring) (hvarpiPrime : Prime varpi)
    (beta : Omega)
    (hbetaPow : beta ^ N = algebraMap K Omega (varpi : K)) :
    let Rₙ := AdjoinRoot (X ^ N - C varpi)
    let F := lowerRadicalField (K := K) e N beta
    let K' := higherRadicalFieldOverLower (K := K) e N beta
    letI : Algebra K K' :=
      ((algebraMap F K').comp (algebraMap K F)).toAlgebra
    letI : Algebra Rₙ K' :=
      higherRadicalFieldOverLowerRootAlgebra
        (e := e) base hN varpi hvarpiPrime beta hbetaPow
    IsFractionRing Rₙ K' := by
  dsimp only
  let V := base.valuationSubring
  let Rₙ := AdjoinRoot (X ^ N - C varpi)
  let F := lowerRadicalField (K := K) e N beta
  let K' := higherRadicalFieldOverLower (K := K) e N beta
  let : IsFractionRing V K := base.valuationSubring_isFractionRing
  let : IsIntegrallyClosed V :=
    base.valuationSubring_isIntegrallyClosed
  let : IsDomain Rₙ :=
    isDomain_adjoinRoot_X_pow_sub_C_of_prime hN varpi hvarpiPrime
  let : Algebra K K' :=
    ((algebraMap F K').comp (algebraMap K F)).toAlgebra
  let : Algebra V F :=
    ((algebraMap K F).comp (algebraMap V K)).toAlgebra
  let : IsScalarTower V K F := IsScalarTower.of_algebraMap_eq' rfl
  let : IsScalarTower K F K' := IsScalarTower.of_algebraMap_eq' rfl
  let : Algebra V K' :=
    ((algebraMap K K').comp (algebraMap V K)).toAlgebra
  let : IsScalarTower V K K' := IsScalarTower.of_algebraMap_eq' rfl
  let : Algebra Rₙ K' :=
    higherRadicalFieldOverLowerRootAlgebra
      (e := e) base hN varpi hvarpiPrime beta hbetaPow
  exact isFractionRing_of_genericFiberAlgEquiv
    (higherRadicalFieldOverLowerGenericFiberAlgEquiv
      (e := e) base hN varpi hvarpiPrime beta hbetaPow)
theorem

higherRadicalFieldOverLower_root_isScalarTower

L150 ↗
EtaleFundamentalGroups.Kummer.higherRadicalFieldOverLower_root_isScalarTower
Documentation

The lower-to-higher root map and the two generic-fibre maps form the canonical scalar tower inside the common ambient field.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
universe uK uV uOmega uF
Lean source · full declaration
theorem higherRadicalFieldOverLower_root_isScalarTower
    {K : Type uK} {Omega : Type uOmega}
    [Field K] [Field Omega] [Algebra K Omega]
    (base : DVF.{uK, uV} K)
    {e N : ℕ} (he : 0 < e) (hN : 0 < N) (hdiv : e ∣ N)
    (varpi : base.valuationSubring) (hvarpiPrime : Prime varpi)
    (beta : Omega)
    (hbetaPow : beta ^ N = algebraMap K Omega (varpi : K)) :
    let V := base.valuationSubring
    let alpha := beta ^ (N / e)
    let Rₑ := AdjoinRoot (X ^ e - C varpi)
    let Rₙ := AdjoinRoot (X ^ N - C varpi)
    let F := lowerRadicalField (K := K) e N beta
    let K' := higherRadicalFieldOverLower (K := K) e N beta
    letI : Algebra V F :=
      ((algebraMap K F).comp (algebraMap V K)).toAlgebra
    letI : IsScalarTower V K F := IsScalarTower.of_algebraMap_eq' rfl
    let eRₑ : (K ⊗[V] Rₑ) ≃ₐ[K] F :=
      pureRadicalGenericFiberAlgEquiv he varpi hvarpiPrime alpha (by
        change (beta ^ (N / e)) ^ e =
          algebraMap K Omega (varpi : K)
        rw [← pow_mul]
        rw [Nat.div_mul_cancel hdiv, hbetaPow])
    letI : Algebra Rₑ F :=
      (genericFiberRightAlgHom eRₑ).toRingHom.toAlgebra
    letI : Algebra K K' :=
      ((algebraMap F K').comp (algebraMap K F)).toAlgebra
    letI : Algebra Rₑ K' :=
      ((algebraMap F K').comp (algebraMap Rₑ F)).toAlgebra
    letI : Algebra Rₙ K' :=
      higherRadicalFieldOverLowerRootAlgebra
        (e := e) base hN varpi hvarpiPrime beta hbetaPow
    let higherRootMap : Rₑ →ₐ[V] Rₙ :=
      adjoinRootPowerMapOfDvd hdiv varpi
    letI : Algebra Rₑ Rₙ := higherRootMap.toRingHom.toAlgebra
    IsScalarTower Rₑ Rₙ K' := by
  dsimp only
  let V := base.valuationSubring
  let alpha := beta ^ (N / e)
  let Rₑ := AdjoinRoot (X ^ e - C varpi)
  let Rₙ := AdjoinRoot (X ^ N - C varpi)
  let F := lowerRadicalField (K := K) e N beta
  let K' := higherRadicalFieldOverLower (K := K) e N beta
  let : IsFractionRing V K := base.valuationSubring_isFractionRing
  let : IsIntegrallyClosed V :=
    base.valuationSubring_isIntegrallyClosed
  let : Algebra V F :=
    ((algebraMap K F).comp (algebraMap V K)).toAlgebra
  let : IsScalarTower V K F := IsScalarTower.of_algebraMap_eq' rfl
  have halphaPow : alpha ^ e =
      algebraMap K Omega (varpi : K) := by
    rw [show alpha ^ e = beta ^ ((N / e) * e) by
      simp only [alpha, pow_mul]]
    rw [Nat.div_mul_cancel hdiv, hbetaPow]
  let eRₑ : (K ⊗[V] Rₑ) ≃ₐ[K] F :=
    pureRadicalGenericFiberAlgEquiv
      he varpi hvarpiPrime alpha halphaPow
  let : Algebra Rₑ F :=
    (genericFiberRightAlgHom eRₑ).toRingHom.toAlgebra
  let : Algebra K K' :=
    ((algebraMap F K').comp (algebraMap K F)).toAlgebra
  let : IsScalarTower K F K' := IsScalarTower.of_algebraMap_eq' rfl
  let : Algebra Rₑ K' :=
    ((algebraMap F K').comp (algebraMap Rₑ F)).toAlgebra
  let eRₙ : (K ⊗[V] Rₙ) ≃ₐ[K] K' :=
    higherRadicalFieldOverLowerGenericFiberAlgEquiv
      (e := e) base hN varpi hvarpiPrime beta hbetaPow
  let : Algebra V K' :=
    ((algebraMap K K').comp (algebraMap V K)).toAlgebra
  let : IsScalarTower V K K' := IsScalarTower.of_algebraMap_eq' rfl
  let : Algebra Rₙ K' :=
    higherRadicalFieldOverLowerRootAlgebra
      (e := e) base hN varpi hvarpiPrime beta hbetaPow
  let higherRootMap : Rₑ →ₐ[V] Rₙ :=
    adjoinRootPowerMapOfDvd hdiv varpi
  let : Algebra Rₑ Rₙ := higherRootMap.toRingHom.toAlgebra
  have hRₙRoot :
      (((genericFiberRightAlgHom eRₙ)
          (AdjoinRoot.root (X ^ N - C varpi)) : K') : Omega) = beta := by
    change (((pureRadicalGenericFiberAlgEquiv hN varpi hvarpiPrime beta
        hbetaPow) (1 ⊗ₜ[V] AdjoinRoot.root (X ^ N - C varpi)) :
      IntermediateField.adjoin K ({beta} : Set Omega)) : Omega) = beta
    exact congrArg Subtype.val
      (pureRadicalGenericFiberAlgEquiv_tmul_root
        hN varpi hvarpiPrime beta hbetaPow)
  have hRₙBase (z : V) :
      (((genericFiberRightAlgHom eRₙ)
          (algebraMap V Rₙ z) : K') : Omega) =
        algebraMap K Omega (z : K) := by
    rw [(genericFiberRightAlgHom eRₙ).commutes]
    rfl
  have hRₑBase (z : V) :
      ((algebraMap F K' ((genericFiberRightAlgHom eRₑ)
          (algebraMap V Rₑ z)) : K') : Omega) =
        algebraMap K Omega (z : K) := by
    rw [(genericFiberRightAlgHom eRₑ).commutes]
    rfl
  have hRₑRoot :
      (((genericFiberRightAlgHom eRₑ)
          (AdjoinRoot.root (X ^ e - C varpi)) : F) : Omega) = alpha := by
    change (((pureRadicalGenericFiberAlgEquiv he varpi hvarpiPrime alpha
        halphaPow) (1 ⊗ₜ[V] AdjoinRoot.root (X ^ e - C varpi)) :
      IntermediateField.adjoin K ({alpha} : Set Omega)) : Omega) = alpha
    exact congrArg Subtype.val
      (pureRadicalGenericFiberAlgEquiv_tmul_root
        he varpi hvarpiPrime alpha halphaPow)
  have hcomp :
      (genericFiberRightAlgHom eRₙ).toRingHom.comp higherRootMap.toRingHom =
        (algebraMap F K').comp (genericFiberRightAlgHom eRₑ).toRingHom := by
    exact higherRoot_genericMaps_comp_eq
      (K := K) (Omega := Omega) F K' varpi hdiv
      (genericFiberRightAlgHom eRₙ).toRingHom
      (genericFiberRightAlgHom eRₑ).toRingHom
      (fun z ↦ hRₙBase z |>.trans (hRₑBase z).symm)
      beta alpha hRₙRoot hRₑRoot rfl
  apply IsScalarTower.of_algebraMap_eq
  intro z
  change ((algebraMap F K').comp
      (genericFiberRightAlgHom eRₑ).toRingHom) z =
    ((genericFiberRightAlgHom eRₙ).toRingHom.comp
      higherRootMap.toRingHom) z
  exact DFunLike.congr_fun hcomp z |>.symm
def

higherRadicalFractionFieldAlgEquivHigherField

L275 ↗
EtaleFundamentalGroups.Kummer.higherRadicalFractionFieldAlgEquivHigherField
Documentation

Any chosen fraction field of the higher root ring is canonically equivalent, over that root ring, to the embedded higher radical field.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
universe uK uV uOmega uF
Lean source · full declaration
def higherRadicalFractionFieldAlgEquivHigherField
    {K : Type uK} {Omega : Type uOmega} {Froot : Type uF}
    [Field K] [Field Omega] [Field Froot] [Algebra K Omega]
    (base : DVF.{uK, uV} K)
    {e N : ℕ} (hN : 0 < N)
    (varpi : base.valuationSubring) (hvarpiPrime : Prime varpi)
    (beta : Omega)
    (hbetaPow : beta ^ N = algebraMap K Omega (varpi : K))
    [Algebra (AdjoinRoot (X ^ N - C varpi)) Froot]
    [IsFractionRing (AdjoinRoot (X ^ N - C varpi)) Froot] :
    let Rₙ := AdjoinRoot (X ^ N - C varpi)
    let F := lowerRadicalField (K := K) e N beta
    let K' := higherRadicalFieldOverLower (K := K) e N beta
    letI : Algebra K K' :=
      ((algebraMap F K').comp (algebraMap K F)).toAlgebra
    letI : Algebra Rₙ K' :=
      higherRadicalFieldOverLowerRootAlgebra
        (e := e) base hN varpi hvarpiPrime beta hbetaPow
    Froot ≃ₐ[Rₙ] K' := by
  dsimp only
  let Rₙ := AdjoinRoot (X ^ N - C varpi)
  let F := lowerRadicalField (K := K) e N beta
  let K' := higherRadicalFieldOverLower (K := K) e N beta
  letI : IsDomain Rₙ :=
    isDomain_adjoinRoot_X_pow_sub_C_of_prime hN varpi hvarpiPrime
  letI : Algebra K K' :=
    ((algebraMap F K').comp (algebraMap K F)).toAlgebra
  letI : Algebra Rₙ K' :=
    higherRadicalFieldOverLowerRootAlgebra
      (e := e) base hN varpi hvarpiPrime beta hbetaPow
  letI : IsFractionRing Rₙ K' :=
    higherRadicalFieldOverLower_isFractionRing
      (e := e) base hN varpi hvarpiPrime beta hbetaPow
  exact IsLocalization.algEquiv (nonZeroDivisors Rₙ) Froot K'

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