Module

SemidirectSubgroups.lean

Nyll.ProCGroups.GroupTheory.SemidirectSubgroups

2 declarations indexed from sourceView source ↗

Module documentation

Kernels and subgroup preimages in a semidirect product

The actual right-projection kernel is its left factor. The preimage of a subgroup of the right factor is the semidirect product with the restricted action. Both identifications preserve the displayed coordinates.

Imports1

Mathlib.GroupTheory.SemidirectProduct

Imported by4

def

semidirectRightKernelEquiv

L24 ↗

ProCGroups.semidirectRightKernelEquiv

Documentation

The actual kernel of the right projection is the left factor.

Source context 3 commands

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

namespace ProCGroups
universe uA uQ
variable {A : Type uA} [Group A] {Q : Type uQ} [Group Q]

Lean source · full declaration

def semidirectRightKernelEquiv (φ : Q →* MulAut A) :
    (SemidirectProduct.rightHom : A ⋊[φ] Q →* Q).ker ≃* A where
  toFun x := (x : A ⋊[φ] Q).left
  invFun a := ⟨SemidirectProduct.inl a, SemidirectProduct.rightHom_inl a⟩
  left_inv x := by
    apply Subtype.ext
    apply SemidirectProduct.ext
    · rfl
    · exact x.property.symm
  right_inv _ := rfl
  map_mul' x y := by
    change (x : A ⋊[φ] Q).left * φ (x : A ⋊[φ] Q).right
      (y : A ⋊[φ] Q).left = (x : A ⋊[φ] Q).left * (y : A ⋊[φ] Q).left
    have hx : (x : A ⋊[φ] Q).right = 1 := x.property
    rw [hx, map_one, MulAut.one_apply]

def

semidirectRightPreimageEquiv

L42 ↗

ProCGroups.semidirectRightPreimageEquiv