Module

SigmaEmbeddingSolutions.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaEmbeddingSolutions

2 declarations indexed from sourceView source ↗

Module documentation

Proper finite embedding solutions with faithful abelian Sigma kernels

For each finite quotient, the extension with finite abelian Sigma kernel may be chosen separately. A proper solution is surjective. Its image of the original kernel lies in the Sigma kernel, so the actual residual quotient and its abelianization detect the finite faithful action.

Imports8

Imported by3

def

HasFiniteFaithfulAbelianSigmaEmbeddingSolutions

L33 ↗

ProCGroups.FiniteStepSolvableQuotients.HasFiniteFaithfulAbelianSigmaEmbeddingSolutions

Documentation

Each finite quotient of each open subgroup admits a suitable finite extension with faithful abelian Sigma kernel and a proper solution.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.FreeProC.Characterization
universe u

Lean source · statement

def HasFiniteFaithfulAbelianSigmaEmbeddingSolutions
    (sigma : Set ℕ) (G : Type u)
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop

theorem

isSigmaAbFaithful

L49 ↗

ProCGroups.FiniteStepSolvableQuotients.HasFiniteFaithfulAbelianSigmaEmbeddingSolutions.isSigmaAbFaithful