mathlib3 documentation

group_theory.semidirect_product

Semidirect product #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 semidirect_product N G φ

Tags #

group, semidirect product

theorem semidirect_product.ext {N : Type u_1} {G : Type u_2} {_inst_1 : group N} {_inst_2 : group G} {φ : G →* mul_aut N} (x y : N ⋊[φ] G) (h : x.left = y.left) (h_1 : x.right = y.right) :

x = y

@[ext]

structure semidirect_product (N : Type u_1) (G : Type u_2) [group N] [group G] (φ : G →* mul_aut N) :

Type (max u_1 u_2)

left : N
right : G

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₂⟩

Instances for semidirect_product

semidirect_product.has_sizeof_inst
semidirect_product.group
semidirect_product.inhabited

@[protected, instance]

def semidirect_product.decidable_eq (N : Type u_1) [a : decidable_eq N] (G : Type u_2) [a_1 : decidable_eq G] [group N] [group G] (φ : G →* mul_aut N) :

decidable_eq (N ⋊[φ] G)

theorem semidirect_product.ext_iff {N : Type u_1} {G : Type u_2} {_inst_1 : group N} {_inst_2 : group G} {φ : G →* mul_aut N} (x y : N ⋊[φ] G) :

x = y ↔ x.left = y.left ∧ x.right = y.right

@[protected, instance]

def semidirect_product.group {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

group (N ⋊[φ] G)

Equations

semidirect_product.group = {mul := λ (a b : N ⋊[φ] G), ⟨a.left * ⇑(⇑φ a.right) b.left, a.right * b.right⟩, mul_assoc := _, one := ⟨1, 1⟩, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default ⟨1, 1⟩ (λ (a b : N ⋊[φ] G), ⟨a.left * ⇑(⇑φ a.right) b.left, a.right * b.right⟩) semidirect_product.group._proof_4 semidirect_product.group._proof_5, npow_zero' := _, npow_succ' := _, inv := λ (x : N ⋊[φ] G), ⟨⇑(⇑φ (x.right)⁻¹) (x.left)⁻¹, (x.right)⁻¹⟩, div := div_inv_monoid.div._default (λ (a b : N ⋊[φ] G), ⟨a.left * ⇑(⇑φ a.right) b.left, a.right * b.right⟩) semidirect_product.group._proof_8 ⟨1, 1⟩ semidirect_product.group._proof_9 semidirect_product.group._proof_10 (div_inv_monoid.npow._default ⟨1, 1⟩ (λ (a b : N ⋊[φ] G), ⟨a.left * ⇑(⇑φ a.right) b.left, a.right * b.right⟩) semidirect_product.group._proof_4 semidirect_product.group._proof_5) semidirect_product.group._proof_11 semidirect_product.group._proof_12 (λ (x : N ⋊[φ] G), ⟨⇑(⇑φ (x.right)⁻¹) (x.left)⁻¹, (x.right)⁻¹⟩), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (a b : N ⋊[φ] G), ⟨a.left * ⇑(⇑φ a.right) b.left, a.right * b.right⟩) semidirect_product.group._proof_14 ⟨1, 1⟩ semidirect_product.group._proof_15 semidirect_product.group._proof_16 (div_inv_monoid.npow._default ⟨1, 1⟩ (λ (a b : N ⋊[φ] G), ⟨a.left * ⇑(⇑φ a.right) b.left, a.right * b.right⟩) semidirect_product.group._proof_4 semidirect_product.group._proof_5) semidirect_product.group._proof_17 semidirect_product.group._proof_18 (λ (x : N ⋊[φ] G), ⟨⇑(⇑φ (x.right)⁻¹) (x.left)⁻¹, (x.right)⁻¹⟩), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}

@[protected, instance]

def semidirect_product.inhabited {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

inhabited (N ⋊[φ] G)

Equations

semidirect_product.inhabited = {default := 1}

@[simp]

theorem semidirect_product.one_left {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

1.left = 1

@[simp]

theorem semidirect_product.one_right {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

@[simp]

theorem semidirect_product.inv_left {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (a : N ⋊[φ] G) :

a⁻¹.left = ⇑(⇑φ (a.right)⁻¹) (a.left)⁻¹

@[simp]

theorem semidirect_product.inv_right {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (a : N ⋊[φ] G) :

a⁻¹.right = (a.right)⁻¹

@[simp]

theorem semidirect_product.mul_left {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (a b : N ⋊[φ] G) :

(a * b).left = a.left * ⇑(⇑φ a.right) b.left

@[simp]

theorem semidirect_product.mul_right {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (a b : N ⋊[φ] G) :

(a * b).right = a.right * b.right

def semidirect_product.inl {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

N →* N ⋊[φ] G

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

Equations

semidirect_product.inl = {to_fun := λ (n : N), ⟨n, 1⟩, map_one' := _, map_mul' := _}

@[simp]

theorem semidirect_product.left_inl {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (n : N) :

(⇑semidirect_product.inl n).left = n

@[simp]

theorem semidirect_product.right_inl {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (n : N) :

(⇑semidirect_product.inl n).right = 1

theorem semidirect_product.inl_injective {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

function.injective ⇑semidirect_product.inl

@[simp]

theorem semidirect_product.inl_inj {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} {n₁ n₂ : N} :

⇑semidirect_product.inl n₁ = ⇑semidirect_product.inl n₂ ↔ n₁ = n₂

def semidirect_product.inr {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

G →* N ⋊[φ] G

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

Equations

semidirect_product.inr = {to_fun := λ (g : G), ⟨1, g⟩, map_one' := _, map_mul' := _}

@[simp]

theorem semidirect_product.left_inr {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (g : G) :

(⇑semidirect_product.inr g).left = 1

@[simp]

theorem semidirect_product.right_inr {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (g : G) :

(⇑semidirect_product.inr g).right = g

theorem semidirect_product.inr_injective {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

function.injective ⇑semidirect_product.inr

@[simp]

theorem semidirect_product.inr_inj {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} {g₁ g₂ : G} :

⇑semidirect_product.inr g₁ = ⇑semidirect_product.inr g₂ ↔ g₁ = g₂

theorem semidirect_product.inl_aut {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (g : G) (n : N) :

⇑semidirect_product.inl (⇑(⇑φ g) n) = ⇑semidirect_product.inr g * ⇑semidirect_product.inl n * ⇑semidirect_product.inr g⁻¹

theorem semidirect_product.inl_aut_inv {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (g : G) (n : N) :

⇑semidirect_product.inl (⇑(⇑φ g)⁻¹ n) = ⇑semidirect_product.inr g⁻¹ * ⇑semidirect_product.inl n * ⇑semidirect_product.inr g

@[simp]

theorem semidirect_product.mk_eq_inl_mul_inr {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (g : G) (n : N) :

⟨n, g⟩ = ⇑semidirect_product.inl n * ⇑semidirect_product.inr g

@[simp]

theorem semidirect_product.inl_left_mul_inr_right {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (x : N ⋊[φ] G) :

⇑semidirect_product.inl x.left * ⇑semidirect_product.inr x.right = x

def semidirect_product.right_hom {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

N ⋊[φ] G →* G

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

Equations

semidirect_product.right_hom = {to_fun := semidirect_product.right φ, map_one' := _, map_mul' := _}

@[simp]

theorem semidirect_product.right_hom_eq_right {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

⇑semidirect_product.right_hom = semidirect_product.right

@[simp]

theorem semidirect_product.right_hom_comp_inl {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

semidirect_product.right_hom.comp semidirect_product.inl = 1

@[simp]

theorem semidirect_product.right_hom_comp_inr {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

semidirect_product.right_hom.comp semidirect_product.inr = monoid_hom.id G

@[simp]

theorem semidirect_product.right_hom_inl {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (n : N) :

⇑semidirect_product.right_hom (⇑semidirect_product.inl n) = 1

@[simp]

theorem semidirect_product.right_hom_inr {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} (g : G) :

⇑semidirect_product.right_hom (⇑semidirect_product.inr g) = g

theorem semidirect_product.right_hom_surjective {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

function.surjective ⇑semidirect_product.right_hom

theorem semidirect_product.range_inl_eq_ker_right_hom {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} :

semidirect_product.inl.range = semidirect_product.right_hom.ker

def semidirect_product.lift {N : Type u_1} {G : Type u_2} {H : Type u_3} [group N] [group G] [group H] {φ : G →* mul_aut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑mul_aut.conj (⇑f₂ g))).comp f₁) :

N ⋊[φ] G →* H

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

Equations

semidirect_product.lift f₁ f₂ h = {to_fun := λ (a : N ⋊[φ] G), ⇑f₁ a.left * ⇑f₂ a.right, map_one' := _, map_mul' := _}

@[simp]

theorem semidirect_product.lift_inl {N : Type u_1} {G : Type u_2} {H : Type u_3} [group N] [group G] [group H] {φ : G →* mul_aut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑mul_aut.conj (⇑f₂ g))).comp f₁) (n : N) :

⇑(semidirect_product.lift f₁ f₂ h) (⇑semidirect_product.inl n) = ⇑f₁ n

@[simp]

theorem semidirect_product.lift_comp_inl {N : Type u_1} {G : Type u_2} {H : Type u_3} [group N] [group G] [group H] {φ : G →* mul_aut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑mul_aut.conj (⇑f₂ g))).comp f₁) :

(semidirect_product.lift f₁ f₂ h).comp semidirect_product.inl = f₁

@[simp]

theorem semidirect_product.lift_inr {N : Type u_1} {G : Type u_2} {H : Type u_3} [group N] [group G] [group H] {φ : G →* mul_aut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑mul_aut.conj (⇑f₂ g))).comp f₁) (g : G) :

⇑(semidirect_product.lift f₁ f₂ h) (⇑semidirect_product.inr g) = ⇑f₂ g

@[simp]

theorem semidirect_product.lift_comp_inr {N : Type u_1} {G : Type u_2} {H : Type u_3} [group N] [group G] [group H] {φ : G →* mul_aut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑mul_aut.conj (⇑f₂ g))).comp f₁) :

(semidirect_product.lift f₁ f₂ h).comp semidirect_product.inr = f₂

theorem semidirect_product.lift_unique {N : Type u_1} {G : Type u_2} {H : Type u_3} [group N] [group G] [group H] {φ : G →* mul_aut N} (F : N ⋊[φ] G →* H) :

F = semidirect_product.lift (F.comp semidirect_product.inl) (F.comp semidirect_product.inr) _

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

f = g

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

def semidirect_product.map {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} {N₁ : Type u_4} {G₁ : Type u_5} [group N₁] [group G₁] {φ₁ : G₁ →* mul_aut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑φ₁ (⇑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

semidirect_product.map f₁ f₂ h = {to_fun := λ (x : N ⋊[φ] G), ⟨⇑f₁ x.left, ⇑f₂ x.right⟩, map_one' := _, map_mul' := _}

@[simp]

theorem semidirect_product.map_left {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} {N₁ : Type u_4} {G₁ : Type u_5} [group N₁] [group G₁] {φ₁ : G₁ →* mul_aut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑φ₁ (⇑f₂ g))).comp f₁) (g : N ⋊[φ] G) :

(⇑(semidirect_product.map f₁ f₂ h) g).left = ⇑f₁ g.left

@[simp]

theorem semidirect_product.map_right {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} {N₁ : Type u_4} {G₁ : Type u_5} [group N₁] [group G₁] {φ₁ : G₁ →* mul_aut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑φ₁ (⇑f₂ g))).comp f₁) (g : N ⋊[φ] G) :

(⇑(semidirect_product.map f₁ f₂ h) g).right = ⇑f₂ g.right

@[simp]

theorem semidirect_product.right_hom_comp_map {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} {N₁ : Type u_4} {G₁ : Type u_5} [group N₁] [group G₁] {φ₁ : G₁ →* mul_aut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑φ₁ (⇑f₂ g))).comp f₁) :

semidirect_product.right_hom.comp (semidirect_product.map f₁ f₂ h) = f₂.comp semidirect_product.right_hom

@[simp]

theorem semidirect_product.map_inl {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} {N₁ : Type u_4} {G₁ : Type u_5} [group N₁] [group G₁] {φ₁ : G₁ →* mul_aut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑φ₁ (⇑f₂ g))).comp f₁) (n : N) :

⇑(semidirect_product.map f₁ f₂ h) (⇑semidirect_product.inl n) = ⇑semidirect_product.inl (⇑f₁ n)

@[simp]

theorem semidirect_product.map_comp_inl {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} {N₁ : Type u_4} {G₁ : Type u_5} [group N₁] [group G₁] {φ₁ : G₁ →* mul_aut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑φ₁ (⇑f₂ g))).comp f₁) :

(semidirect_product.map f₁ f₂ h).comp semidirect_product.inl = semidirect_product.inl.comp f₁

@[simp]

theorem semidirect_product.map_inr {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} {N₁ : Type u_4} {G₁ : Type u_5} [group N₁] [group G₁] {φ₁ : G₁ →* mul_aut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑φ₁ (⇑f₂ g))).comp f₁) (g : G) :

⇑(semidirect_product.map f₁ f₂ h) (⇑semidirect_product.inr g) = ⇑semidirect_product.inr (⇑f₂ g)

@[simp]

theorem semidirect_product.map_comp_inr {N : Type u_1} {G : Type u_2} [group N] [group G] {φ : G →* mul_aut N} {N₁ : Type u_4} {G₁ : Type u_5} [group N₁] [group G₁] {φ₁ : G₁ →* mul_aut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), f₁.comp (mul_equiv.to_monoid_hom (⇑φ g)) = (mul_equiv.to_monoid_hom (⇑φ₁ (⇑f₂ g))).comp f₁) :

(semidirect_product.map f₁ f₂ h).comp semidirect_product.inr = semidirect_product.inr.comp f₂