Module

PowerCongruenceCore.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.PowerCongruenceCore

1 declaration indexed from sourceView source ↗

Module documentation

Power congruence subgroups inside finite-index idele-class subgroups

Let H be a closed finite-index subgroup of the idele class group and let n = [C_K : H]. Every n-th power belongs to H. If a finite set of finite places contains the support of a congruence subgroup lying in H, the ideles which are local n-th powers on that set and integral units away from it therefore also map into H.

This is the concrete power-congruence core used in the existence proof for global class fields.

Imports9

Imported by2

theorem

ideleClassPowerLocalUnitSubgroup_le_closedFiniteIndexSubgroup

L51 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassPowerLocalUnitSubgroup_le_closedFiniteIndexSubgroup

Documentation

Let n = [C_K : H]. If S contains the support of the canonical congruence subgroup lying in a closed finite-index subgroup H, then the idele-class power-congruence subgroup C_K(n, S, ∅) is contained in H.

The proof assembles the finitely many prescribed local n-th roots into one idele. Dividing by its n-th power leaves an idele in the canonical ray congruence subgroup.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem ideleClassPowerLocalUnitSubgroup_le_closedFiniteIndexSubgroup
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (hS :
      (RayClass.modulusInsideClosedFiniteIndex H hclosed).finitePart.support ⊆ S) :
    ideleClassPowerLocalUnitSubgroup
        (K := K)
        ⟨H.index,
          Nat.pos_of_ne_zero Subgroup.FiniteIndex.index_ne_zero⟩
        S ∅ ≤
      H

Module documentation

Power congruence subgroups inside finite-index idele-class subgroups

Declarations

ideleClassPowerLocalUnitSubgroup_le_closedFiniteIndexSubgroup