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
φ 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
@[ext]
- 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₂⟩
@[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)
@[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} :
@[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₂
@[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} :
@[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) :
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) :
@[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.right_hom_eq_right
{N : Type u_1}
{G : Type u_2}
[group N]
[group G]
{φ : G →* mul_aut N} :
@[simp]
theorem
semidirect_product.right_hom_comp_inl
{N : Type u_1}
{G : Type u_2}
[group N]
[group G]
{φ : G →* mul_aut N} :
@[simp]
theorem
semidirect_product.right_hom_comp_inr
{N : Type u_1}
{G : Type u_2}
[group N]
[group G]
{φ : G →* mul_aut N} :
@[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) :
@[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) :
theorem
semidirect_product.right_hom_surjective
{N : Type u_1}
{G : Type u_2}
[group N]
[group G]
{φ : G →* mul_aut N} :
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} :
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) :
(∀ (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
@[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₂
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₁) :
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).
@[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) :
@[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) :
@[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₁) :
@[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₁) :
@[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₁) :