Theorems · Definition · group theory

SemidirectProduct.congr

{N₁ : Type u_4} →
  {G₁ : Type u_5} →
    {N₂ : Type u_6} →
      {G₂ : Type u_7} →
        [inst : Group N₁] →
          [inst_1 : Group G₁] →
            [inst_2 : Group N₂] →
              [inst_3 : Group G₂] →
                {φ₁ : G₁ →* MulAut N₁} →
                  {φ₂ : G₂ →* MulAut N₂} →
                    (fn : N₁ ≃* N₂) →
                      (fg : G₁ ≃* G₂) →
                        (∀ (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).

Defined in

Mathlib.GroupTheory.SemidirectProduct

Cited by

4 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Quot.sound

Assumes

GroupGroupGroupGroup