NYLL
Module

RegularWreathKernel.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.RegularWreathKernel
6 declarations indexed from sourceView source ↗

Module documentation

Faithful elementary abelian kernels from regular wreath products

The right projection of the regular wreath product has a commutative kernel when the coefficient group is commutative. A nontrivial coefficient group makes the quotient's conjugation action faithful, by evaluation on a function supported at the identity. Finite coefficients killed by q give an actual elementary abelian kernel. No restriction is placed on the finite quotient group's order.

Imports10
Imported by3

Declarations

theorem

sigmaGroup_of_abelianExponent

L37 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_of_abelianExponent
Documentation

An elementary abelian group of prime exponent belongs to every finite Sigma class containing that prime.

Source context 3 commands

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

namespace ProCGroups
universe u
namespace FiniteGroupClass
Lean source · statement
theorem sigmaGroup_of_abelianExponent {sigma : Set ℕ} (q : ℕ) [Fact q.Prime]
    {A : Type u} [Group A] (hq : q ∈ sigma) (hA : abelianExponent q A) :
    sigmaGroup sigma A
theorem

regularWreathKernel_commute

L59 ↗
ProCGroups.FiniteStepSolvableQuotients.regularWreathKernel_commute
Documentation

The kernel of the actual right projection of a regular wreath product is commutative.

Source context 5 commands

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

namespace ProCGroups
universe u
namespace FiniteStepSolvableQuotients
open WreathProducts
variable {A B : Type u} [CommGroup A] [Group B]
Lean source · statement
theorem regularWreathKernel_commute
    (a b : (SemidirectProduct.rightHom : PermutationalWreathProduct A B B →* B).ker) :
    Commute (a : PermutationalWreathProduct A B B)
      (b : PermutationalWreathProduct A B B)
theorem

regularWreath_conj_inl_left_apply

L79 ↗
ProCGroups.FiniteStepSolvableQuotients.regularWreath_conj_inl_left_apply
Documentation

Conjugation on the function kernel of the regular wreath product is left translation by the right coordinate.

Source context 5 commands

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

namespace ProCGroups
universe u
namespace FiniteStepSolvableQuotients
open WreathProducts
variable {A B : Type u} [CommGroup A] [Group B]
Lean source · statement
theorem regularWreath_conj_inl_left_apply
    (w : PermutationalWreathProduct A B B) (f : B → A) (x : B) :
    (w * SemidirectProduct.inl f * w⁻¹).left x = f (w.right⁻¹ * x)
theorem

regularWreathKernel_conjugation_injective

L98 ↗
ProCGroups.FiniteStepSolvableQuotients.regularWreathKernel_conjugation_injective
Documentation

A nontrivial coefficient group makes the actual regular wreath kernel conjugation action faithful.

Source context 5 commands

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

namespace ProCGroups
universe u
namespace FiniteStepSolvableQuotients
open WreathProducts
variable {A B : Type u} [CommGroup A] [Group B]
Lean source · statement
theorem regularWreathKernel_conjugation_injective [Nontrivial A] :
    Function.Injective (abelianKernelConjugation
      (SemidirectProduct.rightHom : PermutationalWreathProduct A B B →* B)
      SemidirectProduct.rightHom_surjective
      (regularWreathKernel_commute (A := A) (B := B)))
theorem

regularWreathKernel_mem_abelianExponent

L124 ↗
ProCGroups.FiniteStepSolvableQuotients.regularWreathKernel_mem_abelianExponent
Documentation

Finite coefficients killed by q produce an actual finite abelian kernel of exponent dividing q.

Source context 5 commands

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

namespace ProCGroups
universe u
namespace FiniteStepSolvableQuotients
open WreathProducts
variable {A B : Type u} [CommGroup A] [Group B]
Lean source · statement
theorem regularWreathKernel_mem_abelianExponent [Finite A] [Finite B]
    (q : ℕ) (hpow : ∀ a : A, a ^ q = 1) :
    FiniteGroupClass.abelianExponent q
      (SemidirectProduct.rightHom : PermutationalWreathProduct A B B →* B).ker
theorem

regularWreathKernel_cyclicZMod_mem_abelianExponent

L156 ↗
ProCGroups.FiniteStepSolvableQuotients.regularWreathKernel_cyclicZMod_mem_abelianExponent
Documentation

The concrete cyclic coefficient group obtained from ZMod q gives an elementary abelian kernel for every finite quotient group.

Source context 6 commands

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

namespace ProCGroups
universe u
namespace FiniteStepSolvableQuotients
open WreathProducts
variable {A B : Type u} [CommGroup A] [Group B]
omit [CommGroup A] in
Lean source · statement
theorem regularWreathKernel_cyclicZMod_mem_abelianExponent [Finite B]
    (q : ℕ) [Fact q.Prime] :
    FiniteGroupClass.abelianExponent q
      (SemidirectProduct.rightHom :
        PermutationalWreathProduct (ULift.{u} (Multiplicative (ZMod q))) B B →* B).ker

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.