Theorems · Definition · group theory

QuotientGroup.liftEquiv

{G : Type u_1} →
  {H : Type u_2} →
    [inst : Group G] →
      [inst_1 : Group H] →
        (N : Subgroup G) → [nN : N.Normal] → {φ : G →* H} → Function.Surjective ⇑φ → N = φ.ker → G ⧸ N ≃* H

A surjective group homomorphism φ : G →* H with N = ker(φ) descends (i.e. lifts) to a group isomorphism G/N ≃* H.

Defined in

Mathlib.GroupTheory.QuotientGroup.Defs

Cited by

2 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroupSubgroup.Normal