Module

CyclotomicQuotient.lean

Nyll.GaloisCohomology.Kummer.Concrete.Cyclotomic.ProfiniteUnitDecomposition.CyclotomicQuotient

1 declaration indexed from sourceView source ↗

Module documentation

Imports1

Imported by3

def

KummerTheory.zHatUnitsTorsionQuotientEquiv

Documentation

Cyclotomic-character form of the torsion decomposition: quotienting ℤ̂ˣ by the closure of its torsion subgroup leaves one copy of ℤ̂.

Source context 4 commands

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

open scoped Topology
noncomputable section
namespace KummerTheory
open ClassFormation

Lean source · statement

def zHatUnitsTorsionQuotientEquiv :
    ZHatˣ ⧸ (CommGroup.torsion ZHatˣ).topologicalClosure ≃ₜ*
      Multiplicative ZHat