Module

RamificationInvariants.lean

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.RamificationInvariants

42 declarations indexed from sourceView source ↗

Module documentation

the fundamental inequality and identity

The first part follows the proof on pp. 149--150: residue-basis lifts are multiplied by representatives of distinct value-group cosets, and the resulting family is linearly independent over the base field. The second part uses the actual valuation rings. For a discrete Henselian base and a finite separable extension, the finite norm-formula theorem identifies the target valuation ring with the integral closure, so the local Dedekind ramification identity applies without completeness.

Imports8

Nyll.ValuedFieldTheory.Valuation.Henselian.UniqueAlgebraicExtensions
Mathlib.LinearAlgebra.Dimension.Finrank
Mathlib.LinearAlgebra.Dimension.Free
Mathlib.Algebra.Order.WithTop.Untop0
Mathlib.GroupTheory.Index
Mathlib.Data.ZMod.QuotientGroup
Mathlib.Algebra.Algebra.Tower
Nyll.ValuedFieldTheory.Valuation.LocalRingEquiv

Imported by12

def

ramificationAddValuation

L37 ↗

AlgebraicNumberTheory.Valuations.ramificationAddValuation

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

def ramificationAddValuation {K : Type*} [Field K]
    (v : LubinTate.Valuations.ExponentialValuation K) : AddValuation K (WithTop ℝ)

theorem

ramificationAddValuation_apply

L45 ↗

AlgebraicNumberTheory.Valuations.ramificationAddValuation_apply

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem ramificationAddValuation_apply {K : Type*} [Field K]
    (v : LubinTate.Valuations.ExponentialValuation K) (x : K) :
    ramificationAddValuation v x = v x

theorem

ramificationAddValuation_finset_sum_eq_of_unique_min

L50 ↗

AlgebraicNumberTheory.Valuations.ramificationAddValuation_finset_sum_eq_of_unique_min

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem ramificationAddValuation_finset_sum_eq_of_unique_min
    {K I : Type*} [Field K]
    (v : LubinTate.Valuations.ExponentialValuation K) (s : Finset I) (f : I → K) (j : I)
    (hj : j ∈ s) (hjtop : v (f j) ≠ ⊤)
    (hmin : ∀ i ∈ s, i ≠ j → v (f j) < v (f i)) :
    v (∑ i ∈ s, f i) = v (f j)

theorem

exponentialValuation_finset_sum_ne_zero_of_value_ne

L65 ↗

AlgebraicNumberTheory.Valuations.exponentialValuation_finset_sum_ne_zero_of_value_ne

Documentation

A finite sum of nonzero terms of pairwise distinct values cannot vanish.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem exponentialValuation_finset_sum_ne_zero_of_value_ne
    {K I : Type*} [Field K]
    (v : LubinTate.Valuations.ExponentialValuation K) (s : Finset I) (f : I → K)
    (hne : ∃ i ∈ s, f i ≠ 0)
    (hpair : ∀ i ∈ s, ∀ j ∈ s, i ≠ j →
      f i ≠ 0 → f j ≠ 0 → v (f i) ≠ v (f j)) :
    ∑ i ∈ s, f i ≠ 0

def

exponentialValuationRingMap

L102 ↗

AlgebraicNumberTheory.Valuations.exponentialValuationRingMap

Documentation

The map of valuation rings induced by an exact extension of exponential exponential valuations.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

def exponentialValuationRingMap
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    LubinTate.Valuations.exponentialValuationSubring v →+*
      LubinTate.Valuations.exponentialValuationSubring w

theorem

exponentialValuationRingMap_apply

L115 ↗

AlgebraicNumberTheory.Valuations.exponentialValuationRingMap_apply

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem exponentialValuationRingMap_apply
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (a : LubinTate.Valuations.exponentialValuationSubring v) :
    ((exponentialValuationRingMap v w hExt a :
      LubinTate.Valuations.exponentialValuationSubring w) : L) =
        algebraMap K L (a : K)

theorem

exponentialValuationRingMap_isLocalHom

L127 ↗

AlgebraicNumberTheory.Valuations.exponentialValuationRingMap_isLocalHom

Documentation

Exact extension makes the induced map of valuation rings local.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem exponentialValuationRingMap_isLocalHom
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    IsLocalHom (exponentialValuationRingMap v w hExt)

theorem

exponentialValuation_residueCombination_value_zero

L147 ↗

AlgebraicNumberTheory.Valuations.exponentialValuation_residueCombination_value_zero

Documentation

A nontrivial residue-linear combination of lifts is a unit in the target valuation ring. This is the residue-basis step in the proof of the fundamental inequality.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

theorem exponentialValuation_residueCombination_value_zero
    {K L J : Type*} [Field K] [Field L] [Algebra K L]
    [Fintype J]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (omega : J → LubinTate.Valuations.exponentialValuationSubring w)
    (homega :
      let V := LubinTate.Valuations.exponentialValuationSubring v
      let W := LubinTate.Valuations.exponentialValuationSubring w
      let i := exponentialValuationRingMap v w hExt
      letI : Algebra V W := i.toAlgebra
      letI : IsLocalHom i :=
        exponentialValuationRingMap_isLocalHom v w hExt
      letI : Algebra (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) :=
        (IsLocalRing.ResidueField.map i).toAlgebra
      LinearIndependent (IsLocalRing.ResidueField V)
        (fun j ↦ IsLocalRing.residue W (omega j)))
    (c : J → LubinTate.Valuations.exponentialValuationSubring v)
    (hc : ∃ j, IsLocalRing.residue
      (LubinTate.Valuations.exponentialValuationSubring v) (c j) ≠ 0) :
    w (∑ j, algebraMap K L (c j : K) * (omega j : L)) = 0 := by
  classical
  let V := LubinTate.Valuations.exponentialValuationSubring v
  let W := LubinTate.Valuations.exponentialValuationSubring w
  let i := exponentialValuationRingMap v w hExt
  let : IsLocalHom i :=
    exponentialValuationRingMap_isLocalHom v w hExt
  let : Algebra V W := i.toAlgebra
  let : Algebra (IsLocalRing.ResidueField V)
      (IsLocalRing.ResidueField W) :=
    (IsLocalRing.ResidueField.map i).toAlgebra
  let s : W := ∑ j, i (c j) * omega j
  have hres_ne : IsLocalRing.residue W s ≠ 0 := by
    intro hs
    have hcoeff_zero :
        ∀ j, IsLocalRing.residue V (c j) = 0 := by
      apply (Fintype.linearIndependent_iff.mp homega
        (fun j ↦ IsLocalRing.residue V (c j)))
      rw [← hs]
      dsimp only [s]
      simp only [map_sum, map_mul]
      apply Finset.sum_congr rfl
      intro j _hj
      rw [← IsLocalRing.ResidueField.map_residue i]
      rfl
    rcases hc with ⟨j, hj⟩
    exact hj (hcoeff_zero j)
  have hsunit : IsUnit s := by
    exact (IsLocalRing.residue_ne_zero_iff_isUnit s).mp hres_ne
  have hsvalue : w (s : L) = 0 :=
    LubinTate.Valuations.exponentialValuation_eq_zero_of_isUnit w hsunit
  have hs_coe :
      (s : L) = ∑ j, algebraMap K L (c j : K) * (omega j : L) := by
    dsimp only [s]
    change W.subtype (∑ j, i (c j) * omega j) = _
    rw [map_sum]
    apply Finset.sum_congr rfl
    intro j _hj
    congr 1
  rw [hs_coe] at hsvalue
  exact hsvalue

theorem

exponentialValuation_div_nonneg_of_le

L213 ↗

AlgebraicNumberTheory.Valuations.exponentialValuation_div_nonneg_of_le

Documentation

Dividing by an element of no larger value produces an element of the valuation ring.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem exponentialValuation_div_nonneg_of_le
    {K : Type*} [Field K] (v : LubinTate.Valuations.ExponentialValuation K)
    {a b : K} (hb : b ≠ 0) (hba : v b ≤ v a) :
    (0 : WithTop ℝ) ≤ v (a / b)

theorem

exponentialValuation_residueCombination_value_in_base

L232 ↗

AlgebraicNumberTheory.Valuations.exponentialValuation_residueCombination_value_in_base

Documentation

A nonzero linear combination of residue-basis lifts has the value of one of its nonzero base coefficients.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

theorem exponentialValuation_residueCombination_value_in_base
    {K L J : Type*} [Field K] [Field L] [Algebra K L]
    [Fintype J]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (omega : J → LubinTate.Valuations.exponentialValuationSubring w)
    (homega :
      let V := LubinTate.Valuations.exponentialValuationSubring v
      let W := LubinTate.Valuations.exponentialValuationSubring w
      let i := exponentialValuationRingMap v w hExt
      letI : Algebra V W := i.toAlgebra
      letI : IsLocalHom i :=
        exponentialValuationRingMap_isLocalHom v w hExt
      letI : Algebra (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) :=
        (IsLocalRing.ResidueField.map i).toAlgebra
      LinearIndependent (IsLocalRing.ResidueField V)
        (fun j ↦ IsLocalRing.residue W (omega j)))
    (a : J → K) (ha : ∃ j, a j ≠ 0) :
    ∃ a₀ : K, a₀ ≠ 0 ∧
      w (∑ j, algebraMap K L (a j) * (omega j : L)) =
        w (algebraMap K L a₀) := by
  classical
  let S : Finset J := Finset.univ.filter fun j ↦ a j ≠ 0
  have hS : S.Nonempty := by
    rcases ha with ⟨j, hj⟩
    exact ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hj⟩⟩
  obtain ⟨j₀, hj₀S, hj₀min⟩ :=
    S.exists_min_image (fun j ↦ v (a j)) hS
  have hj₀ : a j₀ ≠ 0 := (Finset.mem_filter.mp hj₀S).2
  let c : J → LubinTate.Valuations.exponentialValuationSubring v := fun j ↦
    ⟨a j / a j₀, by
      by_cases hj : a j = 0
      · simp [hj]
      · apply exponentialValuation_div_nonneg_of_le v hj₀
        exact hj₀min j (Finset.mem_filter.mpr ⟨Finset.mem_univ _, hj⟩)⟩
  have hcj₀ : IsLocalRing.residue
      (LubinTate.Valuations.exponentialValuationSubring v) (c j₀) ≠ 0 := by
    have hcj₀eq : c j₀ = 1 := by
      ext
      simp [c, hj₀]
    rw [hcj₀eq, map_one]
    exact one_ne_zero
  have hcvalue :=
    exponentialValuation_residueCombination_value_zero
      v w hExt omega homega c ⟨j₀, hcj₀⟩
  have hfactor :
      (∑ j, algebraMap K L (a j) * (omega j : L)) =
        algebraMap K L (a j₀) *
          (∑ j, algebraMap K L (c j : K) * (omega j : L)) := by
    rw [Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro j hj
    simp only [c]
    rw [← mul_assoc, ← map_mul]
    field_simp
  refine ⟨a j₀, hj₀, ?_⟩
  rw [hfactor, w.map_mul, hcvalue, add_zero]

def

exponentialValueSubgroup

L294 ↗

AlgebraicNumberTheory.Valuations.exponentialValueSubgroup

Documentation

The actual additive value group v(Kˣ), realized as a subgroup of ℝ.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

def exponentialValueSubgroup
    {K : Type*} [Field K] (v : LubinTate.Valuations.ExponentialValuation K) :
    AddSubgroup ℝ where
  carrier := {r | ∃ x : K, x ≠ 0 ∧ v x = (r : WithTop ℝ)}
  zero_mem' := ⟨1, one_ne_zero, by simp⟩
  add_mem' := by
    rintro r s ⟨x, hx, hr⟩ ⟨y, hy, hs⟩
    refine ⟨x * y, mul_ne_zero hx hy, ?_⟩
    rw [v.map_mul, hr, hs, WithTop.coe_add]
  neg_mem' := by
    rintro r ⟨x, hx, hr⟩
    refine ⟨x⁻¹, inv_ne_zero hx, ?_⟩
    exact LubinTate.Valuations.exponentialValuation_inv_value v hx hr

theorem

discreteExponentialValuation_of_isDiscreteValuationRing

L310 ↗

AlgebraicNumberTheory.Valuations.discreteExponentialValuation_of_isDiscreteValuationRing

Documentation

Conversely to the valuation-ring criterion, if the valuation ring attached to an exponential exponential valuation is a DVR, its real value group is discrete.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem discreteExponentialValuation_of_isDiscreteValuationRing
    {K : Type*} [Field K] (v : LubinTate.Valuations.ExponentialValuation K)
    [IsDiscreteValuationRing (LubinTate.Valuations.exponentialValuationSubring v)] :
    LubinTate.Valuations.DiscreteExponentialValuation v

theorem

discretePrimeElement_zpow_value_scaled

L370 ↗

AlgebraicNumberTheory.Valuations.discretePrimeElement_zpow_value_scaled

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem discretePrimeElement_zpow_value_scaled
    {K : Type*} [Field K] (v : LubinTate.Valuations.ExponentialValuation K)
    {pi : K} {s : ℝ} (hpi0 : pi ≠ 0)
    (hpival : v pi = (s : WithTop ℝ)) (m : ℤ) :
    v (pi ^ m) = ((((m : ℝ) * s : ℝ)) : WithTop ℝ)

theorem

exponentialValueSubgroup_eq_zmultiples

L392 ↗

AlgebraicNumberTheory.Valuations.exponentialValueSubgroup_eq_zmultiples

Documentation

A discrete value group with least positive value s is literally the cyclic subgroup sℤ of ℝ.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem exponentialValueSubgroup_eq_zmultiples
    {K : Type*} [Field K] (v : LubinTate.Valuations.ExponentialValuation K)
    {s : ℝ}
    (hvalues : ∀ x : K, x ≠ 0 → ∃ m : ℤ,
      v x = ((((m : ℝ) * s : ℝ)) : WithTop ℝ))
    {pi : K} (hpival : v pi = (s : WithTop ℝ)) :
    exponentialValueSubgroup v = AddSubgroup.zmultiples s

theorem

maximalIdeal_eq_span_discretePrimeElement

L419 ↗

AlgebraicNumberTheory.Valuations.maximalIdeal_eq_span_discretePrimeElement

Documentation

The element of least positive discrete discrete value generates the maximal ideal of its valuation ring.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem maximalIdeal_eq_span_discretePrimeElement
    {K : Type*} [Field K] (v : LubinTate.Valuations.ExponentialValuation K)
    {s : ℝ} (hs : 0 < s)
    (hvalues : ∀ x : K, x ≠ 0 → ∃ m : ℤ,
      v x = ((((m : ℝ) * s : ℝ)) : WithTop ℝ))
    {pi : K} (hpival : v pi = (s : WithTop ℝ)) :
    IsLocalRing.maximalIdeal (LubinTate.Valuations.exponentialValuationSubring v) =
      Ideal.span (Set.singleton (LubinTate.Valuations.discretePrimeElementInValuationSubring
        v hs.le hpival) : Set (LubinTate.Valuations.exponentialValuationSubring v))

theorem

exists_valueGroup_generators_scaled_by_ramificationIdx

L469 ↗

AlgebraicNumberTheory.Valuations.exists_valueGroup_generators_scaled_by_ramificationIdx

Documentation

The ideal-theoretic ramification index is exactly the scaling factor between the least positive generators of the two discrete value groups.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

theorem exists_valueGroup_generators_scaled_by_ramificationIdx
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hv : LubinTate.Valuations.DiscreteExponentialValuation v)
    (hw : LubinTate.Valuations.DiscreteExponentialValuation w)
    [IsDiscreteValuationRing (LubinTate.Valuations.exponentialValuationSubring v)]
    [IsDiscreteValuationRing (LubinTate.Valuations.exponentialValuationSubring w)] :
    let V := LubinTate.Valuations.exponentialValuationSubring v
    let W := LubinTate.Valuations.exponentialValuationSubring w
    let i := exponentialValuationRingMap v w hExt
    letI : Algebra V W := i.toAlgebra
    let e := Ideal.ramificationIdx'
      (IsLocalRing.maximalIdeal V) (IsLocalRing.maximalIdeal W)
    ∃ s t : ℝ, t ≠ 0 ∧
      exponentialValueSubgroup v = AddSubgroup.zmultiples s ∧
      exponentialValueSubgroup w = AddSubgroup.zmultiples t ∧
      s = (e : ℝ) * t := by
  let V := LubinTate.Valuations.exponentialValuationSubring v
  let W := LubinTate.Valuations.exponentialValuationSubring w
  let i := exponentialValuationRingMap v w hExt
  let : IsLocalHom i :=
    exponentialValuationRingMap_isLocalHom v w hExt
  let : Algebra V W := i.toAlgebra
  let e := Ideal.ramificationIdx'
    (IsLocalRing.maximalIdeal V) (IsLocalRing.maximalIdeal W)
  rcases hv with ⟨s, hs, hvalues, pi, hpival⟩
  rcases hw with ⟨t, ht, hwvalues, Pi, hPival⟩
  let piV := LubinTate.Valuations.discretePrimeElementInValuationSubring v hs.le hpival
  let PiW := LubinTate.Valuations.discretePrimeElementInValuationSubring w ht.le hPival
  have hVspan : IsLocalRing.maximalIdeal V = Ideal.span ({piV} : Set V) :=
    maximalIdeal_eq_span_discretePrimeElement v hs hvalues hpival
  have hWspan : IsLocalRing.maximalIdeal W = Ideal.span ({PiW} : Set W) :=
    maximalIdeal_eq_span_discretePrimeElement w ht hwvalues hPival
  have hi : Function.Injective i := by
    intro a b hab
    apply Subtype.ext
    exact (algebraMap K L).injective (congrArg Subtype.val hab)
  have hmap :=
    ValuationTheory.map_maximalIdeal_eq_pow_ramificationIdx
      (R := V) (S := W) hi
  change Ideal.map i (IsLocalRing.maximalIdeal V) =
    IsLocalRing.maximalIdeal W ^ e at hmap
  have hspan : Ideal.span ({i piV} : Set W) =
      Ideal.span ({PiW ^ e} : Set W) := by
    calc
      Ideal.span ({i piV} : Set W) =
          Ideal.map i (IsLocalRing.maximalIdeal V) := by
        rw [hVspan, Ideal.map_span, Set.image_singleton]
      _ = IsLocalRing.maximalIdeal W ^ e := hmap
      _ = Ideal.span ({PiW} : Set W) ^ e := by rw [hWspan]
      _ = Ideal.span ({PiW ^ e} : Set W) :=
        Ideal.span_singleton_pow PiW e
  obtain ⟨u, hu⟩ := Ideal.span_singleton_eq_span_singleton.mp hspan
  have huval : w ((((u : Wˣ) : W) : L)) = 0 :=
    LubinTate.Valuations.exponentialValuation_eq_zero_of_isUnit w u.isUnit
  have hfield := congrArg (fun z : W ↦ (z : L)) hu
  have hvalue := congrArg w hfield
  have hscale : s = (e : ℝ) * t := by
    change w (algebraMap K L pi * (((u : Wˣ) : W) : L)) =
      w ((Pi : L) ^ e) at hvalue
    rw [w.map_mul, hExt, hpival, huval, add_zero,
      LubinTate.Valuations.discretePrimeElement_pow_value w hPival] at hvalue
    exact WithTop.coe_eq_coe.mp hvalue
  refine ⟨s, t, ne_of_gt ht,
    exponentialValueSubgroup_eq_zmultiples v hvalues hpival,
    exponentialValueSubgroup_eq_zmultiples w hwvalues hPival,
    hscale⟩

theorem

exponentialValueSubgroup_le_of_extends

L540 ↗

AlgebraicNumberTheory.Valuations.exponentialValueSubgroup_le_of_extends

Documentation

Exact extension embeds the base value group in the target value group.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem exponentialValueSubgroup_le_of_extends
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    exponentialValueSubgroup v ≤ exponentialValueSubgroup w

def

ExponentialValueGroupQuotient

L552 ↗

AlgebraicNumberTheory.Valuations.ExponentialValueGroupQuotient

Documentation

The actual quotient w(Lˣ) / v(Kˣ) of value groups. The comap is the base subgroup viewed inside the target subgroup.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

def ExponentialValueGroupQuotient
    {K L : Type*} [Field K] [Field L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)

def

exponentialRamificationIndex

L561 ↗

AlgebraicNumberTheory.Valuations.exponentialRamificationIndex

Documentation

The ramification index as the actual value-group quotient cardinality.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

def exponentialRamificationIndex
    {K L : Type*} [Field K] [Field L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) : ℕ

theorem

exponentialRamificationIndex_eq_of_cyclic_valueSubgroups

L569 ↗

AlgebraicNumberTheory.Valuations.exponentialRamificationIndex_eq_of_cyclic_valueSubgroups

Documentation

If the target value group is tℤ and the base value group is (e t)ℤ, their actual quotient has cardinality e.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem exponentialRamificationIndex_eq_of_cyclic_valueSubgroups
    {K L : Type*} [Field K] [Field L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    {s t : ℝ} (ht : t ≠ 0) (e : ℕ)
    (hvgroup :
      exponentialValueSubgroup v = AddSubgroup.zmultiples s)
    (hwgroup :
      exponentialValueSubgroup w = AddSubgroup.zmultiples t)
    (hscale : s = (e : ℝ) * t) :
    exponentialRamificationIndex v w = e

theorem

exponentialRamificationIndex_eq_ideal_ramificationIdx

L640 ↗

AlgebraicNumberTheory.Valuations.exponentialRamificationIndex_eq_ideal_ramificationIdx

Documentation

For discrete source and target valuation rings, the quotient-cardinality ramification index agrees with mathlib's local Dedekind ramification index.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

theorem exponentialRamificationIndex_eq_ideal_ramificationIdx
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hv : LubinTate.Valuations.DiscreteExponentialValuation v)
    [IsDiscreteValuationRing (LubinTate.Valuations.exponentialValuationSubring v)]
    [IsDiscreteValuationRing (LubinTate.Valuations.exponentialValuationSubring w)] :
    let V := LubinTate.Valuations.exponentialValuationSubring v
    let W := LubinTate.Valuations.exponentialValuationSubring w
    let i := exponentialValuationRingMap v w hExt
    letI : Algebra V W := i.toAlgebra
    exponentialRamificationIndex v w =
      Ideal.ramificationIdx'
        (IsLocalRing.maximalIdeal V) (IsLocalRing.maximalIdeal W) := by
  let V := LubinTate.Valuations.exponentialValuationSubring v
  let W := LubinTate.Valuations.exponentialValuationSubring w
  let i := exponentialValuationRingMap v w hExt
  let : IsLocalHom i :=
    exponentialValuationRingMap_isLocalHom v w hExt
  let : Algebra V W := i.toAlgebra
  let e := Ideal.ramificationIdx'
    (IsLocalRing.maximalIdeal V) (IsLocalRing.maximalIdeal W)
  have hw : LubinTate.Valuations.DiscreteExponentialValuation w :=
    discreteExponentialValuation_of_isDiscreteValuationRing w
  obtain ⟨s, t, ht, hvgroup, hwgroup, hscale⟩ :=
    exists_valueGroup_generators_scaled_by_ramificationIdx
      v w hExt hv hw
  exact exponentialRamificationIndex_eq_of_cyclic_valueSubgroups
    v w ht e hvgroup hwgroup hscale

def

exponentialResidueDegree

L672 ↗

AlgebraicNumberTheory.Valuations.exponentialResidueDegree

Documentation

The actual residue degree of an exact valued extension.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

def exponentialResidueDegree
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) : ℕ

theorem

exponentialResidueDegree_eq_ideal_inertiaDeg

L690 ↗

AlgebraicNumberTheory.Valuations.exponentialResidueDegree_eq_ideal_inertiaDeg

Documentation

The residue finrank is exactly mathlib's local inertia degree.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

theorem exponentialResidueDegree_eq_ideal_inertiaDeg
    {K L : Type*} [Field K] [Field L] [Algebra 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 := exponentialValuationRingMap v w hExt
    letI : IsLocalHom i :=
      exponentialValuationRingMap_isLocalHom v w hExt
    letI : Algebra V W := i.toAlgebra
    exponentialResidueDegree v w hExt =
      (IsLocalRing.maximalIdeal W).inertiaDeg V := by
  let V := LubinTate.Valuations.exponentialValuationSubring v
  let W := LubinTate.Valuations.exponentialValuationSubring w
  let i := exponentialValuationRingMap v w hExt
  let : IsLocalHom i :=
    exponentialValuationRingMap_isLocalHom v w hExt
  let : Algebra V W := i.toAlgebra
  let Amap : Algebra (IsLocalRing.ResidueField V)
      (IsLocalRing.ResidueField W) :=
    (IsLocalRing.ResidueField.map i).toAlgebra
  let : Algebra (IsLocalRing.ResidueField V)
      (IsLocalRing.ResidueField W) := Amap
  let : (IsLocalRing.maximalIdeal W).LiesOver
      (IsLocalRing.maximalIdeal V) :=
    ⟨(ValuationTheory.DiscreteValuationField.ResidueField.comap_maximalIdeal_eq i).symm⟩
  change Module.finrank (IsLocalRing.ResidueField V)
      (IsLocalRing.ResidueField W) =
    (IsLocalRing.maximalIdeal W).inertiaDeg V
  let Astd : Algebra (IsLocalRing.ResidueField V)
      (IsLocalRing.ResidueField W) :=
    Ideal.Quotient.algebraOfLiesOver
      (IsLocalRing.maximalIdeal W) (IsLocalRing.maximalIdeal V)
  have hmap :
      @algebraMap (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) _ _ Amap =
        @algebraMap (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) _ _ Astd := by
    ext x
    obtain ⟨a, rfl⟩ := IsLocalRing.residue_surjective x
    rfl
  have hAlg : Amap = Astd := by
    apply Algebra.algebra_ext
    intro r
    exact DFunLike.congr_fun hmap r
  have hfin :
      @Module.finrank (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) _ _
          (@Algebra.toModule _ _ _ _ Amap) =
        @Module.finrank (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) _ _
          (@Algebra.toModule _ _ _ _ Astd) := by
    rw [hAlg]
  have h := (Ideal.inertiaDeg_eq_of_isMaximal
    (IsLocalRing.maximalIdeal V) (IsLocalRing.maximalIdeal W)).symm
  exact h

def

exponentialAssociatedAbsoluteValue

L750 ↗

AlgebraicNumberTheory.Valuations.exponentialAssociatedAbsoluteValue

Documentation

The canonical multiplicative presentation exp (-v(x)) of an exponential exponential valuation.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

def exponentialAssociatedAbsoluteValue
    {K : Type*} [Field K] (v : LubinTate.Valuations.ExponentialValuation K) :
    AbsoluteValue K ℝ

theorem

exponentialAssociatedAbsoluteValue_associated

L826 ↗

AlgebraicNumberTheory.Valuations.exponentialAssociatedAbsoluteValue_associated

Documentation

The canonical multiplicative presentation is associated to v, with the fixed base e = exp 1.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem exponentialAssociatedAbsoluteValue_associated
    {K : Type*} [Field K] (v : LubinTate.Valuations.ExponentialValuation K) :
    LubinTate.Valuations.AssociatedAbsoluteValue v (Real.exp 1)
      (exponentialAssociatedAbsoluteValue v)

theorem

associatedAbsoluteValue_nonarchimedean

L841 ↗

AlgebraicNumberTheory.Valuations.associatedAbsoluteValue_nonarchimedean

Documentation

An absolute value associated to a exponential valuation is nonarchimedean; the strong triangle inequality is the exponential ultrametric inequality transported through the decreasing map r ↦ q ^ (-r).

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem associatedAbsoluteValue_nonarchimedean
    {K : Type*} [Field K]
    (v : LubinTate.Valuations.ExponentialValuation K) (q : ℝ)
    (abv : AbsoluteValue K ℝ)
    (hassoc : LubinTate.Valuations.AssociatedAbsoluteValue v q abv) :
    LubinTate.Valuations.NonarchimedeanAbsoluteValue abv

theorem

associatedAbsoluteValue_valuationSubring_eq

L878 ↗

AlgebraicNumberTheory.Valuations.associatedAbsoluteValue_valuationSubring_eq

Documentation

Associated additive and multiplicative presentations have the same valuation subring.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem associatedAbsoluteValue_valuationSubring_eq
    {K : Type*} [Field K]
    (v : LubinTate.Valuations.ExponentialValuation K) (q : ℝ)
    (abv : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue abv)
    (hassoc : LubinTate.Valuations.AssociatedAbsoluteValue v q abv) :
    LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v =
      absoluteValueValuationSubring abv hnonarch

theorem

associatedAbsoluteValue_extends

L896 ↗

AlgebraicNumberTheory.Valuations.associatedAbsoluteValue_extends

Documentation

Exact extension of associated exponential valuations gives exact extension of the associated absolute values.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem associatedAbsoluteValue_extends
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (q : ℝ) (av : AbsoluteValue K ℝ) (aw : AbsoluteValue L ℝ)
    (hav : LubinTate.Valuations.AssociatedAbsoluteValue v q av)
    (haw : LubinTate.Valuations.AssociatedAbsoluteValue w q aw) :
    ∀ a : K, aw (algebraMap K L a) = av a

theorem

isIntegralClosure_of_subring_eq

L920 ↗

AlgebraicNumberTheory.Valuations.isIntegralClosure_of_subring_eq

Documentation

A literal equality with the integral-closure subring produces the corresponding IsIntegralClosure instance.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem isIntegralClosure_of_subring_eq
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : Subring K) (W : Subring L)
    [Algebra V L]
    (h : W = (integralClosure V L).toSubring) :
    IsIntegralClosure W V L

theorem

exponentialValuationSubring_eq_integralClosure_of_henselian

L946 ↗

AlgebraicNumberTheory.Valuations.exponentialValuationSubring_eq_integralClosure_of_henselian

Documentation

the finite norm-formula theorem applied directly to the exponential presentation: a chosen extension of a Henselian valuation has valuation ring equal to the actual integral closure. The required multiplicative presentations are constructed internally.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem exponentialValuationSubring_eq_integralClosure_of_henselian
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (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) :
    (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring w).toSubring =
      (integralClosure
        (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v) L).toSubring

def

exponentialValueCoset

L1004 ↗

AlgebraicNumberTheory.Valuations.exponentialValueCoset

Documentation

The value-coset class of a nonzero target-field element.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

def exponentialValueCoset
    {K L : Type*} [Field K] [Field L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (x : L) (hx : x ≠ 0) : ExponentialValueGroupQuotient v w

theorem

exponentialValueCoset_units_surjective

L1015 ↗

AlgebraicNumberTheory.Valuations.exponentialValueCoset_units_surjective

Documentation

Every class in the actual value-group quotient is represented by the value of a nonzero element of the target field.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

theorem exponentialValueCoset_units_surjective
    {K L : Type*} [Field K] [Field L]
    (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

exponentialValueCoset_eq_of_cross_value_eq

L1033 ↗

AlgebraicNumberTheory.Valuations.exponentialValueCoset_eq_of_cross_value_eq

Documentation

Equality after cross-multiplying by nonzero base elements forces equality of the corresponding value-group quotient classes.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem exponentialValueCoset_eq_of_cross_value_eq
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    {x y : L} (hx : x ≠ 0) (hy : y ≠ 0)
    {a b : K} (ha : a ≠ 0) (hb : b ≠ 0)
    (hcross :
      w (algebraMap K L a * x) = w (algebraMap K L b * y)) :
    exponentialValueCoset v w x hx = exponentialValueCoset v w y hy

def

DistinctExponentialValueCosetRepresentatives

L1081 ↗

AlgebraicNumberTheory.Valuations.DistinctExponentialValueCosetRepresentatives

Documentation

A family in Lˣ represents distinct cosets modulo the values coming from Kˣ exactly in the cross-multiplication form used in the proof. This definition avoids choosing subtraction representatives in WithTop ℝ.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

def DistinctExponentialValueCosetRepresentatives
    {K L I : Type*} [Field K] [Field L] [Algebra K L]
    (_v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) (pi : I → L) : Prop

theorem

distinctExponentialValueCosetRepresentatives_of_injective

L1093 ↗

AlgebraicNumberTheory.Valuations.distinctExponentialValueCosetRepresentatives_of_injective

Documentation

Injectivity of the actual value-coset map supplies the pairwise distinctness condition used by the constructive proof.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

theorem distinctExponentialValueCosetRepresentatives_of_injective
    {K L I : Type*} [Field K] [Field L] [Algebra K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (pi : I → L) (hpi0 : ∀ i, pi i ≠ 0)
    (hinj : Function.Injective
      (fun i ↦ exponentialValueCoset v w (pi i) (hpi0 i))) :
    DistinctExponentialValueCosetRepresentatives v w pi := by
  refine ⟨hpi0, ?_⟩
  intro i j hij a b ha hb hcross
  apply hij
  apply hinj
  exact exponentialValueCoset_eq_of_cross_value_eq
    v w hExt (hpi0 i) (hpi0 j) ha hb hcross

theorem

ramificationInvariants_valueCosets_mul_residueLifts_linearIndependent

L1114 ↗

AlgebraicNumberTheory.Valuations.ramificationInvariants_valueCosets_mul_residueLifts_linearIndependent

Documentation

The constructive core of the fundamental inequality. Distinct value-coset representatives multiplied by linearly independent residue lifts form a linearly independent family over the base field. Repeated roots or a degree formula are not built into the statement: this is the actual linear-independence argument.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

theorem ramificationInvariants_valueCosets_mul_residueLifts_linearIndependent
    {K L I J : Type*} [Field K] [Field L] [Algebra K L]
    [Finite I] [Finite J]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (pi : I → L) (hpi : DistinctExponentialValueCosetRepresentatives v w pi)
    (omega : J → LubinTate.Valuations.exponentialValuationSubring w)
    (homega :
      let V := LubinTate.Valuations.exponentialValuationSubring v
      let W := LubinTate.Valuations.exponentialValuationSubring w
      let i := exponentialValuationRingMap v w hExt
      letI : Algebra V W := i.toAlgebra
      letI : IsLocalHom i :=
        exponentialValuationRingMap_isLocalHom v w hExt
      letI : Algebra (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) :=
        (IsLocalRing.ResidueField.map i).toAlgebra
      LinearIndependent (IsLocalRing.ResidueField V)
        (fun j ↦ IsLocalRing.residue W (omega j))) :
    LinearIndependent K
      (fun p : I × J ↦ (omega p.2 : L) * pi p.1) := by
  classical
  let : Fintype I := Fintype.ofFinite I
  let : Fintype J := Fintype.ofFinite J
  rw [Fintype.linearIndependent_iff]
  intro a hsum p
  let s : I → L := fun i ↦
    ∑ j, algebraMap K L (a (i, j)) * (omega j : L)
  have hsum' : ∑ i, s i * pi i = 0 := by
    simpa only [s, Fintype.sum_prod_type, Algebra.smul_def,
      Finset.sum_mul, mul_assoc] using hsum
  by_contra hap
  have hinner : ∀ i, s i ≠ 0 →
      ∃ a₀ : K, a₀ ≠ 0 ∧
        w (s i) = w (algebraMap K L a₀) := by
    intro i hsi
    have hai : ∃ j, a (i, j) ≠ 0 := by
      by_contra hnone
      push Not at hnone
      apply hsi
      simp [s, hnone]
    exact exponentialValuation_residueCombination_value_in_base
      v w hExt omega homega (fun j ↦ a (i, j)) hai
  have hpvalue :=
    exponentialValuation_residueCombination_value_in_base
      v w hExt omega homega (fun j ↦ a (p.1, j)) ⟨p.2, hap⟩
  change ∃ a₀ : K, a₀ ≠ 0 ∧
      w (s p.1) = w (algebraMap K L a₀) at hpvalue
  obtain ⟨ap, hapzero, hpvalue⟩ := hpvalue
  have hsp : s p.1 ≠ 0 := by
    intro hzero
    rw [hzero, (w.eq_top_iff 0).mpr rfl] at hpvalue
    exact (LubinTate.Valuations.exponentialValuation_ne_top_of_ne_zero w
      ((map_ne_zero (algebraMap K L)).mpr hapzero)) hpvalue.symm
  have hsum_ne : ∑ i, s i * pi i ≠ 0 := by
    apply exponentialValuation_finset_sum_ne_zero_of_value_ne
      w Finset.univ (fun i ↦ s i * pi i)
    · exact ⟨p.1, Finset.mem_univ _, mul_ne_zero hsp (hpi.1 p.1)⟩
    · intro i hi j hj hij hterm_i hterm_j
      have hsi : s i ≠ 0 := by
        intro hzero
        exact hterm_i (by simp [hzero])
      have hsj : s j ≠ 0 := by
        intro hzero
        exact hterm_j (by simp [hzero])
      obtain ⟨ai, hai, hvi⟩ := hinner i hsi
      obtain ⟨aj, haj, hvj⟩ := hinner j hsj
      have hwi :
          w (s i * pi i) = w (algebraMap K L ai * pi i) := by
        rw [w.map_mul, w.map_mul, hvi]
      have hwj :
          w (s j * pi j) = w (algebraMap K L aj * pi j) := by
        rw [w.map_mul, w.map_mul, hvj]
      intro heq
      exact (hpi.2 hij ai aj hai haj)
        (hwi.symm.trans (heq.trans hwj))
  exact hsum_ne hsum'

theorem

ramificationInvariants_valueCosets_mul_residueLifts_linearIndependent_arbitrary

L1197 ↗

AlgebraicNumberTheory.Valuations.ramificationInvariants_valueCosets_mul_residueLifts_linearIndependent_arbitrary

Documentation

The linearly-independent product family does not require the two indexing sets to have been proved finite in advance. Every finite part is contained in a product of finite parts, to which the preceding constructive argument applies.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

theorem ramificationInvariants_valueCosets_mul_residueLifts_linearIndependent_arbitrary
    {K L I J : Type*} [Field K] [Field L] [Algebra K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (pi : I → L) (hpi : DistinctExponentialValueCosetRepresentatives v w pi)
    (omega : J → LubinTate.Valuations.exponentialValuationSubring w)
    (homega :
      let V := LubinTate.Valuations.exponentialValuationSubring v
      let W := LubinTate.Valuations.exponentialValuationSubring w
      let i := exponentialValuationRingMap v w hExt
      letI : Algebra V W := i.toAlgebra
      letI : IsLocalHom i :=
        exponentialValuationRingMap_isLocalHom v w hExt
      letI : Algebra (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) :=
        (IsLocalRing.ResidueField.map i).toAlgebra
      LinearIndependent (IsLocalRing.ResidueField V)
        (fun j ↦ IsLocalRing.residue W (omega j))) :
    LinearIndependent K
      (fun p : I × J ↦ (omega p.2 : L) * pi p.1) := by
  classical
  rw [linearIndependent_iff_finset_linearIndependent]
  intro s
  let sI : Finset I := s.image Prod.fst
  let sJ : Finset J := s.image Prod.snd
  let piI : sI → L := fun i ↦ pi i
  let omegaJ : sJ → LubinTate.Valuations.exponentialValuationSubring w := fun j ↦ omega j
  have hpiI : DistinctExponentialValueCosetRepresentatives v w piI := by
    refine ⟨fun i ↦ hpi.1 i, ?_⟩
    intro i j hij
    apply hpi.2
    intro h
    apply hij
    exact Subtype.ext h
  let V := LubinTate.Valuations.exponentialValuationSubring v
  let W := LubinTate.Valuations.exponentialValuationSubring w
  let i := exponentialValuationRingMap v w hExt
  let : Algebra V W := i.toAlgebra
  let : IsLocalHom i :=
    exponentialValuationRingMap_isLocalHom v w hExt
  let : Algebra (IsLocalRing.ResidueField V)
      (IsLocalRing.ResidueField W) :=
    (IsLocalRing.ResidueField.map i).toAlgebra
  have homegaJ : LinearIndependent (IsLocalRing.ResidueField V)
      (fun j : sJ ↦ IsLocalRing.residue W (omegaJ j)) := by
    exact homega.comp Subtype.val Subtype.val_injective
  have hprod : LinearIndependent K
      (fun p : sI × sJ ↦ (omegaJ p.2 : L) * piI p.1) :=
    ramificationInvariants_valueCosets_mul_residueLifts_linearIndependent
      v w hExt piI hpiI omegaJ homegaJ
  let emb : s → sI × sJ := fun p ↦
    (⟨p.1.1, Finset.mem_image.mpr ⟨p, p.2, rfl⟩⟩,
      ⟨p.1.2, Finset.mem_image.mpr ⟨p, p.2, rfl⟩⟩)
  have hemb : Function.Injective emb := by
    intro p q hpq
    apply Subtype.ext
    exact Prod.ext (congrArg (fun z ↦ (z.1 : I)) hpq)
      (congrArg (fun z ↦ (z.2 : J)) hpq)
  change LinearIndependent K
    ((fun p : sI × sJ ↦ (omegaJ p.2 : L) * piI p.1) ∘ emb)
  exact hprod.comp emb hemb

theorem

ramificationInvariants_valueCosets_mul_residueLifts_card_le_finrank

L1264 ↗

AlgebraicNumberTheory.Valuations.ramificationInvariants_valueCosets_mul_residueLifts_card_le_finrank

Documentation

Fundamental inequality in constructive cardinal form. Thus any complete set of e value-coset representatives and any residue basis of size f give e f ≤ [L : K]; no extension record carrying a pre-assumed degree formula is used.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

theorem ramificationInvariants_valueCosets_mul_residueLifts_card_le_finrank
    {K L I J : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Fintype I] [Fintype J]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (pi : I → L) (hpi : DistinctExponentialValueCosetRepresentatives v w pi)
    (omega : J → LubinTate.Valuations.exponentialValuationSubring w)
    (homega :
      let V := LubinTate.Valuations.exponentialValuationSubring v
      let W := LubinTate.Valuations.exponentialValuationSubring w
      let i := exponentialValuationRingMap v w hExt
      letI : Algebra V W := i.toAlgebra
      letI : IsLocalHom i :=
        exponentialValuationRingMap_isLocalHom v w hExt
      letI : Algebra (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) :=
        (IsLocalRing.ResidueField.map i).toAlgebra
      LinearIndependent (IsLocalRing.ResidueField V)
        (fun j ↦ IsLocalRing.residue W (omega j))) :
    Fintype.card I * Fintype.card J ≤ Module.finrank K L := by
  have hli :=
    ramificationInvariants_valueCosets_mul_residueLifts_linearIndependent
      v w hExt pi hpi omega homega
  simpa using hli.fintype_card_le_finrank

theorem

ramificationInvariants_actual_valueGroup_card_mul_residueLifts_card_le_finrank

L1292 ↗

AlgebraicNumberTheory.Valuations.ramificationInvariants_actual_valueGroup_card_mul_residueLifts_card_le_finrank

Documentation

Fundamental inequality with the ramification index identified as the cardinality of the actual quotient w(Lˣ)/v(Kˣ).

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

theorem ramificationInvariants_actual_valueGroup_card_mul_residueLifts_card_le_finrank
    {K L I J : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Finite I] [Fintype J]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (pi : I → L) (hpi0 : ∀ i, pi i ≠ 0)
    (hpi : Function.Bijective
      (fun i ↦ exponentialValueCoset v w (pi i) (hpi0 i)))
    (omega : J → LubinTate.Valuations.exponentialValuationSubring w)
    (homega :
      let V := LubinTate.Valuations.exponentialValuationSubring v
      let W := LubinTate.Valuations.exponentialValuationSubring w
      let i := exponentialValuationRingMap v w hExt
      letI : Algebra V W := i.toAlgebra
      letI : IsLocalHom i :=
        exponentialValuationRingMap_isLocalHom v w hExt
      letI : Algebra (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) :=
        (IsLocalRing.ResidueField.map i).toAlgebra
      LinearIndependent (IsLocalRing.ResidueField V)
        (fun j ↦ IsLocalRing.residue W (omega j))) :
    exponentialRamificationIndex v w * Fintype.card J ≤ Module.finrank K L := by
  let : Fintype I := Fintype.ofFinite I
  have hdistinct :=
    distinctExponentialValueCosetRepresentatives_of_injective
      v w hExt pi hpi0 hpi.1
  have hle :=
    ramificationInvariants_valueCosets_mul_residueLifts_card_le_finrank
      v w hExt pi hdistinct omega homega
  have he : exponentialRamificationIndex v w = Fintype.card I := by
    rw [exponentialRamificationIndex]
    calc
      Nat.card (ExponentialValueGroupQuotient v w) = Nat.card I :=
        Nat.card_congr (Equiv.ofBijective
          (fun i ↦ exponentialValueCoset v w (pi i) (hpi0 i)) hpi).symm
      _ = Fintype.card I := Nat.card_eq_fintype_card
  rwa [he]

theorem

ramificationInvariants_fundamental_inequality_of_representatives

L1335 ↗

AlgebraicNumberTheory.Valuations.ramificationInvariants_fundamental_inequality_of_representatives

Documentation

the fundamental inequality, general fundamental inequality with both invariants identified literally: e is the cardinality of w(Lˣ)/v(Kˣ) and f is the residue-field finrank. The supplied pi and omega are genuine complete systems of value-coset representatives and residue-basis lifts.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · full declaration

theorem ramificationInvariants_fundamental_inequality_of_representatives
    {K L I J : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Finite I] [Finite J]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (pi : I → L) (hpi0 : ∀ i, pi i ≠ 0)
    (hpi : Function.Bijective
      (fun i ↦ exponentialValueCoset v w (pi i) (hpi0 i)))
    (omega : J → LubinTate.Valuations.exponentialValuationSubring w)
    (beta :
      let V := LubinTate.Valuations.exponentialValuationSubring v
      let W := LubinTate.Valuations.exponentialValuationSubring w
      let i := exponentialValuationRingMap v w hExt
      letI : Algebra V W := i.toAlgebra
      letI : IsLocalHom i :=
        exponentialValuationRingMap_isLocalHom v w hExt
      letI : Algebra (IsLocalRing.ResidueField V)
          (IsLocalRing.ResidueField W) :=
        (IsLocalRing.ResidueField.map i).toAlgebra
      Basis J (IsLocalRing.ResidueField V)
        (IsLocalRing.ResidueField W))
    (homega :
      let W := LubinTate.Valuations.exponentialValuationSubring w
      ∀ j, IsLocalRing.residue W (omega j) = beta j) :
    exponentialRamificationIndex v w * exponentialResidueDegree v w hExt ≤
      Module.finrank K L := by
  let : Fintype I := Fintype.ofFinite I
  let : Fintype J := Fintype.ofFinite J
  let V := LubinTate.Valuations.exponentialValuationSubring v
  let W := LubinTate.Valuations.exponentialValuationSubring w
  let i := exponentialValuationRingMap v w hExt
  let : IsLocalHom i :=
    exponentialValuationRingMap_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
  have hle :=
    ramificationInvariants_actual_valueGroup_card_mul_residueLifts_card_le_finrank
      v w hExt pi hpi0 hpi omega homegaLI
  have hf : exponentialResidueDegree v w hExt = Fintype.card J := by
    change Module.finrank (IsLocalRing.ResidueField V)
      (IsLocalRing.ResidueField W) = Fintype.card J
    exact Module.finrank_eq_card_basis beta
  rwa [hf]

theorem

ramificationInvariants_fundamental_inequality

L1391 ↗

AlgebraicNumberTheory.Valuations.ramificationInvariants_fundamental_inequality

Documentation

The fundamental inequality in its explicit form. The value coset representatives and the residue-basis lifts are chosen internally. Their indexing sets are proved finite from the product family's linear independence, rather than assumed finite at the theorem boundary.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem ramificationInvariants_fundamental_inequality
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [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 * exponentialResidueDegree v w hExt ≤
      Module.finrank K L

theorem

ramificationInvariants_fundamental_identity_of_discrete_of_separable

L1479 ↗

AlgebraicNumberTheory.Valuations.ramificationInvariants_fundamental_identity_of_discrete_of_separable

Documentation

the fundamental inequality, equality case. For a finite separable extension of a Henselian discretely valued field, the chosen extension valuation ring is first identified with the actual integral closure by the norm-formula and unique-extension theorems. Its DVR structure and module-finiteness are then derived, so the local Dedekind identity gives [L : K] = e f for the actual value-group and residue invariants. No completeness hypothesis is used.

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicNumberTheory
namespace Valuations
open Module

Lean source · statement

theorem ramificationInvariants_fundamental_identity_of_discrete_of_separable
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hvdisc : LubinTate.Valuations.DiscreteExponentialValuation v)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation) :
    Module.finrank K L =
      exponentialRamificationIndex v w * exponentialResidueDegree v w hExt

Module documentation

the fundamental inequality and identity

Declarations