Module

FiniteNormArithmetic.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormTopology.FiniteNormArithmetic

9 declarations indexed from sourceView source ↗

Module documentation

Finite-place arithmetic of idele norms

This file relates the finite components of the ordinary idele norm to local orders and positive prime norms. It also proves the degree formula for the finite positive norm under scalar extension.

Imports7

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Norm
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.IdeleNormComponents
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.IdealClass
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.NormLocalOrder
Mathlib.Algebra.BigOperators.Finprod
Mathlib.NumberTheory.NumberField.Completion.Ramification
Mathlib.RingTheory.Ideal.Norm.RelNorm

Imported by3

theorem

finprod_over_fibers

L43 ↗

IdeleGroup.finprod_over_fibers

Source context 8 commands

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

open scoped BigOperators NNReal NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
open Function
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]

Lean source · statement

theorem finprod_over_fibers
    {α β G : Type*} [CommMonoid G]
    (g : α → β) (f : α → G)
    (hf : HasFiniteMulSupport f) :
    (∏ᶠ b : β,
        ∏ᶠ x : {x : α // g x = b}, f x.1) =
      ∏ᶠ x : α, f x

theorem

finiteAbsoluteNorm_eq_finprod

L81 ↗

IdeleGroup.finiteAbsoluteNorm_eq_finprod

Documentation

A finite idele norm is its finitely supported product of local prime norms raised to the corresponding local orders.

Source context 8 commands

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

open scoped BigOperators NNReal NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
open Function
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]

Lean source · statement

theorem finiteAbsoluteNorm_eq_finprod
    (a : FiniteIdeleGroup K) :
    FiniteIdeleGroup.absoluteNorm a =
      ∏ᶠ v : HeightOneSpectrum (𝓞 K),
        FiniteIdeleGroup.primeNorm v ^
          (FiniteIdeleGroup.localOrder v (a v)).toAdd

theorem

primeNorm_above

L129 ↗

IdeleGroup.primeNorm_above

Documentation

The positive prime norm upstairs is the inertia-degree power of the positive prime norm below.

Source context 9 commands

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

open scoped BigOperators NNReal NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
open Function
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem primeNorm_above
    (v₀ : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      _root_.finitePlaceBelow (K := K) W = v₀}) :
    FiniteIdeleGroup.primeNorm W.1 =
      FiniteIdeleGroup.primeNorm v₀ ^
        W.1.asIdeal.inertiaDeg (𝓞 K)

theorem

zpow_finset_sum

L151 ↗

IdeleGroup.zpow_finset_sum

Documentation

An integer power of a commutative-group element carries a finite sum of exponents to the corresponding finite product.

Source context 8 commands

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

open scoped BigOperators NNReal NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
open Function
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]

Lean source · statement

theorem zpow_finset_sum
    {G : Type*} [CommGroup G]
    {ι : Type*} (g : G) (s : Finset ι) (e : ι → ℤ) :
    g ^ (∑ i ∈ s, e i) =
      ∏ i ∈ s, g ^ e i

theorem

finiteComponentOrder_norm

L165 ↗

IdeleGroup.finiteComponentOrder_norm

Documentation

The order of a finite component of the ordinary idele norm is the sum of the upstairs orders weighted by their inertia degrees.

Source context 8 commands

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

open scoped BigOperators NNReal NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
open Function
universe u v
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 finiteComponentOrder_norm
    (v₀ : HeightOneSpectrum (𝓞 K))
    (a : IdeleGroup L) :
    let vK := HeightOneSpectrum.adicAbv K v₀
    let hvK : vK.IsNontrivial :=
      RayClass.adicAbv_isNontrivial v₀
    letI :=
      completionTensorDecomposition_extensionFintype
        (K := K) (L := L) vK hvK
    let eAbove :=
      finitePlaceExtensionEquivAbove
        (K := K) (L := L) v₀
    letI : Fintype {W : HeightOneSpectrum (𝓞 L) //
        _root_.finitePlaceBelow (K := K) W = v₀} :=
      Fintype.ofEquiv (AbsoluteValueExtension vK L) eAbove
    letI : ∀ W : {W : HeightOneSpectrum (𝓞 L) //
        _root_.finitePlaceBelow (K := K) W = v₀},
        Algebra (v₀.adicCompletion K) (W.1.adicCompletion L) :=
      fun W =>
        (finitePlaceAdicCompletionMap
          K L v₀ W).toAlgebra
    (FiniteIdeleGroup.localOrder v₀
      (finiteComponent v₀ (norm K L a))).toAdd =
      ∑ W : {W : HeightOneSpectrum (𝓞 L) //
          _root_.finitePlaceBelow (K := K) W = v₀},
        (W.1.asIdeal.inertiaDeg (𝓞 K) : ℤ) *
          (FiniteIdeleGroup.localOrder W.1
            (finiteComponent W.1 a)).toAdd := by
  classical
  dsimp only
  let vK := HeightOneSpectrum.adicAbv K v₀
  let hvK : vK.IsNontrivial :=
    RayClass.adicAbv_isNontrivial v₀
  let :=
    completionTensorDecomposition_extensionFintype
      (K := K) (L := L) vK hvK
  let eAbove :=
    finitePlaceExtensionEquivAbove
      (K := K) (L := L) v₀
  let : Fintype {W : HeightOneSpectrum (𝓞 L) //
      _root_.finitePlaceBelow (K := K) W = v₀} :=
    Fintype.ofEquiv (AbsoluteValueExtension vK L) eAbove
  let : ∀ W : {W : HeightOneSpectrum (𝓞 L) //
      _root_.finitePlaceBelow (K := K) W = v₀},
      Algebra (v₀.adicCompletion K) (W.1.adicCompletion L) :=
    fun W =>
      (finitePlaceAdicCompletionMap
        K L v₀ W).toAlgebra
  have hcomponent :
      finiteComponent v₀ (norm K L a) =
        ∏ W : {W : HeightOneSpectrum (𝓞 L) //
            _root_.finitePlaceBelow (K := K) W = v₀},
          LocalFieldTheory.normUnits
            (v₀.adicCompletion K) (W.1.adicCompletion L)
            (finiteComponent W.1 a) := by
    simpa only using
      finiteComponent_norm_eq_prod (K := K) (L := L) v₀ a
  rw [hcomponent]
  rw [map_prod]
  change
    (∑ W : {W : HeightOneSpectrum (𝓞 L) //
        _root_.finitePlaceBelow (K := K) W = v₀},
      (FiniteIdeleGroup.localOrder v₀
        (LocalFieldTheory.normUnits
          (v₀.adicCompletion K) (W.1.adicCompletion L)
          (finiteComponent W.1 a))).toAdd) =
      ∑ W : {W : HeightOneSpectrum (𝓞 L) //
          _root_.finitePlaceBelow (K := K) W = v₀},
        (W.1.asIdeal.inertiaDeg (𝓞 K) : ℤ) *
          (FiniteIdeleGroup.localOrder W.1
            (finiteComponent W.1 a)).toAdd
  apply Finset.sum_congr rfl
  intro W _
  exact
    FiniteIdeleGroup.localOrder_normUnits
      K L v₀ W (finiteComponent W.1 a)

theorem

finiteAbsoluteNorm_norm

L244 ↗

IdeleGroup.finiteAbsoluteNorm_norm

Documentation

The finite positive idele norm is preserved by the ordinary idele norm.

Source context 8 commands

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

open scoped BigOperators NNReal NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
open Function
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]

Lean source · statement

theorem finiteAbsoluteNorm_norm
    (a : IdeleGroup L) :
    FiniteIdeleGroup.absoluteNorm (norm K L a).2 =
      FiniteIdeleGroup.absoluteNorm a.2

theorem

fractionalIdealAbsoluteNorm_extension_prime

L364 ↗

IdeleGroup.fractionalIdealAbsoluteNorm_extension_prime

Documentation

Extending a prime fractional ideal raises its positive absolute norm to the degree of the number-field extension.

Source context 9 commands

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

open scoped BigOperators NNReal NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
open Function
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem fractionalIdealAbsoluteNorm_extension_prime
    (v₀ : HeightOneSpectrum (𝓞 K)) :
    FractionalIdealGroup.absoluteNorm
        (FractionalIdealGroup.extension K L
          (FractionalIdealGroup.prime v₀)) =
      FractionalIdealGroup.absoluteNorm
          (FractionalIdealGroup.prime v₀) ^
        Module.finrank K L

theorem

fractionalIdealAbsoluteNorm_extension

L437 ↗

IdeleGroup.fractionalIdealAbsoluteNorm_extension

Documentation

Extension of a nonzero fractional ideal raises its positive absolute norm to the degree of the number-field extension.

Source context 9 commands

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

open scoped BigOperators NNReal NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
open Function
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem fractionalIdealAbsoluteNorm_extension
    (I : FractionalIdealGroup K) :
    FractionalIdealGroup.absoluteNorm
        (FractionalIdealGroup.extension K L I) =
      FractionalIdealGroup.absoluteNorm I ^
        Module.finrank K L

theorem

finiteAbsoluteNorm_extension

L478 ↗

IdeleGroup.finiteAbsoluteNorm_extension

Documentation

Scalar extension raises the finite positive idele norm to the degree of the number-field extension.

Source context 8 commands

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

open scoped BigOperators NNReal NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
open Function
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]

Lean source · statement

theorem finiteAbsoluteNorm_extension
    (a : IdeleGroup K) :
    FiniteIdeleGroup.absoluteNorm
        (extension K L a).2 =
      FiniteIdeleGroup.absoluteNorm a.2 ^
        Module.finrank K L

Module documentation

Finite-place arithmetic of idele norms

Declarations