Module

CyclotomicPrincipalIdele.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.CyclotomicPrincipalIdele

32 declarations indexed from sourceView source ↗

Module documentation

Principal ideles and the rational cyclotomic value

This file isolates the part of the rational principal-idele product formula which follows from the existing archimedean reciprocity API. Every rational idele is split into its archimedean and finite parts. The archimedean part has Artin image of order at most two at every finite layer; the actual Galois group of the rational ZHat-extension is torsion-free, so its image in that extension is trivial.

Consequently the rational cyclotomic value of a principal idele is exactly the value of its finite part. At every finite cyclotomic layer that remaining value is the genuine finite product of the chosen local Artin maps. Proving that product trivial requires a pointwise compatibility theorem between the chosen finite-place Artin map and the explicit cyclotomic action; no such compatibility is assumed here.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.CyclotomicIdeleValue

Imported by3

instance

rationalCyclotomicPrimePowerNumberField

L39 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrimePowerNumberField

Source context 5 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.

Lean source · statement

instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩)

instance

rationalCyclotomicPrimePowerIsGalois

L47 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrimePowerIsGalois

Source context 6 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩

Lean source · statement

instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩)

instance

rationalCyclotomicPrimePowerIsAbelianGalois

L55 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrimePowerIsAbelianGalois

Source context 7 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩

Lean source · statement

instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩)

instance

(anonymous instance)

L64 ↗

Source context 8 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val

Lean source · statement

instance (p : Nat.Primes) : Fact p.1.Prime

instance

cyclotomicPrincipalLevelIsAbelianGalois

L67 ↗

GlobalClassFieldTheory.Reciprocity.cyclotomicPrincipalLevelIsAbelianGalois

Source context 9 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · statement

instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m)

theorem

finiteSubfieldOfRationalCyclotomicField_le_level

L88 ↗

GlobalClassFieldTheory.Reciprocity.finiteSubfieldOfRationalCyclotomicField_le_level

Documentation

Every finite subextension of the rational cyclotomic closure is contained in one of its internal finite cyclotomic levels. The proof uses finite generation of the intermediate field together with the divisibility-directed presentation of ℚ(μ∞).

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem finiteSubfieldOfRationalCyclotomicField_le_level
    (E :
      IntermediateField ℚ
        KummerTheory.rationalCyclotomicField)
    [FiniteDimensional ℚ E] :
    ∃ n : ℕ+,
      E ≤ KummerTheory.rationalCyclotomicLevel n

theorem

finiteSubfieldOfRationalCyclotomicZHatField_mapsIntoLevel

L169 ↗

GlobalClassFieldTheory.Reciprocity.finiteSubfieldOfRationalCyclotomicZHatField_mapsIntoLevel

Documentation

Every finite Galois coordinate of the rational cyclotomic ZHat-extension has a canonical image inside a finite internal cyclotomic level. The image field is retained explicitly so that restriction of actual global Artin automorphisms can be applied in a scalar tower.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem finiteSubfieldOfRationalCyclotomicZHatField_mapsIntoLevel
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    ∃ (n : ℕ+)
        (F :
          IntermediateField ℚ
            KummerTheory.rationalCyclotomicField)
        (_e : E ≃ₐ[ℚ] F),
      F ≤ KummerTheory.rationalCyclotomicLevel n

theorem

rationalCyclotomicFullRestrictionToZHat_commutes

L207 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicFullRestrictionToZHat_commutes

Documentation

Restriction to the lifted torsion-free cyclotomic field commutes with its canonical inclusion into the full rational cyclotomic field. Keeping this pointwise compatibility separate prevents the finite-coordinate Artin comparison below from accumulating the cost of unfolding the lift.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalCyclotomicFullRestrictionToZHat_commutes
    (σ : KummerTheory.rationalCyclotomicField ≃ₐ[ℚ]
      KummerTheory.rationalCyclotomicField)
    (x : rationalCyclotomicZHatField) :
    (IntermediateField.inclusion
        (IntermediateField.lift_le
          KummerTheory.rationalCyclotomicTorsionFixedField))
        (rationalCyclotomicFullRestrictionToZHat σ x) =
      σ
        ((IntermediateField.inclusion
          (IntermediateField.lift_le
            KummerTheory.rationalCyclotomicTorsionFixedField)) x)

theorem

restrictNormalHom_eq_of_commuting_square

L255 ↗

GlobalClassFieldTheory.Reciprocity.restrictNormalHom_eq_of_commuting_square

Documentation

Restriction along the two sides of a commuting tower square gives the same automorphism of the finite bottom field. Keeping the field types abstract makes this a stable interface for concrete inverse-limit fields.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem restrictNormalHom_eq_of_commuting_square
    (K E Z Ω : Type*)
    [Field K] [Field E] [Field Z] [Field Ω]
    [Algebra K E] [Algebra K Z] [Algebra K Ω]
    [Algebra E Z] [Algebra E Ω] [Algebra Z Ω]
    [IsScalarTower K E Z] [IsScalarTower K E Ω]
    [IsScalarTower K Z Ω] [IsScalarTower E Z Ω]
    [Normal K E]
    (τ : Z ≃ₐ[K] Z) (σ : Ω ≃ₐ[K] Ω)
    (hcommutes : ∀ z : Z,
      algebraMap Z Ω (τ z) = σ (algebraMap Z Ω z)) :
    AlgEquiv.restrictNormalHom E τ =
      AlgEquiv.restrictNormalHom E σ

theorem

rationalCyclotomicZHatGlobalArtin_eq_fullRestriction

L290 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatGlobalArtin_eq_fullRestriction

Documentation

The infinite Artin automorphism of the actual rational ZHat-field is the restriction of the infinite Artin automorphism of the full rational cyclotomic field. The statement uses the genuine torsion-fixed subfield and its actual lift inside SeparableClosure ℚ.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalCyclotomicZHatGlobalArtin_eq_fullRestriction
    (a : IdeleGroup ℚ) :
    rationalCyclotomicZHatGlobalArtin a =
      rationalCyclotomicFullRestrictionToZHat
        (infiniteGlobalArtinMonoidHom
          ℚ KummerTheory.rationalCyclotomicField a)

theorem

rationalCyclotomicZHatIdeleValue_eq_fullCharacterFreePart

L388 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValue_eq_fullCharacterFreePart

Documentation

The rational cyclotomic idele value is the genuine torsion-free factor of the full cyclotomic character of its infinite Artin symbol.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalCyclotomicZHatIdeleValue_eq_fullCharacterFreePart
    (a : IdeleGroup ℚ) :
    rationalCyclotomicZHatIdeleValue a =
      (KummerTheory.zHatUnitsDecomposition
        (KummerTheory.rationalCyclotomicCharacterContinuousMulEquiv
          (infiniteGlobalArtinMonoidHom
            ℚ KummerTheory.rationalCyclotomicField a))).1

def

rationalIdeleArchimedeanPart

L401 ↗

GlobalClassFieldTheory.Reciprocity.rationalIdeleArchimedeanPart

Documentation

The archimedean part of a rational idele, with all finite components replaced by one.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

def rationalIdeleArchimedeanPart
    (a : IdeleGroup ℚ) :
    IdeleGroup ℚ

def

rationalIdeleFinitePart

L408 ↗

GlobalClassFieldTheory.Reciprocity.rationalIdeleFinitePart

Documentation

The finite part of a rational idele, with its archimedean component replaced by one.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

def rationalIdeleFinitePart
    (a : IdeleGroup ℚ) :
    IdeleGroup ℚ

theorem

rationalIdeleArchimedeanPart_infiniteComponent

L415 ↗

GlobalClassFieldTheory.Reciprocity.rationalIdeleArchimedeanPart_infiniteComponent

Documentation

The archimedean part preserves every infinite component.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalIdeleArchimedeanPart_infiniteComponent
    (a : IdeleGroup ℚ)
    (v : InfinitePlace ℚ) :
    IdeleGroup.infiniteComponent v
        (rationalIdeleArchimedeanPart a) =
      IdeleGroup.infiniteComponent v a

theorem

rationalIdeleArchimedeanPart_finiteComponent

L425 ↗

GlobalClassFieldTheory.Reciprocity.rationalIdeleArchimedeanPart_finiteComponent

Documentation

Every finite component of the archimedean part is one.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalIdeleArchimedeanPart_finiteComponent
    (a : IdeleGroup ℚ)
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    IdeleGroup.finiteComponent v
        (rationalIdeleArchimedeanPart a) =
      1

theorem

rationalIdeleFinitePart_infiniteComponent

L435 ↗

GlobalClassFieldTheory.Reciprocity.rationalIdeleFinitePart_infiniteComponent

Documentation

Every infinite component of the finite part is one.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalIdeleFinitePart_infiniteComponent
    (a : IdeleGroup ℚ)
    (v : InfinitePlace ℚ) :
    IdeleGroup.infiniteComponent v
        (rationalIdeleFinitePart a) =
      1

theorem

rationalIdeleFinitePart_finiteComponent

L445 ↗

GlobalClassFieldTheory.Reciprocity.rationalIdeleFinitePart_finiteComponent

Documentation

The finite part preserves every finite component.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalIdeleFinitePart_finiteComponent
    (a : IdeleGroup ℚ)
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    IdeleGroup.finiteComponent v
        (rationalIdeleFinitePart a) =
      IdeleGroup.finiteComponent v a

theorem

globalArtinMonoidHom_rationalIdeleFinitePart

L453 ↗

GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_rationalIdeleFinitePart

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem globalArtinMonoidHom_rationalIdeleFinitePart
    {L : Type}
    [Field L] [NumberField L] [Algebra ℚ L]
    [IsAbelianGalois ℚ L]
    (a : IdeleGroup ℚ) :
    globalArtinMonoidHom (K := ℚ) (L := L)
        (rationalIdeleFinitePart a) =
      ∏ᶠ v : HeightOneSpectrum (𝓞 ℚ),
        chosenFinitePlaceArtinMonoidHom
          (K := ℚ) (L := L) v
          (IdeleGroup.finiteComponent v a)

theorem

rationalIdeleArchimedeanPart_mul_finitePart

L489 ↗

GlobalClassFieldTheory.Reciprocity.rationalIdeleArchimedeanPart_mul_finitePart

Documentation

The archimedean and finite parts multiply back to the original rational idele.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalIdeleArchimedeanPart_mul_finitePart
    (a : IdeleGroup ℚ) :
    rationalIdeleArchimedeanPart a *
        rationalIdeleFinitePart a =
      a

theorem

globalArtinMonoidHom_rationalIdeleArchimedeanPart_sq

L499 ↗

GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_rationalIdeleArchimedeanPart_sq

Documentation

At a finite abelian layer, the global Artin image of the archimedean part of a rational idele has order at most two.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem globalArtinMonoidHom_rationalIdeleArchimedeanPart_sq
    {L : Type}
    [Field L] [NumberField L] [Algebra ℚ L]
    [IsAbelianGalois ℚ L]
    (a : IdeleGroup ℚ) :
    globalArtinMonoidHom
          (K := ℚ) (L := L)
          (rationalIdeleArchimedeanPart a) ^ 2 =
      1

theorem

rationalCyclotomicZHatGlobalArtin_rationalIdeleArchimedeanPart

L553 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatGlobalArtin_rationalIdeleArchimedeanPart

Documentation

The actual rational ZHat Artin homomorphism kills every idele supported at the archimedean place. The finite-layer images have order at most two, while the inverse-limit Galois group is torsion-free.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem
    rationalCyclotomicZHatGlobalArtin_rationalIdeleArchimedeanPart
    (a : IdeleGroup ℚ) :
    rationalCyclotomicZHatGlobalArtin
        (rationalIdeleArchimedeanPart a) =
      1

theorem

rationalCyclotomicZHatIdeleValue_rationalIdeleArchimedeanPart

L606 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValue_rationalIdeleArchimedeanPart

Documentation

The rational cyclotomic value kills the archimedean part of every rational idele.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem
    rationalCyclotomicZHatIdeleValue_rationalIdeleArchimedeanPart
    (a : IdeleGroup ℚ) :
    rationalCyclotomicZHatIdeleValue
        (rationalIdeleArchimedeanPart a) =
      1

theorem

rationalCyclotomicZHatIdeleValue_eq_finitePart

L618 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValue_eq_finitePart

Documentation

The rational cyclotomic value depends only on the finite part of an idele.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalCyclotomicZHatIdeleValue_eq_finitePart
    (a : IdeleGroup ℚ) :
    rationalCyclotomicZHatIdeleValue a =
      rationalCyclotomicZHatIdeleValue
        (rationalIdeleFinitePart a)

theorem

rationalCyclotomicGlobalArtin_restrict_primePowerLevel

L643 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicGlobalArtin_restrict_primePowerLevel

Documentation

Restriction of the infinite Artin symbol to a concrete prime-power cyclotomic level is its finite global Artin symbol.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalCyclotomicGlobalArtin_restrict_primePowerLevel
    (a : IdeleGroup ℚ) (p : Nat.Primes) (k : ℕ) :
    AlgEquiv.restrictNormalHom
        (KummerTheory.rationalCyclotomicLevel
          ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        (infiniteGlobalArtinMonoidHom
          ℚ KummerTheory.rationalCyclotomicField a) =
      globalArtinMonoidHom
        (K := ℚ)
        (L := KummerTheory.rationalCyclotomicLevel
          ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        a

theorem

rationalCyclotomicGlobalArtin_projection_toZModPow

L665 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicGlobalArtin_projection_toZModPow

Documentation

Applying the prime-power cyclotomic character to a finite projection of the infinite Artin symbol gives the finite global Artin symbol. This is kept separate from character evaluation so both dependent comparisons elaborate within the default heartbeat budget.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalCyclotomicGlobalArtin_projection_toZModPow
    (a : IdeleGroup ℚ) (p : Nat.Primes) (k : ℕ) :
    IsCyclotomicExtension.Rat.galEquivZMod
        (p.1 ^ k)
        (KummerTheory.rationalCyclotomicLevel
          ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        (hK :=
          KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        ((infiniteGlobalArtinMonoidHom
            ℚ KummerTheory.rationalCyclotomicField a).restrictNormal
          (KummerTheory.rationalCyclotomicLevel
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩)) =
      IsCyclotomicExtension.Rat.galEquivZMod
        (p.1 ^ k)
        (KummerTheory.rationalCyclotomicLevel
          ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        (hK :=
          KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        (globalArtinMonoidHom
          (K := ℚ)
          (L := KummerTheory.rationalCyclotomicLevel
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
          a)

theorem

rationalCyclotomicGlobalArtin_character_toZModPow

L706 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicGlobalArtin_character_toZModPow

Documentation

Evaluating the actual infinite global Artin symbol in the full rational cyclotomic extension at the p ^ k cyclotomic character is exactly the finite global Artin symbol at the internal p ^ k-th cyclotomic level. This is the field-theoretic bridge from the inverse limit Artin map to the explicit cyclotomic character.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalCyclotomicGlobalArtin_character_toZModPow
    (a : IdeleGroup ℚ) (p : Nat.Primes) (k : ℕ) :
    Units.map (PadicInt.toZModPow k).toMonoidHom
        (KummerTheory.rationalCyclotomicCharacterPrimeProduct
          (infiniteGlobalArtinMonoidHom
            ℚ KummerTheory.rationalCyclotomicField a) p) =
      IsCyclotomicExtension.Rat.galEquivZMod
        (p.1 ^ k)
        (KummerTheory.rationalCyclotomicLevel
          ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        (hK :=
          KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        (globalArtinMonoidHom
          (K := ℚ)
          (L :=
            KummerTheory.rationalCyclotomicLevel
              ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
          a)

theorem

rationalCyclotomicGlobalArtin_character_toZModPow_finitePart

L734 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicGlobalArtin_character_toZModPow_finitePart

Documentation

After removing the archimedean component, the p ^ k coordinate of the full rational cyclotomic Artin character is the genuine finite product of the chosen finite-place Artin maps.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem rationalCyclotomicGlobalArtin_character_toZModPow_finitePart
    (a : IdeleGroup ℚ) (p : Nat.Primes) (k : ℕ) :
    Units.map (PadicInt.toZModPow k).toMonoidHom
        (KummerTheory.rationalCyclotomicCharacterPrimeProduct
          (infiniteGlobalArtinMonoidHom
            ℚ KummerTheory.rationalCyclotomicField
            (rationalIdeleFinitePart a)) p) =
      IsCyclotomicExtension.Rat.galEquivZMod
        (p.1 ^ k)
        (KummerTheory.rationalCyclotomicLevel
          ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        (hK :=
          KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        (∏ᶠ v : HeightOneSpectrum (𝓞 ℚ),
          chosenFinitePlaceArtinMonoidHom
            (K := ℚ)
            (L :=
              KummerTheory.rationalCyclotomicLevel
                ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
            v
            (IdeleGroup.finiteComponent v a))

theorem

rationalCyclotomicGlobalArtin_character_toZModPow_finitePart_eq_finprod

L764 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicGlobalArtin_character_toZModPow_finitePart_eq_finprod

Documentation

The finite-part cyclotomic character is the finprod of the actual chosen local Artin characters. This is the pointwise form into which the p-adic unit formula and the unramified Frobenius formula substitute directly.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem
    rationalCyclotomicGlobalArtin_character_toZModPow_finitePart_eq_finprod
    (a : IdeleGroup ℚ) (p : Nat.Primes) (k : ℕ) :
    Units.map (PadicInt.toZModPow k).toMonoidHom
        (KummerTheory.rationalCyclotomicCharacterPrimeProduct
          (infiniteGlobalArtinMonoidHom
            ℚ KummerTheory.rationalCyclotomicField
            (rationalIdeleFinitePart a)) p) =
      ∏ᶠ v : HeightOneSpectrum (𝓞 ℚ),
        IsCyclotomicExtension.Rat.galEquivZMod
          (p.1 ^ k)
          (KummerTheory.rationalCyclotomicLevel
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
          (hK :=
            KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension
              ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
          (chosenFinitePlaceArtinMonoidHom
            (K := ℚ)
            (L :=
              KummerTheory.rationalCyclotomicLevel
                ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
            v
            (IdeleGroup.finiteComponent v a))

theorem

rationalCyclotomicZHatIdeleValue_principalIdele_eq_finitePart

L806 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValue_principalIdele_eq_finitePart

Documentation

Principal-idele evaluation reduced to its genuine finite local part.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem
    rationalCyclotomicZHatIdeleValue_principalIdele_eq_finitePart
    (x : ℚˣ) :
    rationalCyclotomicZHatIdeleValue
        (IdeleGroup.principalIdele ℚ x) =
      rationalCyclotomicZHatIdeleValue
        (rationalIdeleFinitePart
          (IdeleGroup.principalIdele ℚ x))

theorem

restrictNormalHom_rationalCyclotomicZHatGlobalArtin_finitePart

L820 ↗

GlobalClassFieldTheory.Reciprocity.restrictNormalHom_rationalCyclotomicZHatGlobalArtin_finitePart

Documentation

At a finite cyclotomic layer, the Artin image of the finite part of a rational idele is exactly the finite product of the chosen local Artin symbols.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · full declaration

theorem
    restrictNormalHom_rationalCyclotomicZHatGlobalArtin_finitePart
    (a : IdeleGroup ℚ)
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    letI : NumberField E :=
      NumberField.of_module_finite ℚ E
    letI : IsAbelianGalois ℚ E :=
      IsAbelianGalois.of_algHom E.toIntermediateField.val
    AlgEquiv.restrictNormalHom E
        (rationalCyclotomicZHatGlobalArtin
          (rationalIdeleFinitePart a)) =
      ∏ᶠ v : HeightOneSpectrum (𝓞 ℚ),
        chosenFinitePlaceArtinMonoidHom
          (K := ℚ) (L := E) v
          (IdeleGroup.finiteComponent v a) := by
  let hE : NumberField E :=
    NumberField.of_module_finite ℚ E
  let hAbelian : IsAbelianGalois ℚ E :=
    IsAbelianGalois.of_algHom E.toIntermediateField.val
  let _ : NumberField E := hE
  let _ : IsAbelianGalois ℚ E := hAbelian
  exact
    (restrictNormalHom_rationalCyclotomicZHatGlobalArtin_of_structures
      (rationalIdeleFinitePart a) E hE hAbelian).trans
      (globalArtinMonoidHom_rationalIdeleFinitePart
        (L := E) a)

theorem

cyclotomicZHatNormComposite_principalIdele_eq_finitePart

L852 ↗

GlobalClassFieldTheory.Reciprocity.cyclotomicZHatNormComposite_principalIdele_eq_finitePart

Documentation

The unnormalized value on a principal idele over a number field is the rational cyclotomic value of the finite part of its field-norm principal idele.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem cyclotomicZHatNormComposite_principalIdele_eq_finitePart
    (K : Type) [Field K] [NumberField K]
    (x : Kˣ) :
    cyclotomicZHatNormComposite K
        (Additive.ofMul
          (IdeleGroup.principalIdele K x)) =
      Multiplicative.toAdd
        (rationalCyclotomicZHatIdeleValue
          (rationalIdeleFinitePart
            (IdeleGroup.principalIdele ℚ
              (Units.map (Algebra.norm ℚ) x))))

theorem

normalizedCyclotomicZHatIdeleValue_principalIdele_eq_zero_iff_finitePart

L871 ↗

GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleValue_principalIdele_eq_zero_iff_finitePart

Documentation

Normalized principal-idele vanishing is equivalent to the remaining rational finite-part product formula. Thus the only missing input for descent to the idele class group is the finite local cyclotomic compatibility, not an archimedean calculation.

Source context 10 commands

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

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

-- Keep the prime-power presentation explicit for canonical instance synthesis.
-- Both structures are the existing canonical cyclotomic-level instances.
local instance rationalCyclotomicPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
  IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance
    cyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) := by
  have : IsGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
    inferInstance
  let e :=
    IsCyclotomicExtension.Rat.galEquivZMod
      (m : ℕ) (KummerTheory.rationalCyclotomicLevel m)
  exact
    { is_comm.comm σ τ := by
        apply e.injective
        simp only [map_mul]
        exact mul_comm _ _ }

Lean source · statement

theorem
    normalizedCyclotomicZHatIdeleValue_principalIdele_eq_zero_iff_finitePart
    (K : Type) [Field K] [NumberField K]
    (x : Kˣ) :
    normalizedCyclotomicZHatIdeleValue K
          (Additive.ofMul
            (IdeleGroup.principalIdele K x)) =
        0 ↔
      rationalCyclotomicZHatIdeleValue
          (rationalIdeleFinitePart
            (IdeleGroup.principalIdele ℚ
              (Units.map (Algebra.norm ℚ) x))) =
        1

Module documentation

Principal ideles and the rational cyclotomic value

Declarations