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 fn : N →* H and fg : G →* H that satisfy the condition ∀ n g, fn (φ g n) = fg g * fn n * fg 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 is 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_iff {N : Type u_1} {G : Type u_2} {inst✝ : Group N} {inst✝¹ : Group G} {φ : G →* MulAut N} {x y : N ⋊[φ] G} : x = y ↔ x.left = y.left ∧ x.right = y.right

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✝)

def instDecidableEqSemidirectProduct.decEq {N✝ : Type u_4} {G✝ : Type u_5} {inst✝ : Group N✝} {inst✝¹ : Group G✝} {φ✝ : G✝ →* MulAut N✝} [DecidableEq N✝] [DecidableEq G✝] (x✝ x✝¹ : N✝ ⋊[φ✝] G✝) : Decidable (x✝ = x✝¹)

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

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

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

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 = ⟨a.left * (φ a.right) b.left, 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)

@[simp]

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

@[simp]

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

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

@[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)

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

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⟩

@[simp]

theorem SemidirectProduct.left_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (n : N) : (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) : (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 ⇑inl

@[simp]

theorem SemidirectProduct.inl_inj {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} {n₁ n₂ : N} : inl n₁ = 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⟩

@[simp]

theorem SemidirectProduct.left_inr {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (g : G) : (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) : (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 ⇑inr

@[simp]

theorem SemidirectProduct.inr_inj {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} {g₁ g₂ : G} : inr g₁ = 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) : inl ((φ g) n) = inr g * inl n * 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) : inl ((φ g)⁻¹ n) = inr g⁻¹ * inl n * 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) : ⟨n, g⟩ = inl n * 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) : inl x.left * 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.

@[simp]

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

@[simp]

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

@[simp]

theorem SemidirectProduct.rightHom_comp_inr {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : rightHom.comp 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) : rightHom (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) : rightHom (inr g) = g

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

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

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

The bijection between the semidirect product and the product.

@[simp]

theorem SemidirectProduct.equivProd_symm_apply_right {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (x : N × G) : (equivProd.symm x).right = x.2

@[simp]

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

@[simp]

theorem SemidirectProduct.equivProd_symm_apply_left {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (x : N × G) : (equivProd.symm x).left = x.1

def SemidirectProduct.mulEquivProd {N : Type u_1} {G : Type u_2} [Group N] [Group G] : N ⋊[1] G ≃* N × G

The group isomorphism between a semidirect product with respect to the trivial map and the product.

@[simp]

theorem SemidirectProduct.mulEquivProd_apply {N : Type u_1} {G : Type u_2} [Group N] [Group G] (x : N ⋊[1] G) : mulEquivProd x = (x.left, x.right)

@[simp]

theorem SemidirectProduct.mulEquivProd_symm_apply_left {N : Type u_1} {G : Type u_2} [Group N] [Group G] (x : N × G) : (mulEquivProd.symm x).left = x.1

@[simp]

theorem SemidirectProduct.mulEquivProd_symm_apply_right {N : Type u_1} {G : Type u_2} [Group N] [Group G] (x : N × G) : (mulEquivProd.symm x).right = x.2

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

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

@[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} (fn : N →* H) (fg : G →* H) (h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn) (n : N) : (lift fn fg h) (inl n) = fn 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} (fn : N →* H) (fg : G →* H) (h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn) : (lift fn fg h).comp inl = fn

@[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} (fn : N →* H) (fg : G →* H) (h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn) (g : G) : (lift fn fg h) (inr g) = fg 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} (fn : N →* H) (fg : G →* H) (h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn) : (lift fn fg h).comp inr = fg

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 = lift (F.comp inl) (F.comp 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 inl = g.comp inl) (hr : f.comp inr = g.comp 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.monoidHomSubgroup {G : Type u_2} [Group G] {H K : Subgroup G} (h : K ≤ H.normalizer) : ↥H ⋊[H.normalizerMonoidHom.comp (Subgroup.inclusion h)] ↥K →* G

The homomorphism from a semidirect product of subgroups to the ambient group.

@[simp]

theorem SemidirectProduct.monoidHomSubgroup_apply {G : Type u_2} [Group G] {H K : Subgroup G} (h : K ≤ H.normalizer) (a : ↥H ⋊[H.normalizerMonoidHom.comp (Subgroup.inclusion h)] ↥K) : (monoidHomSubgroup h) a = ↑a.left * ↑a.right

noncomputable def SemidirectProduct.mulEquivSubgroup {G : Type u_2} [Group G] {H K : Subgroup G} [H.Normal] (h : H.IsComplement' K) : ↥H ⋊[H.normalizerMonoidHom.comp (Subgroup.inclusion ⋯)] ↥K ≃* G

The isomorphism from a semidirect product of complementary subgroups to the ambient group.

@[simp]

theorem SemidirectProduct.mulEquivSubgroup_symm_apply {G : Type u_2} [Group G] {H K : Subgroup G} [H.Normal] (h : H.IsComplement' K) (b : G) : (mulEquivSubgroup h).symm b = Function.surjInv ⋯ b

@[simp]

theorem SemidirectProduct.mulEquivSubgroup_apply {G : Type u_2} [Group G] {H K : Subgroup G} [H.Normal] (h : H.IsComplement' K) (a : ↥H ⋊[H.normalizerMonoidHom.comp (Subgroup.inclusion ⋯)] ↥K) : (mulEquivSubgroup h) a = ↑a.left * ↑a.right

def SemidirectProduct.map {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [Group N₁] [Group G₁] [Group N₂] [Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ →* N₂) (fg : G₁ →* G₂) (h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn) : 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, fn (φ₁ g n) = φ₂ (fg g) (fn n).

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def SemidirectProduct.congr {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [Group N₁] [Group G₁] [Group N₂] [Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂) (h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))) : N₁ ⋊[φ₁] G₁ ≃* N₂ ⋊[φ₂] G₂

Define an isomorphism from N₁ ⋊[φ₁] G₁ to N₂ ⋊[φ₂] G₂ given isomorphisms N₁ ≃* N₂ and G₁ ≃* G₂ that satisfy a commutativity condition ∀ n g, fn (φ₁ g n) = φ₂ (fg g) (fn n).

@[simp]

theorem SemidirectProduct.congr_symm_apply_left {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [Group N₁] [Group G₁] [Group N₂] [Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂) (h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))) (x : N₂ ⋊[φ₂] G₂) : ((congr fn fg h).symm x).left = fn.symm x.left

@[simp]

theorem SemidirectProduct.congr_apply_left {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [Group N₁] [Group G₁] [Group N₂] [Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂) (h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))) (x : N₁ ⋊[φ₁] G₁) : ((congr fn fg h) x).left = fn x.left

@[simp]

theorem SemidirectProduct.congr_apply_right {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [Group N₁] [Group G₁] [Group N₂] [Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂) (h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))) (x : N₁ ⋊[φ₁] G₁) : ((congr fn fg h) x).right = fg x.right

@[simp]

theorem SemidirectProduct.congr_symm_apply_right {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [Group N₁] [Group G₁] [Group N₂] [Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂) (h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))) (x : N₂ ⋊[φ₂] G₂) : ((congr fn fg h).symm x).right = fg.symm x.right

def SemidirectProduct.congr' {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [Group N₁] [Group G₁] [Group N₂] [Group G₂] {φ₁ : G₁ →* MulAut N₁} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂) : N₁ ⋊[φ₁] G₁ ≃* N₂ ⋊[(↑(MulAut.congr fn)).comp (φ₁.comp ↑fg.symm)] G₂

Define an isomorphism from N₁ ⋊[φ₁] G₁ to N₂ ⋊[φ₂] G₂ without specifying φ₂.

@[simp]

theorem SemidirectProduct.congr'_apply_left {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [Group N₁] [Group G₁] [Group N₂] [Group G₂] {φ₁ : G₁ →* MulAut N₁} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂) (x : N₁ ⋊[φ₁] G₁) : ((congr' fn fg) x).left = fn x.left

@[simp]

theorem SemidirectProduct.congr'_symm_apply_right {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [Group N₁] [Group G₁] [Group N₂] [Group G₂] {φ₁ : G₁ →* MulAut N₁} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂) (x : N₂ ⋊[(↑(MulAut.congr fn)).comp (φ₁.comp ↑fg.symm)] G₂) : ((congr' fn fg).symm x).right = fg.symm x.right

@[simp]

theorem SemidirectProduct.congr'_symm_apply_left {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [Group N₁] [Group G₁] [Group N₂] [Group G₂] {φ₁ : G₁ →* MulAut N₁} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂) (x : N₂ ⋊[(↑(MulAut.congr fn)).comp (φ₁.comp ↑fg.symm)] G₂) : ((congr' fn fg).symm x).left = fn.symm x.left

@[simp]

theorem SemidirectProduct.congr'_apply_right {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [Group N₁] [Group G₁] [Group N₂] [Group G₂] {φ₁ : G₁ →* MulAut N₁} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂) (x : N₁ ⋊[φ₁] G₁) : ((congr' fn fg) x).right = fg x.right

@[simp]

theorem SemidirectProduct.card {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} : Nat.card (N ⋊[φ] G) = Nat.card N * Nat.card G