NYLL
Module

OnePlaceBaseNorm.lean

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

Module documentation

Norms of base units supported at one finite place

For a finite place v of an extension field, embed a unit of the completion at the place below v into the completion at v, and support it only at v. Its ordinary idele norm is supported only at the place below v; the surviving component is the corresponding local-degree power.

Imports3
Imported by3

Declarations

def

finitePlaceBaseUnitExtension

L41 ↗
IdeleGroup.finitePlaceBaseUnitExtension
Documentation

The map from units of the completion below v to units of the completion at v, using the actual finite-place completion map.

Source context 7 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
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
def finitePlaceBaseUnitExtension
    (v : HeightOneSpectrum (𝓞 L)) :
    ((_root_.finitePlaceBelow (K := K) v).adicCompletion K)ˣ →*
      (v.adicCompletion L)ˣ
def

finitePlaceCompletionDegree

L53 ↗
IdeleGroup.finitePlaceCompletionDegree
Documentation

The degree of the actual completed extension at v over the completion at the place below v.

Source context 7 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
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
def finitePlaceCompletionDegree
    (v : HeightOneSpectrum (𝓞 L)) : ℕ
theorem

finitePlaceCompletionDegree_pos

L67 ↗
IdeleGroup.finitePlaceCompletionDegree_pos
Documentation

The completed local degree at an actual finite place is positive.

Source context 7 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
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 finitePlaceCompletionDegree_pos
    (v : HeightOneSpectrum (𝓞 L)) :
    0 <
      finitePlaceCompletionDegree
        (K := K) (L := L) v
theorem

norm_finitePlaceIdele_finitePlaceBaseUnitExtension

L91 ↗
IdeleGroup.norm_finitePlaceIdele_finitePlaceBaseUnitExtension
Documentation

The idele norm of a base-completion unit supported at one extension place is the corresponding local-degree power supported at the place below it.

Source context 8 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
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 norm_finitePlaceIdele_finitePlaceBaseUnitExtension
    (v : HeightOneSpectrum (𝓞 L))
    (x :
      ((_root_.finitePlaceBelow (K := K) v).adicCompletion K)ˣ) :
    norm K L
        (finitePlaceIdele v
          (finitePlaceBaseUnitExtension
            (K := K) (L := L) v x)) =
      finitePlaceIdele
        (_root_.finitePlaceBelow (K := K) v)
        (x ^ finitePlaceCompletionDegree
          (K := K) (L := L) v)
theorem

norm_finitePlaceIdele_eq_finitePlaceIdele_normUnits

L208 ↗
IdeleGroup.norm_finitePlaceIdele_eq_finitePlaceIdele_normUnits
Documentation

The ordinary idele norm of an arbitrary unit supported at one upper finite place is supported at the place below, with surviving component equal to the genuine completed local norm.

Source context 8 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
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 · full declaration
theorem norm_finitePlaceIdele_eq_finitePlaceIdele_normUnits
    (v : HeightOneSpectrum (𝓞 K))
    (W :
      {W : HeightOneSpectrum (𝓞 L) //
        _root_.finitePlaceBelow (K := K) W = v})
    (y : (W.1.adicCompletion L)ˣ) :
    letI :
        Algebra (v.adicCompletion K) (W.1.adicCompletion L) :=
      (finitePlaceAdicCompletionMap K L v W).toAlgebra
    norm K L (finitePlaceIdele W.1 y) =
      finitePlaceIdele v
        (LocalFieldTheory.normUnits
          (v.adicCompletion K) (W.1.adicCompletion L) y) := by
  classical
  let :
      Algebra (v.adicCompletion K) (W.1.adicCompletion L) :=
    (finitePlaceAdicCompletionMap K L v W).toAlgebra
  apply Prod.ext
  · apply ContinuousMulEquiv.piUnits.injective
    funext w
    change
      infiniteComponent w
          (norm K L (finitePlaceIdele W.1 y)) =
        infiniteComponent w
          (finitePlaceIdele v
            (LocalFieldTheory.normUnits
              (v.adicCompletion K) (W.1.adicCompletion L) y))
    rw [infiniteComponent_norm_eq_prod]
    rw [finitePlaceIdele_infiniteComponent]
    apply Finset.prod_eq_one
    intro W' _
    rw [finitePlaceIdele_infiniteComponent]
    exact map_one _
  · apply Subtype.ext
    funext r
    change
      finiteComponent r
          (norm K L (finitePlaceIdele W.1 y)) =
        finiteComponent r
          (finitePlaceIdele v
            (LocalFieldTheory.normUnits
              (v.adicCompletion K) (W.1.adicCompletion L) y))
    by_cases hr : r = v
    · subst r
      rw [finiteComponent_norm_eq_prod,
        finitePlaceIdele_finiteComponent_same]
      rw [Finset.prod_eq_single W]
      · rw [finitePlaceIdele_finiteComponent_same]
      · intro W' _ hW'
        have hne : W'.1 ≠ W.1 := by
          intro h
          apply hW'
          exact Subtype.ext h
        rw [
          finitePlaceIdele_finiteComponent_of_ne W.1 W'.1 y hne,
          map_one]
      · simp
    · rw [
        finiteComponent_norm_eq_prod,
        finitePlaceIdele_finiteComponent_of_ne
          v r
          (LocalFieldTheory.normUnits
            (v.adicCompletion K) (W.1.adicCompletion L) y)
          hr]
      apply Finset.prod_eq_one
      intro W' _
      have hne : W'.1 ≠ W.1 := by
        intro h
        apply hr
        calc
          r = _root_.finitePlaceBelow (K := K) W'.1 :=
            W'.2.symm
          _ = v := by rw [h, W.2]
      rw [
        finitePlaceIdele_finiteComponent_of_ne W.1 W'.1 y hne,
        map_one]
theorem

ideleClassNorm_finitePlaceIdeleClass_eq_normUnits

L289 ↗
IdeleGroup.ideleClassNorm_finitePlaceIdeleClass_eq_normUnits
Documentation

Passing the preceding one-place norm identity to ordinary idele classes gives the norm--restriction input used in the global reciprocity square.

Source context 8 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
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 · full declaration
theorem ideleClassNorm_finitePlaceIdeleClass_eq_normUnits
    (v : HeightOneSpectrum (𝓞 K))
    (W :
      {W : HeightOneSpectrum (𝓞 L) //
        _root_.finitePlaceBelow (K := K) W = v})
    (y : (W.1.adicCompletion L)ˣ) :
    letI :
        Algebra (v.adicCompletion K) (W.1.adicCompletion L) :=
      (finitePlaceAdicCompletionMap K L v W).toAlgebra
    _root_.ideleClassNorm K L
        (finitePlaceIdeleClass W.1 y) =
      finitePlaceIdeleClass v
        (LocalFieldTheory.normUnits
          (v.adicCompletion K) (W.1.adicCompletion L) y) := by
  classical
  let :
      Algebra (v.adicCompletion K) (W.1.adicCompletion L) :=
    (finitePlaceAdicCompletionMap K L v W).toAlgebra
  rw [
    finitePlaceIdeleClass,
    MonoidHom.coe_comp,
    Function.comp_apply,
    _root_.ideleClassNorm_mk,
    norm_finitePlaceIdele_eq_finitePlaceIdele_normUnits]
  rfl

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