Nyll.ValuedFieldTheory.LocalField.Unramified.MaximalResidue

theorem

maximalUnramifiedSubextension_valueSubgroup_eq

AlgebraicNumberTheory.Valuations.maximalUnramifiedSubextension_valueSubgroup_eq

Documentation

the maximal-residue theorem, exact value-group equality for the maximal unramified subextension.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section MaximalUnramifiedSubextensionInvariants
variable {K L : Type u} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem maximalUnramifiedSubextension_valueSubgroup_eq
    (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) :
    exponentialValueSubgroup
        (exponentialValuationRestrict w
          (maximalUnramifiedSubextension v w hExt)) =
      exponentialValueSubgroup v

theorem

maximalUnramifiedSubextension_residue_fieldRange_le_separableClosure

L73 ↗

AlgebraicNumberTheory.Valuations.maximalUnramifiedSubextension_residue_fieldRange_le_separableClosure

Documentation

the maximal-residue theorem, the residue field of T embeds into the separable closure of the base residue field in the ambient residue field.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section MaximalUnramifiedSubextensionInvariants
variable {K L : Type u} [Field K] [Field L] [Algebra K L]

Lean source · full declaration

theorem maximalUnramifiedSubextension_residue_fieldRange_le_separableClosure
    (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) :
    let T := maximalUnramifiedSubextension v w hExt
    let wT := exponentialValuationRestrict w T
    let V := LubinTate.Valuations.exponentialValuationSubring v
    let VT := LubinTate.Valuations.exponentialValuationSubring wT
    let W := LubinTate.Valuations.exponentialValuationSubring w
    let i := unramifiedValuationRingValuationRingMap v wT
      (exponentialValuationRestrict_extends v w hExt T)
    let b := unramifiedValuationRingValuationRingMap v w hExt
    letI : IsLocalHom i :=
      unramifiedValuationRingValuationRingMap_isLocalHom v wT
        (exponentialValuationRestrict_extends v w hExt T)
    letI : IsLocalHom b :=
      unramifiedValuationRingValuationRingMap_isLocalHom v w hExt
    let k := IsLocalRing.ResidueField V
    let kT := IsLocalRing.ResidueField VT
    let ell := IsLocalRing.ResidueField W
    letI : Algebra k kT := (IsLocalRing.ResidueField.map i).toAlgebra
    letI : Algebra k ell := (IsLocalRing.ResidueField.map b).toAlgebra
    (restrictedResidueAlgHomToAmbient v w hExt T).fieldRange ≤
      separableClosure k ell := by
  classical
  simp only
  intro y hy
  rcases hy with ⟨yT, rfl⟩
  let T := maximalUnramifiedSubextension v w hExt
  let wT := exponentialValuationRestrict w T
  let VT := LubinTate.Valuations.exponentialValuationSubring wT
  obtain ⟨t, rfl⟩ := IsLocalRing.residue_surjective yT
  obtain ⟨E, htE, hEunramified⟩ :=
    exists_finiteUnramifiedSubextension_of_mem_maximal
      v w hExt hhens (show ((t : T) : L) ∈ T from (t : T).property)
  let wE := exponentialValuationRestrict w E
  let VE := LubinTate.Valuations.exponentialValuationSubring wE
  let z : VE :=
    ⟨⟨((t : T) : L), htE⟩, by
      change (0 : WithTop ℝ) ≤ w ((t : T) : L)
      exact t.property⟩
  have hz :=
    finiteUnramifiedSubextension_residue_image_mem_separableClosure
      v w hExt hEunramified (IsLocalRing.residue VE z)
  exact hz

MaximalResidue.lean

Module documentation

The maximal unramified subextension from residue-field data

maximalUnramifiedSubextension_valueSubgroup_eq

maximalUnramifiedSubextension_residue_fieldRange_le_separableClosure

Module documentation

The maximal unramified subextension from residue-field data

Declarations

maximalUnramifiedSubextension_valueSubgroup_eq

maximalUnramifiedSubextension_residue_fieldRange_le_separableClosure