English
For a ring hom f: A → B with a right inverse f_inv and any g: A → C with ker f ≤ ker g, there exists a unique φ: B → C such that φ ∘ f = g; this yields a bijection between admissible g and φ.
Русский
Для кольцевого гомоморфа f: A → B с правой обратной f_inv и любого g: A → C с ker f ≤ ker g существует единственный φ: B → C такой, что φ ∘ f = g; образуется биекция между допустимыми g и φ.
LaTeX
$$$$ \\exists!\\, φ: B \\to C \\;\\big(φ \\circ f = g \\text{ and } \\ker f \\le \\ker φ\\big). $$$$
Lean4
/-- Auxiliary definition used to define `liftOfRightInverse` -/
def liftOfRightInverseAux (hf : Function.RightInverse f_inv f) (g : A →+* C) (hg : RingHom.ker f ≤ RingHom.ker g) :
B →+* C :=
{
AddMonoidHom.liftOfRightInverse f.toAddMonoidHom f_inv hf
⟨g.toAddMonoidHom, hg⟩ with
toFun := fun b => g (f_inv b)
map_one' := by
rw [← map_one g, ← sub_eq_zero, ← map_sub g, ← mem_ker]
apply hg
rw [mem_ker, map_sub f, sub_eq_zero, map_one f]
exact hf 1
map_mul' := by
intro x y
rw [← map_mul g, ← sub_eq_zero, ← map_sub g, ← mem_ker]
apply hg
rw [mem_ker, map_sub f, sub_eq_zero, map_mul f]
simp only [hf _] }
