NYLL
Module

FinitePlaceArtinQuotient.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.FinitePlaceArtinQuotient
6 declarations indexed from sourceView source ↗

Module documentation

Finite-place Artin quotients

For a finite abelian extension of number fields, the chosen local Artin homomorphism has image equal to the actual decomposition group and kernel equal to the chosen local norm subgroup. Restricting its codomain and applying the first isomorphism theorem therefore identifies the concrete local norm quotient with the decomposition group.

Imports1
Imported by2

Declarations

def

chosenFinitePlaceArtinToDecompositionGroup

L37 ↗
GlobalClassFieldTheory.GlobalClassFields.chosenFinitePlaceArtinToDecompositionGroup
Documentation

The chosen finite-place Artin homomorphism with codomain restricted to the actual decomposition group at the chosen place above v.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
def chosenFinitePlaceArtinToDecompositionGroup
    (v : HeightOneSpectrum (𝓞 K)) :
    (v.adicCompletion K)ˣ →*
      _root_.finitePlaceDecompositionGroup
        (K := K) (L := L) v
theorem

chosenFinitePlaceArtinToDecompositionGroup_surjective

L54 ↗
GlobalClassFieldTheory.GlobalClassFields.chosenFinitePlaceArtinToDecompositionGroup_surjective
Documentation

The decomposition-group-valued finite-place Artin homomorphism is surjective.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem chosenFinitePlaceArtinToDecompositionGroup_surjective
    (v : HeightOneSpectrum (𝓞 K)) :
    Function.Surjective
      (chosenFinitePlaceArtinToDecompositionGroup
        (K := K) (L := L) v)
theorem

chosenFinitePlaceArtinToDecompositionGroup_ker

L74 ↗
GlobalClassFieldTheory.GlobalClassFields.chosenFinitePlaceArtinToDecompositionGroup_ker
Documentation

The kernel of the decomposition-group-valued finite-place Artin homomorphism is exactly the chosen local norm subgroup.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem chosenFinitePlaceArtinToDecompositionGroup_ker
    (v : HeightOneSpectrum (𝓞 K)) :
    MonoidHom.ker
        (chosenFinitePlaceArtinToDecompositionGroup
          (K := K) (L := L) v) =
      _root_.chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v
def

chosenFinitePlaceNormQuotientEquivDecompositionGroup

L87 ↗
GlobalClassFieldTheory.GlobalClassFields.chosenFinitePlaceNormQuotientEquivDecompositionGroup
Documentation

The first-isomorphism identification of the chosen local norm quotient with the actual finite-place decomposition group.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
def chosenFinitePlaceNormQuotientEquivDecompositionGroup
    (v : HeightOneSpectrum (𝓞 K)) :
    _root_.ChosenFinitePlaceNormQuotient
        (K := K) (L := L) v ≃*
      _root_.finitePlaceDecompositionGroup
        (K := K) (L := L) v
theorem

chosenFinitePlaceNormQuotientEquivDecompositionGroup_mk

L104 ↗
GlobalClassFieldTheory.GlobalClassFields.chosenFinitePlaceNormQuotientEquivDecompositionGroup_mk
Documentation

On a quotient representative, the finite-place first-isomorphism equivalence is the decomposition-group-valued Artin map.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem chosenFinitePlaceNormQuotientEquivDecompositionGroup_mk
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    chosenFinitePlaceNormQuotientEquivDecompositionGroup
        (K := K) (L := L) v
        (QuotientGroup.mk x) =
      chosenFinitePlaceArtinToDecompositionGroup
        (K := K) (L := L) v x
theorem

chosenFinitePlaceNormQuotient_card_eq_finitePlaceLocalDegree

L116 ↗
GlobalClassFieldTheory.GlobalClassFields.chosenFinitePlaceNormQuotient_card_eq_finitePlaceLocalDegree
Documentation

The order of the chosen finite-place norm quotient is the actual local extension degree.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem chosenFinitePlaceNormQuotient_card_eq_finitePlaceLocalDegree
    (v : HeightOneSpectrum (𝓞 K)) :
    Nat.card
        (_root_.ChosenFinitePlaceNormQuotient
          (K := K) (L := L) v) =
      _root_.finitePlaceLocalDegree
        (K := K) (L := L) v

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