Theorems · Definition · group theory

AddMonoidHom.liftOfRightInverse

{G₁ : Type u_5} →
  {G₂ : Type u_6} →
    {G₃ : Type u_7} →
      [inst : AddGroup G₁] →
        [inst_1 : AddGroup G₂] →
          [inst_2 : AddGroup G₃] →
            (f : G₁ →+ G₂) → (f_neg : G₂ → G₁) → Function.RightInverse f_neg ⇑f → { g // f.ker ≤ g.ker } ≃ (G₂ →+ G₃)

liftOfRightInverse f f_inv hf g hg is the unique additive group homomorphism φ * such that φ.comp f = g (AddMonoidHom.liftOfRightInverse_comp), * where f : G₁ →+ G₂ has a RightInverse f_inv (hf), * and g : G₂ →+ G₃ satisfies hg : f.ker ≤ g.ker. See AddMonoidHom.eq_liftOfRightInverse for the uniqueness lemma. `` G₁. | \ f | \ g | \ v \⌟ G₂ -> G₃ ∃!φ ``

Defined in

Mathlib.Algebra.Group.Subgroup.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroupAddGroup