This file constructs the closed subgroup generated by all pth powers and all commutators. It is the concrete side of the pro-p Frattini formula; the identification with frattini G will require the pro-p maximal-subgroup argument and is deliberately not assumed here.
The algebraic subgroup generated by all pth powers in G.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
namespace ClassFieldTower.ProP
universe u
section Algebraic
variable (p : ℕ) (G : Type u) [Group G]def powerSubgroup : Subgroup GEvery pth power belongs to the subgroup generated by the pth powers.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
namespace ClassFieldTower.ProP
universe u
section Algebraic
variable (p : ℕ) (G : Type u) [Group G]theorem pow_mem_powerSubgroup (g : G) : g ^ p ∈ powerSubgroup p GHomomorphisms carry the p-power subgroup into the p-power subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
namespace ClassFieldTower.ProP
universe u
section Algebraic
variable (p : ℕ) (G : Type u) [Group G]theorem powerSubgroup_map_le
{H : Type*} [Group H] (f : G →* H) :
(powerSubgroup p G).map f ≤ powerSubgroup p HThe p-power subgroup is fixed by every continuous automorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
namespace ClassFieldTower.ProP
universe u
section Characteristic
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G]theorem powerSubgroup_topologicallyCharacteristic :
(powerSubgroup p G).TopologicallyCharacteristicThe closed subgroup generated by the pth powers and the commutator subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
namespace ClassFieldTower.ProP
universe u
section Topological
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]def closedPowerCommutator : Subgroup GThe closed power--commutator subgroup is topologically characteristic.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
namespace ClassFieldTower.ProP
universe u
section Topological
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]theorem closedPowerCommutator_topologicallyCharacteristic :
(closedPowerCommutator p G).TopologicallyCharacteristicThe closed power--commutator subgroup is topologically closed.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
namespace ClassFieldTower.ProP
universe u
section Topological
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]theorem isClosed_closedPowerCommutator :
IsClosed (closedPowerCommutator p G : Set G)The algebraic p-power subgroup lies in the closed power--commutator subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
namespace ClassFieldTower.ProP
universe u
section Topological
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]theorem powerSubgroup_le_closedPowerCommutator :
powerSubgroup p G ≤ closedPowerCommutator p GThe commutator subgroup lies in the closed power--commutator subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
namespace ClassFieldTower.ProP
universe u
section Topological
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]theorem commutator_le_closedPowerCommutator :
commutator G ≤ closedPowerCommutator p GEvery pth power lies in the closed power--commutator subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
namespace ClassFieldTower.ProP
universe u
section Topological
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]theorem pow_mem_closedPowerCommutator (g : G) :
g ^ p ∈ closedPowerCommutator p GThe closed power--commutator subgroup is normal.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
namespace ClassFieldTower.ProP
universe u
section Topological
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]theorem closedPowerCommutator_normal :
(closedPowerCommutator p G).NormalContinuous homomorphisms preserve the closed power--commutator filtration term.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
namespace ClassFieldTower.ProP
universe u
section Topological
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]theorem closedPowerCommutator_map_le
{H : Type*} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
(f : G →ₜ* H) :
(closedPowerCommutator p G).map f.toMonoidHom ≤ closedPowerCommutator p H