Module

ProfiniteFrattini.lean

Nyll.ProCGroups.ProP.ProfiniteFrattini

9 declarations indexed from sourceView source ↗

Module documentation

The Frattini subgroup of a pro-p group

This file defines the profinite Frattini subgroup by detection in every open normal finite quotient. For a group with an open-normal finite p-group basis, it proves the pro-p formula

profiniteFrattini G = closedPowerCommutator p G.

The proof reuses the finite Burnside--Frattini formula quotient by quotient. No commutative-group or module structure is exported from this file.

Imports3

Imported by4

theorem

powerSubgroup_le_map_of_surjective

L32 ↗

ClassFieldTower.ProP.powerSubgroup_le_map_of_surjective

Documentation

A surjective homomorphism realizes every target p-power inside the image of the source p-power subgroup.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
namespace ClassFieldTower.ProP
universe u v

Lean source · statement

theorem powerSubgroup_le_map_of_surjective
    {p : ℕ} {G : Type u} {H : Type v} [Group G] [Group H]
    (f : G →* H) (hf : Function.Surjective f) :
    powerSubgroup p H ≤ (powerSubgroup p G).map f

theorem

commutator_le_map_of_surjective

L43 ↗

ClassFieldTower.ProP.commutator_le_map_of_surjective

Documentation

A surjective homomorphism realizes the target commutator subgroup inside the image of the source commutator subgroup.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
namespace ClassFieldTower.ProP
universe u v

Lean source · statement

theorem commutator_le_map_of_surjective
    {G : Type u} {H : Type v} [Group G] [Group H]
    (f : G →* H) (hf : Function.Surjective f) :
    commutator H ≤ (commutator G).map f

theorem

closedPowerCommutator_le_map_of_surjective_finite

L58 ↗

ClassFieldTower.ProP.closedPowerCommutator_le_map_of_surjective_finite

Documentation

Over a finite Hausdorff target, a surjective continuous homomorphism maps the closed power--commutator subgroup onto the target one, reverse-inclusion direction.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
namespace ClassFieldTower.ProP
universe u v

Lean source · statement

theorem closedPowerCommutator_le_map_of_surjective_finite
    {p : ℕ} {G : Type u} {H : Type v}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace H] [Group H] [IsTopologicalGroup H] [T1Space H] [Finite H]
    (f : G →ₜ* H) (hf : Function.Surjective f) :
    closedPowerCommutator p H ≤
      (closedPowerCommutator p G).map f.toMonoidHom

theorem

closedPowerCommutator_map_eq_of_surjective_finite

L76 ↗

ClassFieldTower.ProP.closedPowerCommutator_map_eq_of_surjective_finite

Documentation

A surjective continuous homomorphism onto a finite Hausdorff group maps the closed power--commutator subgroup exactly onto the target one.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
namespace ClassFieldTower.ProP
universe u v

Lean source · statement

theorem closedPowerCommutator_map_eq_of_surjective_finite
    {p : ℕ} {G : Type u} {H : Type v}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace H] [Group H] [IsTopologicalGroup H] [T1Space H] [Finite H]
    (f : G →ₜ* H) (hf : Function.Surjective f) :
    (closedPowerCommutator p G).map f.toMonoidHom =
      closedPowerCommutator p H

def

profiniteFrattini

L87 ↗

ClassFieldTower.ProP.profiniteFrattini

Documentation

The profinite Frattini subgroup, detected in every open normal finite quotient.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
namespace ClassFieldTower.ProP
universe u v

Lean source · statement

def profiniteFrattini
    (G : Type u) [TopologicalSpace G] [Group G] : Subgroup G

theorem

mem_profiniteFrattini_iff

L94 ↗

ClassFieldTower.ProP.mem_profiniteFrattini_iff

Documentation

Membership in the profinite Frattini subgroup is membership in the Frattini subgroup after every open normal quotient projection.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
namespace ClassFieldTower.ProP
universe u v

Lean source · statement

theorem mem_profiniteFrattini_iff
    {G : Type u} [TopologicalSpace G] [Group G] {x : G} :
    x ∈ profiniteFrattini G ↔
      ∀ U : OpenNormalSubgroup G,
        QuotientGroup.mk' (U : Subgroup G) x ∈ frattini (G ⧸ (U : Subgroup G))

theorem

closedPowerCommutator_le_profiniteFrattini

L103 ↗

ClassFieldTower.ProP.closedPowerCommutator_le_profiniteFrattini

Documentation

In a pro-p group, the closed power--commutator subgroup lies in the profinite Frattini subgroup.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
namespace ClassFieldTower.ProP
universe u v

Lean source · statement

theorem closedPowerCommutator_le_profiniteFrattini
    {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)]
    (hG : ProCGroups.ProC.HasPGroupOpenNormalBasis p G) :
    closedPowerCommutator p G ≤ profiniteFrattini G

theorem

profiniteFrattini_le_closedPowerCommutator

L119 ↗

ClassFieldTower.ProP.profiniteFrattini_le_closedPowerCommutator

Documentation

In a pro-p group, finite-quotient Frattini detection gives no elements beyond the closed power--commutator subgroup.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
namespace ClassFieldTower.ProP
universe u v

Lean source · statement

theorem profiniteFrattini_le_closedPowerCommutator
    {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)]
    (hG : ProCGroups.ProC.HasPGroupOpenNormalBasis p G) :
    profiniteFrattini G ≤ closedPowerCommutator p G

theorem

profiniteFrattini_eq_closedPowerCommutator

L139 ↗

ClassFieldTower.ProP.profiniteFrattini_eq_closedPowerCommutator

Documentation

The pro-p Burnside--Frattini formula.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
namespace ClassFieldTower.ProP
universe u v

Lean source · statement

theorem profiniteFrattini_eq_closedPowerCommutator
    {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)]
    (hG : ProCGroups.ProC.HasPGroupOpenNormalBasis p G) :
    profiniteFrattini G = closedPowerCommutator p G

Module documentation

The Frattini subgroup of a pro-p group

Declarations