Module

BurnsideBasis.lean

Nyll.ProCGroups.ProP.BurnsideBasis

3 declarations indexed from sourceView source ↗

Module documentation

The pro-p Burnside basis criterion

For a profinite group with an open-normal finite p-group basis, a set topologically generates the group exactly when its image generates the power--commutator quotient. This is the topological Burnside basis criterion, with the Frattini subgroup interpreted through finite continuous quotients.

The only locally synthesized structure in the main theorem is normality of the closed power--commutator subgroup. No quotient algebra or module instance is exported.

Imports3

Imported by4

theorem

topologicallyGenerates_union_normal_of_quotient

L34 ↗

ClassFieldTower.ProP.topologicallyGenerates_union_normal_of_quotient

Documentation

If a set generates a quotient, adjoining the kernel makes it generate the source.

Source context 4 commands

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

open Set
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation

Lean source · statement

theorem topologicallyGenerates_union_normal_of_quotient
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    {N : Subgroup G} [N.Normal] {X : Set G}
    (hX : TopologicallyGenerates (G := G ⧸ N) ((QuotientGroup.mk' N) '' X)) :
    TopologicallyGenerates (G := G) (X ∪ (N : Set G))

theorem

topologicallyGenerates_of_union_frattini_finite

L64 ↗

ClassFieldTower.ProP.topologicallyGenerates_of_union_frattini_finite

Documentation

Over a finite discrete group, adjoining the Frattini subgroup does not help a set topologically generate.

Source context 4 commands

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

open Set
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation

Lean source · statement

theorem topologicallyGenerates_of_union_frattini_finite
    {Q : Type u} [TopologicalSpace Q] [Group Q] [DiscreteTopology Q] [Finite Q]
    {S : Set Q}
    (hS : TopologicallyGenerates (G := Q) (S ∪ (frattini Q : Set Q))) :
    TopologicallyGenerates (G := Q) S

theorem

topologicallyGenerates_iff_powerCommutatorQuotient_image

L78 ↗

ClassFieldTower.ProP.topologicallyGenerates_iff_powerCommutatorQuotient_image

Documentation

The pro-p Burnside basis criterion: topological generation is detected by the power--commutator quotient.

Source context 4 commands

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

open Set
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation

Lean source · full declaration

theorem topologicallyGenerates_iff_powerCommutatorQuotient_image
    {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) {X : Set G} :
    letI : (closedPowerCommutator p G).Normal := closedPowerCommutator_normal p G
    TopologicallyGenerates (G := G) X ↔
      TopologicallyGenerates (G := powerCommutatorQuotient p G)
        ((powerCommutatorQuotientMk p G) '' X) := by
  let _ : (closedPowerCommutator p G).Normal := closedPowerCommutator_normal p G
  constructor
  · exact topologicallyGenerates_quotient_image
      (closedPowerCommutator p G)
  · intro hX
    have hXcore : TopologicallyGenerates (G := G)
        (X ∪ (closedPowerCommutator p G : Set G)) :=
      topologicallyGenerates_union_normal_of_quotient hX
    apply (topologicallyGenerates_iff_forall_quotientProj_image (G := G)).2
    intro U
    have hQU := ProCGroups.ProC.HasOpenNormalBasisInClass.quotient_mem
      (ProCGroups.FiniteGroupClass.pGroup_formation p) hG U
    have hgenUnion := topologicallyGenerates_quotient_image
      (U : Subgroup G) hXcore
    have hsubset :
        (QuotientGroup.mk' (U : Subgroup G)) ''
            (X ∪ (closedPowerCommutator p G : Set G)) ⊆
          ((QuotientGroup.mk' (U : Subgroup G)) '' X) ∪
            (frattini (G ⧸ (U : Subgroup G)) : Set (G ⧸ (U : Subgroup G))) := by
      rintro _ ⟨x, hx, rfl⟩
      rcases hx with hx | hx
      · exact Or.inl ⟨x, hx, rfl⟩
      · apply Or.inr
        rw [frattini_eq_closedPowerCommutator_of_isPGroup hQU.2]
        exact closedPowerCommutator_map_le p G
          (ProCGroups.ProC.OpenNormalSubgroup.quotientProj U) ⟨x, hx, rfl⟩
    have hgenWithFrattini :
        TopologicallyGenerates (G := G ⧸ (U : Subgroup G))
          (((QuotientGroup.mk' (U : Subgroup G)) '' X) ∪
            (frattini (G ⧸ (U : Subgroup G)) : Set (G ⧸ (U : Subgroup G)))) :=
      topologicallyGenerates_mono hgenUnion hsubset
    exact topologicallyGenerates_of_union_frattini_finite hgenWithFrattini

Module documentation

The pro-p Burnside basis criterion

Declarations

topologicallyGenerates_union_normal_of_quotient

topologicallyGenerates_of_union_frattini_finite

topologicallyGenerates_iff_powerCommutatorQuotient_image