Semidirect product

This file defines semidirect products of groups, and the canonical maps in and out of the semidirect product. The semidirect product of N and G given a hom φ from G to the automorphism group of N is the product of sets with the group ⟨n₁, g₁⟩ * ⟨n₂, g₂⟩ = ⟨n₁ * φ g₁ n₂, g₁ * g₂⟩

Key definitions

There are two homs into the semidirect product inl : N →* N ⋊[φ] G and inr : G →* N ⋊[φ] G, and lift can be used to define maps N ⋊[φ] G →* H out of the semidirect product given maps f₁ : N →* H and f₂ : G →* H that satisfy the condition ∀ n g, f₁ (φ g n) = f₂ g * f₁ n * f₂ g⁻¹

Notation

This file introduces the global notation N ⋊[φ] G for SemidirectProduct N G φ

Tags

group, semidirect product

structure SemidirectProduct (N : Type u_1) (G : Type u_2) [Group N] [Group G] (φ : G →* MulAut N) : Type (max u_1 u_2)

The semidirect product of groups N and G, given a map φ from G to the automorphism group of N. It the product of sets with the group operation ⟨n₁, g₁⟩ * ⟨n₂, g₂⟩ = ⟨n₁ * φ g₁ n₂, g₁ * g₂⟩

• left : N

  The element of N

• right : G

  The element of G

theorem SemidirectProduct.ext {N : Type u_1} {G : Type u_2} {inst✝ : Group N} {inst✝¹ : Group G} {φ : G →* MulAut N} {x y : N ⋊[φ] G} (left : x.left = y.left) (right : x.right = y.right) : x = y

instance instDecidableEqSemidirectProduct {N✝ : Type u_4} {G✝ : Type u_5} {inst✝ : Group N✝} {inst✝¹ : Group G✝} {φ✝ : G✝ →* MulAut N✝} [DecidableEq N✝] [DecidableEq G✝] : DecidableEq (N✝ ⋊[φ✝] G✝)

Equations

• instDecidableEqSemidirectProduct = decEqSemidirectProduct✝

def «term_⋊[_]_» : Lean.TrailingParserDescr

The semidirect product of groups N and G, given a map φ from G to the automorphism group of N. It the product of sets with the group operation ⟨n₁, g₁⟩ * ⟨n₂, g₂⟩ = ⟨n₁ * φ g₁ n₂, g₁ * g₂⟩

Equations

• One or more equations did not get rendered due to their size.

instance SemidirectProduct.instMul {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : Mul (N ⋊[φ] G)

Equations

• SemidirectProduct.instMul = { mul := fun (a b : N ⋊[φ] G) => { left := a.left * (φ a.right) b.left, right := a.right * b.right } }

theorem SemidirectProduct.mul_def {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (a b : N ⋊[φ] G) : a * b = { left := a.left * (φ a.right) b.left, right := a.right * b.right }

@[simp]

theorem SemidirectProduct.mul_left {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (a b : N ⋊[φ] G) : (a * b).left = a.left * (φ a.right) b.left

@[simp]

theorem SemidirectProduct.mul_right {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (a b : N ⋊[φ] G) : (a * b).right = a.right * b.right

instance SemidirectProduct.instOne {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : One (N ⋊[φ] G)

Equations

• SemidirectProduct.instOne = { one := { left := 1, right := 1 } }

@[simp]

theorem SemidirectProduct.one_left {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : SemidirectProduct.left 1 = 1

@[simp]

theorem SemidirectProduct.one_right {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : SemidirectProduct.right 1 = 1

instance SemidirectProduct.instInv {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : Inv (N ⋊[φ] G)

Equations

• SemidirectProduct.instInv = { inv := fun (x : N ⋊[φ] G) => { left := (φ x.right⁻¹) x.left⁻¹, right := x.right⁻¹ } }

@[simp]

theorem SemidirectProduct.inv_left {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (a : N ⋊[φ] G) : a⁻¹.left = (φ a.right⁻¹) a.left⁻¹

@[simp]

theorem SemidirectProduct.inv_right {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (a : N ⋊[φ] G) : a⁻¹.right = a.right⁻¹

instance SemidirectProduct.instGroup {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : Group (N ⋊[φ] G)

Equations

• SemidirectProduct.instGroup = Group.mk ⋯

instance SemidirectProduct.instInhabited {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : Inhabited (N ⋊[φ] G)

Equations

• SemidirectProduct.instInhabited = { default := 1 }

def SemidirectProduct.inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : N →* N ⋊[φ] G

The canonical map N →* N ⋊[φ] G sending n to ⟨n, 1⟩

Equations

• SemidirectProduct.inl = { toFun := fun (n : N) => { left := n, right := 1 }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem SemidirectProduct.left_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (n : N) : (SemidirectProduct.inl n).left = n

@[simp]

theorem SemidirectProduct.right_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (n : N) : (SemidirectProduct.inl n).right = 1

theorem SemidirectProduct.inl_injective {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : Function.Injective ⇑SemidirectProduct.inl

@[simp]

theorem SemidirectProduct.inl_inj {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} {n₁ n₂ : N} : SemidirectProduct.inl n₁ = SemidirectProduct.inl n₂ ↔ n₁ = n₂

def SemidirectProduct.inr {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : G →* N ⋊[φ] G

The canonical map G →* N ⋊[φ] G sending g to ⟨1, g⟩

Equations

• SemidirectProduct.inr = { toFun := fun (g : G) => { left := 1, right := g }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem SemidirectProduct.left_inr {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (g : G) : (SemidirectProduct.inr g).left = 1

@[simp]

theorem SemidirectProduct.right_inr {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (g : G) : (SemidirectProduct.inr g).right = g

theorem SemidirectProduct.inr_injective {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : Function.Injective ⇑SemidirectProduct.inr

@[simp]

theorem SemidirectProduct.inr_inj {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} {g₁ g₂ : G} : SemidirectProduct.inr g₁ = SemidirectProduct.inr g₂ ↔ g₁ = g₂

theorem SemidirectProduct.inl_aut {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (g : G) (n : N) : SemidirectProduct.inl ((φ g) n) = SemidirectProduct.inr g * SemidirectProduct.inl n * SemidirectProduct.inr g⁻¹

theorem SemidirectProduct.inl_aut_inv {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (g : G) (n : N) : SemidirectProduct.inl ((φ g)⁻¹ n) = SemidirectProduct.inr g⁻¹ * SemidirectProduct.inl n * SemidirectProduct.inr g

@[simp]

theorem SemidirectProduct.mk_eq_inl_mul_inr {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (g : G) (n : N) : { left := n, right := g } = SemidirectProduct.inl n * SemidirectProduct.inr g

@[simp]

theorem SemidirectProduct.inl_left_mul_inr_right {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (x : N ⋊[φ] G) : SemidirectProduct.inl x.left * SemidirectProduct.inr x.right = x

def SemidirectProduct.rightHom {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : N ⋊[φ] G →* G

The canonical projection map N ⋊[φ] G →* G, as a group hom.

Equations

• SemidirectProduct.rightHom = { toFun := SemidirectProduct.right, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem SemidirectProduct.rightHom_eq_right {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : ⇑SemidirectProduct.rightHom = SemidirectProduct.right

@[simp]

theorem SemidirectProduct.rightHom_comp_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : SemidirectProduct.rightHom.comp SemidirectProduct.inl = 1

@[simp]

theorem SemidirectProduct.rightHom_comp_inr {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : SemidirectProduct.rightHom.comp SemidirectProduct.inr = MonoidHom.id G

@[simp]

theorem SemidirectProduct.rightHom_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (n : N) : SemidirectProduct.rightHom (SemidirectProduct.inl n) = 1

@[simp]

theorem SemidirectProduct.rightHom_inr {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (g : G) : SemidirectProduct.rightHom (SemidirectProduct.inr g) = g

theorem SemidirectProduct.rightHom_surjective {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : Function.Surjective ⇑SemidirectProduct.rightHom

theorem SemidirectProduct.range_inl_eq_ker_rightHom {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : SemidirectProduct.inl.range = SemidirectProduct.rightHom.ker

def SemidirectProduct.lift {N : Type u_1} {G : Type u_2} {H : Type u_3} [Group N] [Group G] [Group H] {φ : G →* MulAut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁) : N ⋊[φ] G →* H

Define a group hom N ⋊[φ] G →* H, by defining maps N →* H and G →* H

Equations

• SemidirectProduct.lift f₁ f₂ h = { toFun := fun (a : N ⋊[φ] G) => f₁ a.left * f₂ a.right, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem SemidirectProduct.lift_inl {N : Type u_1} {G : Type u_2} {H : Type u_3} [Group N] [Group G] [Group H] {φ : G →* MulAut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁) (n : N) : (SemidirectProduct.lift f₁ f₂ h) (SemidirectProduct.inl n) = f₁ n

@[simp]

theorem SemidirectProduct.lift_comp_inl {N : Type u_1} {G : Type u_2} {H : Type u_3} [Group N] [Group G] [Group H] {φ : G →* MulAut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁) : (SemidirectProduct.lift f₁ f₂ h).comp SemidirectProduct.inl = f₁

@[simp]

theorem SemidirectProduct.lift_inr {N : Type u_1} {G : Type u_2} {H : Type u_3} [Group N] [Group G] [Group H] {φ : G →* MulAut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁) (g : G) : (SemidirectProduct.lift f₁ f₂ h) (SemidirectProduct.inr g) = f₂ g

@[simp]

theorem SemidirectProduct.lift_comp_inr {N : Type u_1} {G : Type u_2} {H : Type u_3} [Group N] [Group G] [Group H] {φ : G →* MulAut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁) : (SemidirectProduct.lift f₁ f₂ h).comp SemidirectProduct.inr = f₂

theorem SemidirectProduct.lift_unique {N : Type u_1} {G : Type u_2} {H : Type u_3} [Group N] [Group G] [Group H] {φ : G →* MulAut N} (F : N ⋊[φ] G →* H) : F = SemidirectProduct.lift (F.comp SemidirectProduct.inl) (F.comp SemidirectProduct.inr) ⋯

theorem SemidirectProduct.hom_ext {N : Type u_1} {G : Type u_2} {H : Type u_3} [Group N] [Group G] [Group H] {φ : G →* MulAut N} {f g : N ⋊[φ] G →* H} (hl : f.comp SemidirectProduct.inl = g.comp SemidirectProduct.inl) (hr : f.comp SemidirectProduct.inr = g.comp SemidirectProduct.inr) : f = g

Two maps out of the semidirect product are equal if they're equal after composition with both inl and inr

def SemidirectProduct.map {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} {N₁ : Type u_4} {G₁ : Type u_5} [Group N₁] [Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁) : N ⋊[φ] G →* N₁ ⋊[φ₁] G₁

Define a map from N ⋊[φ] G to N₁ ⋊[φ₁] G₁ given maps N →* N₁ and G →* G₁ that satisfy a commutativity condition ∀ n g, f₁ (φ g n) = φ₁ (f₂ g) (f₁ n).

Equations

• SemidirectProduct.map f₁ f₂ h = { toFun := fun (x : N ⋊[φ] G) => { left := f₁ x.left, right := f₂ x.right }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem SemidirectProduct.map_left {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} {N₁ : Type u_4} {G₁ : Type u_5} [Group N₁] [Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁) (g : N ⋊[φ] G) : ((SemidirectProduct.map f₁ f₂ h) g).left = f₁ g.left

@[simp]

theorem SemidirectProduct.map_right {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} {N₁ : Type u_4} {G₁ : Type u_5} [Group N₁] [Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁) (g : N ⋊[φ] G) : ((SemidirectProduct.map f₁ f₂ h) g).right = f₂ g.right

@[simp]

theorem SemidirectProduct.rightHom_comp_map {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} {N₁ : Type u_4} {G₁ : Type u_5} [Group N₁] [Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁) : SemidirectProduct.rightHom.comp (SemidirectProduct.map f₁ f₂ h) = f₂.comp SemidirectProduct.rightHom

@[simp]

theorem SemidirectProduct.map_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} {N₁ : Type u_4} {G₁ : Type u_5} [Group N₁] [Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁) (n : N) : (SemidirectProduct.map f₁ f₂ h) (SemidirectProduct.inl n) = SemidirectProduct.inl (f₁ n)

@[simp]

theorem SemidirectProduct.map_comp_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} {N₁ : Type u_4} {G₁ : Type u_5} [Group N₁] [Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁) : (SemidirectProduct.map f₁ f₂ h).comp SemidirectProduct.inl = SemidirectProduct.inl.comp f₁

@[simp]

theorem SemidirectProduct.map_inr {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} {N₁ : Type u_4} {G₁ : Type u_5} [Group N₁] [Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁) (g : G) : (SemidirectProduct.map f₁ f₂ h) (SemidirectProduct.inr g) = SemidirectProduct.inr (f₂ g)

@[simp]

theorem SemidirectProduct.map_comp_inr {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} {N₁ : Type u_4} {G₁ : Type u_5} [Group N₁] [Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁) : (SemidirectProduct.map f₁ f₂ h).comp SemidirectProduct.inr = SemidirectProduct.inr.comp f₂