Module

SupportedIdelePowerLocalUnitQuotient.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.SupportedIdelePowerLocalUnitQuotient

8 declarations indexed from sourceView source ↗

Module documentation

Supported idele power-local-unit quotient

This module restricts the power-local-unit subgroup to ideles supported at the prescribed finite places and identifies the resulting quotient with the product of its archimedean and finite local power-class groups.

Imports2

Imported by3

def

quotientEquivOfSurjectiveWithKernel

L30 ↗

GlobalClassFieldTheory.ClassFieldAxiom.quotientEquivOfSurjectiveWithKernel

Source context 6 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

def quotientEquivOfSurjectiveWithKernel
    {G H : Type*} [Group G] [Group H]
    (f : G →* H)
    (N : Subgroup G) [N.Normal]
    (hf : Function.Surjective f)
    (hker : f.ker = N) :
    G ⧸ N ≃* H

def

supportedIdelePowerLocalUnitSubgroup

L42 ↗

GlobalClassFieldTheory.ClassFieldAxiom.supportedIdelePowerLocalUnitSubgroup

Documentation

The power/local-unit subgroup h(S,T), regarded inside I_K^{S ∪ T}.

Source context 6 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

def supportedIdelePowerLocalUnitSubgroup
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Subgroup
      (IdeleGroup.supportedAt
        (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))))

theorem

idelePowerLocalUnitSubgroup_le_supportedAt

L54 ↗

GlobalClassFieldTheory.ClassFieldAxiom.idelePowerLocalUnitSubgroup_le_supportedAt

Documentation

Membership in h(S,T) automatically supplies the restricted-product condition defining I_K^{S ∪ T}.

Source context 6 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

theorem idelePowerLocalUnitSubgroup_le_supportedAt
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    idelePowerLocalUnitSubgroup (K := K) n S T ≤
      IdeleGroup.supportedAt
        (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K)))

def

supportedIdelePowerClassMap

L71 ↗

GlobalClassFieldTheory.ClassFieldAxiom.supportedIdelePowerClassMap

Documentation

Reduction modulo local n-th powers at all infinite places and at the finite places in S. The coordinates in T and the integral coordinates away from S ∪ T disappear in the supported-idele index calculation.

Source context 6 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]

Lean source · full declaration

def supportedIdelePowerClassMap
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    IdeleGroup.supportedAt
        (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))) →*
      ((
        ∀ w : InfinitePlace K,
          w.Completionˣ ⧸
            (powMonoidHom (n : ℕ) :
              w.Completionˣ →* w.Completionˣ).range) ×
        (∀ v : ↥S,
          (v.1.adicCompletion K)ˣ ⧸
            (powMonoidHom (n : ℕ) :
              (v.1.adicCompletion K)ˣ →*
                (v.1.adicCompletion K)ˣ).range)) where
  toFun a :=
    (fun w =>
      QuotientGroup.mk'
        (powMonoidHom (n : ℕ) :
          w.Completionˣ →* w.Completionˣ).range
        (IdeleGroup.infiniteComponent w a.1),
     fun v =>
      QuotientGroup.mk'
        (powMonoidHom (n : ℕ) :
          (v.1.adicCompletion K)ˣ →*
            (v.1.adicCompletion K)ˣ).range
        (IdeleGroup.finiteComponent v.1 a.1))
  map_one' := by
    apply Prod.ext
    · funext w
      apply (QuotientGroup.eq_one_iff _).mpr
      apply
        (MonoidHom.mem_range
          (G := w.Completionˣ)).mpr
      refine ⟨1, ?_⟩
      rw [powMonoidHom_apply, one_pow]
      exact (IdeleGroup.infiniteComponent w).map_one.symm
    · funext v
      simp
  map_mul' a b := by
    apply Prod.ext
    · funext w
      change
        QuotientGroup.mk'
            (powMonoidHom (n : ℕ) :
              w.Completionˣ →* w.Completionˣ).range
            (IdeleGroup.infiniteComponent w (a.1 * b.1)) =
          QuotientGroup.mk'
              (powMonoidHom (n : ℕ) :
                w.Completionˣ →* w.Completionˣ).range
              (IdeleGroup.infiniteComponent w a.1) *
            QuotientGroup.mk'
              (powMonoidHom (n : ℕ) :
                w.Completionˣ →* w.Completionˣ).range
              (IdeleGroup.infiniteComponent w b.1)
      rw [map_mul, map_mul]
    · funext v
      simp

theorem

supportedIdelePowerClassMap_ker

L132 ↗

GlobalClassFieldTheory.ClassFieldAxiom.supportedIdelePowerClassMap_ker

Documentation

The kernel of the local-power class map is precisely h(S,T) inside I_K^{S ∪ T}.

Source context 6 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

theorem supportedIdelePowerClassMap_ker
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    (supportedIdelePowerClassMap (K := K) n S T).ker =
      supportedIdelePowerLocalUnitSubgroup (K := K) n S T

theorem

supportedIdelePowerClassMap_surjective

L177 ↗

GlobalClassFieldTheory.ClassFieldAxiom.supportedIdelePowerClassMap_surjective

Documentation

The local-power class map is onto: choose representatives independently at the finitely many constrained finite places and at all archimedean places, then extend the finite family by 1.

Source context 6 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

theorem supportedIdelePowerClassMap_surjective
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Function.Surjective
      (supportedIdelePowerClassMap (K := K) n S T)

def

supportedIdeleQuotientEquivLocalPowerClasses

L245 ↗

GlobalClassFieldTheory.ClassFieldAxiom.supportedIdeleQuotientEquivLocalPowerClasses

Documentation

The algebraic supported-idele index decomposition:

I_K^{S ∪ T} / h(S,T) is the product of the local n-power class groups at all infinite places and at the finite places in S.

Source context 6 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

def supportedIdeleQuotientEquivLocalPowerClasses
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    IdeleGroup.supportedAt
          (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))) ⧸
        supportedIdelePowerLocalUnitSubgroup (K := K) n S T ≃*
      ((
        ∀ w : InfinitePlace K,
          w.Completionˣ ⧸
            (powMonoidHom (n : ℕ) :
              w.Completionˣ →* w.Completionˣ).range) ×
        (∀ v : ↥S,
          (v.1.adicCompletion K)ˣ ⧸
            (powMonoidHom (n : ℕ) :
              (v.1.adicCompletion K)ˣ →*
                (v.1.adicCompletion K)ˣ).range))

theorem

card_supportedIdeleQuotient_eq_localPowerClasses

L281 ↗

GlobalClassFieldTheory.ClassFieldAxiom.card_supportedIdeleQuotient_eq_localPowerClasses

Documentation

Cardinal form of the supported-idele index decomposition. The subsequent local power-index and product-formula calculation evaluates the right-hand side.

Source context 6 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

theorem card_supportedIdeleQuotient_eq_localPowerClasses
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Nat.card
        (IdeleGroup.supportedAt
              (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))) ⧸
          supportedIdelePowerLocalUnitSubgroup (K := K) n S T) =
      Nat.card
        ((
          ∀ w : InfinitePlace K,
            w.Completionˣ ⧸
              (powMonoidHom (n : ℕ) :
                w.Completionˣ →* w.Completionˣ).range) ×
          (∀ v : ↥S,
            (v.1.adicCompletion K)ˣ ⧸
              (powMonoidHom (n : ℕ) :
                (v.1.adicCompletion K)ˣ →*
                  (v.1.adicCompletion K)ˣ).range))

Module documentation

Supported idele power-local-unit quotient

Declarations