KummerTheory.torsionQuotientEquivOfZHatMulDecomposition
A topological decomposition G ≃ ℤ̂ × T with dense torsion in T identifies the quotient of G by the closure of its torsion with ℤ̂.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace KummerTheory
open ClassFormation
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
(continuousMulEquivOfCompactToT2) inLean source · statement
def torsionQuotientEquivOfZHatMulDecomposition
(G T : Type*) [CommGroup G] [CommGroup T]
[TopologicalSpace G] [TopologicalSpace T]
[IsTopologicalGroup G] [IsTopologicalGroup T]
[CompactSpace G]
(E : G ≃ₜ* Multiplicative ZHat × T)
(hT : Dense (CommGroup.torsion T : Set T)) :
G ⧸ (CommGroup.torsion G).topologicalClosure ≃ₜ*
Multiplicative ZHat