NYLL
Module

RationalCyclotomicRayNorm.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.RationalCyclotomicRayNorm
19 declarations indexed from sourceView source ↗

Module documentation

Rational cyclotomic ray norm groups

For a positive integer m, the genuine idèle-class norm range of the actual cyclotomic level ℚ(μ_m) is the rational ray congruence subgroup modulo (m).

The local input is the cyclotomic higher-unit calculation: at a rational prime q, an m.factorization q-th higher unit has trivial Artin action on every prime-power cyclotomic part. On the q-primary part this is the actual multiplicative Lubin--Tate norm theorem; on every other primary part it is the unramified Artin formula together with valuation zero. The finite cyclotomic character then detects that the full local Artin symbol is trivial.

Imports6
Imported by2

Declarations

instance

(anonymous instance)

L48 ↗
Source context 13 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
Lean source · statement
instance (q : Nat.Primes) : Fact q.1.Prime
theorem

rationalRayNorm_integerUnitsMap_mem_higherPrincipalUnits_iff

L69 ↗
GlobalClassFieldTheory.Reciprocity.rationalRayNorm_integerUnitsMap_mem_higherPrincipalUnits_iff
Source context 17 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
Lean source · statement
theorem
    rationalRayNorm_integerUnitsMap_mem_higherPrincipalUnits_iff
    (q : Nat.Primes) (n : ℕ)
    (u : 𝒪[RationalCyclotomicPrincipalPrimeCompletion q]ˣ) :
    Units.mapEquiv
          (((rationalFinitePlaceCompletionIntegerRingEquivPadicInt q).trans
            (padicIntEquivValuationSubring q.1)).toMulEquiv) u ∈
        higherPrincipalUnitGroup
          (padicLocalField q.1).toCompleteDVF n ↔
      u ∈ principalUnits
        (RationalCyclotomicPrincipalPrimeCompletion q) n
theorem

rationalRayNorm_fieldUnitsMap_integerUnits

L94 ↗
GlobalClassFieldTheory.Reciprocity.rationalRayNorm_fieldUnitsMap_integerUnits
Source context 17 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
Lean source · statement
theorem rationalRayNorm_fieldUnitsMap_integerUnits
    (q : Nat.Primes)
    (u : 𝒪[RationalCyclotomicPrincipalPrimeCompletion q]ˣ) :
    Units.map
        (rationalFinitePlaceCompletionRingEquivPadic q).toMonoidHom
        (IsNonarchimedeanLocalField.integerUnitsToFieldUnits
          (RationalCyclotomicPrincipalPrimeCompletion q) u) =
      CompleteDVF.valuationSubringUnitsToFieldUnits
        (padicLocalField q.1).toCompleteDVF
        (Units.mapEquiv
          (((rationalFinitePlaceCompletionIntegerRingEquivPadicInt q).trans
            (padicIntEquivValuationSubring q.1)).toMulEquiv) u)
theorem

rationalFinitePlaceFieldPrincipalUnits_map_eq_padicHigherPrincipalUnits

L150 ↗
GlobalClassFieldTheory.Reciprocity.rationalFinitePlaceFieldPrincipalUnits_map_eq_padicHigherPrincipalUnits
Documentation

The canonical rational-completion equivalence transports the topology-first principal-unit subgroup to the packaged higher-principal-unit subgroup in the standard q-adic field.

Source context 17 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
Lean source · full declaration
theorem
    rationalFinitePlaceFieldPrincipalUnits_map_eq_padicHigherPrincipalUnits
    (q : Nat.Primes) (n : ℕ) :
    let vQ :=
      HeightOneSpectrum.adicAbv ℚ
        (RayClass.rationalPrime q)
    let eK :=
      rationalFinitePlaceCompletionRingEquivPadic q
    (fieldPrincipalUnits vQ.Completion n).map
        (Units.map eK.toMonoidHom) =
      (higherPrincipalUnitGroup
        (padicLocalField q.1).toCompleteDVF n).map
        (CompleteDVF.valuationSubringUnitsToFieldUnits
          (padicLocalField q.1).toCompleteDVF) := by
  let vQ :=
    HeightOneSpectrum.adicAbv ℚ
      (RayClass.rationalPrime q)
  let eO :
      𝒪[vQ.Completion] ≃+*
        (padicLocalField q.1).valuationSubring :=
    (rationalFinitePlaceCompletionIntegerRingEquivPadicInt q).trans
      (padicIntEquivValuationSubring q.1)
  let eU :
      𝒪[vQ.Completion]ˣ ≃*
        (padicLocalField q.1).valuationSubringˣ :=
    Units.mapEquiv eO.toMulEquiv
  let jQ : 𝒪[vQ.Completion]ˣ →* vQ.Completionˣ :=
    IsNonarchimedeanLocalField.integerUnitsToFieldUnits vQ.Completion
  ext x
  constructor
  · rintro ⟨z, hz, rfl⟩
    change
      z ∈
        (principalUnits vQ.Completion n).map jQ at hz
    obtain ⟨u, hu, rfl⟩ := hz
    refine
      ⟨eU u,
        (rationalRayNorm_integerUnitsMap_mem_higherPrincipalUnits_iff
          q n u).2 hu,
        ?_⟩
    exact (rationalRayNorm_fieldUnitsMap_integerUnits q u).symm
  · rintro ⟨u, hu, rfl⟩
    let z : 𝒪[vQ.Completion]ˣ := eU.symm u
    have hzu :
        eU z = u :=
      eU.apply_symm_apply u
    refine
      ⟨jQ z, ⟨z, ?_, rfl⟩, ?_⟩
    · apply
      (rationalRayNorm_integerUnitsMap_mem_higherPrincipalUnits_iff
          q n z).1
      exact hzu.symm ▸ hu
    · exact
        (rationalRayNorm_fieldUnitsMap_integerUnits q z).trans
          (congrArg
            (CompleteDVF.valuationSubringUnitsToFieldUnits
              (padicLocalField q.1).toCompleteDVF)
            hzu)
instance

rationalCyclotomicRayNormPadicLevelIsAbelianGalois

L214 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicRayNormPadicLevelIsAbelianGalois
Source context 19 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
section PrimePowerCalculation
attribute [local instance]
  rationalCyclotomicPrincipalPrimePadicLevelFiniteDimensional
Lean source · statement
instance
    rationalCyclotomicRayNormPadicLevelIsAbelianGalois
    (q : Nat.Primes) (n : ℕ) :
    IsAbelianGalois ℚ_[q.1]
      (RationalCyclotomicPrincipalPrimePadicLevel q n)
theorem

rationalPrimePowerPadicAbelianLocalArtin_eq_one

L227 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimePowerPadicAbelianLocalArtin_eq_one
Documentation

A rational higher unit has trivial local Artin image in the standard multiplicative Lubin--Tate level. This is the purely q-adic part of the prime-power argument; the semilinear transport to the localized global cyclotomic field is handled separately below.

Source context 20 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
section PrimePowerCalculation
attribute [local instance]
  rationalCyclotomicPrincipalPrimePadicLevelFiniteDimensional
noncomputable local instance
    rationalCyclotomicRayNormPadicLevelIsAbelianGalois
    (q : Nat.Primes) (n : ℕ) :
    IsAbelianGalois ℚ_[q.1]
      (RationalCyclotomicPrincipalPrimePadicLevel q n) :=
  standardLubinTateLevelField_isAbelianGalois
    (padicLocalField q.1)
    (padicMultiplicativeLubinTateSeries_isUniformizer q.1) n
Lean source · statement
theorem rationalPrimePowerPadicAbelianLocalArtin_eq_one
    (q : Nat.Primes) (n : ℕ)
    (x : ((RayClass.rationalPrime q).adicCompletion ℚ)ˣ)
    (hx :
      x ∈ RayClass.localHigherUnitGroup
        (RayClass.rationalPrime q) (n + 1)) :
    abelianLocalArtinMonoidHom ℚ_[q.1]
        (RationalCyclotomicPrincipalPrimePadicLevel q n)
        (Units.map
          (rationalFinitePlaceCompletionRingEquivPadic q).toMonoidHom
          ((finitePlaceCompletionUnitsContinuousMulEquiv
            (RayClass.rationalPrime q)).symm x)) = 1
def

rationalPrimePowerChosenFinitePlaceArtinValue

L288 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimePowerChosenFinitePlaceArtinValue
Documentation

The chosen ramified finite-place Artin value, with the cyclotomic level and its instance arguments frozen behind a named boundary.

Source context 20 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
section PrimePowerCalculation
attribute [local instance]
  rationalCyclotomicPrincipalPrimePadicLevelFiniteDimensional
noncomputable local instance
    rationalCyclotomicRayNormPadicLevelIsAbelianGalois
    (q : Nat.Primes) (n : ℕ) :
    IsAbelianGalois ℚ_[q.1]
      (RationalCyclotomicPrincipalPrimePadicLevel q n) :=
  standardLubinTateLevelField_isAbelianGalois
    (padicLocalField q.1)
    (padicMultiplicativeLubinTateSeries_isUniformizer q.1) n
Lean source · statement
def rationalPrimePowerChosenFinitePlaceArtinValue
    (q : Nat.Primes) (n : ℕ)
    (x :
      ((RayClass.rationalPrime q).adicCompletion ℚ)ˣ) :
    KummerTheory.rationalCyclotomicLevel
          (rationalCyclotomicPrincipalPrimeModulus q n) ≃ₐ[ℚ]
        KummerTheory.rationalCyclotomicLevel
          (rationalCyclotomicPrincipalPrimeModulus q n)
theorem

rationalPrimePowerFinitePlaceLocalInputPadicArtin_eq_one

L305 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimePowerFinitePlaceLocalInputPadicArtin_eq_one
Documentation

The standard q-adic calculation evaluated on the canonical input used by the finite-place Artin construction.

Source context 20 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
section PrimePowerCalculation
attribute [local instance]
  rationalCyclotomicPrincipalPrimePadicLevelFiniteDimensional
noncomputable local instance
    rationalCyclotomicRayNormPadicLevelIsAbelianGalois
    (q : Nat.Primes) (n : ℕ) :
    IsAbelianGalois ℚ_[q.1]
      (RationalCyclotomicPrincipalPrimePadicLevel q n) :=
  standardLubinTateLevelField_isAbelianGalois
    (padicLocalField q.1)
    (padicMultiplicativeLubinTateSeries_isUniformizer q.1) n
Lean source · statement
theorem rationalPrimePowerFinitePlaceLocalInputPadicArtin_eq_one
    (q : Nat.Primes) (n : ℕ)
    (x : ((RayClass.rationalPrime q).adicCompletion ℚ)ˣ)
    (hx :
      x ∈ RayClass.localHigherUnitGroup
        (RayClass.rationalPrime q) (n + 1)) :
    abelianLocalArtinMonoidHom ℚ_[q.1]
        (RationalCyclotomicPrincipalPrimePadicLevel q n)
        (Units.map
          (rationalFinitePlaceCompletionRingEquivPadic q).toMonoidHom
          (finitePlaceLocalArtinInput
            (RayClass.rationalPrime q) x)) = 1
theorem

rationalPrimePowerFinitePlaceArtinOfExtension_eq_one

L328 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimePowerFinitePlaceArtinOfExtension_eq_one
Documentation

The normalized local calculation, transported through the decomposition group inclusion. This bridge contains no semilinear instance search.

Source context 20 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
section PrimePowerCalculation
attribute [local instance]
  rationalCyclotomicPrincipalPrimePadicLevelFiniteDimensional
noncomputable local instance
    rationalCyclotomicRayNormPadicLevelIsAbelianGalois
    (q : Nat.Primes) (n : ℕ) :
    IsAbelianGalois ℚ_[q.1]
      (RationalCyclotomicPrincipalPrimePadicLevel q n) :=
  standardLubinTateLevelField_isAbelianGalois
    (padicLocalField q.1)
    (padicMultiplicativeLubinTateSeries_isUniformizer q.1) n
Lean source · statement
theorem rationalPrimePowerFinitePlaceArtinOfExtension_eq_one
    (q : Nat.Primes) (n : ℕ)
    (x :
      ((RayClass.rationalPrime q).adicCompletion ℚ)ˣ)
    (hx :
      x ∈ RayClass.localHigherUnitGroup
        (RayClass.rationalPrime q) (n + 1)) :
    finitePlaceArtinMonoidHomOfExtension
        (K := ℚ)
        (L := KummerTheory.rationalCyclotomicLevel
          (rationalCyclotomicPrincipalPrimeModulus q n))
        (RayClass.rationalPrime q)
        (rationalCyclotomicChosenFinitePlaceExtension
          (rationalCyclotomicPrincipalPrimeModulus q n)
          (RayClass.rationalPrime q)) x = 1
theorem

rationalPrimePowerChosenFinitePlaceArtinValue_eq_one_of_mem_localHigherUnitGroup

L350 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimePowerChosenFinitePlaceArtinValue_eq_one_of_mem_localHigherUnitGroup
Documentation

The local semilinear calculation for a ramified prime-power level. Its statement only exposes the named global Artin value.

Source context 20 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
section PrimePowerCalculation
attribute [local instance]
  rationalCyclotomicPrincipalPrimePadicLevelFiniteDimensional
noncomputable local instance
    rationalCyclotomicRayNormPadicLevelIsAbelianGalois
    (q : Nat.Primes) (n : ℕ) :
    IsAbelianGalois ℚ_[q.1]
      (RationalCyclotomicPrincipalPrimePadicLevel q n) :=
  standardLubinTateLevelField_isAbelianGalois
    (padicLocalField q.1)
    (padicMultiplicativeLubinTateSeries_isUniformizer q.1) n
Lean source · statement
theorem
    rationalPrimePowerChosenFinitePlaceArtinValue_eq_one_of_mem_localHigherUnitGroup
    (q : Nat.Primes) (n : ℕ)
    (x :
      ((RayClass.rationalPrime q).adicCompletion ℚ)ˣ)
    (hx :
      x ∈ RayClass.localHigherUnitGroup
        (RayClass.rationalPrime q) (n + 1)) :
    rationalPrimePowerChosenFinitePlaceArtinValue q n x = 1
theorem

rationalPrimePowerChosenFinitePlaceArtin_eq_one_of_mem_localHigherUnitGroup

L366 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimePowerChosenFinitePlaceArtin_eq_one_of_mem_localHigherUnitGroup
Documentation

A principal unit of depth n + 1 has trivial chosen finite-place Artin symbol in the genuine q ^ (n + 1)-st rational cyclotomic level.

Source context 20 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
section PrimePowerCalculation
attribute [local instance]
  rationalCyclotomicPrincipalPrimePadicLevelFiniteDimensional
noncomputable local instance
    rationalCyclotomicRayNormPadicLevelIsAbelianGalois
    (q : Nat.Primes) (n : ℕ) :
    IsAbelianGalois ℚ_[q.1]
      (RationalCyclotomicPrincipalPrimePadicLevel q n) :=
  standardLubinTateLevelField_isAbelianGalois
    (padicLocalField q.1)
    (padicMultiplicativeLubinTateSeries_isUniformizer q.1) n
Lean source · statement
theorem
    rationalPrimePowerChosenFinitePlaceArtin_eq_one_of_mem_localHigherUnitGroup
    (q : Nat.Primes) (n : ℕ)
    (x :
      ((RayClass.rationalPrime q).adicCompletion ℚ)ˣ)
    (hx :
      x ∈ RayClass.localHigherUnitGroup
        (RayClass.rationalPrime q) (n + 1)) :
    chosenFinitePlaceArtinMonoidHom
        (K := ℚ)
        (L :=
          KummerTheory.rationalCyclotomicLevel
            (rationalCyclotomicPrincipalPrimeModulus q n))
        (RayClass.rationalPrime q) x =
      1
theorem

rationalPrimePowerChosenFinitePlaceArtin_eq_one_of_mem_localHigherUnitGroup_pos

L388 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimePowerChosenFinitePlaceArtin_eq_one_of_mem_localHigherUnitGroup_pos
Documentation

The positive-depth form of the prime-power calculation. Eliminating the successor before introducing a cyclotomic level avoids transporting its dependent field and instance data later in the full-level coordinate proof.

Source context 20 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
section PrimePowerCalculation
attribute [local instance]
  rationalCyclotomicPrincipalPrimePadicLevelFiniteDimensional
noncomputable local instance
    rationalCyclotomicRayNormPadicLevelIsAbelianGalois
    (q : Nat.Primes) (n : ℕ) :
    IsAbelianGalois ℚ_[q.1]
      (RationalCyclotomicPrincipalPrimePadicLevel q n) :=
  standardLubinTateLevelField_isAbelianGalois
    (padicLocalField q.1)
    (padicMultiplicativeLubinTateSeries_isUniformizer q.1) n
Lean source · statement
theorem
    rationalPrimePowerChosenFinitePlaceArtin_eq_one_of_mem_localHigherUnitGroup_pos
    (q : Nat.Primes) (k : ℕ) (hk : k ≠ 0)
    (mp : ℕ+) (hmp : (mp : ℕ) = q.1 ^ k)
    (x : ((RayClass.rationalPrime q).adicCompletion ℚ)ˣ)
    (hx :
      x ∈ RayClass.localHigherUnitGroup
        (RayClass.rationalPrime q) k) :
    chosenFinitePlaceArtinMonoidHom
        (K := ℚ)
        (L := KummerTheory.rationalCyclotomicLevel mp)
        (RayClass.rationalPrime q) x = 1
theorem

rationalCyclotomicRayNormAwayChosenFinitePlaceArtin_eq_one

L413 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicRayNormAwayChosenFinitePlaceArtin_eq_one
Documentation

A valuation-zero input away from a named cyclotomic level has trivial chosen Artin value. Keeping the level as a positive-natural variable makes the instance owner identical on both sides of the imported calculation.

Source context 20 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
section PrimePowerCalculation
attribute [local instance]
  rationalCyclotomicPrincipalPrimePadicLevelFiniteDimensional
noncomputable local instance
    rationalCyclotomicRayNormPadicLevelIsAbelianGalois
    (q : Nat.Primes) (n : ℕ) :
    IsAbelianGalois ℚ_[q.1]
      (RationalCyclotomicPrincipalPrimePadicLevel q n) :=
  standardLubinTateLevelField_isAbelianGalois
    (padicLocalField q.1)
    (padicMultiplicativeLubinTateSeries_isUniformizer q.1) n
Lean source · statement
theorem rationalCyclotomicRayNormAwayChosenFinitePlaceArtin_eq_one
    (mp : ℕ+) (q : Nat.Primes)
    (hq : ¬ q.1 ∣ (mp : ℕ))
    (x : ((RayClass.rationalPrime q).adicCompletion ℚ)ˣ)
    (hzero : rationalCyclotomicArtinLocalExponent q x = 0) :
    chosenFinitePlaceArtinMonoidHom
        (K := ℚ)
        (L := KummerTheory.rationalCyclotomicLevel mp)
        (RayClass.rationalPrime q) x = 1
theorem

rationalCyclotomicRayNormLocalExponent_eq_zero_of_mem_localHigherUnitGroup

L431 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicRayNormLocalExponent_eq_zero_of_mem_localHigherUnitGroup
Documentation

Membership in a rational local higher-unit group forces the normalized cyclotomic Artin exponent to vanish. This boundary keeps the completion and valuation expansion out of the full cyclotomic-coordinate calculation.

Source context 17 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
Lean source · statement
theorem
    rationalCyclotomicRayNormLocalExponent_eq_zero_of_mem_localHigherUnitGroup
    (q : Nat.Primes) (n : ℕ)
    (x : ((RayClass.rationalPrime q).adicCompletion ℚ)ˣ)
    (hx :
      x ∈ RayClass.localHigherUnitGroup
        (RayClass.rationalPrime q) n) :
    rationalCyclotomicArtinLocalExponent q x = 0
theorem

rationalCyclotomicLevel_localHigherUnitGroup_le_chosenLocalNorm

L454 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLevel_localHigherUnitGroup_le_chosenLocalNorm
Documentation

The rational ray-class higher-unit group at q consists of actual local norms from the chosen completion of the genuine cyclotomic level.

Source context 17 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
section FinitePlaceLocalCalculation
attribute [local instance]
  rationalFinitePlaceBaseNontriviallyNormedField
  rationalFinitePlaceBaseLocallyCompactSpace
  rationalFinitePlaceBaseIsUltrametricDist
  rationalFinitePlaceBaseValued
  rationalFinitePlaceBaseValuativeRel
  rationalFinitePlaceBaseValuationIsNontrivial
  rationalFinitePlaceBaseValuationCompatible
  rationalFinitePlaceBaseValuativeRelIsNontrivial
  rationalFinitePlaceBaseIsValuativeTopology
  rationalFinitePlaceBaseIsNonarchimedeanLocalField
Lean source · statement
theorem
    rationalCyclotomicLevel_localHigherUnitGroup_le_chosenLocalNorm
    (m : ℕ+) (q : Nat.Primes) :
    RayClass.localHigherUnitGroup
        (RayClass.rationalPrime q)
        (RayClass.rationalFiniteModulus (m : ℕ)
          (RayClass.rationalPrime q)) ≤
      _root_.chosenFinitePlaceLocalNormSubgroup
        (K := ℚ)
        (L := KummerTheory.rationalCyclotomicLevel m)
        (RayClass.rationalPrime q)
theorem

rationalCyclotomicLevel_rationalModulus_localNorm

L655 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLevel_rationalModulus_localNorm
Documentation

At every finite rational place, the local higher-unit group prescribed by (m) lies in the chosen local norm subgroup of ℚ(μ_m).

Source context 15 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
Lean source · statement
theorem rationalCyclotomicLevel_rationalModulus_localNorm
    (m : ℕ+)
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    RayClass.localHigherUnitGroup v
        (RayClass.rationalFiniteModulus (m : ℕ) v) ≤
      _root_.chosenFinitePlaceLocalNormSubgroup
        (K := ℚ)
        (L := KummerTheory.rationalCyclotomicLevel m) v
theorem

rationalCongruenceSubgroup_le_rationalCyclotomicLevelIdeleClassNormRange

L683 ↗
GlobalClassFieldTheory.Reciprocity.rationalCongruenceSubgroup_le_rationalCyclotomicLevelIdeleClassNormRange
Documentation

The rational ray congruence subgroup modulo (m) is contained in the genuine idèle-class norm range from the actual cyclotomic level ℚ(μ_m).

Source context 15 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
Lean source · full declaration
theorem
    rationalCongruenceSubgroup_le_rationalCyclotomicLevelIdeleClassNormRange
    (m : ℕ) (hm : m ≠ 0) :
    let mp : ℕ+ := ⟨m, Nat.pos_of_ne_zero hm⟩
    RayClass.Modulus.congruenceSubgroup
        (RayClass.rationalModulus m) ≤
      (_root_.ideleClassNorm ℚ
        (KummerTheory.rationalCyclotomicLevel mp)).range := by
  dsimp only
  let mp : ℕ+ := ⟨m, Nat.pos_of_ne_zero hm⟩
  let L := KummerTheory.rationalCyclotomicLevel mp
  have hlocal :
      ∀ v : HeightOneSpectrum (𝓞 ℚ),
        RayClass.localHigherUnitGroup v
            (RayClass.rationalFiniteModulus m v) ≤
          _root_.chosenFinitePlaceLocalNormSubgroup
            (K := ℚ) (L := L) v := by
    intro v
    change
      RayClass.localHigherUnitGroup v
          (RayClass.rationalFiniteModulus (mp : ℕ) v) ≤
        _root_.chosenFinitePlaceLocalNormSubgroup
          (K := ℚ)
          (L := KummerTheory.rationalCyclotomicLevel mp) v
    exact rationalCyclotomicLevel_rationalModulus_localNorm mp v
  have hfinite :
      GlobalClassFields.ideleClassNormDefiningModulus
          (K := ℚ) (L := L) ≤
        RayClass.rationalFiniteModulus m :=
    GlobalClassFields.ideleClassNormDefiningModulus_le_of_localHigherUnitGroup_le
        (K := ℚ) (L := L)
        (RayClass.rationalFiniteModulus m) hlocal
  have hmodulus :
      RayClass.Modulus.narrowOfFinite
          (GlobalClassFields.ideleClassNormDefiningModulus
            (K := ℚ) (L := L)) ≤
        RayClass.rationalModulus m := by
    classical
    refine ⟨hfinite, ?_⟩
    change
      (Finset.univ : Finset (RayClass.RealPlace ℚ)) ⊆
        Finset.univ
    exact fun _ h => h
  exact
    (GlobalClassFields.rayClassCongruenceSubgroup_antitone
      (K := ℚ) hmodulus).trans
      (GlobalClassFields.ideleClassNormDefiningModulus_isDefiningModulus
          (K := ℚ) (L := L))
theorem

rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup

L734 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
Documentation

The genuine idèle-class norm range from the actual finite cyclotomic level is exactly the rational ray congruence subgroup modulo (m).

Source context 15 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
Lean source · full declaration
theorem
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
    (m : ℕ) (hm : m ≠ 0) :
    let mp : ℕ+ := ⟨m, Nat.pos_of_ne_zero hm⟩
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel mp)).range =
      RayClass.Modulus.congruenceSubgroup
        (RayClass.rationalModulus m) := by
  dsimp only
  let : NeZero m := ⟨hm⟩
  let mp : ℕ+ := ⟨m, Nat.pos_of_ne_zero hm⟩
  let L := KummerTheory.rationalCyclotomicLevel mp
  let : IsCyclotomicExtension {m} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, Nat.pos_of_ne_zero hm⟩) :=
    KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension
      ⟨m, Nat.pos_of_ne_zero hm⟩
  let H :=
    RayClass.Modulus.congruenceSubgroup
      (RayClass.rationalModulus m)
  let N :=
    (_root_.ideleClassNorm ℚ L).range
  have hHN : H ≤ N := by
    simpa only [H, N, L, mp] using
      rationalCongruenceSubgroup_le_rationalCyclotomicLevelIdeleClassNormRange
        m hm
  have hindex : H.index = N.index := by
    calc
      H.index =
          Nat.card
            (IdeleClassGroup ℚ ⧸
              RayClass.Modulus.congruenceSubgroup
                (RayClass.rationalModulus m)) := by
        rw [Subgroup.index_eq_card]
      _ = m.totient :=
        KroneckerWeber.rationalRayClassFieldQuotient_card_eq_totient m hm
      _ = Module.finrank ℚ L := by
        simpa only [L, mp] using
          (IsCyclotomicExtension.Rat.finrank m L).symm
      _ = N.index := by
        simpa only [N] using
          (ideleClassNorm_index_eq_finrank_abelian ℚ L).symm
  apply le_antisymm
  · by_contra hNH
    have hne : H ≠ N := by
      intro hEq
      exact hNH hEq.symm.le
    have hstrict : H < N :=
      lt_of_le_of_ne hHN hne
    have hindexStrict :=
      Subgroup.index_strictAnti hstrict
    rw [hindex] at hindexStrict
    exact (Nat.lt_irrefl _ hindexStrict)
  · exact hHN
theorem

rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup

L792 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
Documentation

The standard cyclotomic field CyclotomicField m ℚ has the same actual idèle-class norm range, namely the rational ray congruence subgroup modulo (m).

Source context 15 commands

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

open scoped NNReal NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open LubinTate
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
attribute [local instance]
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois
Lean source · statement
theorem
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
    (m : ℕ) (hm : m ≠ 0) :
    (_root_.ideleClassNorm ℚ
      (CyclotomicField m ℚ)).range =
      RayClass.Modulus.congruenceSubgroup
        (RayClass.rationalModulus m)

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