Group hom factors through surjection

Stream: Is there code for X?

[David Loeffler]

Suppose I have group homs f : G →* H and g : G →* J. If f is surjective, and g is trivial on ker f, then g factors through f. Is there a one-liner proof of this in mathlib?

[Eric Wieser]

docs#MonoidHom.liftOfSurjective or something nearby?

[Adam Topaz]

Not really related, but I wonder what others think of definitions formulated like this. I would much rather be able to write f.liftOfSurjective hf g <| by ... as opposed to f.liftOfSurjective hf \<g, by ...\>, just in terms of ergonomics.

[Eric Wieser]

It's useful to have these Equiv versions because it means you can rewrite by Equiv.surjective.forall or apply Equiv.injective

[Eric Wieser]

maybe we should have a different name for the equiv version; but having two names for everything is possibly worse than a few extra angle brackets

[Eric Wieser]

A few years ago I systematically promoted many of these lift-like results to equivalences

[David Loeffler]

We seem to be missing a lemma MonoidHom.liftOfSurjective_comp stating the defining property.

[Eric Wieser]

Is it docs#AddMonoidHom.liftOfRightInverse_comp ?

[Adam Topaz]

The RHS of that equiv should also be a subtype :)

[Eric Wieser]

What subtype?

[Adam Topaz]

nevermind I'm wrong.

[David Loeffler]

Eric Wieser said:

Is it docs#AddMonoidHom.liftOfRightInverse_comp_apply ?

Yes, that gives it pretty quickly, but if we're going to have liftOfSurjective as an alias for a special case of liftOfRightInverse, then we should have the corresponding lemma too.

[Adam Topaz]

FWIW, I don't think we should get rid of the equiv versions of such lift constructions, but I would rather have both (again, just for ergonomics)

[Eric Wieser]

liftOfSurjective is reducible, so rw [liftOfRightInverse_comp_apply] will work on it. Generally we don't repeat lemmas for reducible def (a.k.a abbrevs), because that defeats the point of it being reducible in the first place