NYLL
Module

InfinitePlaceCompatibility.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.InfinitePlaceCompatibility
25 declarations indexed from sourceView source ↗

Module documentation

Infinite-place local-global Artin compatibility

This module compares the real fixed place and the original ramified place, then transports the special overextension computation through global norm-residue naturality.

Imports2
Imported by2

Declarations

instance

infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative

L37 ↗
GlobalClassFieldTheory.Reciprocity.infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
Source context 8 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]
Lean source · statement
instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
def

ramifiedInfinitePlaceRealFixedPlace

L45 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRealFixedPlace
Documentation

The real infinite place of the conjugation fixed field obtained by restricting the concrete complex place of the overfield.

Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def ramifiedInfinitePlaceRealFixedPlace
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    InfinitePlace
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
theorem

ramifiedInfinitePlaceRealFixedPlace_isReal

L63 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRealFixedPlace_isReal
Documentation

The fixed-field place is genuinely real: every element of the fixed field is fixed by ambient complex conjugation.

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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {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 ramifiedInfinitePlaceRealFixedPlace_isReal
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    (ramifiedInfinitePlaceRealFixedPlace
      (K := K) (L := L) v hRamified).IsReal
theorem

infinitePlaceBelow_ramifiedInfinitePlaceRealFixedPlace

L119 ↗
GlobalClassFieldTheory.Reciprocity.infinitePlaceBelow_ramifiedInfinitePlaceRealFixedPlace
Documentation

Restricting the concrete real fixed-field place to the original base recovers the prescribed ramified place v.

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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [FiniteDimensional K L] in
Lean source · statement
theorem infinitePlaceBelow_ramifiedInfinitePlaceRealFixedPlace
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    infinitePlaceBelow (K := K)
        (ramifiedInfinitePlaceRealFixedPlace
          (K := K) (L := L) v hRamified) =
      v
theorem

ramifiedInfinitePlaceOverextension_chosenPlace_isRamified

L160 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextension_chosenPlace_isRamified
Documentation

The chosen place of the special overextension above its concrete fixed-field place is ramified.

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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {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_chosenPlace_isRamified
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    (chosenInfinitePlaceAbove
      (L :=
        infinitePlaceComplexificationOverfield
          (K := K) (L := L) v)
      (ramifiedInfinitePlaceRealFixedPlace
        (K := K) (L := L) v hRamified)).IsRamified
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
theorem

ramifiedInfinitePlaceOverextension_localArtin_neg_one

L188 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextension_localArtin_neg_one
Documentation

At the concrete real fixed-field place, the local Artin symbol of negative one is the distinguished ambient complex conjugation.

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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {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_localArtin_neg_one
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    chosenInfinitePlaceArtinMonoidHom
        (K :=
          ramifiedInfinitePlaceRealFixedField
            (K := K) (L := L) v hRamified)
        (L :=
          infinitePlaceComplexificationOverfield
            (K := K) (L := L) v)
        (ramifiedInfinitePlaceRealFixedPlace
          (K := K) (L := L) v hRamified)
        (-1 :
          (ramifiedInfinitePlaceRealFixedPlace
            (K := K) (L := L) v hRamified).Completionˣ) =
      ramifiedInfinitePlaceOverextensionConjugation
        (K := K) (L := L) v hRamified
theorem

ramifiedInfinitePlaceOverextension_globalNormResidue_neg_one

L242 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextension_globalNormResidue_neg_one
Documentation

The canonical global norm-residue value of the concrete fixed-field one-place negative-one class is ambient complex conjugation.

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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {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_globalNormResidue_neg_one
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    globalNormResidueMonoidHom
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v)
        (IdeleGroup.infinitePlaceIdeleClass
          (ramifiedInfinitePlaceRealFixedPlace
            (K := K) (L := L) v hRamified)
          (-1 :
            (ramifiedInfinitePlaceRealFixedPlace
              (K := K) (L := L) v hRamified).Completionˣ)) =
      ramifiedInfinitePlaceOverextensionConjugation
        (K := K) (L := L) v hRamified
def

ramifiedInfinitePlaceOverextensionRestriction

L266 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionRestriction
Documentation

Restriction from the complex-conjugation overextension back to the original finite abelian extension.

Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def ramifiedInfinitePlaceOverextensionRestriction
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    Gal(
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) /
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)) →*
      Gal(L / K)
theorem

ramifiedInfinitePlaceOverextensionRestriction_conjugation

L283 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionRestriction_conjugation
Documentation

Restricting ambient complex conjugation from L(i) to L recovers the actual chosen local Artin symbol of negative one at the original ramified place.

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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [FiniteDimensional K L] in
Lean source · statement
theorem ramifiedInfinitePlaceOverextensionRestriction_conjugation
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    ramifiedInfinitePlaceOverextensionRestriction
        (K := K) (L := L) v hRamified
        (ramifiedInfinitePlaceOverextensionConjugation
          (K := K) (L := L) v hRamified) =
      chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v
        (-1 : v.Completionˣ)
def

infinitePlaceComplexificationOverfieldSeparableClosureEmbedding

L347 ↗
GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfieldSeparableClosureEmbedding
Documentation

A rational-separable-closure embedding of the complexification overfield extending the standard embedding of its original top field.

Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    infinitePlaceComplexificationOverfieldSeparableClosureEmbedding
    (v : InfinitePlace K) :
    infinitePlaceComplexificationOverfield
        (K := K) (L := L) v →ₐ[ℚ]
      SeparableClosure ℚ
theorem

infinitePlaceComplexificationOverfieldSeparableClosureEmbedding_restrictDomain

L366 ↗
GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationOverfieldSeparableClosureEmbedding_restrictDomain
Documentation

The separable-closure embedding of the complexification overfield restricts to the standard embedding of its original top field.

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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {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
    infinitePlaceComplexificationOverfieldSeparableClosureEmbedding_restrictDomain
    (v : InfinitePlace K) :
    (infinitePlaceComplexificationOverfieldSeparableClosureEmbedding
      (K := K) (L := L) v).domRestrict L =
        AlgebraicNumberTheory.numberFieldSeparableClosureEmbedding L
theorem

ramifiedInfinitePlaceOverextension_globalNormResidueOfEmbedding_eq_one_iff

L385 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextension_globalNormResidueOfEmbedding_eq_one_iff
Documentation

The explicitly embedded norm-residue map for the quadratic overextension has the genuine idele-class norm range as its kernel.

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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {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_globalNormResidueOfEmbedding_eq_one_iff
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (j :
      infinitePlaceComplexificationOverfield
          (K := K) (L := L) v →ₐ[ℚ]
        SeparableClosure ℚ)
    (c :
      IdeleClassGroup
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)) :
    globalNormResidueMonoidHomOfEmbedding
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v)
        j c =
      1 ↔
    c ∈
      (_root_.ideleClassNorm
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v)).range
theorem

ramifiedInfinitePlaceOverextension_globalNormResidueOfEmbedding_neg_one

L485 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextension_globalNormResidueOfEmbedding_neg_one
Documentation

For every rational-separable-closure embedding, the norm-residue value of the concrete upper negative-one one-place class is ambient complex conjugation. The point is independent of the embedding because the upper Galois group is the actual two-element group and all these maps have the same genuine norm kernel.

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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {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_globalNormResidueOfEmbedding_neg_one
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K)
    (j :
      infinitePlaceComplexificationOverfield
          (K := K) (L := L) v →ₐ[ℚ]
        SeparableClosure ℚ) :
    globalNormResidueMonoidHomOfEmbedding
        (ramifiedInfinitePlaceRealFixedField
          (K := K) (L := L) v hRamified)
        (infinitePlaceComplexificationOverfield
          (K := K) (L := L) v)
        j
        (IdeleGroup.infinitePlaceIdeleClass
          (ramifiedInfinitePlaceRealFixedPlace
            (K := K) (L := L) v hRamified)
          (-1 :
            (ramifiedInfinitePlaceRealFixedPlace
              (K := K) (L := L) v hRamified).Completionˣ)) =
      ramifiedInfinitePlaceOverextensionConjugation
        (K := K) (L := L) v hRamified
def

ramifiedInfinitePlaceGlobalNormResidueNegOneValue

L570 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceGlobalNormResidueNegOneValue
Documentation

The base global norm-residue value at the negative-one class of v.

Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def ramifiedInfinitePlaceGlobalNormResidueNegOneValue
    (v : InfinitePlace K) :
    Gal(L / K)
def

ramifiedInfinitePlaceLocalArtinNegOneValue

L577 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceLocalArtinNegOneValue
Documentation

The chosen local Artin value at negative one at v.

Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def ramifiedInfinitePlaceLocalArtinNegOneValue
    (v : InfinitePlace K) :
    Gal(L / K)
def

infinitePlaceComplexificationLowerSeparableClosureEmbedding

L585 ↗
GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationLowerSeparableClosureEmbedding
Documentation

The embedding of L induced by the chosen embedding of its complexification overfield.

Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    infinitePlaceComplexificationLowerSeparableClosureEmbedding
    (v : InfinitePlace K) :
    L →ₐ[ℚ] SeparableClosure ℚ
theorem

infinitePlaceComplexificationLowerSeparableClosureEmbedding_eq_standard

L597 ↗
GlobalClassFieldTheory.Reciprocity.infinitePlaceComplexificationLowerSeparableClosureEmbedding_eq_standard
Documentation

The induced lower embedding is the standard number-field embedding.

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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {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
    infinitePlaceComplexificationLowerSeparableClosureEmbedding_eq_standard
    (v : InfinitePlace K) :
    infinitePlaceComplexificationLowerSeparableClosureEmbedding
        (K := K) (L := L) v =
      AlgebraicNumberTheory.numberFieldSeparableClosureEmbedding L
def

ramifiedInfinitePlaceOverextensionNegOneIdeleClass

L610 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionNegOneIdeleClass
Documentation

The upper negative-one idele class used in the overextension diamond.

Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def ramifiedInfinitePlaceOverextensionNegOneIdeleClass
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    IdeleClassGroup
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified)
def

ramifiedInfinitePlaceOverextensionGlobalNormResidueNegOneValue

L625 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceOverextensionGlobalNormResidueNegOneValue
Documentation

The upper global norm-residue value in the overextension diamond.

Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    ramifiedInfinitePlaceOverextensionGlobalNormResidueNegOneValue
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    Gal(
      (infinitePlaceComplexificationOverfield
        (K := K) (L := L) v) /
      (ramifiedInfinitePlaceRealFixedField
        (K := K) (L := L) v hRamified))
def

ramifiedInfinitePlaceRestrictedOverextensionNormResidueNegOneValue

L646 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceRestrictedOverextensionNormResidueNegOneValue
Documentation

The upper norm-residue value after actual Galois restriction.

Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    ramifiedInfinitePlaceRestrictedOverextensionNormResidueNegOneValue
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    Gal(L / K)
def

ramifiedInfinitePlaceNormedOverextensionNormResidueNegOneValue

L658 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlaceNormedOverextensionNormResidueNegOneValue
Documentation

The lower norm-residue value of the normed upper negative-one class.

Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    ramifiedInfinitePlaceNormedOverextensionNormResidueNegOneValue
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    Gal(L / K)
theorem

ramifiedInfinitePlace_normResidueDiamond_neg_one

L673 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlace_normResidueDiamond_neg_one
Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem ramifiedInfinitePlace_normResidueDiamond_neg_one
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    ramifiedInfinitePlaceRestrictedOverextensionNormResidueNegOneValue
        (K := K) (L := L) v hRamified =
      ramifiedInfinitePlaceNormedOverextensionNormResidueNegOneValue
        (K := K) (L := L) v hRamified
theorem

ramifiedInfinitePlace_restrictedOverextensionNormResidue_neg_one

L697 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlace_restrictedOverextensionNormResidue_neg_one
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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [FiniteDimensional K L] in
Lean source · statement
theorem
    ramifiedInfinitePlace_restrictedOverextensionNormResidue_neg_one
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    ramifiedInfinitePlaceRestrictedOverextensionNormResidueNegOneValue
        (K := K) (L := L) v hRamified =
      ramifiedInfinitePlaceLocalArtinNegOneValue
        (K := K) (L := L) v
theorem

ramifiedInfinitePlace_normedNormResidue_neg_one

L714 ↗
GlobalClassFieldTheory.Reciprocity.ramifiedInfinitePlace_normedNormResidue_neg_one
Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem ramifiedInfinitePlace_normedNormResidue_neg_one
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    ramifiedInfinitePlaceNormedOverextensionNormResidueNegOneValue
        (K := K) (L := L) v hRamified =
      ramifiedInfinitePlaceGlobalNormResidueNegOneValue
        (K := K) (L := L) v
theorem

globalNormResidueMonoidHom_infinitePlaceIdeleClass_neg_one_of_ramified

L748 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_infinitePlaceIdeleClass_neg_one_of_ramified
Documentation

At every ramified real place of a finite abelian extension, the canonical global norm-residue symbol of the one-place negative-one idele class is the actual chosen local Artin symbol.

The proof is the concrete complex-conjugation overextension diamond: the upper equality is the rational fourth-root product formula, the vertical map on idele classes is the genuine one-place norm, and the vertical map on Galois groups is actual restriction.

Source context 9 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]
local instance
    infinitePlaceCompatibilityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem
    globalNormResidueMonoidHom_infinitePlaceIdeleClass_neg_one_of_ramified
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    ramifiedInfinitePlaceGlobalNormResidueNegOneValue
        (K := K) (L := L) v =
      ramifiedInfinitePlaceLocalArtinNegOneValue
        (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.