Module

Conjugation.lean

Nyll.ProCGroups.GroupTheory.Conjugation

4 declarations indexed from sourceView source ↗

Module documentation

Conjugation on characteristic quotients

This module constructs the automorphism induced on a characteristic quotient and uses it to descend conjugation by a normal subgroup to an action of the ambient quotient.

Imports1

Mathlib.GroupTheory.QuotientGroup.Basic

Imported by2

def

quotientMulEquiv

L26 ↗

ProCGroups.Subgroup.Characteristic.quotientMulEquiv

Documentation

An automorphism descends to the quotient by a characteristic subgroup.

Source context 5 commands

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

namespace ProCGroups
namespace Subgroup
namespace Characteristic
universe u
variable {G : Type u} [Group G] {H : Subgroup G}

Lean source · statement

def quotientMulEquiv
    (hH : H.Characteristic) (e : G ≃* G) :
    G ⧸ H ≃* G ⧸ H

theorem

quotientMulEquiv_mk

L36 ↗

ProCGroups.Subgroup.Characteristic.quotientMulEquiv_mk

Documentation

The quotient equivalence induced by a characteristic subgroup sends representatives to representatives.

Source context 5 commands

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

namespace ProCGroups
namespace Subgroup
namespace Characteristic
universe u
variable {G : Type u} [Group G] {H : Subgroup G}

Lean source · statement

theorem quotientMulEquiv_mk
    (hH : H.Characteristic) (e : G ≃* G) (g : G) :
    quotientMulEquiv hH e (QuotientGroup.mk' H g) = QuotientGroup.mk' H (e g)

def

quotientConjugationOnCharacteristicQuotient

L54 ↗

ProCGroups.GroupTheory.quotientConjugationOnCharacteristicQuotient

Documentation

If \(K\) is characteristic in a normal subgroup \(N\) and inner conjugation by elements of \(N\) is trivial on \(N/K\), then \(G/N\) acts on \(N/K\) by conjugation.

Source context 2 commands

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

namespace ProCGroups.GroupTheory
universe u

Lean source · statement

def quotientConjugationOnCharacteristicQuotient
    {G : Type u} [Group G]
    (N : Subgroup G) [N.Normal] (K : Subgroup N) [K.Characteristic]
    (hNactsTrivially :
      ∀ n x : N, (((MulAut.conjNormal (n : G)) x) * x⁻¹ : N) ∈ K) :
    (G ⧸ N) →* MulAut (N ⧸ K)

theorem

quotientConjugationOnCharacteristicQuotient_mk_apply_mk

L98 ↗

ProCGroups.GroupTheory.quotientConjugationOnCharacteristicQuotient_mk_apply_mk

Documentation

The algebraic conjugation action sends representatives to conjugates.

Source context 2 commands

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

namespace ProCGroups.GroupTheory
universe u

Lean source · statement

theorem quotientConjugationOnCharacteristicQuotient_mk_apply_mk
    {G : Type u} [Group G]
    (N : Subgroup G) [N.Normal] (K : Subgroup N) [K.Characteristic]
    (hNactsTrivially :
      ∀ n x : N, (((MulAut.conjNormal (n : G)) x) * x⁻¹ : N) ∈ K)
    (g : G) (n : N) :
    quotientConjugationOnCharacteristicQuotient
      (G := G) N K hNactsTrivially
      (QuotientGroup.mk' N g) (QuotientGroup.mk' K n) =
        QuotientGroup.mk' K ((MulAut.conjNormal g) n)

Module documentation

Conjugation on characteristic quotients

Declarations

quotientMulEquiv

quotientMulEquiv_mk

quotientConjugationOnCharacteristicQuotient

quotientConjugationOnCharacteristicQuotient_mk_apply_mk