ClassFieldTower.ProP.zassenhausSubgroup
The mod-p Zassenhaus subgroup defined by the closed augmentation filtration.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]Lean source · full declaration
def zassenhausSubgroup (n : ℕ) : Subgroup G where
carrier := {g | groupLikeDifference p G g ∈ closedAugmentationPower p G n}
one_mem' := by simp [groupLikeDifference_one]
mul_mem' := by
intro g h hg hh
change groupLikeDifference p G g ∈ closedAugmentationPower p G n at hg
change groupLikeDifference p G h ∈ closedAugmentationPower p G n at hh
change groupLikeDifference p G (g * h) ∈ closedAugmentationPower p G n
rw [groupLikeDifference_mul]
exact (closedAugmentationPower p G n).add_mem
((closedAugmentationPower p G n).add_mem hg hh)
((closedAugmentationPower p G n).mul_mem_left _ hh)
inv_mem' := by
intro g hg
change groupLikeDifference p G g ∈ closedAugmentationPower p G n at hg
change groupLikeDifference p G g⁻¹ ∈ closedAugmentationPower p G n
rw [groupLikeDifference_inv]
exact (closedAugmentationPower p G n).mul_mem_left _ hg