NYLL
Module

AbelianKernelOpenSubgroup.lean

Nyll.ProCGroups.FreeProC.Characterization.AbelianKernelOpenSubgroup
2 declarations indexed from sourceView source ↗

Module documentation

Split abelian-kernel solvability passes to open subgroups

A finite quotient of the open subgroup is placed inside an actual finite ambient quotient. Inducing its kernel action gives a split problem for the ambient group. Its proper solution restricts surjectively to the required semidirect subgroup, and evaluation recovers the original problem.

Imports8
Imported by2

Declarations

theorem

exists_semidirect_lift

L36 ↗
ProCGroups.FreeProC.Characterization.exists_semidirect_lift
Documentation

Apply the solver to the actual right projection, using the isomorphism of its kernel with the specified commutative coefficient group.

Source context 4 commands

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

namespace ProCGroups.FreeProC.Characterization
open ProCGroups.InducedFunctions
universe u
variable {C : FiniteGroupClass.{u}}
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem exists_semidirect_lift
    (hsolve : HasFiniteSplitAbelianKernelEmbeddingSolutions C G)
    {Q I : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    [Finite Q] [DiscreteTopology Q] [CommGroup I]
    (φ : Q →* MulAut I) [TopologicalSpace (I ⋊[φ] Q)]
    [DiscreteTopology (I ⋊[φ] Q)]
    (hI : C I) (q : G →ₜ* Q) (hq : Function.Surjective q) :
    ∃ σ : G →ₜ* I ⋊[φ] Q, Function.Surjective σ ∧
      ∀ g : G, (σ g).right = q g
theorem

openSubgroup

L81 ↗
ProCGroups.FreeProC.Characterization.HasFiniteSplitAbelianKernelEmbeddingSolutions.openSubgroup
Documentation

Solvability of all finite split embedding problems whose abelian kernel belongs to C passes to open subgroups. Only subgroup and finite-product closure of C are used; the whole covering and quotient groups are unrestricted.

Source context 4 commands

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

namespace ProCGroups.FreeProC.Characterization
open ProCGroups.InducedFunctions
universe u
variable {C : FiniteGroupClass.{u}}
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem HasFiniteSplitAbelianKernelEmbeddingSolutions.openSubgroup
    (hsolve : HasFiniteSplitAbelianKernelEmbeddingSolutions C G)
    (hSub : C.SubgroupClosed) (hProd : C.FiniteProductClosed)
    [CompactSpace G] (H : OpenSubgroup G) :
    HasFiniteSplitAbelianKernelEmbeddingSolutions C (H : Subgroup G)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.