Module

ProfiniteAPI.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.ProfiniteAPI

3 declarations indexed from sourceView source ↗

Module documentation

Profinite reciprocity facade

This module specializes the three principal finite reciprocity endpoints to a bundled profinite group. The bundle supplies the ambient topology, compactness, separation, and total disconnectedness instances required by the generic theorems.

Imports2

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.ClassField

Imported by1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.All

def

normSubgroupOrderIso

L28 ↗

ClassFormation.Profinite.normSubgroupOrderIso

Documentation

The finite abelian norm-subgroup classification for a bundled profinite group. This is the thin specialization of the existing generic order isomorphism; the profinite bundle supplies all ambient topological instances.

Source context 3 commands

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

noncomputable section
namespace ClassFormation.Profinite
open CyclicCohomology KummerTheory

Lean source · statement

def normSubgroupOrderIso
    (P : ProfiniteGrp) {D : DegreeData P} {A : Rep ℤ P}
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    (K : FiniteAbstractField P) :
    FiniteAbelianSubextension K.field ≃o
      (FiniteAbelianSubextension.NormOpenAddSubgroup A K.field)ᵒᵈ

def

classField

L39 ↗

ClassFormation.Profinite.classField

Documentation

The class field attached to a norm-open subgroup for a bundled profinite group. This thin specialization consumes the profinite norm-subgroup facade, so callers do not enumerate ambient topological instances.

Source context 3 commands

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

noncomputable section
namespace ClassFormation.Profinite
open CyclicCohomology KummerTheory

Lean source · statement

def classField
    (P : ProfiniteGrp) {D : DegreeData P} {A : Rep ℤ P}
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    (K : FiniteAbstractField P)
    (N : FiniteAbelianSubextension.NormOpenAddSubgroup A K.field) :
    FiniteAbelianSubextension K.field

def

normResidueSymbol

L50 ↗

ClassFormation.Profinite.normResidueSymbol

Documentation

The finite norm-residue symbol for a bundled profinite group. This is the thin specialization of the existing generic symbol; the profinite bundle supplies all ambient topological instances.

Source context 3 commands

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

noncomputable section
namespace ClassFormation.Profinite
open CyclicCohomology KummerTheory

Lean source · full declaration

def normResidueSymbol
    (P : ProfiniteGrp) (D : DegreeData P) (A : Rep ℤ P)
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    (K : FiniteAbstractField P) (L : FiniteGaloisSubextension K.field) :
    letI : Finite
        (K.field.toSubgroup ⧸
          extensionSubgroup K.field L.field L.below) := L.finite
    FiniteNormQuotient A K.field L.field L.below ≃+
      Additive (Abelianization L.extensionQuotient) :=
  D.normResidueSymbol A v hcf K L

Module documentation

Profinite reciprocity facade

Declarations

normSubgroupOrderIso

classField

normResidueSymbol