Theorems · Definition · group theory

SemidirectProduct.lift

{N : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group G] →
          [inst_2 : Group H] →
            {φ : G →* MulAut N} →
              (fn : N →* H) →
                (fg : G →* 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

Defined in

Mathlib.GroupTheory.SemidirectProduct

Cited by

7 results in Mathlib

Foundations

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

Assumes

GroupGroupGroup