Documentation

Mathlib.GroupTheory.SemidirectProduct

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

Tags #

group, semidirect product

source
ink
theorem SemidirectProduct.ext {N : Type u_1} {G : Type u_2} :
∀ {inst : Group N} {inst_1 : Group G} {φ : G →* MulAut N} (x y : N ⋊[φ] G), x.left = y.left → x.right = y.right → x = y
source
ink
theorem SemidirectProduct.ext_iff {N : Type u_1} {G : Type u_2} :
∀ {inst : Group N} {inst_1 : Group G} {φ : G →* MulAut N} (x y : N ⋊[φ] G), x = y ↔ x.left = y.left ∧ x.right = y.right
source
ink
structure SemidirectProduct (N : Type u_1) (G : Type u_2) [inst : Group N] [inst : Group G] (φ : G →* MulAut N) :
Type (maxu_1u_2)

  • The element of N

    left : N

  • The element of G

    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
    source
    ink
    instance instDecidableEqSemidirectProduct :
    {N : Type u_1} → {G : Type u_2} → {inst : Group N} → {inst_1 : Group G} → {φ : G →* MulAut N} → [inst_2 : DecidableEq N] → [inst_3 : DecidableEq G] → DecidableEq (N ⋊[φ] G)
    Equations
    • instDecidableEqSemidirectProduct = decEqSemidirectProduct✝
    source
    ink
    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.
    source
    ink
    instance SemidirectProduct.instMulSemidirectProduct {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    Mul (N ⋊[φ] G)
    Equations
    • SemidirectProduct.instMulSemidirectProduct = { mul := fun a b => { left := a.left * ↑(↑φ a.right) b.left, right := a.right * b.right } }
    source
    ink
    theorem SemidirectProduct.mul_def {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (a : N ⋊[φ] G) (b : N ⋊[φ] G) :
    a * b = { left := a.left * ↑(↑φ a.right) b.left, right := a.right * b.right }
    source
    ink
    @[simp]
    theorem SemidirectProduct.mul_left {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (a : N ⋊[φ] G) (b : N ⋊[φ] G) :
    (a * b).left = a.left * ↑(↑φ a.right) b.left
    source
    ink
    @[simp]
    theorem SemidirectProduct.mul_right {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (a : N ⋊[φ] G) (b : N ⋊[φ] G) :
    (a * b).right = a.right * b.right
    source
    ink
    instance SemidirectProduct.instOneSemidirectProduct {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    One (N ⋊[φ] G)
    Equations
    • SemidirectProduct.instOneSemidirectProduct = { one := { left := 1, right := 1 } }
    source
    ink
    @[simp]
    theorem SemidirectProduct.one_left {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    1.left = 1
    source
    ink
    @[simp]
    theorem SemidirectProduct.one_right {N : Type u_2} {G : Type u_1} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    1.right = 1
    source
    ink
    instance SemidirectProduct.instInvSemidirectProduct {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    Inv (N ⋊[φ] G)
    Equations
    • SemidirectProduct.instInvSemidirectProduct = { inv := fun x => { left := ↑(↑φ x.right⁻¹) x.left⁻¹, right := x.right⁻¹ } }
    source
    ink
    @[simp]
    theorem SemidirectProduct.inv_left {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (a : N ⋊[φ] G) :
    a⁻¹.left = ↑(↑φ a.right⁻¹) a.left⁻¹
    source
    ink
    @[simp]
    theorem SemidirectProduct.inv_right {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (a : N ⋊[φ] G) :
    a⁻¹.right = a.right⁻¹
    source
    ink
    instance SemidirectProduct.instGroupSemidirectProduct {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    Group (N ⋊[φ] G)
    Equations
    source
    ink
    instance SemidirectProduct.instInhabitedSemidirectProduct {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    Inhabited (N ⋊[φ] G)
    Equations
    • SemidirectProduct.instInhabitedSemidirectProduct = { default := 1 }
    source
    ink
    def SemidirectProduct.inl {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    N →* N ⋊[φ] G

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

    Equations
    • One or more equations did not get rendered due to their size.
    source
    ink
    @[simp]
    theorem SemidirectProduct.left_inl {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (n : N) :
    (↑SemidirectProduct.inl n).left = n
    source
    ink
    @[simp]
    theorem SemidirectProduct.right_inl {N : Type u_2} {G : Type u_1} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (n : N) :
    (↑SemidirectProduct.inl n).right = 1
    source
    ink
    theorem SemidirectProduct.inl_injective {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    Function.Injective ↑SemidirectProduct.inl
    source
    ink
    @[simp]
    theorem SemidirectProduct.inl_inj {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} {n₁ : N} {n₂ : N} :
    ↑SemidirectProduct.inl n₁ = ↑SemidirectProduct.inl n₂ ↔ n₁ = n₂
    source
    ink
    def SemidirectProduct.inr {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    G →* N ⋊[φ] G

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

    Equations
    • One or more equations did not get rendered due to their size.
    source
    ink
    @[simp]
    theorem SemidirectProduct.left_inr {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (g : G) :
    (↑SemidirectProduct.inr g).left = 1
    source
    ink
    @[simp]
    theorem SemidirectProduct.right_inr {N : Type u_2} {G : Type u_1} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (g : G) :
    (↑SemidirectProduct.inr g).right = g
    source
    ink
    theorem SemidirectProduct.inr_injective {N : Type u_2} {G : Type u_1} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    Function.Injective ↑SemidirectProduct.inr
    source
    ink
    @[simp]
    theorem SemidirectProduct.inr_inj {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} {g₁ : G} {g₂ : G} :
    ↑SemidirectProduct.inr g₁ = ↑SemidirectProduct.inr g₂ ↔ g₁ = g₂
    source
    ink
    theorem SemidirectProduct.inl_aut {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (g : G) (n : N) :
    ↑SemidirectProduct.inl (↑(↑φ g) n) = ↑SemidirectProduct.inr g * ↑SemidirectProduct.inl n * ↑SemidirectProduct.inr g⁻¹
    source
    ink
    theorem SemidirectProduct.inl_aut_inv {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (g : G) (n : N) :
    ↑SemidirectProduct.inl (↑(↑φ g)⁻¹ n) = ↑SemidirectProduct.inr g⁻¹ * ↑SemidirectProduct.inl n * ↑SemidirectProduct.inr g
    source
    ink
    @[simp]
    theorem SemidirectProduct.mk_eq_inl_mul_inr {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (g : G) (n : N) :
    { left := n, right := g } = ↑SemidirectProduct.inl n * ↑SemidirectProduct.inr g
    source
    ink
    @[simp]
    theorem SemidirectProduct.inl_left_mul_inr_right {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (x : N ⋊[φ] G) :
    ↑SemidirectProduct.inl x.left * ↑SemidirectProduct.inr x.right = x
    source
    ink
    def SemidirectProduct.rightHom {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    N ⋊[φ] G →* G

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

    Equations
    • One or more equations did not get rendered due to their size.
    source
    ink
    @[simp]
    theorem SemidirectProduct.rightHom_eq_right {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    ↑SemidirectProduct.rightHom = SemidirectProduct.right
    source
    ink
    @[simp]
    theorem SemidirectProduct.rightHom_comp_inl {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    MonoidHom.comp SemidirectProduct.rightHom SemidirectProduct.inl = 1
    source
    ink
    @[simp]
    theorem SemidirectProduct.rightHom_comp_inr {N : Type u_2} {G : Type u_1} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    MonoidHom.comp SemidirectProduct.rightHom SemidirectProduct.inr = MonoidHom.id G
    source
    ink
    @[simp]
    theorem SemidirectProduct.rightHom_inl {N : Type u_2} {G : Type u_1} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (n : N) :
    ↑SemidirectProduct.rightHom (↑SemidirectProduct.inl n) = 1
    source
    ink
    @[simp]
    theorem SemidirectProduct.rightHom_inr {N : Type u_2} {G : Type u_1} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} (g : G) :
    ↑SemidirectProduct.rightHom (↑SemidirectProduct.inr g) = g
    source
    ink
    theorem SemidirectProduct.rightHom_surjective {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    Function.Surjective ↑SemidirectProduct.rightHom
    source
    ink
    theorem SemidirectProduct.range_inl_eq_ker_rightHom {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} :
    MonoidHom.range SemidirectProduct.inl = MonoidHom.ker SemidirectProduct.rightHom
    source
    ink
    def SemidirectProduct.lift {N : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group N] [inst : Group G] [inst : Group H] {φ : G →* MulAut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁) :
    N ⋊[φ] G →* H

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

    Equations
    • One or more equations did not get rendered due to their size.
    source
    ink
    @[simp]
    theorem SemidirectProduct.lift_inl {N : Type u_2} {G : Type u_3} {H : Type u_1} [inst : Group N] [inst : Group G] [inst : Group H] {φ : G →* MulAut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁) (n : N) :
    ↑(SemidirectProduct.lift f₁ f₂ h) (↑SemidirectProduct.inl n) = ↑f₁ n
    source
    ink
    @[simp]
    theorem SemidirectProduct.lift_comp_inl {N : Type u_1} {G : Type u_3} {H : Type u_2} [inst : Group N] [inst : Group G] [inst : Group H] {φ : G →* MulAut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁) :
    MonoidHom.comp (SemidirectProduct.lift f₁ f₂ h) SemidirectProduct.inl = f₁
    source
    ink
    @[simp]
    theorem SemidirectProduct.lift_inr {N : Type u_2} {G : Type u_3} {H : Type u_1} [inst : Group N] [inst : Group G] [inst : Group H] {φ : G →* MulAut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁) (g : G) :
    ↑(SemidirectProduct.lift f₁ f₂ h) (↑SemidirectProduct.inr g) = ↑f₂ g
    source
    ink
    @[simp]
    theorem SemidirectProduct.lift_comp_inr {N : Type u_3} {G : Type u_1} {H : Type u_2} [inst : Group N] [inst : Group G] [inst : Group H] {φ : G →* MulAut N} (f₁ : N →* H) (f₂ : G →* H) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁) :
    MonoidHom.comp (SemidirectProduct.lift f₁ f₂ h) SemidirectProduct.inr = f₂
    source
    ink
    theorem SemidirectProduct.lift_unique {N : Type u_2} {G : Type u_1} {H : Type u_3} [inst : Group N] [inst : Group G] [inst : Group H] {φ : G →* MulAut N} (F : N ⋊[φ] G →* H) :
    F = SemidirectProduct.lift (MonoidHom.comp F SemidirectProduct.inl) (MonoidHom.comp F SemidirectProduct.inr) (_ : ∀ (x : G), MonoidHom.comp (MonoidHom.comp F SemidirectProduct.inl) (MulEquiv.toMonoidHom (↑φ x)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F SemidirectProduct.inr) x))) (MonoidHom.comp F SemidirectProduct.inl))
    source
    ink
    theorem SemidirectProduct.hom_ext {N : Type u_2} {G : Type u_1} {H : Type u_3} [inst : Group N] [inst : Group G] [inst : Group H] {φ : G →* MulAut N} {f : N ⋊[φ] G →* H} {g : N ⋊[φ] G →* H} (hl : MonoidHom.comp f SemidirectProduct.inl = MonoidHom.comp g SemidirectProduct.inl) (hr : MonoidHom.comp f SemidirectProduct.inr = MonoidHom.comp g SemidirectProduct.inr) :
    f = g

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

    source
    ink
    def SemidirectProduct.map {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} {N₁ : Type u_3} {G₁ : Type u_4} [inst : Group N₁] [inst : Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) 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
    • One or more equations did not get rendered due to their size.
    source
    ink
    @[simp]
    theorem SemidirectProduct.map_left {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} {N₁ : Type u_3} {G₁ : Type u_4} [inst : Group N₁] [inst : Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁) (g : N ⋊[φ] G) :
    (↑(SemidirectProduct.map f₁ f₂ h) g).left = ↑f₁ g.left
    source
    ink
    @[simp]
    theorem SemidirectProduct.map_right {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} {N₁ : Type u_4} {G₁ : Type u_3} [inst : Group N₁] [inst : Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁) (g : N ⋊[φ] G) :
    (↑(SemidirectProduct.map f₁ f₂ h) g).right = ↑f₂ g.right
    source
    ink
    @[simp]
    theorem SemidirectProduct.rightHom_comp_map {N : Type u_1} {G : Type u_2} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} {N₁ : Type u_4} {G₁ : Type u_3} [inst : Group N₁] [inst : Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁) :
    MonoidHom.comp SemidirectProduct.rightHom (SemidirectProduct.map f₁ f₂ h) = MonoidHom.comp f₂ SemidirectProduct.rightHom
    source
    ink
    @[simp]
    theorem SemidirectProduct.map_inl {N : Type u_3} {G : Type u_4} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} {N₁ : Type u_1} {G₁ : Type u_2} [inst : Group N₁] [inst : Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁) (n : N) :
    ↑(SemidirectProduct.map f₁ f₂ h) (↑SemidirectProduct.inl n) = ↑SemidirectProduct.inl (↑f₁ n)
    source
    ink
    @[simp]
    theorem SemidirectProduct.map_comp_inl {N : Type u_1} {G : Type u_4} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} {N₁ : Type u_2} {G₁ : Type u_3} [inst : Group N₁] [inst : Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁) :
    MonoidHom.comp (SemidirectProduct.map f₁ f₂ h) SemidirectProduct.inl = MonoidHom.comp SemidirectProduct.inl f₁
    source
    ink
    @[simp]
    theorem SemidirectProduct.map_inr {N : Type u_3} {G : Type u_4} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} {N₁ : Type u_1} {G₁ : Type u_2} [inst : Group N₁] [inst : Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁) (g : G) :
    ↑(SemidirectProduct.map f₁ f₂ h) (↑SemidirectProduct.inr g) = ↑SemidirectProduct.inr (↑f₂ g)
    source
    ink
    @[simp]
    theorem SemidirectProduct.map_comp_inr {N : Type u_4} {G : Type u_1} [inst : Group N] [inst : Group G] {φ : G →* MulAut N} {N₁ : Type u_2} {G₁ : Type u_3} [inst : Group N₁] [inst : Group G₁] {φ₁ : G₁ →* MulAut N₁} (f₁ : N →* N₁) (f₂ : G →* G₁) (h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁) :
    MonoidHom.comp (SemidirectProduct.map f₁ f₂ h) SemidirectProduct.inr = MonoidHom.comp SemidirectProduct.inr f₂