Module

RationalComplexification.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.RationalComplexification

29 declarations indexed from sourceView source ↗

Module documentation

The rational cyclotomic complexification

This module realizes the quadratic complexification as the fourth-root cyclotomic field and proves the rational principal-idele Artin formula.

Imports4

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.RationalCyclotomicPrincipalProduct
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.InfiniteOnePlaceBaseNorm
Mathlib.NumberTheory.NumberField.CMField
Mathlib.RingTheory.RootsOfUnity.Complex

Imported by4

def

rationalComplexificationPrime

L32 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationPrime

Documentation

The rational prime used to realize the quadratic complexification as the fourth-root cyclotomic field.

Source context 6 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

def rationalComplexificationPrime : Nat.Primes

abbrev

rationalComplexificationCyclotomicOrder

L36 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCyclotomicOrder

Documentation

The cyclotomic level 4 used for the rational complexification.

Source context 6 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

abbrev rationalComplexificationCyclotomicOrder : ℕ+

instance

rationalComplexificationPrimeFact

L40 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationPrimeFact

Source context 6 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime

instance

rationalComplexificationPrimeSquareNeZero

L44 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationPrimeSquareNeZero

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩

Lean source · statement

instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2)

abbrev

rationalComplexificationCyclotomicField

L50 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCyclotomicField

Documentation

The actual rational cyclotomic field generated by fourth roots of unity, inside the rational cyclotomic closure.

Source context 8 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩

Lean source · statement

abbrev rationalComplexificationCyclotomicField :
    IntermediateField ℚ KummerTheory.rationalCyclotomicField

instance

rationalComplexificationCyclotomicField_isCyclotomicFour

L55 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCyclotomicField_isCyclotomicFour

Source context 8 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩

Lean source · statement

instance
    rationalComplexificationCyclotomicField_isCyclotomicFour :
    IsCyclotomicExtension {4} ℚ
      rationalComplexificationCyclotomicField

instance

rationalComplexificationCyclotomicField_isCMField

L67 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCyclotomicField_isCMField

Source context 8 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩

Lean source · statement

instance
    rationalComplexificationCyclotomicField_isCMField :
    NumberField.IsCMField rationalComplexificationCyclotomicField

instance

rationalComplexificationCyclotomicField_finiteDimensional

L76 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCyclotomicField_finiteDimensional

Source context 8 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩

Lean source · statement

instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField

instance

rationalComplexificationCyclotomicField_numberField

L82 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCyclotomicField_numberField

Source context 9 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder

Lean source · statement

instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField

instance

rationalComplexificationCyclotomicField_isAbelianGalois

L88 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCyclotomicField_isAbelianGalois

Source context 10 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder

Lean source · statement

instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField

theorem

complexI_isPrimitiveRoot_four

L95 ↗

GlobalClassFieldTheory.Reciprocity.complexI_isPrimitiveRoot_four

Documentation

The complex number I is a primitive fourth root of unity.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem complexI_isPrimitiveRoot_four :
    IsPrimitiveRoot Complex.I 4

def

complexFourthRootField

L112 ↗

GlobalClassFieldTheory.Reciprocity.complexFourthRootField

Documentation

The concrete fourth-root cyclotomic field inside ℂ.

It is defined by adjoining all fourth roots of unity, so it is independent of a choice between I and -I and is visibly preserved by complex conjugation.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

def complexFourthRootField :
    IntermediateField ℚ ℂ

instance

complexFourthRootField_isCyclotomic

L118 ↗

GlobalClassFieldTheory.Reciprocity.complexFourthRootField_isCyclotomic

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

instance complexFourthRootField_isCyclotomic :
    IsCyclotomicExtension {4} ℚ complexFourthRootField

instance

complexFourthRootField_finiteDimensional

L128 ↗

GlobalClassFieldTheory.Reciprocity.complexFourthRootField_finiteDimensional

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

instance complexFourthRootField_finiteDimensional :
    FiniteDimensional ℚ complexFourthRootField

instance

complexFourthRootField_numberField

L133 ↗

GlobalClassFieldTheory.Reciprocity.complexFourthRootField_numberField

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

instance complexFourthRootField_numberField :
    NumberField complexFourthRootField

def

rationalComplexificationComplexEquiv

L141 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationComplexEquiv

Documentation

Identification of the abstract rational fourth-root cyclotomic field used by the rational product formula with its concrete copy in ℂ.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

def rationalComplexificationComplexEquiv :
    rationalComplexificationCyclotomicField ≃ₐ[ℚ]
      complexFourthRootField

theorem

complexFourthRootField_map_complexConjugation

L151 ↗

GlobalClassFieldTheory.Reciprocity.complexFourthRootField_map_complexConjugation

Documentation

The concrete fourth-root field is stable under complex conjugation.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem complexFourthRootField_map_complexConjugation :
    complexFourthRootField.map
        (Complex.conjAe.restrictScalars ℚ).toAlgHom =
      complexFourthRootField

theorem

rationalComplexification_chosenInfinitePlace_isRamified

L172 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexification_chosenInfinitePlace_isRamified

Documentation

The chosen infinite place of the rational complexification is ramified over the unique real place of ℚ.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem rationalComplexification_chosenInfinitePlace_isRamified :
    (chosenInfinitePlaceAbove
      (L := rationalComplexificationCyclotomicField)
      Rat.infinitePlace).IsRamified ℚ

theorem

rationalComplexification_galoisGroup_card

L184 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexification_galoisGroup_card

Documentation

The rational fourth-root cyclotomic field has Galois group of order two.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem
    rationalComplexification_galoisGroup_card :
    Nat.card
        (rationalComplexificationCyclotomicField ≃ₐ[ℚ]
          rationalComplexificationCyclotomicField) =
      2

theorem

rationalPrincipalInfiniteComponent_realCoordinate

L212 ↗

GlobalClassFieldTheory.Reciprocity.rationalPrincipalInfiniteComponent_realCoordinate

Documentation

The real coordinate of the infinite component of a rational principal idele is the original rational number.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem
    rationalPrincipalInfiniteComponent_realCoordinate
    (x : ℚˣ) :
    InfinitePlace.Completion.ringEquivRealOfIsReal
        Rat.isReal_infinitePlace
        ((IdeleGroup.infiniteComponent
          Rat.infinitePlace
          (IdeleGroup.principalIdele ℚ x) :
            Rat.infinitePlace.Completionˣ) :
          Rat.infinitePlace.Completion) =
      (x : ℚ)

theorem

rationalComplexificationPrincipalInfiniteArtin_eq_one_of_num_pos

L230 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationPrincipalInfiniteArtin_eq_one_of_num_pos

Documentation

A rational principal idele with positive numerator has trivial infinite Artin factor in the rational complexification.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem
    rationalComplexificationPrincipalInfiniteArtin_eq_one_of_num_pos
    (x : ℚˣ) (hx : 0 < (x : ℚ).num) :
    chosenInfinitePlaceArtinMonoidHom
        (K := ℚ)
        (L := rationalComplexificationCyclotomicField)
        Rat.infinitePlace
        (IdeleGroup.infiniteComponent
          Rat.infinitePlace
          (IdeleGroup.principalIdele ℚ x)) =
      1

theorem

rationalComplexificationPrincipalInfiniteArtin_ne_one_of_num_neg

L251 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationPrincipalInfiniteArtin_ne_one_of_num_neg

Documentation

A rational principal idele with negative numerator has nontrivial infinite Artin factor in the rational complexification.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem
    rationalComplexificationPrincipalInfiniteArtin_ne_one_of_num_neg
    (x : ℚˣ) (hx : (x : ℚ).num < 0) :
    chosenInfinitePlaceArtinMonoidHom
        (K := ℚ)
        (L := rationalComplexificationCyclotomicField)
        Rat.infinitePlace
        (IdeleGroup.infiniteComponent
          Rat.infinitePlace
          (IdeleGroup.principalIdele ℚ x)) ≠
      1

def

rationalComplexificationCharacter

L295 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCharacter

Documentation

The cyclotomic character of the rational fourth-root field.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

def rationalComplexificationCharacter :
    (rationalComplexificationCyclotomicField ≃ₐ[ℚ]
        rationalComplexificationCyclotomicField) ≃*
      (ZMod (rationalComplexificationPrime.1 ^ 2))ˣ

theorem

rationalComplexificationCharacter_apply

L306 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationCharacter_apply

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem rationalComplexificationCharacter_apply
    (σ : rationalComplexificationCyclotomicField ≃ₐ[ℚ]
      rationalComplexificationCyclotomicField) :
    rationalComplexificationCharacter σ =
      IsCyclotomicExtension.Rat.galEquivZMod
        (rationalComplexificationPrime.1 ^ 2)
        rationalComplexificationCyclotomicField
        (hK :=
          KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension
            rationalComplexificationCyclotomicOrder) σ

theorem

rationalComplexificationFiniteArtin_character

L320 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationFiniteArtin_character

Documentation

The finite-place Artin product of a rational principal idele in the fourth-root character is its rational sign unit.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem rationalComplexificationFiniteArtin_character
    (x : ℚˣ) :
    rationalComplexificationCharacter
        (∏ᶠ v : HeightOneSpectrum (𝓞 ℚ),
          chosenFinitePlaceArtinMonoidHom
            (K := ℚ)
            (L := rationalComplexificationCyclotomicField)
            v
            (IdeleGroup.finiteComponent v
              (IdeleGroup.principalIdele ℚ x))) =
      Units.map (PadicInt.toZModPow 2).toMonoidHom
        (rationalSignPadicUnit x rationalComplexificationPrime)

theorem

rationalComplexification_existsUnique_nontrivial

L365 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexification_existsUnique_nontrivial

Documentation

A group of order two has a unique nonidentity automorphism.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem rationalComplexification_existsUnique_nontrivial :
    ∃! σ :
      rationalComplexificationCyclotomicField ≃ₐ[ℚ]
        rationalComplexificationCyclotomicField,
      σ ≠ 1

theorem

rationalComplexification_signCharacter_ne_one_of_num_neg

L375 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexification_signCharacter_ne_one_of_num_neg

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem rationalComplexification_signCharacter_ne_one_of_num_neg
    (x : ℚˣ) (hx : (x : ℚ).num < 0) :
    Units.map (PadicInt.toZModPow 2).toMonoidHom
        (rationalSignPadicUnit x rationalComplexificationPrime) ≠
      1

theorem

rationalComplexification_signCharacter_eq_one_of_num_pos

L387 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexification_signCharacter_eq_one_of_num_pos

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem rationalComplexification_signCharacter_eq_one_of_num_pos
    (x : ℚˣ) (hx : 0 < (x : ℚ).num) :
    Units.map (PadicInt.toZModPow 2).toMonoidHom
        (rationalSignPadicUnit x rationalComplexificationPrime) =
      1

theorem

rationalComplexificationGlobalArtin_principalIdele

L400 ↗

GlobalClassFieldTheory.Reciprocity.rationalComplexificationGlobalArtin_principalIdele

Documentation

The chosen global Artin product for the actual rational complexification is trivial on every rational principal idele.

Source context 11 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance rationalComplexificationPrimeFact :
    Fact rationalComplexificationPrime.1.Prime :=
  ⟨rationalComplexificationPrime.2⟩
local instance rationalComplexificationPrimeSquareNeZero :
    NeZero (rationalComplexificationPrime.1 ^ 2) :=
  ⟨pow_ne_zero 2 rationalComplexificationPrime.2.ne_zero⟩
noncomputable local instance
    rationalComplexificationCyclotomicField_finiteDimensional :
    FiniteDimensional ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_numberField :
    NumberField rationalComplexificationCyclotomicField :=
  KummerTheory.rationalCyclotomicLevel_numberField
    rationalComplexificationCyclotomicOrder
noncomputable local instance
    rationalComplexificationCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ rationalComplexificationCyclotomicField :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
    rationalComplexificationCyclotomicOrder

Lean source · statement

theorem rationalComplexificationGlobalArtin_principalIdele
    (x : ℚˣ) :
    globalArtinMonoidHom
        (K := ℚ)
        (L := rationalComplexificationCyclotomicField)
        (IdeleGroup.principalIdele ℚ x) =
      1

Module documentation

The rational cyclotomic complexification

Declarations