Module

InfiniteOnePlaceBaseNorm.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.InfiniteOnePlaceBaseNorm

9 declarations indexed from sourceView source ↗

Module documentation

Norms of base units supported at one infinite place

For an infinite place W of an extension field, a unit of the completion at the place below W can be extended to W and inserted as a one-place idele. Its ordinary idele norm remains supported at the place below W; the surviving component is the corresponding local degree power.

Imports3

Imported by2

def

infinitePlaceBaseUnitExtension

L39 ↗

IdeleGroup.infinitePlaceBaseUnitExtension

Documentation

Extend a unit of the completion below W to the completion at W.

Source context 6 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

def infinitePlaceBaseUnitExtension
    (W : InfinitePlace L) :
    ((_root_.infinitePlaceBelow (K := K) W).Completion)ˣ →*
      W.Completionˣ

theorem

infinitePlaceBaseUnitExtension_neg_one

L54 ↗

IdeleGroup.infinitePlaceBaseUnitExtension_neg_one

Documentation

The actual completion map carries negative one to negative one.

Source context 6 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem infinitePlaceBaseUnitExtension_neg_one
    (W : InfinitePlace L) :
    infinitePlaceBaseUnitExtension
        (K := K) (L := L) W
        (-1 :
          ((_root_.infinitePlaceBelow (K := K) W).Completion)ˣ) =
      (-1 : W.Completionˣ)

def

infinitePlaceCompletionDegree

L69 ↗

IdeleGroup.infinitePlaceCompletionDegree

Documentation

The degree of the completed extension at W over the completion at the place below it.

Source context 6 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

def infinitePlaceCompletionDegree
    (W : InfinitePlace L) : ℕ

theorem

norm_infinitePlaceIdele_infinitePlaceBaseUnitExtension

L80 ↗

IdeleGroup.norm_infinitePlaceIdele_infinitePlaceBaseUnitExtension

Documentation

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

Source context 6 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem norm_infinitePlaceIdele_infinitePlaceBaseUnitExtension
    (W : InfinitePlace L)
    (x :
      ((_root_.infinitePlaceBelow (K := K) W).Completion)ˣ) :
    norm K L
        (infinitePlaceIdele W
          (infinitePlaceBaseUnitExtension
            (K := K) (L := L) W x)) =
      infinitePlaceIdele
        (_root_.infinitePlaceBelow (K := K) W)
        (x ^ infinitePlaceCompletionDegree
          (K := K) (L := L) W)

theorem

norm_infinitePlaceIdele_infinitePlaceBaseUnitExtension_of_isUnramified

L193 ↗

IdeleGroup.norm_infinitePlaceIdele_infinitePlaceBaseUnitExtension_of_isUnramified

Documentation

If the chosen infinite place is unramified over the base, the completed extension has degree one, so the norm of the extended one-place idele is exactly the original one-place idele.

Source context 6 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem norm_infinitePlaceIdele_infinitePlaceBaseUnitExtension_of_isUnramified
    (W : InfinitePlace L)
    (hW : W.IsUnramified K)
    (x :
      ((_root_.infinitePlaceBelow (K := K) W).Completion)ˣ) :
    norm K L
        (infinitePlaceIdele W
          (infinitePlaceBaseUnitExtension
            (K := K) (L := L) W x)) =
      infinitePlaceIdele
        (_root_.infinitePlaceBelow (K := K) W) x

theorem

norm_infinitePlaceIdele_infinitePlaceBaseUnitExtension_of_isReal

L222 ↗

IdeleGroup.norm_infinitePlaceIdele_infinitePlaceBaseUnitExtension_of_isReal

Documentation

A real infinite place upstairs is unramified over every lower number field, so the one-place norm of an extended base unit is unchanged.

Source context 6 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem norm_infinitePlaceIdele_infinitePlaceBaseUnitExtension_of_isReal
    (W : InfinitePlace L)
    (hWReal : W.IsReal)
    (x :
      ((_root_.infinitePlaceBelow (K := K) W).Completion)ˣ) :
    norm K L
        (infinitePlaceIdele W
          (infinitePlaceBaseUnitExtension
            (K := K) (L := L) W x)) =
      infinitePlaceIdele
        (_root_.infinitePlaceBelow (K := K) W) x

theorem

ideleClassNorm_infinitePlaceIdeleClass_infinitePlaceBaseUnitExtension_of_isUnramified

L240 ↗

IdeleGroup.ideleClassNorm_infinitePlaceIdeleClass_infinitePlaceBaseUnitExtension_of_isUnramified

Documentation

The degree-one one-place norm equality descends verbatim to the actual idele class groups.

Source context 6 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem ideleClassNorm_infinitePlaceIdeleClass_infinitePlaceBaseUnitExtension_of_isUnramified
    (W : InfinitePlace L)
    (hW : W.IsUnramified K)
    (x :
      ((_root_.infinitePlaceBelow (K := K) W).Completion)ˣ) :
    _root_.ideleClassNorm K L
        (infinitePlaceIdeleClass W
          (infinitePlaceBaseUnitExtension
            (K := K) (L := L) W x)) =
      infinitePlaceIdeleClass
        (_root_.infinitePlaceBelow (K := K) W) x

theorem

ideleClassNorm_infinitePlaceIdeleClass_infinitePlaceBaseUnitExtension_of_isReal

L269 ↗

IdeleGroup.ideleClassNorm_infinitePlaceIdeleClass_infinitePlaceBaseUnitExtension_of_isReal

Documentation

Idele-class form of the one-place norm equality at a real place upstairs.

Source context 6 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem ideleClassNorm_infinitePlaceIdeleClass_infinitePlaceBaseUnitExtension_of_isReal
    (W : InfinitePlace L)
    (hWReal : W.IsReal)
    (x :
      ((_root_.infinitePlaceBelow (K := K) W).Completion)ˣ) :
    _root_.ideleClassNorm K L
        (infinitePlaceIdeleClass W
          (infinitePlaceBaseUnitExtension
            (K := K) (L := L) W x)) =
      infinitePlaceIdeleClass
        (_root_.infinitePlaceBelow (K := K) W) x

theorem

ideleClassNorm_infinitePlaceIdeleClass_neg_one_of_isReal

L287 ↗

IdeleGroup.ideleClassNorm_infinitePlaceIdeleClass_neg_one_of_isReal

Documentation

At a real place upstairs, the idele-class norm of the one-place negative-one class is the one-place negative-one class below.

Source context 6 commands

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

open scoped BigOperators NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem ideleClassNorm_infinitePlaceIdeleClass_neg_one_of_isReal
    (W : InfinitePlace L)
    (hWReal : W.IsReal) :
    _root_.ideleClassNorm K L
        (infinitePlaceIdeleClass W (-1 : W.Completionˣ)) =
      infinitePlaceIdeleClass
        (_root_.infinitePlaceBelow (K := K) W)
        (-1 :
          ((_root_.infinitePlaceBelow (K := K) W).Completion)ˣ)

Module documentation

Norms of base units supported at one infinite place

Declarations