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

Instances For
    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✝

    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.
    Instances For
      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} :
      @[simp]
      theorem SemidirectProduct.one_right {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} :
      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
      instance SemidirectProduct.instInhabited {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} :
      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' := }
      Instances For
        @[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' := }
        Instances For
          @[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' := }
          Instances For
            @[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.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.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem SemidirectProduct.equivProd_apply {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (x✝ : N ⋊[φ] G) :
              SemidirectProduct.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) :
              (SemidirectProduct.equivProd.symm x✝).left = x✝.1
              @[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) :
              (SemidirectProduct.equivProd.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

              Equations
              Instances For
                @[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) :
                (SemidirectProduct.lift fn fg h) (SemidirectProduct.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) :
                (SemidirectProduct.lift fn fg h).comp SemidirectProduct.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) :
                (SemidirectProduct.lift fn fg h) (SemidirectProduct.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) :
                (SemidirectProduct.lift fn fg h).comp SemidirectProduct.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 = 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.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.

                Equations
                Instances For
                  @[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) :
                  (SemidirectProduct.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.

                  Equations
                  Instances For
                    @[simp]
                    theorem SemidirectProduct.mulEquivSubgroup_symm_apply {G : Type u_2} [Group G] {H K : Subgroup G} [H.Normal] (h : H.IsComplement' K) (b : G) :
                    @[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) :
                    (SemidirectProduct.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).

                    Equations
                    • SemidirectProduct.map fn fg h = { toFun := fun (x : N₁ ⋊[φ₁] G₁) => { left := fn x.left, right := fg x.right }, map_one' := , map_mul' := }
                    Instances For
                      @[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₁) :
                      ((SemidirectProduct.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₁) :
                      ((SemidirectProduct.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) :
                      SemidirectProduct.rightHom.comp (SemidirectProduct.map fn fg h) = fg.comp SemidirectProduct.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₁) :
                      (SemidirectProduct.map fn fg h) (SemidirectProduct.inl n) = SemidirectProduct.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) :
                      (SemidirectProduct.map fn fg h).comp SemidirectProduct.inl = SemidirectProduct.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₁) :
                      (SemidirectProduct.map fn fg h) (SemidirectProduct.inr g) = SemidirectProduct.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) :
                      (SemidirectProduct.map fn fg h).comp SemidirectProduct.inr = SemidirectProduct.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).

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[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₂) :
                        ((SemidirectProduct.congr fn fg h).symm x).right = fg.symm x.right
                        @[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₁) :
                        ((SemidirectProduct.congr fn fg h) x).right = fg x.right
                        @[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₁) :
                        ((SemidirectProduct.congr fn fg h) x).left = fn x.left
                        @[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₂) :
                        ((SemidirectProduct.congr fn fg h).symm x).left = fn.symm x.left
                        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 a isomorphism from N₁ ⋊[φ₁] G₁ to N₂ ⋊[φ₂] G₂ without specifying φ₂.

                        Equations
                        Instances For
                          @[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₁) :
                          ((SemidirectProduct.congr' fn fg) x).right = fg 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₂) :
                          ((SemidirectProduct.congr' fn fg).symm x).left = fn.symm 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₂) :
                          ((SemidirectProduct.congr' fn fg).symm x).right = fg.symm x.right
                          @[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₁) :
                          ((SemidirectProduct.congr' fn fg) x).left = fn x.left