Theorems · Definition · group theory

QuotientAddGroup.lift

{G : Type u_1} →
  {M : Type u_4} →
    [inst : AddGroup G] →
      [inst_1 : AddMonoid M] → (N : AddSubgroup G) → [nN : N.Normal] → (φ : G →+ M) → N ≤ φ.ker → G ⧸ N →+ M

An AddGroup homomorphism φ : G →+ M with N ⊆ ker(φ) descends (i.e. lifts) to an AddGroup homomorphism G/N →+ M.

Defined in

Mathlib.GroupTheory.QuotientGroup.Defs

Cited by

15 results in Mathlib

Foundations

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

Assumes

AddGroupAddMonoidAddSubgroup.Normal