English
The liftOfRightInverse is the unique map φ: B → C with φ ∘ f = g, given the data of f, f_inv, g, and ker conditions.
Русский
Едиственный отображение φ: B → C удовлетворяет φ ∘ f = g при данных f, f_inv, g и условии ker.
LaTeX
$$$$ (f.liftOfRightInverse f_{inv} hf g) \\circ f = g. $$$$
Lean4
/-- `liftOfRightInverse f hf g hg` is the unique ring homomorphism `φ`
* such that `φ.comp f = g` (`RingHom.liftOfRightInverse_comp`),
* where `f : A →+* B` has a right_inverse `f_inv` (`hf`),
* and `g : B →+* C` satisfies `hg : f.ker ≤ g.ker`.
See `RingHom.eq_liftOfRightInverse` for the uniqueness lemma.
```
A .
| \
f | \ g
| \
v \⌟
B ----> C
∃!φ
```
-/
def liftOfRightInverse (hf : Function.RightInverse f_inv f) :
{ g : A →+* C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C)
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]
