Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.ElementaryFaithfulEmbeddingSolution

Module documentation

Faithful prime-kernel solutions from elementary split solvability

For each actual finite quotient, apply the elementary-kernel solver to the regular wreath product with cyclic coefficient group of order q. Its right projection and canonical section give the split problem, while its actual kernel has the faithful conjugation action constructed previously.

theorem

exists_faithful_primeKernel_embedding_solution

L32 ↗

ProCGroups.FiniteStepSolvableQuotients.exists_faithful_primeKernel_embedding_solution

Documentation

An elementary-kernel solver produces a suitable finite extension with faithful abelian singleton-Sigma kernel for every actual finite quotient.

Source context 3 commands

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

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

Lean source · statement

theorem exists_faithful_primeKernel_embedding_solution
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (q : ℕ) [Fact q.Prime]
    (hsolve : HasFiniteSplitAbelianKernelEmbeddingSolutions
      (FiniteGroupClass.abelianExponent q) H)
    (B : TopGrp.{u}) [Finite B] [DiscreteTopology B]
    (π : H →ₜ* B) (hπ : Function.Surjective π) :
    ∃ E : TopGrp.{u}, Finite E ∧ DiscreteTopology E ∧
      ∃ α : E →ₜ* B, ∃ hα : Function.Surjective α,
        ∃ hcomm : ∀ a b : α.toMonoidHom.ker, Commute (a : E) (b : E),
          FiniteGroupClass.sigmaGroup {q} α.toMonoidHom.ker ∧
            Function.Injective (abelianKernelConjugation α.toMonoidHom hα hcomm) ∧
              Nonempty (⟨E, B, α, hα, π, hπ⟩ : TopologicalEmbeddingProblem H).ProperSolution

Module documentation

Faithful prime-kernel solutions from elementary split solvability

Declarations

exists_faithful_primeKernel_embedding_solution