Module

SplitSemidirect.lean

Nyll.ProCGroups.GroupTheory.SplitSemidirect

3 declarations indexed from sourceView source ↗

Module documentation

A split homomorphism as its kernel semidirect product

The section acts on the actual kernel by conjugation. Multiplication of a kernel element by the image of the section reconstructs the original group. No commutativity or finiteness assumption is required.

Imports2

Mathlib.GroupTheory.SemidirectProduct
Mathlib.Algebra.Group.Hom.Basic

Imported by2

def

splitKernelSemidirectMulEquiv

L26 ↗

ProCGroups.splitKernelSemidirectMulEquiv

Documentation

A section identifies the kernel semidirect product with the original group, using conjugation by that same section as the action.

Source context 3 commands

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

namespace ProCGroups
universe uE uB
variable {E : Type uE} [Group E] {B : Type uB} [Group B]

Lean source · statement

def splitKernelSemidirectMulEquiv
    (α : E →* B) (s : B →* E) (hs : α.comp s = MonoidHom.id B) :
    α.ker ⋊[(MulAut.conjNormal : E →* MulAut α.ker).comp s] B ≃* E

theorem

splitKernelSemidirectMulEquiv_apply

L60 ↗

ProCGroups.splitKernelSemidirectMulEquiv_apply

Documentation

The equivalence is the actual multiplication map determined by the section.

Source context 3 commands

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

namespace ProCGroups
universe uE uB
variable {E : Type uE} [Group E] {B : Type uB} [Group B]

Lean source · statement

theorem splitKernelSemidirectMulEquiv_apply
    (α : E →* B) (s : B →* E) (hs : α.comp s = MonoidHom.id B)
    (a : α.ker) (b : B) :
    splitKernelSemidirectMulEquiv α s hs ⟨a, b⟩ = (a : E) * s b

theorem

splitKernelSemidirectMulEquiv_commutes

L68 ↗

ProCGroups.splitKernelSemidirectMulEquiv_commutes

Documentation

The equivalence intertwines the original epimorphism and the projection to the second semidirect-product coordinate.

Source context 3 commands

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

namespace ProCGroups
universe uE uB
variable {E : Type uE} [Group E] {B : Type uB} [Group B]

Lean source · statement

theorem splitKernelSemidirectMulEquiv_commutes
    (α : E →* B) (s : B →* E) (hs : α.comp s = MonoidHom.id B)
    (x : α.ker ⋊[(MulAut.conjNormal : E →* MulAut α.ker).comp s] B) :
    α (splitKernelSemidirectMulEquiv α s hs x) = x.right

Module documentation

A split homomorphism as its kernel semidirect product

Declarations

splitKernelSemidirectMulEquiv

splitKernelSemidirectMulEquiv_apply

splitKernelSemidirectMulEquiv_commutes