NYLL
Module

SupportedPrincipalQuotient.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.IdeleClassPowerLocalUnitQuotient.SupportedPrincipalQuotient
17 declarations indexed from sourceView source ↗

Module documentation

Supported principal ideles and the idele-class quotient

This file identifies supported principal ideles with the corresponding S-unit group and derives the exact-sequence cardinal identities.

Imports5
Imported by6

Declarations

def

supportedPrincipalIdeleSubgroup

L37 ↗
GlobalClassFieldTheory.ClassFieldAxiom.supportedPrincipalIdeleSubgroup
Documentation

Principal ideles lying in I_K^{S ∪ T}, expressed as a subgroup of the supported idele group.

Source context 9 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
def supportedPrincipalIdeleSubgroup
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Subgroup
      (IdeleGroup.supportedAt
        (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))))
def

sUnitEquivSupportedPrincipalIdeleSubgroup

L49 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitEquivSupportedPrincipalIdeleSubgroup
Documentation

The diagonal map identifies the (S ∪ T)-units with the principal ideles lying in I_K^{S ∪ T}.

Source context 10 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
def sUnitEquivSupportedPrincipalIdeleSubgroup
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    SUnitGroup (K := K) (S ∪ T) ≃*
      supportedPrincipalIdeleSubgroup (K := K) S T
theorem

sUnitEquivSupportedPrincipalIdeleSubgroup_coe

L116 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitEquivSupportedPrincipalIdeleSubgroup_coe
Documentation

The supported-principal-idele equivalence has underlying idele equal to the principal idele of the original S-unit.

Source context 10 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
theorem sUnitEquivSupportedPrincipalIdeleSubgroup_coe
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
    (x : SUnitGroup (K := K) (S ∪ T)) :
    (((sUnitEquivSupportedPrincipalIdeleSubgroup
          (K := K) S T x :
        supportedPrincipalIdeleSubgroup (K := K) S T) :
      IdeleGroup.supportedAt
        (K := K)
        (S ∪ T : Set (HeightOneSpectrum (𝓞 K)))) :
      IdeleGroup K) =
        IdeleGroup.principalIdele K (x : Kˣ)
def

sUnitPrincipalIdelePowerSubgroup

L132 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitPrincipalIdelePowerSubgroup
Documentation

Under the preceding diagonal equivalence, this is the subgroup of (S ∪ T)-units whose principal ideles belong to h(S,T).

Source context 10 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
def sUnitPrincipalIdelePowerSubgroup
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Subgroup (SUnitGroup (K := K) (S ∪ T))
theorem

sUnitPrincipalIdelePowerSubgroup_map

L141 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitPrincipalIdelePowerSubgroup_map
Documentation

The diagonal equivalence carries the principal part of h(S,T) to the intersection of h(S,T) with the supported principal ideles.

Source context 9 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem sUnitPrincipalIdelePowerSubgroup_map
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    (sUnitPrincipalIdelePowerSubgroup (K := K) n S T).map
        (sUnitEquivSupportedPrincipalIdeleSubgroup
          (K := K) S T).toMonoidHom =
      (supportedIdelePowerLocalUnitSubgroup
        (K := K) n S T).subgroupOf
          (supportedPrincipalIdeleSubgroup (K := K) S T)
def

sUnitPrincipalIdelePowerQuotientEquivSupportedPrincipalQuotient

L199 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitPrincipalIdelePowerQuotientEquivSupportedPrincipalQuotient
Documentation

The left term in the supported exact sequence, expressed as the actual quotient of (S ∪ T)-units satisfying the principal h(S,T)-condition.

Source context 10 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
def
    sUnitPrincipalIdelePowerQuotientEquivSupportedPrincipalQuotient
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    SUnitGroup (K := K) (S ∪ T) ⧸
        sUnitPrincipalIdelePowerSubgroup (K := K) n S T ≃*
      supportedPrincipalIdeleSubgroup (K := K) S T ⧸
        (supportedIdelePowerLocalUnitSubgroup
          (K := K) n S T).subgroupOf
            (supportedPrincipalIdeleSubgroup (K := K) S T)
theorem

card_supportedPrincipalQuotient_eq_sUnitPrincipalQuotient

L222 ↗
GlobalClassFieldTheory.ClassFieldAxiom.card_supportedPrincipalQuotient_eq_sUnitPrincipalQuotient
Documentation

Cardinal form of the diagonal identification of the left term in the supported exact sequence.

Source context 10 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
theorem card_supportedPrincipalQuotient_eq_sUnitPrincipalQuotient
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Nat.card
        (supportedPrincipalIdeleSubgroup (K := K) S T ⧸
          (supportedIdelePowerLocalUnitSubgroup
            (K := K) n S T).subgroupOf
              (supportedPrincipalIdeleSubgroup (K := K) S T)) =
      Nat.card
        (SUnitGroup (K := K) (S ∪ T) ⧸
          sUnitPrincipalIdelePowerSubgroup (K := K) n S T)
def

supportedIdeleClassPowerDenominator

L240 ↗
GlobalClassFieldTheory.ClassFieldAxiom.supportedIdeleClassPowerDenominator
Documentation

The denominator in the supported realization of C_K/C_K(S,T): it is generated by h(S,T) and the principal ideles which are supported at S ∪ T.

Source context 9 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
def supportedIdeleClassPowerDenominator
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Subgroup
      (IdeleGroup.supportedAt
        (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))))
instance

supportedClassQuotient_isMulCommutative

L251 ↗
GlobalClassFieldTheory.ClassFieldAxiom.supportedClassQuotient_isMulCommutative
Source context 10 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
section SupportedClassQuotient
Lean source · statement
instance supportedClassQuotient_isMulCommutative :
    IsMulCommutative (IdeleClassGroup K)
def

supportedIdeleToClassPowerQuotient

L257 ↗
GlobalClassFieldTheory.ClassFieldAxiom.supportedIdeleToClassPowerQuotient
Documentation

The natural map from supported ideles to C_K/C_K(S,T).

Source context 11 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
section SupportedClassQuotient
local instance supportedClassQuotient_isMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def supportedIdeleToClassPowerQuotient
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    IdeleGroup.supportedAt
          (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))) →*
      IdeleClassPowerLocalUnitQuotient (K := K) n S T
theorem

supportedIdeleToClassPowerQuotient_ker

L272 ↗
GlobalClassFieldTheory.ClassFieldAxiom.supportedIdeleToClassPowerQuotient_ker
Documentation

The kernel of the supported class-quotient map is precisely the subgroup generated by h(S,T) and the supported principal ideles.

Source context 11 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
section SupportedClassQuotient
local instance supportedClassQuotient_isMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem supportedIdeleToClassPowerQuotient_ker
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    (supportedIdeleToClassPowerQuotient
      (K := K) n S T).ker =
      supportedIdeleClassPowerDenominator (K := K) n S T
theorem

supportedIdeleToClassPowerQuotient_surjective

L355 ↗
GlobalClassFieldTheory.ClassFieldAxiom.supportedIdeleToClassPowerQuotient_surjective
Documentation

If S ∪ T is sufficiently large, every class modulo C_K(S,T) has a supported representative.

Source context 11 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
section SupportedClassQuotient
local instance supportedClassQuotient_isMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem supportedIdeleToClassPowerQuotient_surjective
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
    (hLarge :
      IdeleGroup.supportedAt
            (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))) ⊔
          IdeleGroup.principalSubgroup K =
        ⊤) :
    Function.Surjective
      (supportedIdeleToClassPowerQuotient
        (K := K) n S T)
def

supportedIdeleClassPowerQuotientEquiv

L400 ↗
GlobalClassFieldTheory.ClassFieldAxiom.supportedIdeleClassPowerQuotientEquiv
Documentation

Supported realization of the idele-class index quotient.

Source context 11 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
section SupportedClassQuotient
local instance supportedClassQuotient_isMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    supportedIdeleClassPowerQuotientEquiv
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
    (hLarge :
      IdeleGroup.supportedAt
            (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))) ⊔
          IdeleGroup.principalSubgroup K =
        ⊤) :
    IdeleGroup.supportedAt
          (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))) ⧸
        supportedIdeleClassPowerDenominator (K := K) n S T ≃*
      IdeleClassPowerLocalUnitQuotient (K := K) n S T
theorem

card_ideleClassPowerLocalUnitQuotient_eq_supported

L424 ↗
GlobalClassFieldTheory.ClassFieldAxiom.card_ideleClassPowerLocalUnitQuotient_eq_supported
Documentation

Cardinal form of the supported realization of [C_K:C_K(S,T)].

Source context 11 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
section SupportedClassQuotient
local instance supportedClassQuotient_isMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem card_ideleClassPowerLocalUnitQuotient_eq_supported
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
    (hLarge :
      IdeleGroup.supportedAt
            (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))) ⊔
          IdeleGroup.principalSubgroup K =
        ⊤) :
    Nat.card
        (IdeleClassPowerLocalUnitQuotient (K := K) n S T) =
      Nat.card
        (IdeleGroup.supportedAt
              (K := K) (S ∪ T :
                Set (HeightOneSpectrum (𝓞 K))) ⧸
          supportedIdeleClassPowerDenominator (K := K) n S T)
theorem

card_supportedPrincipalQuotient_mul_card_supportedClassQuotient

L453 ↗
GlobalClassFieldTheory.ClassFieldAxiom.card_supportedPrincipalQuotient_mul_card_supportedClassQuotient
Documentation

The cardinal identity furnished by the supported exact sequence:

1 → (I_K^{S∪T} ∩ Kˣ)/(h(S,T) ∩ Kˣ) → I_K^{S∪T}/h(S,T) → I_K^{S∪T}Kˣ/h(S,T)Kˣ → 1.

The first factor is written intrinsically as the relative index of h(S,T) in the supported principal ideles.

Source context 9 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem card_supportedPrincipalQuotient_mul_card_supportedClassQuotient
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Nat.card
          (supportedPrincipalIdeleSubgroup (K := K) S T ⧸
            (supportedIdelePowerLocalUnitSubgroup (K := K) n S T).subgroupOf
              (supportedPrincipalIdeleSubgroup (K := K) S T)) *
        Nat.card
          (IdeleGroup.supportedAt
                (K := K) (S ∪ T :
                  Set (HeightOneSpectrum (𝓞 K))) ⧸
            supportedIdeleClassPowerDenominator (K := K) n S T) =
      Nat.card
        (IdeleGroup.supportedAt
              (K := K) (S ∪ T :
                Set (HeightOneSpectrum (𝓞 K))) ⧸
          supportedIdelePowerLocalUnitSubgroup (K := K) n S T)
theorem

card_supportedPrincipalQuotient_mul_card_ideleClassQuotient

L486 ↗
GlobalClassFieldTheory.ClassFieldAxiom.card_supportedPrincipalQuotient_mul_card_ideleClassQuotient
Documentation

The exact-sequence cardinal identity with the right-hand term identified with the actual idele-class quotient C_K/C_K(S,T).

Source context 9 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem card_supportedPrincipalQuotient_mul_card_ideleClassQuotient
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
    (hLarge :
      IdeleGroup.supportedAt
            (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))) ⊔
          IdeleGroup.principalSubgroup K =
        ⊤) :
    Nat.card
          (supportedPrincipalIdeleSubgroup (K := K) S T ⧸
            (supportedIdelePowerLocalUnitSubgroup (K := K) n S T).subgroupOf
              (supportedPrincipalIdeleSubgroup (K := K) S T)) *
        Nat.card
          (IdeleClassPowerLocalUnitQuotient (K := K) n S T) =
      Nat.card
        (IdeleGroup.supportedAt
              (K := K) (S ∪ T :
                Set (HeightOneSpectrum (𝓞 K))) ⧸
          supportedIdelePowerLocalUnitSubgroup (K := K) n S T)
theorem

card_sUnitPrincipalQuotient_mul_card_ideleClassQuotient

L514 ↗
GlobalClassFieldTheory.ClassFieldAxiom.card_sUnitPrincipalQuotient_mul_card_ideleClassQuotient
Documentation

The exact-sequence identity in intrinsic S-unit notation.

Source context 10 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
theorem card_sUnitPrincipalQuotient_mul_card_ideleClassQuotient
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
    (hLarge :
      IdeleGroup.supportedAt
            (K := K) (S ∪ T : Set (HeightOneSpectrum (𝓞 K))) ⊔
          IdeleGroup.principalSubgroup K =
        ⊤) :
    Nat.card
          (SUnitGroup (K := K) (S ∪ T) ⧸
            sUnitPrincipalIdelePowerSubgroup (K := K) n S T) *
        Nat.card
          (IdeleClassPowerLocalUnitQuotient (K := K) n S T) =
      Nat.card
        (IdeleGroup.supportedAt
              (K := K) (S ∪ T :
                Set (HeightOneSpectrum (𝓞 K))) ⧸
          supportedIdelePowerLocalUnitSubgroup (K := K) n S T)

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