Module

SigmaEmbeddingFormulation.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaEmbeddingFormulation

2 declarations indexed from sourceView source ↗

Module documentation

The finite embedding formulation of Sigma-abelianization-faithfulness

The actual finite ambient quotient constructed from a faithful residual abelian quotient supplies the extension and its proper solution. Its kernel is exactly the image of the original normal subgroup, so it is a Sigma group. No Sigma restriction is placed on the original finite quotient.

Imports9

Imported by1

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.All

theorem

hasFiniteFaithfulAbelianSigmaEmbeddingSolutions

L34 ↗

ProCGroups.FiniteStepSolvableQuotients.IsSigmaAbFaithful.hasFiniteFaithfulAbelianSigmaEmbeddingSolutions

Documentation

Sigma-abelianization-faithfulness constructs a suitable finite extension with faithful abelian Sigma kernel and a proper solution for each quotient.

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

theorem IsSigmaAbFaithful.hasFiniteFaithfulAbelianSigmaEmbeddingSolutions
    {sigma : Set ℕ} {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : IsSigmaAbFaithful sigma G) :
    HasFiniteFaithfulAbelianSigmaEmbeddingSolutions sigma G

theorem

isSigmaAbFaithful_iff_hasFiniteFaithfulAbelianSigmaEmbeddingSolutions

L107 ↗

ProCGroups.FiniteStepSolvableQuotients.isSigmaAbFaithful_iff_hasFiniteFaithfulAbelianSigmaEmbeddingSolutions