English
A noncomputable version of lifting exists for surjective f: there is an equivalence between surjective lifts and functions G2→G3.
Русский
Существуют неконкретные подъемы при сюръективном отображении; существует эквивалентность между прообразами и отображениями G2→G3.
LaTeX
$$$ \\text{liftOfSurjective}(f) : \\{ g : G1 \\to* G3 // f.ker ≤ g.ker \\} \\simeq (G2 \\to* G3) $$$
Lean4
/-- A non-computable version of `MonoidHom.liftOfRightInverse` for when no computable right
inverse is available, that uses `Function.surjInv`. -/
@[to_additive (attr := simp) /-- A non-computable version of `AddMonoidHom.liftOfRightInverse` for when no
computable right inverse is available. -/
]
noncomputable abbrev liftOfSurjective (hf : Function.Surjective f) : { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃) :=
f.liftOfRightInverse (Function.surjInv hf) (Function.rightInverse_surjInv hf)
