NYLL
Module

OverextensionArtin.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.OverextensionArtin
22 declarations indexed from sourceView source ↗

Module documentation

Artin reciprocity on the ramified infinite-place overextension

This module proves principal-idele triviality, descends the chosen Artin product to the norm quotient, and identifies it with global reciprocity.

Imports2
Imported by3

Declarations

instance

ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative

L41 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
Source context 10 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
Lean source · statement
instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
def

quotientLiftData

L47 ↗
GlobalClassFieldTheory.Reciprocity.quotientLiftData
Source context 11 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def quotientLiftData
    {A B : Type} [CommGroup A] [Group B]
    (N : Subgroup A) (f : A →* B)
    (hN : ∀ x, x ∈ N → f x = 1) :
    {g : A ⧸ N →* B //
      ∀ x, g (QuotientGroup.mk' N x) = f x}
theorem

globalNormResidueEquiv_mk_one

L57 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueEquiv_mk_one
Source context 11 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueEquiv_mk_one
    (F E : Type)
    [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E] :
    AddEquiv.toMultiplicative
        (globalNormResidueEquiv F E)
        (QuotientGroup.mk (1 : IdeleClassGroup F)) =
      1
theorem

globalNormResidueEquiv_mk

L77 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueEquiv_mk
Source context 11 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueEquiv_mk
    (F E : Type)
    [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
    (c : IdeleClassGroup F) :
    AddEquiv.toMultiplicative
        (globalNormResidueEquiv F E)
        (QuotientGroup.mk c) =
      globalNormResidueMonoidHom F E c
theorem

globalNormResidueEquiv_ne_one_of_ne_mk_one

L96 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueEquiv_ne_one_of_ne_mk_one
Source context 11 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueEquiv_ne_one_of_ne_mk_one
    (F E : Type)
    [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
    (q :
      IdeleClassGroup F ⧸
        (_root_.ideleClassNorm F E).range)
    (hq : q ≠ QuotientGroup.mk (1 : IdeleClassGroup F)) :
    AddEquiv.toMultiplicative
        (globalNormResidueEquiv F E) q ≠
      1
theorem

ramifiedInfinitePlaceOverextensionGlobalArtin_principalIdele

L121 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionGlobalArtin_principalIdele
Documentation

The chosen local-factor Artin product on the actual special overextension L(i)/K' is trivial on principal ideles.

Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionGlobalArtin_principalIdele
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (x :
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)ˣ) :
    globalArtinMonoidHom
        (K :=
          ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified)
        (L :=
          infinitePlaceComplexificationOverfield
            (K := K) (L := L) v)
        (IdeleGroup.principalIdele
          (ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified) x) =
      1
def

ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom

L188 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom
Documentation

The actual local-factor product for the special overextension, descended through principal ideles of its real fixed field.

Source context 11 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    IdeleClassGroup
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified) →*
      Gal(
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v) /
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified))
theorem

ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom_mk

L223 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom_mk
Documentation

Evaluation of the descended special-overextension Artin map on an idele representative is the genuine product of chosen local symbols.

Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom_mk
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (a :
      IdeleGroup
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)) :
    ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom
        (K := K) (L := L) v hRamified
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup
            (ramifiedInfinitePlaceRealFixedField
              (K := K) (L := L) v hRamified))
          a) =
      globalArtinMonoidHom
        (K :=
          ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified)
        (L :=
          infinitePlaceComplexificationOverfield
            (K := K) (L := L) v)
        a
theorem

ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom_ideleClassNorm

L254 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom_ideleClassNorm
Documentation

The descended special-overextension Artin map kills every genuine idele-class norm from its top field.

Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom_ideleClassNorm
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (c :
      IdeleClassGroup
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v)) :
    ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom
        (K := K) (L := L) v hRamified
        (_root_.ideleClassNorm
          (ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified)
          (infinitePlaceComplexificationOverfield
            (K := K) (L := L) v)
          c) =
      1
def

ramifiedInfinitePlaceOverextensionNormQuotientArtinData

L300 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionNormQuotientArtinData
Source context 11 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    ramifiedInfinitePlaceOverextensionNormQuotientArtinData
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
def

ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom

L331 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom
Documentation

The chosen-local-factor Artin map on the actual norm quotient of the special overextension.

Source context 11 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
theorem

ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom_mk

L343 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom_mk
Documentation

Evaluation of the norm-quotient Artin map on an idele-class representative.

Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom_mk
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    ∀ c :
        IdeleClassGroup
          (ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified),
      ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom
          (K := K) (L := L) v hRamified
          (QuotientGroup.mk c) =
        ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom
          (K := K) (L := L) v hRamified c
theorem

ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom_surjective

L363 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom_surjective
Documentation

The norm-quotient Artin map for the special overextension is surjective onto its actual Galois group.

Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom_surjective
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    Function.Surjective
      (ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom
        (K := K) (L := L) v hRamified)
theorem

ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom_bijective

L399 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom_bijective
Documentation

The norm-quotient Artin map for the special overextension is bijective.

Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom_bijective
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    Function.Bijective
      (ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom
        (K := K) (L := L) v hRamified)
theorem

ramifiedInfinitePlaceOverextension_galois_eq_of_ne_one

L428 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextension_galois_eq_of_ne_one
Documentation

Any two nonidentity automorphisms of the quadratic overextension agree.

Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextension_galois_eq_of_ne_one
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    {σ τ : Gal((infinitePlaceComplexificationOverfield
      (K := K) (L := L) v)/(ramifiedInfinitePlaceRealFixedField
      (K := K) (L := L) v hRamified))}
    (hσ : σ ≠ 1)
    (hτ : τ ≠ 1) :
    σ = τ
theorem

ramifiedInfinitePlaceOverextensionGlobalNormResidue_ne_one_of_ne_mk_one

L450 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionGlobalNormResidue_ne_one_of_ne_mk_one
Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionGlobalNormResidue_ne_one_of_ne_mk_one
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (q :
      IdeleClassGroup
          (ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified) ⧸
        (_root_.ideleClassNorm
          (ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified)
          (infinitePlaceComplexificationOverfield
            (K := K) (L := L) v)).range)
    (hq :
      q ≠
        QuotientGroup.mk
          (1 :
            IdeleClassGroup
              (ramifiedInfinitePlaceRealFixedField
                (K := K) (L := L) v hRamified))) :
    AddEquiv.toMultiplicative
        (globalNormResidueEquiv
          (ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified)
          (infinitePlaceComplexificationOverfield
            (K := K) (L := L) v)) q ≠
      1
theorem

ramifiedInfinitePlaceOverextensionGlobalNormResidue_mk

L487 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionGlobalNormResidue_mk
Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionGlobalNormResidue_mk
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (c :
      IdeleClassGroup
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)) :
    AddEquiv.toMultiplicative
        (globalNormResidueEquiv
          (ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified)
          (infinitePlaceComplexificationOverfield
            (K := K) (L := L) v))
        (QuotientGroup.mk c) =
      globalNormResidueMonoidHom
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v) c
theorem

ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom_eq_globalNormResidue_apply

L520 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom_eq_globalNormResidue_apply
Documentation

At each class in the genuine norm quotient of the special overextension, the chosen-local-factor product is the canonical global norm-residue equivalence.

Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom_eq_globalNormResidue_apply
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (q :
      IdeleClassGroup
          (ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified) ⧸
        (_root_.ideleClassNorm
          (ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified)
          (infinitePlaceComplexificationOverfield
            (K := K) (L := L) v)).range) :
    ramifiedInfinitePlaceOverextensionNormQuotientArtinMonoidHom
        (K := K) (L := L) v hRamified q =
      AddEquiv.toMultiplicative
        (globalNormResidueEquiv
          (ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified)
          (infinitePlaceComplexificationOverfield
            (K := K) (L := L) v)) q
theorem

ramifiedInfinitePlaceOverextensionIdeleClassArtin_eq_globalNormResidueEquiv_mk

L622 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionIdeleClassArtin_eq_globalNormResidueEquiv_mk
Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionIdeleClassArtin_eq_globalNormResidueEquiv_mk
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (c :
      IdeleClassGroup
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)) :
    ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom
        (K := K) (L := L) v hRamified c =
      AddEquiv.toMultiplicative
        (globalNormResidueEquiv
          (ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified)
          (infinitePlaceComplexificationOverfield
            (K := K) (L := L) v))
        (QuotientGroup.mk c)
theorem

ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom_eq_globalNormResidue_apply

L651 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom_eq_globalNormResidue_apply
Documentation

On idele classes of the real fixed field, the actual product of chosen local symbols for the special overextension is the canonical global norm-residue map.

Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom_eq_globalNormResidue_apply
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (c :
      IdeleClassGroup
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)) :
    ramifiedInfinitePlaceOverextensionIdeleClassArtinMonoidHom
        (K := K) (L := L) v hRamified c =
      globalNormResidueMonoidHom
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v) c
theorem

globalNormResidueMonoidHom_ramifiedInfinitePlaceOverextension_ideleClass_mk

L679 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_ramifiedInfinitePlaceOverextension_ideleClass_mk
Documentation

On an actual idele representative of the real fixed field, the canonical global norm-residue map for the special overextension is the product of the chosen local Artin symbols.

Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    globalNormResidueMonoidHom_ramifiedInfinitePlaceOverextension_ideleClass_mk
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (a :
      IdeleGroup
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)) :
    globalNormResidueMonoidHom
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v)
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup
            (ramifiedInfinitePlaceRealFixedField
              (K := K) (L := L) v hRamified))
          a) =
      globalArtinMonoidHom
        (K :=
          ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified)
        (L :=
          infinitePlaceComplexificationOverfield
            (K := K) (L := L) v)
        a
theorem

globalNormResidueMonoidHom_ramifiedInfinitePlaceOverextension_infinitePlaceIdeleClass

L722 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_ramifiedInfinitePlaceOverextension_infinitePlaceIdeleClass
Documentation

The canonical global norm-residue symbol of an archimedean one-place idele class in the special overextension is the chosen infinite local Artin symbol.

Source context 12 commands

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

open scoped IsMulCommutative
open NumberField
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section ComplexConjugationOverextension
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section
attribute [-instance]
  ramifiedInfinitePlaceRealFixedField_ratScalarTower
local instance
    ramifiedInfinitePlaceOverextensionIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    globalNormResidueMonoidHom_ramifiedInfinitePlaceOverextension_infinitePlaceIdeleClass
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (w :
      InfinitePlace
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified))
    (x : w.Completionˣ) :
    globalNormResidueMonoidHom
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v)
        (IdeleGroup.infinitePlaceIdeleClass w x) =
      chosenInfinitePlaceArtinMonoidHom
        (K :=
          ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified)
        (L :=
          infinitePlaceComplexificationOverfield
            (K := K) (L := L) v)
        w x

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