Theorems · Definition · group theory

SemidirectProduct.map

{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₁),
                            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).

Defined in

Mathlib.GroupTheory.SemidirectProduct

Cited by

8 results in Mathlib

Foundations

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

Assumes

GroupGroupGroupGroup