Module

IdeleIntegralCharacterRadical.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdeleIntegralCharacterRadical

8 declarations indexed from sourceView source ↗

Module documentation

Integral idele characters annihilate the ideal-power radical

A continuous character trivial on each finite integral one-place idele is trivial on their entire product, by convergence of the finite partial products. Odd powers are surjective on the archimedean factors. Thus an odd mod-p character with these local triviality conditions kills the whole integral-idele subgroup.

The fractional-ideal map is surjective and has this integral subgroup as kernel. Lifting the ideal root of a radical element therefore writes its principal idele as a p-th power times an integral idele. The character annihilates it. No global reciprocity comparison is an extra hypothesis.

Imports5

Imported by4

instance

integralCharacterTopology

L37 ↗

ClassFieldTower.Martinet.Shafarevich.integralCharacterTopology

Source context 6 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))

Lean source · statement

instance integralCharacterTopology : TopologicalSpace (ZMod (n : ℕ))

instance

integralCharacterDiscrete

L38 ↗

ClassFieldTower.Martinet.Shafarevich.integralCharacterDiscrete

Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance integralCharacterTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥

Lean source · statement

instance integralCharacterDiscrete : DiscreteTopology (ZMod (n : ℕ))

theorem

multiplicativeZMod_pow_eq_one

L42 ↗

ClassFieldTower.Martinet.Shafarevich.multiplicativeZMod_pow_eq_one

Documentation

Every multiplicative mod-p coefficient has p-th power one.

Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance integralCharacterTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance integralCharacterDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _

Lean source · statement

theorem multiplicativeZMod_pow_eq_one (a : Multiplicative (ZMod (n : ℕ))) :
    a ^ (n : ℕ) = 1

def

integralFiniteIdeleContinuousHom

L49 ↗

ClassFieldTower.Martinet.Shafarevich.integralFiniteIdeleContinuousHom

Documentation

The actual product of finite integral units, with archimedean part one.

Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance integralCharacterTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance integralCharacterDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _

Lean source · full declaration

def integralFiniteIdeleContinuousHom :
    (∀ v : HeightOneSpectrum (𝓞 F), (v.adicCompletionIntegers F).units) →ₜ* IdeleGroup F where
  toFun a := (1, FiniteIdeleGroup.integralStructureMap a)
  map_one' := rfl
  map_mul' a b := by
    apply Prod.ext
    · exact (one_mul 1).symm
    · rfl
  continuous_toFun := continuous_const.prodMk
    RestrictedProduct.isEmbedding_structureMap.continuous

theorem

ideleCharacter_integralFinite_eq_one

L61 ↗

ClassFieldTower.Martinet.Shafarevich.ideleCharacter_integralFinite_eq_one

Documentation

Pointwise triviality on integral units implies triviality on their product.

Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance integralCharacterTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance integralCharacterDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _

Lean source · statement

theorem ideleCharacter_integralFinite_eq_one
    (chi : IdeleGroup F →ₜ* Multiplicative (ZMod (n : ℕ)))
    (hchi : ∀ (v : HeightOneSpectrum (𝓞 F)) (a : (v.adicCompletion F)ˣ),
      a ∈ (v.adicCompletionIntegers F).units → chi (IdeleGroup.finitePlaceIdele v a) = 1)
    (a : ∀ v : HeightOneSpectrum (𝓞 F), (v.adicCompletionIntegers F).units) :
    chi (integralFiniteIdeleContinuousHom F a) = 1

theorem

infiniteIdele_pow_surjective_of_odd

L112 ↗

ClassFieldTower.Martinet.Shafarevich.infiniteIdele_pow_surjective_of_odd

Documentation

Odd powers are surjective on all archimedean idele factors.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance integralCharacterTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance integralCharacterDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
include hpOdd
omit [NumberField F] [Fact (n : ℕ).Prime] in

Lean source · full declaration

theorem infiniteIdele_pow_surjective_of_odd :
    Function.Surjective (fun a : InfiniteIdeleGroup F => a ^ (n : ℕ)) := by
  classical
  intro a
  let e : InfiniteIdeleGroup F ≃ₜ* (∀ w : InfinitePlace F, w.Completionˣ) :=
    ContinuousMulEquiv.piUnits
  have hroot : ∀ w : InfinitePlace F, ∃ b : w.Completionˣ, b ^ (n : ℕ) = e a w := by
    intro w
    by_cases hw : w.IsReal
    · have hmem : e a w ∈ (powMonoidHom (n : ℕ) : w.Completionˣ →* w.Completionˣ).range := by
        rw [GlobalClassFieldTheory.ClassFieldAxiom.nthPowerSubgroup_eq_top_of_real_odd n w hw hpOdd]
        exact Subgroup.mem_top _
      exact hmem
    · apply exists_infinitePositiveSubgroup_nthRoot w (n : ℕ) n.pos
      rw [RayClass.mem_infinitePositiveSubgroup_iff]
      intro hreal
      exact (hw hreal).elim
  choose b hb using hroot
  refine ⟨e.symm b, ?_⟩
  apply e.injective
  rw [map_pow, e.apply_symm_apply]
  exact funext hb

theorem

ideleCharacter_integral_eq_one

L136 ↗

ClassFieldTower.Martinet.Shafarevich.ideleCharacter_integral_eq_one

Documentation

An odd mod-p character trivial on local integral units kills integral ideles.

Source context 9 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance integralCharacterTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance integralCharacterDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
include hpOdd

Lean source · statement

theorem ideleCharacter_integral_eq_one
    (chi : IdeleGroup F →ₜ* Multiplicative (ZMod (n : ℕ)))
    (hchi : ∀ (v : HeightOneSpectrum (𝓞 F)) (a : (v.adicCompletion F)ˣ),
      a ∈ (v.adicCompletionIntegers F).units → chi (IdeleGroup.finitePlaceIdele v a) = 1)
    (a : IdeleGroup F) (ha : a ∈ IdeleGroup.integralAtFinitePlaces (K := F)) :
    chi a = 1

theorem

ideleCharacter_principal_radical_eq_one_of_integral_local

L157 ↗

ClassFieldTower.Martinet.Shafarevich.ideleCharacter_principal_radical_eq_one_of_integral_local

Documentation

Such a character kills principal ideles of ideal-power radical elements.

Source context 9 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance integralCharacterTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance integralCharacterDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
include hpOdd

Lean source · statement

theorem ideleCharacter_principal_radical_eq_one_of_integral_local
    (chi : IdeleGroup F →ₜ* Multiplicative (ZMod (n : ℕ)))
    (hchi : ∀ (v : HeightOneSpectrum (𝓞 F)) (a : (v.adicCompletion F)ˣ),
      a ∈ (v.adicCompletionIntegers F).units → chi (IdeleGroup.finitePlaceIdele v a) = 1)
    (a : (idealNthPowerRadicalKummerSubgroup F n).1) :
    chi (IdeleGroup.principalIdele F a.1) = 1

Module documentation

Integral idele characters annihilate the ideal-power radical

Declarations