Module

Theorem2Dot1ElementarySplitCriterion.lean

Nyll.Yamaguchi26AbfaithfulGalois.Theorem2Dot1ElementarySplitCriterion

1 declaration indexed from sourceView source ↗

Module documentation

Proposition 2.1: finite split embedding problems

Source: Yamaguchi, arXiv:2610.05634v1, Proposition 2.1. The stronger regular-module quotient construction is retained in GroupTheory/ElementarySplitRegularQuotient.lean.

Imports2

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.ElementarySplitCriterion
Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Imported by1

Nyll.Yamaguchi26AbfaithfulGalois.All

theorem

elementary_split_criterion_2_1

L27 ↗

Yamaguchi26AbfaithfulGalois.elementary_split_criterion_2_1

Documentation

Proper solvability of finite split embedding problems with elementary abelian q-kernel implies q-ab-faithfulness.

Source context 4 commands

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

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

Lean source · statement

theorem elementary_split_criterion_2_1
    {q : ℕ} [Fact q.Prime] (G : ProfiniteGrp.{u})
    (hsolve : HasFiniteSplitAbelianKernelEmbeddingSolutions
      (FiniteGroupClass.abelianExponent q) G) :
    IsSigmaAbFaithful {q} G

Module documentation

Proposition 2.1: finite split embedding problems

Declarations

elementary_split_criterion_2_1