Module

FaithfulKernel.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.FaithfulKernel

4 declarations indexed from sourceView source ↗

Module documentation

Faithful conjugation on an abelian kernel

Conjugation descends along an epimorphism with abelian kernel. Its faithfulness is characterized by the kernel being its own centralizer.

Imports1

Mathlib.GroupTheory.QuotientGroup.Basic

Imported by6

theorem

abelianKernel_le_ker_conjNormal

L23 ↗

ProCGroups.FiniteStepSolvableQuotients.abelianKernel_le_ker_conjNormal

Documentation

An abelian kernel acts trivially on itself by conjugation.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
universe u v
variable {E : Type u} [Group E] {B : Type v} [Group B]

Lean source · statement

theorem abelianKernel_le_ker_conjNormal (α : E →* B)
    (hcomm : ∀ a b : α.ker, Commute (a : E) (b : E)) :
    α.ker ≤ (MulAut.conjNormal : E →* MulAut α.ker).ker

def

abelianKernelConjugation

L34 ↗

ProCGroups.FiniteStepSolvableQuotients.abelianKernelConjugation

Documentation

The action of the quotient target on the abelian kernel of an epimorphism.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
universe u v
variable {E : Type u} [Group E] {B : Type v} [Group B]

Lean source · statement

def abelianKernelConjugation (α : E →* B)
    (hsurj : Function.Surjective α)
    (hcomm : ∀ a b : α.ker, Commute (a : E) (b : E)) :
    B →* MulAut α.ker

theorem

abelianKernelConjugation_apply

L43 ↗

ProCGroups.FiniteStepSolvableQuotients.abelianKernelConjugation_apply

Documentation

The descended action agrees with conjugation by every lift.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
universe u v
variable {E : Type u} [Group E] {B : Type v} [Group B]

Lean source · statement

theorem abelianKernelConjugation_apply (α : E →* B)
    (hsurj : Function.Surjective α)
    (hcomm : ∀ a b : α.ker, Commute (a : E) (b : E))
    (e : E) (a : α.ker) :
    abelianKernelConjugation α hsurj hcomm (α e) a = MulAut.conjNormal e a

theorem

abelianKernelConjugation_injective_iff

L61 ↗

ProCGroups.FiniteStepSolvableQuotients.abelianKernelConjugation_injective_iff

Documentation

Faithfulness is equivalent to the abelian kernel being self-centralizing.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
universe u v
variable {E : Type u} [Group E] {B : Type v} [Group B]

Lean source · statement

theorem abelianKernelConjugation_injective_iff (α : E →* B)
    (hsurj : Function.Surjective α)
    (hcomm : ∀ a b : α.ker, Commute (a : E) (b : E)) :
    Function.Injective (abelianKernelConjugation α hsurj hcomm) ↔
      ∀ e : E, (∀ a : α.ker, Commute e (a : E)) → e ∈ α.ker

Module documentation

Faithful conjugation on an abelian kernel

Declarations

abelianKernel_le_ker_conjNormal

abelianKernelConjugation

abelianKernelConjugation_apply

abelianKernelConjugation_injective_iff