Module

GlobalArtin.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalArtin

13 declarations indexed from sourceView source ↗

Module documentation

The preliminary global Artin homomorphism

For a finite abelian extension L / K, the global norm-residue symbol on ideles is the product of its archimedean and finite-place local Artin factors.

Imports4

Imported by10

def

globalArtinMonoidHom_continuous

L48 ↗

GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_continuous

Documentation

The preliminary global Artin homomorphism is continuous.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
  NumberField.LiesOver
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem globalArtinMonoidHom_continuous :
    Continuous
      (globalArtinMonoidHom
        (K := K) (L := L))

theorem

globalArtinMonoidHom_relativeIdeleNorm_eq_one

L83 ↗

GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_relativeIdeleNorm_eq_one

Documentation

The preliminary global Artin homomorphism of L / K kills every actual relative-idele norm from L. At each finite and infinite place this is exactly the corresponding local reciprocity kernel theorem.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
  NumberField.LiesOver
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem globalArtinMonoidHom_relativeIdeleNorm_eq_one
    (z : RelativeIdeleGroup K L) :
    globalArtinMonoidHom
        (K := K) (L := L)
        (RelativeIdeleGroup.norm K L z) =
      1

theorem

globalArtinMonoidHom_ideleNorm_eq_one

L132 ↗

GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_ideleNorm_eq_one

Documentation

The preliminary global Artin homomorphism kills the ordinary idele norm N_{L/K} : I_L → I_K. This is the relative-idele kernel theorem above, transported by the canonical scalar-extension equivalence used in the definition of IdeleGroup.norm.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
  NumberField.LiesOver
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem globalArtinMonoidHom_ideleNorm_eq_one
    (a : IdeleGroup L) :
    globalArtinMonoidHom
        (K := K) (L := L)
        (IdeleGroup.norm K L a) =
      1

theorem

globalArtinMonoidHom_norm_eq_place_products

L155 ↗

GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_norm_eq_place_products

Documentation

The actual global Artin symbol after an ordinary idele norm, expanded simultaneously at all archimedean and finite places. The factors are indexed by the genuine places upstairs, and use the ordinary LCFT field norm on the corresponding completions.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
  NumberField.LiesOver
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · full declaration

theorem globalArtinMonoidHom_norm_eq_place_products
    {M : Type}
    [Field M] [NumberField M] [Algebra K M]
    (a : IdeleGroup M) :
    letI : ∀ W : InfinitePlace M,
        W.1.LiesOver
      (infinitePlaceBelow (K := K) W).1 :=
      fun _ => ⟨rfl⟩
    letI : ∀ W : HeightOneSpectrum (𝓞 M),
        Algebra
          ((finitePlaceBelow
            (K := K) W).adicCompletion K)
          (W.adicCompletion M) :=
      fun W =>
        (finitePlaceAdicCompletionMap
          K M
          (finitePlaceBelow (K := K) W)
          ⟨W, rfl⟩).toAlgebra
    globalArtinMonoidHom
        (K := K) (L := L)
        (IdeleGroup.norm K M a) =
      (∏ W : InfinitePlace M,
        chosenInfinitePlaceArtinMonoidHom
          (K := K) (L := L)
          (infinitePlaceBelow (K := K) W)
          (LocalFieldTheory.normUnits
            (infinitePlaceBelow
              (K := K) W).Completion
            W.Completion
            (IdeleGroup.infiniteComponent W a))) *
      ∏ᶠ W : HeightOneSpectrum (𝓞 M),
        chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L)
          (finitePlaceBelow (K := K) W)
          (LocalFieldTheory.normUnits
            ((finitePlaceBelow
              (K := K) W).adicCompletion K)
            (W.adicCompletion M)
            (IdeleGroup.finiteComponent W a)) := by
  classical
  let : ∀ W : InfinitePlace M,
      W.1.LiesOver
        (infinitePlaceBelow (K := K) W).1 :=
    fun _ => ⟨rfl⟩
  let : ∀ W : HeightOneSpectrum (𝓞 M),
      Algebra
        ((finitePlaceBelow
          (K := K) W).adicCompletion K)
        (W.adicCompletion M) :=
    fun W =>
      (finitePlaceAdicCompletionMap
        K M
        (finitePlaceBelow (K := K) W)
        ⟨W, rfl⟩).toAlgebra
  change
    infinitePlaceGlobalArtinMonoidHom
        (K := K) (L := L)
        (IdeleGroup.norm K M a) *
      finitePlaceGlobalArtinMonoidHom
        (K := K) (L := L)
        (IdeleGroup.norm K M a) = _
  rw [infinitePlaceGlobalArtinMonoidHom_norm_eq_prod,
    finitePlaceGlobalArtinMonoidHom_norm_eq_finprod]

theorem

restrict_globalArtinMonoidHom_apply

L225 ↗

GlobalClassFieldTheory.Reciprocity.restrict_globalArtinMonoidHom_apply

Documentation

In an actual field diamond K ⊂ K', L ⊂ L', the standard restriction map distributes over every local factor of the upper global Artin symbol. The vertical Galois map is exactly the composite supplied by mathlib: first restrict scalars from K' to K, then restrict the automorphism of L' to the normal subextension L.

Source context 8 commands

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

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

Lean source · statement

theorem restrict_globalArtinMonoidHom_apply
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (a : IdeleGroup K') :
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K))
        (globalArtinMonoidHom
          (K := K') (L := L') a) =
      (∏ v : InfinitePlace K',
        ((AlgEquiv.restrictNormalHom L).comp
            (AlgEquiv.restrictScalarsHom K))
          (chosenInfinitePlaceArtinMonoidHom
            (K := K') (L := L') v
            (IdeleGroup.infiniteComponent v a))) *
      ∏ᶠ v : HeightOneSpectrum (𝓞 K'),
        ((AlgEquiv.restrictNormalHom L).comp
            (AlgEquiv.restrictScalarsHom K))
          (chosenFinitePlaceArtinMonoidHom
            (K := K') (L := L') v
            (IdeleGroup.finiteComponent v a))

theorem

globalArtinMonoidHom_norm_restriction

L260 ↗

GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_norm_restriction

Documentation

Norm--restriction for the actual global Artin homomorphism. In a number-field diamond K ⊂ K', L ⊂ L', the ordinary idele norm and mathlib's standard restriction composite form a commuting square.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
  NumberField.LiesOver
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem globalArtinMonoidHom_norm_restriction
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L'] :
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K)).comp
        (globalArtinMonoidHom
          (K := K') (L := L')) =
      (globalArtinMonoidHom
        (K := K) (L := L)).comp
        (IdeleGroup.norm K K')

theorem

globalArtinMonoidHom_restrict_tower

L321 ↗

GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_restrict_tower

Documentation

For an abelian tower with fixed base field, the global Artin map commutes with the genuine restriction homomorphism.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
  NumberField.LiesOver
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem globalArtinMonoidHom_restrict_tower
    {E : Type}
    [Field E] [NumberField E]
    [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    [IsAbelianGalois K E] :
    (AlgEquiv.restrictNormalHom E).comp
        (globalArtinMonoidHom
          (K := K) (L := L)) =
      globalArtinMonoidHom
        (K := K) (L := E)

theorem

globalArtinMonoidHom_infinitePlaceIdele

L379 ↗

GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_infinitePlaceIdele

Documentation

The global Artin symbol of an archimedean one-place idele is its local infinite-place Artin symbol.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
  NumberField.LiesOver
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem globalArtinMonoidHom_infinitePlaceIdele
    (v : InfinitePlace K)
    (x : v.Completionˣ) :
    globalArtinMonoidHom
        (K := K) (L := L)
        (infinitePlaceIdele v x) =
      chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v x

theorem

globalArtinMonoidHom_finitePlaceIdele

L428 ↗

GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_finitePlaceIdele

Documentation

The global Artin symbol of a finite one-place idele is its local finite-place Artin symbol.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
  NumberField.LiesOver
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem globalArtinMonoidHom_finitePlaceIdele
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    globalArtinMonoidHom
        (K := K) (L := L)
        (finitePlaceIdele v x) =
      chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v x

theorem

finitePlaceDecompositionGroup_le_globalArtinMonoidHom_range

L448 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceDecompositionGroup_le_globalArtinMonoidHom_range

Documentation

Every chosen finite-place decomposition group is contained in the image of the global Artin homomorphism.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
  NumberField.LiesOver
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem finitePlaceDecompositionGroup_le_globalArtinMonoidHom_range
    (v : HeightOneSpectrum (𝓞 K)) :
    finitePlaceDecompositionGroup
        (K := K) (L := L) v ≤
      (globalArtinMonoidHom
        (K := K) (L := L)).range

theorem

globalArtinMonoidHom_surjective

L465 ↗

GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_surjective

Documentation

The actual global Artin homomorphism of a finite abelian extension of number fields is surjective.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
  NumberField.LiesOver
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem globalArtinMonoidHom_surjective :
    Function.Surjective
      (globalArtinMonoidHom
        (K := K) (L := L))

Module documentation

The preliminary global Artin homomorphism

Declarations