Module

Tower.lean

Nyll.SchemeTheory.AbhyankarLemma.Kummer.Tower

9 declarations indexed from sourceView source ↗

Module documentation

Ramification in towers of radical extensions

The ramification index is the cardinality of the actual value-group quotient. This file records its multiplicativity in a tower and then applies the one-radical calculation successively.

Imports2

Imported by4

theorem

tameResidueFieldMap_comp_in_tower

L35 ↗

AlgebraicNumberTheory.Valuations.tameResidueFieldMap_comp_in_tower

Documentation

The residue-field map of a valued tower is the composite of the two successive residue-field maps.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
open scoped IntermediateField
section ResidueTower
variable {K M L : Type u} [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]

Lean source · statement

theorem tameResidueFieldMap_comp_in_tower
    (v : LubinTate.Valuations.ExponentialValuation K)
    (u : LubinTate.Valuations.ExponentialValuation M)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hKM : ∀ a : K, u (algebraMap K M a) = v a)
    (hML : ∀ a : M, w (algebraMap M L a) = u a)
    (hKL : ∀ a : K, w (algebraMap K L a) = v a) :
    tameResidueFieldMap v w hKL =
      (tameResidueFieldMap u w hML).comp
        (tameResidueFieldMap v u hKM)

theorem

tameResidueFieldMap_surjective_left_of_comp

L65 ↗

AlgebraicNumberTheory.Valuations.tameResidueFieldMap_surjective_left_of_comp

Documentation

Surjectivity of the composite residue map implies surjectivity onto an intermediate residue field.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
open scoped IntermediateField
section ResidueTower
variable {K M L : Type u} [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]

Lean source · statement

theorem tameResidueFieldMap_surjective_left_of_comp
    (v : LubinTate.Valuations.ExponentialValuation K)
    (u : LubinTate.Valuations.ExponentialValuation M)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hKM : ∀ a : K, u (algebraMap K M a) = v a)
    (hML : ∀ a : M, w (algebraMap M L a) = u a)
    (hKL : ∀ a : K, w (algebraMap K L a) = v a)
    (hres : Function.Surjective (tameResidueFieldMap v w hKL)) :
    Function.Surjective (tameResidueFieldMap v u hKM)

theorem

tameResidueFieldMap_surjective_right_of_comp

L90 ↗

AlgebraicNumberTheory.Valuations.tameResidueFieldMap_surjective_right_of_comp

Documentation

Surjectivity of the composite residue map also implies surjectivity of the second map in the tower.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
open scoped IntermediateField
section ResidueTower
variable {K M L : Type u} [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]

Lean source · statement

theorem tameResidueFieldMap_surjective_right_of_comp
    (v : LubinTate.Valuations.ExponentialValuation K)
    (u : LubinTate.Valuations.ExponentialValuation M)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hKM : ∀ a : K, u (algebraMap K M a) = v a)
    (hML : ∀ a : M, w (algebraMap M L a) = u a)
    (hKL : ∀ a : K, w (algebraMap K L a) = v a)
    (hres : Function.Surjective (tameResidueFieldMap v w hKL)) :
    Function.Surjective (tameResidueFieldMap u w hML)

theorem

residueFiniteDimensional_for_tameResidueFieldMap

L114 ↗

AlgebraicNumberTheory.Valuations.residueFiniteDimensional_for_tameResidueFieldMap

Documentation

Finite-dimensionality transported from the quotient-induced residue module to the module induced by the chosen residue-field map.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
open scoped IntermediateField
section ResidueTower
variable {K M L : Type u} [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]

Lean source · full declaration

theorem residueFiniteDimensional_for_tameResidueFieldMap
    {F E : Type u} [Field F] [Field E] [Algebra F E]
    [FiniteDimensional F E]
    (v : LubinTate.Valuations.ExponentialValuation F)
    (w : LubinTate.Valuations.ExponentialValuation E)
    (hExt : ∀ a : F, w (algebraMap F E a) = v a) :
    let V := LubinTate.Valuations.exponentialValuationSubring v
    let W := LubinTate.Valuations.exponentialValuationSubring w
    let k := IsLocalRing.ResidueField V
    let ell := IsLocalRing.ResidueField W
    let f : k →+* ell := tameResidueFieldMap v w hExt
    letI : Algebra k ell := f.toAlgebra
    FiniteDimensional k ell := by
  let V := LubinTate.Valuations.exponentialValuationSubring v
  let W := LubinTate.Valuations.exponentialValuationSubring w
  let i := unramifiedValuationRingValuationRingMap v w hExt
  let : IsLocalHom i :=
    unramifiedValuationRingValuationRingMap_isLocalHom v w hExt
  let k := IsLocalRing.ResidueField V
  let ell := IsLocalRing.ResidueField W
  let f : k →+* ell := tameResidueFieldMap v w hExt
  let : Algebra k ell := f.toAlgebra
  let algebraModule : Module k ell :=
    (inferInstance : Algebra k ell).toModule
  let : Algebra V W := i.toAlgebra
  let residueModule : Module k ell :=
    @IsLocalRing.ResidueField.instModule
      V W _ _ _ _ (i.toAlgebra) inferInstance
  have hfinite :
      @FiniteDimensional k ell _ _ residueModule :=
    residueExtension_finiteDimensional_of_finiteDimensional
      v w hExt
  have hmodule : residueModule = algebraModule := by
    apply Module.ext
    funext r x
    obtain ⟨r, rfl⟩ := IsLocalRing.residue_surjective r
    obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective x
    rfl
  change @FiniteDimensional k ell _ _ algebraModule
  rw [← hmodule]
  exact hfinite

theorem

exponentialResidueDegree_eq_finrank_tameResidueFieldMap

L158 ↗

AlgebraicNumberTheory.Valuations.exponentialResidueDegree_eq_finrank_tameResidueFieldMap

Documentation

The residue degree is the finrank for the algebra induced by the chosen residue-field map.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
open scoped IntermediateField
section ResidueTower
variable {K M L : Type u} [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]

Lean source · full declaration

theorem exponentialResidueDegree_eq_finrank_tameResidueFieldMap
    {F E : Type u} [Field F] [Field E] [Algebra F E]
    (v : LubinTate.Valuations.ExponentialValuation F)
    (w : LubinTate.Valuations.ExponentialValuation E)
    (hExt : ∀ a : F, w (algebraMap F E a) = v a) :
    let V := LubinTate.Valuations.exponentialValuationSubring v
    let W := LubinTate.Valuations.exponentialValuationSubring w
    let k := IsLocalRing.ResidueField V
    let ell := IsLocalRing.ResidueField W
    let f : k →+* ell := tameResidueFieldMap v w hExt
    letI : Algebra k ell := f.toAlgebra
    exponentialResidueDegree v w hExt = Module.finrank k ell := by
  let V := LubinTate.Valuations.exponentialValuationSubring v
  let W := LubinTate.Valuations.exponentialValuationSubring w
  let k := IsLocalRing.ResidueField V
  let ell := IsLocalRing.ResidueField W
  let f : k →+* ell := tameResidueFieldMap v w hExt
  let : Algebra k ell := f.toAlgebra
  let algebraModule : Module k ell :=
    (inferInstance : Algebra k ell).toModule
  let i := exponentialValuationRingMap v w hExt
  let : IsLocalHom i :=
    exponentialValuationRingMap_isLocalHom v w hExt
  let : Algebra V W := i.toAlgebra
  let residueModule : Module k ell :=
    @IsLocalRing.ResidueField.instModule
      V W _ _ _ _ (i.toAlgebra) inferInstance
  have hmodule : residueModule = algebraModule := by
    apply Module.ext
    funext r x
    obtain ⟨r, rfl⟩ := IsLocalRing.residue_surjective r
    obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective x
    rfl
  change @Module.finrank k ell _ _ residueModule =
    @Module.finrank k ell _ _ algebraModule
  rw [hmodule]

theorem

exponentialResidueDegree_mul_in_tower

L197 ↗

AlgebraicNumberTheory.Valuations.exponentialResidueDegree_mul_in_tower

Documentation

The actual residue degree is multiplicative in a finite valued-field tower.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
open scoped IntermediateField
section ResidueTower
variable {K M L : Type u} [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]

Lean source · statement

theorem exponentialResidueDegree_mul_in_tower
    [FiniteDimensional K M] [FiniteDimensional M L]
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (u : LubinTate.Valuations.ExponentialValuation M)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hKM : ∀ a : K, u (algebraMap K M a) = v a)
    (hML : ∀ a : M, w (algebraMap M L a) = u a)
    (hKL : ∀ a : K, w (algebraMap K L a) = v a) :
    exponentialResidueDegree v u hKM * exponentialResidueDegree u w hML =
      exponentialResidueDegree v w hKL

theorem

exponentialResidueDegree_eq_one_of_surjective

L240 ↗

AlgebraicNumberTheory.Valuations.exponentialResidueDegree_eq_one_of_surjective

Documentation

A surjective actual residue-field map has residue degree one.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
open scoped IntermediateField
section ResidueTower
variable {K M L : Type u} [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]

Lean source · statement

theorem exponentialResidueDegree_eq_one_of_surjective
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hres : Function.Surjective (tameResidueFieldMap v w hExt)) :
    exponentialResidueDegree v w hExt = 1

theorem

tameResidueFieldMap_surjective_to_intermediate

L270 ↗

AlgebraicNumberTheory.Valuations.tameResidueFieldMap_surjective_to_intermediate

Documentation

If the residue map to the ambient field is onto, then so is the residue map to every intermediate field.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
open scoped IntermediateField
section IntermediateResidue
variable {K L : Type u} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem tameResidueFieldMap_surjective_to_intermediate
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hres : Function.Surjective (tameResidueFieldMap v w hExt))
    (E : IntermediateField K L) :
    Function.Surjective
      (tameResidueFieldMap v (exponentialValuationRestrict w E)
        (exponentialValuationRestrict_extends v w hExt E))

theorem

exponentialRamificationIndex_eq_finrank_of_radical_family

L298 ↗

AlgebraicNumberTheory.Valuations.exponentialRamificationIndex_eq_finrank_of_radical_family

Documentation

Successively adjoining finitely many prime-to-p radicals over a Henselian field, with no residue-field extension, gives a totally ramified extension. This is the degree calculation used in tame radical generation.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
open scoped IntermediateField
section RadicalTower
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]

Lean source · statement

theorem exponentialRamificationIndex_eq_finrank_of_radical_family
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hp : PositiveResidueCharacteristic v)
    (hres : Function.Surjective (tameResidueFieldMap v w hExt))
    (r : ℕ) (m : Fin r → ℕ) (a : Fin r → K) (α : Fin r → L)
    (hmpos : ∀ i, 0 < m i)
    (hmcop : ∀ i, Nat.Coprime (m i) (residueCharacteristic v))
    (hpow : ∀ i, α i ^ m i = algebraMap K L (a i))
    (hgen : IntermediateField.adjoin K (Set.range α) = ⊤) :
    exponentialRamificationIndex v w = Module.finrank K L

Module documentation

Ramification in towers of radical extensions

Declarations