KummerTheory.torsionQuotientEquivOfZHatMulDecomposition_mk
The torsion-quotient equivalence evaluates a quotient class by taking the genuine torsion-free coordinate of the chosen product decomposition. This is the commuting square needed to pass between an actual cyclotomic character and the ZHat-coordinate of its torsion fixed field.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace KummerTheory
open ClassFormationLean source · statement
theorem torsionQuotientEquivOfZHatMulDecomposition_mk
(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 : G) :
torsionQuotientEquivOfZHatMulDecomposition
G T E hT (QuotientGroup.mk g) =
(E g).1