The quotient by the closed subgroup generated by pth powers and commutators is universal for continuous homomorphisms into commutative exponent-p topological groups with closed identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.ProP
universe u v
section
variable {p : ℕ}
variable {G : Type u} {A : Type v}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable [TopologicalSpace A] [CommGroup A] [T1Space A]instance : (closedPowerCommutator p G).NormalUniversal lift from the power--commutator quotient to a commutative exponent-p target.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.ProP
universe u v
section
variable {p : ℕ}
variable {G : Type u} {A : Type v}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable [TopologicalSpace A] [CommGroup A] [T1Space A]
local instance : (closedPowerCommutator p G).Normal :=
closedPowerCommutator_normal p Gdef powerCommutatorQuotientLift
(f : G →ₜ* A) (hA : ∀ a : A, a ^ p = 1) :
powerCommutatorQuotient p G →ₜ* ASurrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.ProP
universe u v
section
variable {p : ℕ}
variable {G : Type u} {A : Type v}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable [TopologicalSpace A] [CommGroup A] [T1Space A]
local instance : (closedPowerCommutator p G).Normal :=
closedPowerCommutator_normal p Gtheorem powerCommutatorQuotientLift_apply_mk
(f : G →ₜ* A) (hA : ∀ a : A, a ^ p = 1) (g : G) :
powerCommutatorQuotientLift f hA (powerCommutatorQuotientMk p G g) = f gThe universal lift is the unique continuous homomorphism whose composite with the quotient map is the given homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.ProP
universe u v
section
variable {p : ℕ}
variable {G : Type u} {A : Type v}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable [TopologicalSpace A] [CommGroup A] [T1Space A]
local instance : (closedPowerCommutator p G).Normal :=
closedPowerCommutator_normal p Gtheorem powerCommutatorQuotientLift_unique
(f : G →ₜ* A) (hA : ∀ a : A, a ^ p = 1)
(φ : powerCommutatorQuotient p G →ₜ* A)
(hφ : φ.comp (powerCommutatorQuotientMk p G) = f) :
φ = powerCommutatorQuotientLift f hA