NYLL
Module

BasicInvariants.lean

Nyll.ValuedFieldTheory.LocalField.Unramified.BasicInvariants
11 declarations indexed from sourceView source ↗

Module documentation

Value-group invariants of finite unramified extensions

The first finite step in the unramified base-change theorem is forced already by the finite unramified-extension definition and the fundamental inequality of the fundamental inequality. The actual quotient of value groups is finite; degree equality then forces its cardinality to be one, and hence the source and target value subgroups coincide.

Imports2
Imported by5

Declarations

theorem

exponentialValueCoset_units_surjective

L35 ↗
AlgebraicNumberTheory.Valuations.exponentialValueCoset_units_surjective
Documentation

Every class of the actual value-group quotient has a representative in Lˣ. This is the public representative source needed to apply the arbitrary linear-independence theorem from the fundamental inequality.

Source context 7 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Module
section FiniteValuedExtensionInvariants
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
omit [Algebra K L] in
Lean source · full declaration
theorem exponentialValueCoset_units_surjective
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    Function.Surjective
      (fun x : Lˣ ↦ exponentialValueCoset v w (x : L) x.ne_zero) := by
  intro q
  obtain ⟨gamma, hgamma⟩ := QuotientAddGroup.mk_surjective q
  obtain ⟨x, hx, hvalue⟩ := gamma.property
  refine ⟨Units.mk0 x hx, ?_⟩
  rw [← hgamma]
  unfold exponentialValueCoset
  apply congrArg QuotientAddGroup.mk
  apply Subtype.ext
  simp [hvalue]
theorem

exponentialValueGroupQuotient_finite_of_finiteDimensional

L57 ↗
AlgebraicNumberTheory.Valuations.exponentialValueGroupQuotient_finite_of_finiteDimensional
Documentation

For a finite-dimensional valued extension, the actual quotient w(Lˣ) / v(Kˣ) is finite.

The proof is the one-element residue-lift specialization of the fundamental inequality: representatives of distinct value cosets form a linearly independent family over K, so their indexing type is finite in the finite-dimensional space L.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Module
section FiniteValuedExtensionInvariants
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exponentialValueGroupQuotient_finite_of_finiteDimensional
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    Finite (ExponentialValueGroupQuotient v w)
theorem

exponentialRamificationIndex_pos_of_finiteDimensional

L108 ↗
AlgebraicNumberTheory.Valuations.exponentialRamificationIndex_pos_of_finiteDimensional
Documentation

The value-group ramification index of a finite-dimensional exact valued extension is positive.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Module
section FiniteValuedExtensionInvariants
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exponentialRamificationIndex_pos_of_finiteDimensional
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    0 < exponentialRamificationIndex v w
theorem

residueBasisLifts_linearIndependent

L127 ↗
AlgebraicNumberTheory.Valuations.residueBasisLifts_linearIndependent
Documentation

Lifts to the target valuation ring of an arbitrary residue-field basis are linearly independent over the base field.

This is the one-value-coset specialization of the public arbitrary-index linear-independence theorem in the fundamental inequality. No finiteness or separability hypothesis on L/K is used.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Module
section FiniteValuedExtensionInvariants
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · full declaration
theorem residueBasisLifts_linearIndependent
    {J : Type*}
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (beta :
      let V := LubinTate.Valuations.exponentialValuationSubring v
      let W := LubinTate.Valuations.exponentialValuationSubring w
      let i := unramifiedValuationRingValuationRingMap v w hExt
      letI : IsLocalHom i :=
        unramifiedValuationRingValuationRingMap_isLocalHom v w hExt
      letI : Algebra V W := i.toAlgebra
      letI : Algebra (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) :=
        (IsLocalRing.ResidueField.map i).toAlgebra
      Basis J (IsLocalRing.ResidueField V)
        (IsLocalRing.ResidueField W))
    (omega : J → LubinTate.Valuations.exponentialValuationSubring w)
    (homega :
      let W := LubinTate.Valuations.exponentialValuationSubring w
      ∀ j, IsLocalRing.residue W (omega j) = beta j) :
    LinearIndependent K (fun j ↦ (omega j : L)) := 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 : Algebra V W := i.toAlgebra
  let : Algebra (IsLocalRing.ResidueField V)
      (IsLocalRing.ResidueField W) :=
    (IsLocalRing.ResidueField.map i).toAlgebra
  have homegaLI : LinearIndependent (IsLocalRing.ResidueField V)
      (fun j ↦ IsLocalRing.residue W (omega j)) := by
    rw [show (fun j ↦ IsLocalRing.residue W (omega j)) = beta from
      funext homega]
    exact beta.linearIndependent
  let piOne : Unit → L := fun _ ↦ 1
  have hpiOne : DistinctExponentialValueCosetRepresentatives v w piOne := by
    refine ⟨by intro; simp [piOne], ?_⟩
    intro a b hab
    exact (hab (Subsingleton.elim a b)).elim
  have hprod : LinearIndependent K
      (fun p : Unit × J ↦ (omega p.2 : L) * piOne p.1) :=
    ramificationInvariants_valueCosets_mul_residueLifts_linearIndependent_arbitrary
      v w hExt piOne hpiOne omega homegaLI
  have hcomp := hprod.comp (fun j ↦ ((), j)) (by
    intro a b hab
    exact congrArg Prod.snd hab)
  simpa only [Function.comp_def, piOne, mul_one] using hcomp
theorem

residueExtension_finiteDimensional_of_finiteDimensional

L180 ↗
AlgebraicNumberTheory.Valuations.residueExtension_finiteDimensional_of_finiteDimensional
Documentation

In every finite-dimensional valued field extension, the actual residue extension is finite-dimensional. Its finiteness is produced by lifting a chosen residue basis and applying the preceding linear-independence theorem.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Module
section FiniteValuedExtensionInvariants
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · full declaration
theorem residueExtension_finiteDimensional_of_finiteDimensional
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    let V := LubinTate.Valuations.exponentialValuationSubring v
    let W := LubinTate.Valuations.exponentialValuationSubring w
    let i := unramifiedValuationRingValuationRingMap v w hExt
    letI : IsLocalHom i :=
      unramifiedValuationRingValuationRingMap_isLocalHom v w hExt
    letI : Algebra V W := i.toAlgebra
    letI : Algebra (IsLocalRing.ResidueField V)
        (IsLocalRing.ResidueField W) :=
      (IsLocalRing.ResidueField.map i).toAlgebra
    FiniteDimensional (IsLocalRing.ResidueField V)
      (IsLocalRing.ResidueField W) := by
  classical
  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 : Algebra V W := i.toAlgebra
  let k := IsLocalRing.ResidueField V
  let ell := IsLocalRing.ResidueField W
  let : Algebra k ell := (IsLocalRing.ResidueField.map i).toAlgebra
  let J := Module.Free.ChooseBasisIndex k ell
  let beta : Basis J k ell := Module.Free.chooseBasis k ell
  let omega : J → W := fun j ↦
    Classical.choose (IsLocalRing.residue_surjective (beta j))
  have homega : ∀ j, IsLocalRing.residue W (omega j) = beta j := by
    intro j
    exact Classical.choose_spec (IsLocalRing.residue_surjective (beta j))
  have hli : LinearIndependent K (fun j ↦ (omega j : L)) :=
    residueBasisLifts_linearIndependent v w hExt beta omega homega
  have hfiniteJ : Finite J := hli.finite
  let : Finite J := hfiniteJ
  exact beta.finiteDimensional_of_finite
theorem

exponentialResidueDegree_pos_of_finiteDimensional

L221 ↗
AlgebraicNumberTheory.Valuations.exponentialResidueDegree_pos_of_finiteDimensional
Documentation

The residue degree of a finite-dimensional exact valued extension is positive.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Module
section FiniteValuedExtensionInvariants
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exponentialResidueDegree_pos_of_finiteDimensional
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    0 < exponentialResidueDegree v w hExt
theorem

exponentialRamificationIndex_le_finrank

L245 ↗
AlgebraicNumberTheory.Valuations.exponentialRamificationIndex_le_finrank
Documentation

The value-group ramification index of a finite-dimensional exact valued extension is at most its field degree.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Module
section FiniteValuedExtensionInvariants
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exponentialRamificationIndex_le_finrank
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    exponentialRamificationIndex v w ≤ Module.finrank K L
theorem

finiteUnramifiedExtension_residueBasis_card_eq_finrank

L259 ↗
AlgebraicNumberTheory.Valuations.finiteUnramifiedExtension_residueBasis_card_eq_finrank
Documentation

Under the finite unramified-extension definition, every residue basis has the same cardinality as the field degree. The statement uses Nat.card, so no finiteness assumption on the chosen index type is added to the theorem boundary.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Module
section FiniteValuedExtensionInvariants
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · full declaration
theorem finiteUnramifiedExtension_residueBasis_card_eq_finrank
    [FiniteDimensional K L] {J : Type*}
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hUnramified : FiniteUnramifiedExtension v w hExt)
    (beta :
      let V := LubinTate.Valuations.exponentialValuationSubring v
      let W := LubinTate.Valuations.exponentialValuationSubring w
      let i := unramifiedValuationRingValuationRingMap v w hExt
      letI : IsLocalHom i :=
        unramifiedValuationRingValuationRingMap_isLocalHom v w hExt
      letI : Algebra V W := i.toAlgebra
      letI : Algebra (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) :=
        (IsLocalRing.ResidueField.map i).toAlgebra
      Basis J (IsLocalRing.ResidueField V)
        (IsLocalRing.ResidueField W))
    (omega : J → LubinTate.Valuations.exponentialValuationSubring w)
    (homega :
      let W := LubinTate.Valuations.exponentialValuationSubring w
      ∀ j, IsLocalRing.residue W (omega j) = beta j) :
    Nat.card J = Module.finrank K L := 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 : Algebra V W := i.toAlgebra
  let k := IsLocalRing.ResidueField V
  let ell := IsLocalRing.ResidueField W
  let : Algebra k ell := (IsLocalRing.ResidueField.map i).toAlgebra
  have hli : LinearIndependent K (fun j ↦ (omega j : L)) :=
    residueBasisLifts_linearIndependent v w hExt beta omega homega
  have hfiniteJ : Finite J := hli.finite
  let : Finite J := hfiniteJ
  let : Fintype J := Fintype.ofFinite J
  have hresfinite : FiniteDimensional k ell :=
    beta.finiteDimensional_of_finite
  let : FiniteDimensional k ell := hresfinite
  have hdegree :=
    finiteUnramifiedExtension_degree_eq_residueDegree
      v w hExt hUnramified
  change Module.finrank K L = Module.finrank k ell at hdegree
  calc
    Nat.card J = Fintype.card J := Nat.card_eq_fintype_card
    _ = Module.finrank k ell := (Module.finrank_eq_card_basis beta).symm
    _ = Module.finrank K L := hdegree.symm
theorem

exists_basis_eq_residueBasisLifts_of_finiteUnramifiedExtension

L311 ↗
AlgebraicNumberTheory.Valuations.exists_basis_eq_residueBasisLifts_of_finiteUnramifiedExtension
Documentation

Valuation-ring lifts of any chosen residue basis form a basis of L/K for a finite unramified extension. Finiteness and nonemptiness of the index type are derived internally rather than assumed.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Module
section FiniteValuedExtensionInvariants
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · full declaration
theorem exists_basis_eq_residueBasisLifts_of_finiteUnramifiedExtension
    [FiniteDimensional K L] {J : Type*}
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hUnramified : FiniteUnramifiedExtension v w hExt)
    (beta :
      let V := LubinTate.Valuations.exponentialValuationSubring v
      let W := LubinTate.Valuations.exponentialValuationSubring w
      let i := unramifiedValuationRingValuationRingMap v w hExt
      letI : IsLocalHom i :=
        unramifiedValuationRingValuationRingMap_isLocalHom v w hExt
      letI : Algebra V W := i.toAlgebra
      letI : Algebra (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) :=
        (IsLocalRing.ResidueField.map i).toAlgebra
      Basis J (IsLocalRing.ResidueField V)
        (IsLocalRing.ResidueField W))
    (omega : J → LubinTate.Valuations.exponentialValuationSubring w)
    (homega :
      let W := LubinTate.Valuations.exponentialValuationSubring w
      ∀ j, IsLocalRing.residue W (omega j) = beta j) :
    ∃ b : Basis J K L, ∀ j, b j = (omega j : L) := by
  have hli : LinearIndependent K (fun j ↦ (omega j : L)) :=
    residueBasisLifts_linearIndependent v w hExt beta omega homega
  have hfiniteJ : Finite J := hli.finite
  let : Finite J := hfiniteJ
  let : Fintype J := Fintype.ofFinite J
  have hcardNat : Nat.card J = Module.finrank K L :=
    finiteUnramifiedExtension_residueBasis_card_eq_finrank
      v w hExt hUnramified beta omega homega
  have hcard : Fintype.card J = Module.finrank K L := by
    rw [← Nat.card_eq_fintype_card]
    exact hcardNat
  have hcardpos : 0 < Fintype.card J := by
    rw [hcard]
    exact Module.finrank_pos
  let : Nonempty J := Fintype.card_pos_iff.mp hcardpos
  let b : Basis J K L :=
    basisOfLinearIndependentOfCardEqFinrank hli hcard
  refine ⟨b, ?_⟩
  intro j
  exact congrFun
    (coe_basisOfLinearIndependentOfCardEqFinrank hli hcard) j
theorem

exponentialRamificationIndex_eq_one_of_finiteUnramifiedExtension

L359 ↗
AlgebraicNumberTheory.Valuations.exponentialRamificationIndex_eq_one_of_finiteUnramifiedExtension
Documentation

the finite unramified-extension definition and the fundamental inequality force the actual ramification index of a finite unramified extension to be one.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Module
section FiniteValuedExtensionInvariants
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exponentialRamificationIndex_eq_one_of_finiteUnramifiedExtension
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hUnramified : FiniteUnramifiedExtension v w hExt) :
    exponentialRamificationIndex v w = 1
theorem

exponentialValueSubgroup_eq_of_finiteUnramifiedExtension

L391 ↗
AlgebraicNumberTheory.Valuations.exponentialValueSubgroup_eq_of_finiteUnramifiedExtension
Documentation

The value subgroup does not change in a finite unramified extension.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Module
section FiniteValuedExtensionInvariants
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exponentialValueSubgroup_eq_of_finiteUnramifiedExtension
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hUnramified : FiniteUnramifiedExtension v w hExt) :
    exponentialValueSubgroup w = exponentialValueSubgroup v

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