Module

InfiniteLocalGlobalArtinCompatibility.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.InfiniteLocalGlobalArtinCompatibility

16 declarations indexed from sourceView source ↗

Module documentation

Archimedean local-global compatibility of Artin homomorphisms

This file compares the actual Artin homomorphism at an infinite place with the global norm-residue homomorphism on idele classes. The one-place norm statements are proved from genuine relative ideles supported at the chosen archimedean place.

Imports9

Imported by4

theorem

infinitePlaceIdeleClass_mem_ideleClassNorm_range_of_mem_infiniteTensorNorm

L47 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceIdeleClass_mem_ideleClassNorm_range_of_mem_infiniteTensorNorm

Documentation

A determinant norm at one infinite place gives an actual global idele-class norm. The witness is the relative idele supported at that place, transported to an ordinary idele of the extension field.

Source context 8 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [IsAbelianGalois K L] in

Lean source · statement

theorem infinitePlaceIdeleClass_mem_ideleClassNorm_range_of_mem_infiniteTensorNorm
    (v : InfinitePlace K)
    (x : v.Completionˣ)
    (hx :
      x ∈ infiniteTensorNormSubgroup
        (K := K) (L := L) v) :
    IdeleGroup.infinitePlaceIdeleClass v x ∈
      (_root_.ideleClassNorm K L).range

theorem

chosenInfinitePlaceArtinMonoidHom_eq_one_iff_infiniteTensorNorm

L82 ↗

GlobalClassFieldTheory.Reciprocity.chosenInfinitePlaceArtinMonoidHom_eq_one_iff_infiniteTensorNorm

Documentation

Triviality of the actual chosen infinite-place Artin symbol is equivalent to membership in the corresponding determinant-norm subgroup.

Source context 8 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem chosenInfinitePlaceArtinMonoidHom_eq_one_iff_infiniteTensorNorm
    (v : InfinitePlace K)
    (x : v.Completionˣ) :
    chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v x = 1 ↔
      x ∈ infiniteTensorNormSubgroup
        (K := K) (L := L) v

theorem

globalNormResidueMonoidHom_infinitePlaceIdeleClass_eq_one_of_localArtin_eq_one

L98 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_infinitePlaceIdeleClass_eq_one_of_localArtin_eq_one

Documentation

An infinite-place element killed by the actual local Artin homomorphism is killed by the global norm-residue homomorphism after insertion as a one-place idele class.

Source context 7 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalNormResidueMonoidHom_infinitePlaceIdeleClass_eq_one_of_localArtin_eq_one
    (v : InfinitePlace K)
    (x : v.Completionˣ)
    (hx :
      chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v x = 1) :
    globalNormResidueMonoidHom K L
        (IdeleGroup.infinitePlaceIdeleClass v x) = 1

theorem

infiniteTensorNormSubgroup_le_globalNormResidueKernel

L115 ↗

GlobalClassFieldTheory.Reciprocity.infiniteTensorNormSubgroup_le_globalNormResidueKernel

Documentation

The infinite tensor norm subgroup lies in the kernel of the global norm-residue homomorphism restricted to the one-place idele class map.

Source context 7 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem infiniteTensorNormSubgroup_le_globalNormResidueKernel
    (v : InfinitePlace K) :
    infiniteTensorNormSubgroup
        (K := K) (L := L) v ≤
      ((globalNormResidueMonoidHom K L).comp
        (IdeleGroup.infinitePlaceIdeleClass v)).ker

theorem

infinitePlaceIdeleClass_mem_ideleClassNorm_range_of_real_pos

L130 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceIdeleClass_mem_ideleClassNorm_range_of_real_pos

Documentation

A positive element at a real infinite place gives an actual idele-class norm.

Source context 7 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem infinitePlaceIdeleClass_mem_ideleClassNorm_range_of_real_pos
    (v : InfinitePlace K)
    (hvReal : v.IsReal)
    (x : v.Completionˣ)
    (hx :
      0 <
        InfinitePlace.Completion.ringEquivRealOfIsReal
          hvReal (x : v.Completion)) :
    IdeleGroup.infinitePlaceIdeleClass v x ∈
      (_root_.ideleClassNorm K L).range

theorem

globalNormResidueMonoidHom_infinitePlaceIdeleClass_eq_one_of_real_pos

L151 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_infinitePlaceIdeleClass_eq_one_of_real_pos

Documentation

The global norm-residue symbol of a positive real one-place idele class is trivial.

Source context 7 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalNormResidueMonoidHom_infinitePlaceIdeleClass_eq_one_of_real_pos
    (v : InfinitePlace K)
    (hvReal : v.IsReal)
    (x : v.Completionˣ)
    (hx :
      0 <
        InfinitePlace.Completion.ringEquivRealOfIsReal
          hvReal (x : v.Completion)) :
    globalNormResidueMonoidHom K L
        (IdeleGroup.infinitePlaceIdeleClass v x) = 1

theorem

globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass_of_unramified

L169 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass_of_unramified

Documentation

At an actually unramified infinite place, both the restricted global norm-residue map and the chosen local Artin map are trivial, hence the local-global compatibility square commutes.

Source context 7 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass_of_unramified
    (v : InfinitePlace K)
    (hUnramified :
      (chosenInfinitePlaceAbove (L := L) v).IsUnramified K) :
    (globalNormResidueMonoidHom K L).comp
        (IdeleGroup.infinitePlaceIdeleClass v) =
      chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v

theorem

globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass_of_isComplex

L196 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass_of_isComplex

Documentation

At a complex base place the chosen place upstairs is automatically unramified, so the archimedean local-global compatibility square is trivial.

Source context 7 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass_of_isComplex
    (v : InfinitePlace K)
    (hvComplex : v.IsComplex) :
    (globalNormResidueMonoidHom K L).comp
        (IdeleGroup.infinitePlaceIdeleClass v) =
      chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v

theorem

infinitePlaceIdeleClass_mem_ideleClassNorm_range_iff_of_unramified

L213 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceIdeleClass_mem_ideleClassNorm_range_iff_of_unramified

Documentation

At an actually unramified infinite place, one-place idele-class norm membership is exactly local determinant-norm membership.

Source context 7 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem infinitePlaceIdeleClass_mem_ideleClassNorm_range_iff_of_unramified
    (v : InfinitePlace K)
    (hUnramified :
      (chosenInfinitePlaceAbove (L := L) v).IsUnramified K)
    (x : v.Completionˣ) :
    IdeleGroup.infinitePlaceIdeleClass v x ∈
        (_root_.ideleClassNorm K L).range ↔
      x ∈ infiniteTensorNormSubgroup
        (K := K) (L := L) v

theorem

neg_one_not_mem_infiniteTensorNormSubgroup_of_ramified

L241 ↗

GlobalClassFieldTheory.Reciprocity.neg_one_not_mem_infiniteTensorNormSubgroup_of_ramified

Documentation

At an actually ramified real place, negative one is not a local determinant norm. This is the concrete real/complex norm obstruction: every norm from the complex completion is positive.

Source context 8 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem neg_one_not_mem_infiniteTensorNormSubgroup_of_ramified
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    (-1 : v.Completionˣ) ∉
      infiniteTensorNormSubgroup
        (K := K) (L := L) v

theorem

chosenInfinitePlaceArtinMonoidHom_neg_one_ne_one_of_ramified

L275 ↗

GlobalClassFieldTheory.Reciprocity.chosenInfinitePlaceArtinMonoidHom_neg_one_ne_one_of_ramified

Documentation

The actual chosen local Artin symbol of negative one is nontrivial at a ramified real place.

Source context 8 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem chosenInfinitePlaceArtinMonoidHom_neg_one_ne_one_of_ramified
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v
        (-1 : v.Completionˣ) ≠ 1

theorem

realCompletionUnit_pos_or_neg_one_mul_pos

L292 ↗

GlobalClassFieldTheory.Reciprocity.realCompletionUnit_pos_or_neg_one_mul_pos

Documentation

Every unit at a real completion is positive either as given or after multiplication by negative one.

Source context 8 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [NumberField K] in

Lean source · statement

theorem realCompletionUnit_pos_or_neg_one_mul_pos
    (v : InfinitePlace K)
    (hvReal : v.IsReal)
    (x : v.Completionˣ) :
    0 <
        InfinitePlace.Completion.ringEquivRealOfIsReal
          hvReal (x : v.Completion) ∨
      0 <
        InfinitePlace.Completion.ringEquivRealOfIsReal
          hvReal
          (((-1 : v.Completionˣ) * x : v.Completionˣ) :
            v.Completion)

theorem

globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass_eq_iff_neg_one

L320 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass_eq_iff_neg_one

Documentation

At a real place, the full archimedean local-global Artin square is equivalent to its single value at negative one. Positivity kills both maps, so this isolates the unique ramified real source calculation.

Source context 7 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass_eq_iff_neg_one
    (v : InfinitePlace K)
    (hvReal : v.IsReal) :
    (globalNormResidueMonoidHom K L).comp
          (IdeleGroup.infinitePlaceIdeleClass v) =
        chosenInfinitePlaceArtinMonoidHom
          (K := K) (L := L) v ↔
      globalNormResidueMonoidHom K L
          (IdeleGroup.infinitePlaceIdeleClass v
            (-1 : v.Completionˣ)) =
        chosenInfinitePlaceArtinMonoidHom
          (K := K) (L := L) v
          (-1 : v.Completionˣ)

theorem

globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass_eq_iff_real_neg_one

L385 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass_eq_iff_real_neg_one

Documentation

For an arbitrary infinite place, the local-global Artin square is reduced canonically to the negative-one calculation in the real case; the complex case is already trivial.

Source context 7 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem
    globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass_eq_iff_real_neg_one
    (v : InfinitePlace K) :
    (globalNormResidueMonoidHom K L).comp
          (IdeleGroup.infinitePlaceIdeleClass v) =
        chosenInfinitePlaceArtinMonoidHom
          (K := K) (L := L) v ↔
      ∀ _hvReal : v.IsReal,
        globalNormResidueMonoidHom K L
            (IdeleGroup.infinitePlaceIdeleClass v
              (-1 : v.Completionˣ)) =
          chosenInfinitePlaceArtinMonoidHom
            (K := K) (L := L) v
            (-1 : v.Completionˣ)

theorem

globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass

L420 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass

Documentation

The global norm-residue homomorphism restricted to a single archimedean component is the actual local Artin homomorphism at that place.

At an unramified archimedean place both maps are trivial. In the only remaining case, a ramified real place, positivity reduces the equality to negative one and the complexification overextension identifies its global symbol with the genuine local complex conjugation.

Source context 7 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalNormResidueMonoidHom_comp_infinitePlaceIdeleClass
    (v : InfinitePlace K) :
    (globalNormResidueMonoidHom K L).comp
          (IdeleGroup.infinitePlaceIdeleClass v) =
      chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v

theorem

infinitePlaceIdeleClass_mem_ideleClassNorm_range_iff

L444 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceIdeleClass_mem_ideleClassNorm_range_iff

Documentation

One-place archimedean norm membership is exactly membership in the local determinant-norm subgroup. This is the norm-kernel form of archimedean local-global Artin compatibility.

Source context 7 commands

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

open scoped NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem infinitePlaceIdeleClass_mem_ideleClassNorm_range_iff
    (v : InfinitePlace K)
    (x : v.Completionˣ) :
    IdeleGroup.infinitePlaceIdeleClass v x ∈
        (_root_.ideleClassNorm K L).range ↔
      x ∈ infiniteTensorNormSubgroup
        (K := K) (L := L) v

Module documentation

Archimedean local-global compatibility of Artin homomorphisms

Declarations