Module

Theorem5Dot2AbelianSplitSolvableSlim.lean

Nyll.Yamaguchi26AbfaithfulGalois.Theorem5Dot2AbelianSplitSolvableSlim

2 declarations indexed from sourceView source ↗

Module documentation

Proposition 5.2: finite split abelian embedding problems imply finite-step slimness

Source: Yamaguchi, arXiv:2610.05634v1, Proposition 5.2. For an open subgroup of G^m, choose a smaller open normal subgroup avoiding a nonidentity centralizing element. Lemma 5.1 supplies the finite split problem. Its proper solution factors through G^m, and faithfulness gives the contradiction.

Imports10

Nyll.Yamaguchi26AbfaithfulGalois.Theorem5Dot1FaithfulAbelianExtension
Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SlimnessAndTorsion
Nyll.ProCGroups.FreeProC.Characterization.AbelianKernelEmbeddingProblems
Nyll.ProCGroups.FiniteGroups.StandardClasses
Nyll.ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients
Nyll.ProCGroups.ProC.OpenNormalSubgroups.Basic
Nyll.ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
Nyll.ProCGroups.ProC.Quotients.ClosedNormal
Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Mathlib.Topology.Algebra.Group.Quotient

Imported by1

Nyll.Yamaguchi26AbfaithfulGalois.All

theorem

discrete_topDerivedTop_eq_derivedSeries

L34 ↗

Yamaguchi26AbfaithfulGalois.discrete_topDerivedTop_eq_derivedSeries

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 discrete_topDerivedTop_eq_derivedSeries
    (A : Type u) [Group A] [TopologicalSpace A] [DiscreteTopology A] (n : ℕ) :
    topDerivedTop A n = derivedSeries A n

theorem

abelian_split_solvable_slim

L51 ↗

Yamaguchi26AbfaithfulGalois.abelian_split_solvable_slim

Documentation

Proposition 5.2: proper solvability of every finite split embedding problem with abelian kernel makes all solvable quotients of length at least two slim.