English
If h ∘ f = g, then h = liftOfRightInverse(f, f^{-1}, hf) ⟨g, hg⟩.
Русский
Если g ∘ f = h, то h равно liftOfRightInverse(f, f^{-1}, hf) ⟨g, hg⟩.
LaTeX
$$$ h \\circ f = g \\Rightarrow h = f.liftOfRightInverse f^{-1} hf ⟨g, hg⟩ $$$
Lean4
/-- `liftOfRightInverse f hf g hg` is the unique group homomorphism `φ`
* such that `φ.comp f = g` (`MonoidHom.liftOfRightInverse_comp`),
* where `f : G₁ →+* G₂` has a RightInverse `f_inv` (`hf`),
* and `g : G₂ →+* G₃` satisfies `hg : f.ker ≤ g.ker`.
See `MonoidHom.eq_liftOfRightInverse` for the uniqueness lemma.
```
G₁.
| \
f | \ g
| \
v \⌟
G₂----> G₃
∃!φ
```
-/
@[to_additive /-- `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₃
∃!φ
``` -/
]
def liftOfRightInverse (hf : Function.RightInverse f_inv f) : { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃)
where
toFun g := f.liftOfRightInverseAux f_inv hf g.1 g.2
invFun φ := ⟨φ.comp f, fun x hx ↦ mem_ker.mpr <| by simp [mem_ker.mp hx]⟩
left_inv
g := by
ext
simp only [comp_apply, liftOfRightInverseAux_comp_apply]
right_inv
φ := by
ext b
simp [liftOfRightInverseAux, hf b]
