NYLL
Module

ArchimedeanPowerIndex.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.IdeleClassPowerLocalUnitQuotient.ArchimedeanPowerIndex
12 declarations indexed from sourceView source ↗

Module documentation

Archimedean power indices in idele class quotients

This file defines the concrete idele-class subgroup attached to local power conditions and computes its archimedean local indices.

Imports5
Imported by9

Declarations

def

ideleClassPowerLocalUnitSubgroup

L34 ↗
GlobalClassFieldTheory.ClassFieldAxiom.ideleClassPowerLocalUnitSubgroup
Documentation

The subgroup C_K(S,T) = h(S,T)Kˣ/Kˣ inside the idele class group.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
def ideleClassPowerLocalUnitSubgroup
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Subgroup (IdeleClassGroup K)
theorem

mem_ideleClassPowerLocalUnitSubgroup_iff

L42 ↗
GlobalClassFieldTheory.ClassFieldAxiom.mem_ideleClassPowerLocalUnitSubgroup_iff
Documentation

Elementwise form of C_K(S,T)=h(S,T)Kˣ/Kˣ.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem mem_ideleClassPowerLocalUnitSubgroup_iff
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
    (c : IdeleClassGroup K) :
    c ∈ ideleClassPowerLocalUnitSubgroup (K := K) n S T ↔
      ∃ a : IdeleGroup K,
        a ∈ idelePowerLocalUnitSubgroup (K := K) n S T ∧
          QuotientGroup.mk' (IdeleGroup.principalSubgroup K) a = c
abbrev

IdeleClassPowerLocalUnitQuotient

L54 ↗
GlobalClassFieldTheory.ClassFieldAxiom.IdeleClassPowerLocalUnitQuotient
Documentation

The quotient whose cardinality is the index [C_K : C_K(S,T)].

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
abbrev IdeleClassPowerLocalUnitQuotient
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
theorem

nthPowerSubgroup_le_infinitePositiveSubgroup

L63 ↗
GlobalClassFieldTheory.ClassFieldAxiom.nthPowerSubgroup_le_infinitePositiveSubgroup
Documentation

If the exponent is even, or the place is complex, every local n-th power is positive in the archimedean sense.

Source context 7 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem nthPowerSubgroup_le_infinitePositiveSubgroup
    (n : ℕ+)
    (w : InfinitePlace K)
    (harch : Even (n : ℕ) ∨ ¬ w.IsReal) :
    (powMonoidHom (n : ℕ) :
        w.Completionˣ →* w.Completionˣ).range ≤
      RayClass.infinitePositiveSubgroup w
def

realInfinitePlaceSignHom

L93 ↗
GlobalClassFieldTheory.ClassFieldAxiom.realInfinitePlaceSignHom
Documentation

The sign of a unit at a real infinite place.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
def realInfinitePlaceSignHom
    (w : InfinitePlace K)
    (hw : w.IsReal) :
    w.Completionˣ →* SignTypeˣ
theorem

realInfinitePlaceSignHom_ker

L106 ↗
GlobalClassFieldTheory.ClassFieldAxiom.realInfinitePlaceSignHom_ker
Documentation

The positive subgroup at a real infinite place is exactly the kernel of the sign homomorphism.

Source context 7 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem realInfinitePlaceSignHom_ker
    (w : InfinitePlace K)
    (hw : w.IsReal) :
    (realInfinitePlaceSignHom w hw).ker =
      RayClass.infinitePositiveSubgroup w
theorem

realInfinitePlaceSignHom_surjective

L140 ↗
GlobalClassFieldTheory.ClassFieldAxiom.realInfinitePlaceSignHom_surjective
Documentation

Both signs occur at a real infinite place.

Source context 7 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem realInfinitePlaceSignHom_surjective
    (w : InfinitePlace K)
    (hw : w.IsReal) :
    Function.Surjective (realInfinitePlaceSignHom w hw)
def

realInfinitePositiveQuotientEquivSign

L163 ↗
GlobalClassFieldTheory.ClassFieldAxiom.realInfinitePositiveQuotientEquivSign
Documentation

The quotient by positive units at a real place is its two-element sign group.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
def realInfinitePositiveQuotientEquivSign
    (w : InfinitePlace K)
    (hw : w.IsReal) :
    w.Completionˣ ⧸ RayClass.infinitePositiveSubgroup w ≃*
      SignTypeˣ
theorem

card_realInfinitePositiveQuotient

L176 ↗
GlobalClassFieldTheory.ClassFieldAxiom.card_realInfinitePositiveQuotient
Documentation

The positive-unit quotient at a real place has order two.

Source context 7 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem card_realInfinitePositiveQuotient
    (w : InfinitePlace K)
    (hw : w.IsReal) :
    Nat.card
        (w.Completionˣ ⧸
          RayClass.infinitePositiveSubgroup w) =
      2
theorem

nthPowerSubgroup_eq_infinitePositiveSubgroup

L197 ↗
GlobalClassFieldTheory.ClassFieldAxiom.nthPowerSubgroup_eq_infinitePositiveSubgroup
Documentation

In the even-real or complex cases, the local power subgroup is exactly the usual archimedean positive subgroup.

Source context 7 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem nthPowerSubgroup_eq_infinitePositiveSubgroup
    (n : ℕ+)
    (w : InfinitePlace K)
    (harch : Even (n : ℕ) ∨ ¬ w.IsReal) :
    (powMonoidHom (n : ℕ) :
        w.Completionˣ →* w.Completionˣ).range =
      RayClass.infinitePositiveSubgroup w
theorem

nthPowerSubgroup_eq_top_of_real_odd

L220 ↗
GlobalClassFieldTheory.ClassFieldAxiom.nthPowerSubgroup_eq_top_of_real_odd
Documentation

At a real place an odd power map on local units is surjective.

Source context 7 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem nthPowerSubgroup_eq_top_of_real_odd
    (n : ℕ+)
    (w : InfinitePlace K)
    (hw : w.IsReal)
    (hn : Odd (n : ℕ)) :
    (powMonoidHom (n : ℕ) :
        w.Completionˣ →* w.Completionˣ).range =
      ⊤
theorem

card_infinitePlace_nthPowerQuotient

L274 ↗
GlobalClassFieldTheory.ClassFieldAxiom.card_infinitePlace_nthPowerQuotient
Documentation

The archimedean factor in the local power-index product: it is 2 exactly for an even exponent at a real place, and 1 otherwise.

Source context 8 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
omit [NumberField K] in
open scoped Classical in
Lean source · full declaration
theorem card_infinitePlace_nthPowerQuotient
    (n : ℕ+)
    (w : InfinitePlace K) :
    Nat.card
        (w.Completionˣ ⧸
          (powMonoidHom (n : ℕ) :
            w.Completionˣ →* w.Completionˣ).range) =
      if w.IsReal ∧ Even (n : ℕ) then 2 else 1 := by
  classical
  by_cases hw : w.IsReal
  · by_cases hn : Even (n : ℕ)
    · rw [
        nthPowerSubgroup_eq_infinitePositiveSubgroup
          n w (Or.inl hn)]
      simpa [hw, hn] using
        card_realInfinitePositiveQuotient w hw
    · have hodd : Odd (n : ℕ) :=
        (Nat.even_or_odd (n : ℕ)).resolve_left hn
      rw [nthPowerSubgroup_eq_top_of_real_odd n w hw hodd]
      let :
          Subsingleton
            (w.Completionˣ ⧸ (⊤ : Subgroup w.Completionˣ)) :=
        QuotientGroup.subsingleton_quotient_top
      simp [hw, hn]
  · have hpower :
        (powMonoidHom (n : ℕ) :
            w.Completionˣ →* w.Completionˣ).range =
          RayClass.infinitePositiveSubgroup w :=
      nthPowerSubgroup_eq_infinitePositiveSubgroup
        n w (Or.inr hw)
    have hpositive :
        RayClass.infinitePositiveSubgroup w = ⊤ := by
      ext x
      simp [RayClass.mem_infinitePositiveSubgroup_iff, hw]
    rw [hpower, hpositive]
    let :
        Subsingleton
          (w.Completionˣ ⧸ (⊤ : Subgroup w.Completionˣ)) :=
      QuotientGroup.subsingleton_quotient_top
    simp [hw]

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