The cyclotomic torsion calculation uses the decomposition Gal(ℚ_cyc/ℚ) ≃ ℤ̂ × f, where the torsion subgroup is dense in the second factor. This file proves the topological-group calculation which turns that decomposition into a ℤ̂-extension.
The additive group of ℤ̂ is torsion-free.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFormationinstance : IsAddTorsionFree ZHatThe multiplicative presentation of additive ℤ̂ is torsion-free.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFormationinstance : IsMulTorsionFree (Multiplicative ZHat)In a product ℤ̂ × T whose torsion is dense in T, the closure of the torsion subgroup is precisely the second factor.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFormationtheorem topologicalClosure_torsion_zHatMul_prod
(T : Type*) [CommGroup T] [TopologicalSpace T] [IsTopologicalGroup T]
(hT : Dense (CommGroup.torsion T : Set T)) :
(CommGroup.torsion (Multiplicative ZHat × T)).topologicalClosure =
(⊥ : Subgroup (Multiplicative ZHat)).prod (⊤ : Subgroup T)Algebraic quotient form of the cyclotomic torsion decomposition: after a cyclotomic decomposition with dense torsion factor, quotienting by the closure of torsion leaves the ℤ̂ factor.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFormationdef torsionQuotientZHatMulProdEquiv
(T : Type*) [CommGroup T] [TopologicalSpace T] [IsTopologicalGroup T]
(hT : Dense (CommGroup.torsion T : Set T)) :
(Multiplicative ZHat × T) ⧸
(CommGroup.torsion (Multiplicative ZHat × T)).topologicalClosure ≃*
Multiplicative ZHat