Module

AbelianKernelEmbeddingProblems.lean

Nyll.ProCGroups.FreeProC.Characterization.AbelianKernelEmbeddingProblems

1 declaration indexed from sourceView source ↗

Module documentation

Split embedding problems with a condition on the abelian kernel

The finite quotient and covering group are arbitrary finite discrete groups. Only the kernel of the covering epimorphism belongs to the specified class. For the Sigma group class this is exactly the split abelian Sigma-kernel solvability condition; the elementary class gives its elementary variant.

Imports2

Imported by6

def

HasFiniteSplitAbelianKernelEmbeddingSolutions

L25 ↗

ProCGroups.FreeProC.Characterization.HasFiniteSplitAbelianKernelEmbeddingSolutions

Documentation

Every finite split problem with abelian kernel in C has a proper solution. There is no class-membership condition on either whole endpoint.

Source context 2 commands

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

namespace ProCGroups.FreeProC.Characterization
universe u

Lean source · statement

def HasFiniteSplitAbelianKernelEmbeddingSolutions
    (C : ProCGroups.FiniteGroupClass.{u})
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop

Module documentation

Split embedding problems with a condition on the abelian kernel

Declarations

HasFiniteSplitAbelianKernelEmbeddingSolutions