NYLL
Module

NormLocalOrder.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.NormLocalOrder
6 declarations indexed from sourceView source ↗

Module documentation

Local orders of finite-place norms

For a finite extension of number fields and a place upstairs, the order of the concrete local field norm is the inertia degree times the upstairs order. The proof uses the actual norm–valuation theorem for finite separable local-field extensions. The two normalization comparisons needed here are also concrete:

  • the intrinsic local-field valuation is compared with the distinguished

ℤᵐ⁰-valued completion valuation;

  • the residue degree of the completed extension is identified with the

inertia degree of the corresponding prime of the number-field extension.

Imports8
Imported by4

Declarations

lemma

withZeroMultiplicativeInt_le_exp_neg_one_of_lt_one

L42 ↗
FiniteIdeleGroup.withZeroMultiplicativeInt_le_exp_neg_one_of_lt_one
Source context 5 commands

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

open scoped NumberField ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace FiniteIdeleGroup
universe u v w
Lean source · statement
lemma withZeroMultiplicativeInt_le_exp_neg_one_of_lt_one
    (γ : WithZero (Multiplicative ℤ)) (hγ : γ < 1) :
    γ ≤ WithZero.exp (-1 : ℤ)
theorem

normalizedValue_eq_withZeroLog_of_surjective

L63 ↗
FiniteIdeleGroup.normalizedValue_eq_withZeroLog_of_surjective
Documentation

A surjective standard integer valuation gives the same normalized integer value as the intrinsic local-field valuation.

Source context 5 commands

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

open scoped NumberField ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace FiniteIdeleGroup
universe u v w
Lean source · statement
theorem normalizedValue_eq_withZeroLog_of_surjective
    (F : Type w)
    [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    (ν : Valuation F (WithZero (Multiplicative ℤ)))
    [ν.Compatible]
    (hν : Function.Surjective ν)
    (x : Fˣ) :
    LocalFieldTheory.IsNonarchimedeanLocalField.v F
        (Additive.ofMul x) =
      WithZero.log (ν (x : F))
def

intrinsicIntegerEquivValuedInteger

L217 ↗
FiniteIdeleGroup.intrinsicIntegerEquivValuedInteger
Documentation

Identity on the underlying field gives the equivalence between the intrinsic valuation ring and the distinguished valued-field integer ring.

Source context 5 commands

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

open scoped NumberField ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace FiniteIdeleGroup
universe u v w
Lean source · statement
def intrinsicIntegerEquivValuedInteger
    (F : Type w)
    [Field F] [ValuativeRel F]
    [Valued F (WithZero (Multiplicative ℤ))]
    [(Valued.v :
      Valuation F (WithZero (Multiplicative ℤ))).Compatible] :
    𝒪[F] ≃+* Valued.integer F
def

intrinsicResidueFieldEquivValuedResidueField

L236 ↗
FiniteIdeleGroup.intrinsicResidueFieldEquivValuedResidueField
Documentation

The residue field for the intrinsic valuation is the residue field of the distinguished ℤᵐ⁰-valued completion valuation.

Source context 5 commands

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

open scoped NumberField ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace FiniteIdeleGroup
universe u v w
Lean source · statement
def intrinsicResidueFieldEquivValuedResidueField
    (F : Type w)
    [Field F] [ValuativeRel F]
    [Valued F (WithZero (Multiplicative ℤ))]
    [(Valued.v :
      Valuation F (WithZero (Multiplicative ℤ))).Compatible] :
    𝓀[F] ≃+* Valued.ResidueField F
theorem

absNorm_eq_card_intrinsicAdicResidueField

L247 ↗
FiniteIdeleGroup.absNorm_eq_card_intrinsicAdicResidueField
Source context 5 commands

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

open scoped NumberField ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace FiniteIdeleGroup
universe u v w
Lean source · statement
theorem absNorm_eq_card_intrinsicAdicResidueField
    (K : Type u) [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K))
    [ValuativeRel (v.adicCompletion K)]
    [(Valued.v :
      Valuation (v.adicCompletion K)
        (WithZero (Multiplicative ℤ))).Compatible] :
    Ideal.absNorm v.asIdeal =
      Nat.card 𝓀[v.adicCompletion K]
theorem

localOrder_normUnits

L279 ↗
FiniteIdeleGroup.localOrder_normUnits
Documentation

The local order of the actual norm between finite-place completions is multiplied by the inertia degree of the upstairs prime.

Source context 6 commands

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

open scoped NumberField ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace FiniteIdeleGroup
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
Lean source · full declaration
theorem localOrder_normUnits
    (v₀ : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      _root_.finitePlaceBelow (K := K) W = v₀})
    (x : (W.1.adicCompletion L)ˣ) :
    letI : Algebra
        (v₀.adicCompletion K) (W.1.adicCompletion L) :=
      (finitePlaceAdicCompletionMap K L v₀ W).toAlgebra
    (localOrder v₀
      (LocalFieldTheory.normUnits
        (v₀.adicCompletion K) (W.1.adicCompletion L) x)).toAdd =
      (W.1.asIdeal.inertiaDeg (𝓞 K) : ℤ) *
        (localOrder W.1 x).toAdd := by
  classical
  let F := v₀.adicCompletion K
  let E := W.1.adicCompletion L
  let : Algebra F E :=
    (finitePlaceAdicCompletionMap K L v₀ W).toAlgebra
  let : IsScalarTower K F E :=
    finitePlaceAdicCompletionMap_isScalarTower K L v₀ W
  let : FiniteDimensional F E :=
    finitePlaceAdicCompletionMap_moduleFinite K L v₀ W
  let : CharZero F :=
    charZero_of_injective_algebraMap
      (algebraMap K F).injective
  let : Algebra.IsIntegral F E :=
    Algebra.IsIntegral.of_finite F E
  let : Algebra.IsSeparable F E :=
    Algebra.IsSeparable.of_integral F E
  let νF : Valuation F (WithZero (Multiplicative ℤ)) :=
    Valued.v
  let νE : Valuation E (WithZero (Multiplicative ℤ)) :=
    Valued.v
  have hνF : Function.Surjective νF := by
    simpa [F, νF] using
      v₀.valuedAdicCompletion_surjective K
  have hνE : Function.Surjective νE := by
    simpa [E, νE] using
      W.1.valuedAdicCompletion_surjective L
  let : ValuativeRel F :=
    ValuativeRel.ofValuation νF
  let : ValuativeRel E :=
    ValuativeRel.ofValuation νE
  let : νF.Compatible :=
    Valuation.Compatible.ofValuation νF
  let : νE.Compatible :=
    Valuation.Compatible.ofValuation νE
  let : νF.IsNontrivial := by
    obtain ⟨π, hπ⟩ :=
      hνF (WithZero.exp (-1 : ℤ))
    refine ⟨⟨π, ?_, ?_⟩⟩
    · rw [hπ]
      simp
    · rw [hπ]
      change
        WithZero.exp (-1 : ℤ) ≠
          WithZero.exp (0 : ℤ)
      simp
  let : νE.IsNontrivial := by
    obtain ⟨π, hπ⟩ :=
      hνE (WithZero.exp (-1 : ℤ))
    refine ⟨⟨π, ?_, ?_⟩⟩
    · rw [hπ]
      simp
    · rw [hπ]
      change
        WithZero.exp (-1 : ℤ) ≠
          WithZero.exp (0 : ℤ)
      simp
  let : ValuativeRel.IsNontrivial F :=
    (ValuativeRel.isNontrivial_iff_isNontrivial νF).2
      inferInstance
  let : ValuativeRel.IsNontrivial E :=
    (ValuativeRel.isNontrivial_iff_isNontrivial νE).2
      inferInstance
  let : IsValuativeTopology F :=
    LocalFieldTheory.isValuativeTopology_of_valued_ofValuation
      F (WithZero (Multiplicative ℤ))
  let : IsValuativeTopology E :=
    LocalFieldTheory.isValuativeTopology_of_valued_ofValuation
      E (WithZero (Multiplicative ℤ))
  let : IsNonarchimedeanLocalField F :=
    { toIsValuativeTopology := inferInstance
      toLocallyCompactSpace := inferInstance
      toIsNontrivial := inferInstance }
  let : IsNonarchimedeanLocalField E :=
    { toIsValuativeTopology := inferInstance
      toLocallyCompactSpace := inferInstance
      toIsNontrivial := inferInstance }
  let ν₀F := ValuativeRel.valuation F
  let ν₀E := ValuativeRel.valuation E
  let : W.1.asIdeal.LiesOver v₀.asIdeal := by
    constructor
    exact congrArg HeightOneSpectrum.asIdeal W.2.symm
  let : ν₀F.HasExtension ν₀E := by
    apply Valuation.HasExtension.ofComapInteger
    ext z
    change
      ν₀E (algebraMap F E z) ≤ 1 ↔
        ν₀F z ≤ 1
    rw [(ValuativeRel.isEquiv ν₀E νE).le_one_iff_le_one,
      (ValuativeRel.isEquiv ν₀F νF).le_one_iff_le_one]
    have hmap :
        νE (algebraMap F E z) =
          νF z ^
            W.1.asIdeal.ramificationIdx (𝓞 K) := by
      have h :=
        finitePlaceAdicCompletionMap_valued
          K L v₀ W z
      rw [Ideal.ramificationIdx'_eq_ramificationIdx
        v₀.asIdeal W.1.asIdeal v₀.ne_bot] at h
      exact h
    rw [hmap,
      pow_le_one_iff
        (W.1.asIdeal.ramificationIdx_pos
          (𝓞 K)).ne']
  let : Algebra 𝒪[F] E :=
    Algebra.ofSubsemiring 𝒪[F]
  let : IsIntegralClosure 𝒪[E] 𝒪[F] E :=
    LocalFieldTheory.localCompleteDVF_integerRing_isIntegralClosure F E
  have hNormValue :=
    LocalClassFieldTheory.v_normUnits_eq_residue_finrank_mul_of_isSeparable
      F E x
  rw [
    normalizedValue_eq_withZeroLog_of_surjective
      F νF hνF
        (LocalFieldTheory.normUnits F E x),
    normalizedValue_eq_withZeroLog_of_surjective
      E νE hνE x
  ] at hNormValue
  have hResidueDegree :
      Module.finrank 𝓀[F] 𝓀[E] =
        W.1.asIdeal.inertiaDeg (𝓞 K) := by
    apply
      Nat.pow_right_injective
        (Nat.succ_le_iff.mpr
          (HeightOneSpectrum.one_lt_absNorm v₀))
    calc
      Ideal.absNorm v₀.asIdeal ^
            Module.finrank 𝓀[F] 𝓀[E] =
          Nat.card 𝓀[F] ^
            Module.finrank 𝓀[F] 𝓀[E] := by
              rw [
                absNorm_eq_card_intrinsicAdicResidueField
                  K v₀
              ]
      _ = Nat.card 𝓀[E] :=
        Module.natCard_eq_pow_finrank.symm
      _ = Ideal.absNorm W.1.asIdeal := by
        rw [
          absNorm_eq_card_intrinsicAdicResidueField
            L W.1
        ]
      _ =
          Ideal.absNorm v₀.asIdeal ^
            W.1.asIdeal.inertiaDeg (𝓞 K) := by
        exact
          (Ideal.absNorm_pow_inertiaDeg
            v₀.asIdeal W.1.asIdeal).symm
  rw [hResidueDegree] at hNormValue
  rw [localOrder_apply, localOrder_apply]
  change
    -WithZero.log
        (νF
          (LocalFieldTheory.normUnits F E x : F)) =
      (W.1.asIdeal.inertiaDeg (𝓞 K) : ℤ) *
        -WithZero.log (νE (x : E))
  calc
    -WithZero.log
          (νF
            (LocalFieldTheory.normUnits F E x : F)) =
        -((W.1.asIdeal.inertiaDeg (𝓞 K) : ℤ) *
          WithZero.log (νE (x : E))) := by
            rw [hNormValue]
    _ =
        (W.1.asIdeal.inertiaDeg (𝓞 K) : ℤ) *
          -WithZero.log (νE (x : E)) := by
            ring

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