Push an endomorphism accross a surjective homomorphism

Stream: Is there code for X?

[Daniel Weber]

I have a surjective homomorphism f : R →+ R2, and an endomorphism g : R →+ R which is closed on f's kernel. I want to lift g to a R2 →+ R2, by f ∘ g ∘ f^-1. Is there a way to do that in Mathlib?
mwe:

import Mathlib

variable (R : Type*) [AddCommGroup R] (R2 : Type*) [AddCommGroup R2]

example (g : R →+ R) (f : R →+ R2) (h1 : Function.Surjective f)
    (h2 : ∀ x ∈ (AddMonoidHom.ker f), g x ∈ (AddMonoidHom.ker f)) : R2 →+ R2 :=
  sorry

[Kevin Buzzard]

Here are the ingredients (note that the quotient group symbol ⧸ isn't /, it's \/ in VS Code):

import Mathlib.Tactic

variable (R : Type*) [AddCommGroup R] (R2 : Type*) [AddCommGroup R2]
  (S : Type*) [AddCommGroup S]

open Function

-- descent of an additive group hom
example (f : R →+ R2) (gtilde : R →+ S) (h : f.ker ≤ gtilde.ker) :
  R ⧸ f.ker →+ S := QuotientAddGroup.lift f.ker gtilde h

-- diagram commutes
example (f : R →+ R2) (gtilde : R →+ S) (h : f.ker ≤ gtilde.ker) (r : R) :
  QuotientAddGroup.lift f.ker gtilde h (QuotientAddGroup.mk r) = gtilde r := rfl -- (!)

-- relationship between quotient group and surjective hom
noncomputable example (f : R →+ R2) (hf : Surjective f) : R ⧸ f.ker ≃+ R2 :=
  QuotientAddGroup.quotientKerEquivOfSurjective f hf

-- diagram commutes
example (f : R →+ R2) (hf : Surjective f) (r : R) :
  QuotientAddGroup.quotientKerEquivOfSurjective f hf (QuotientAddGroup.mk r) = f r := rfl

[Eric Wieser]

Is this docs#AddMonoidHom.liftOfSurjective ?

[Kevin Buzzard]

Plus a little bit more, yes.