English
There is a natural bijection between { g : G1 →* G3 | f.ker ≤ g.ker } and G2 →* G3, given by lifting along f with a right inverse.
Русский
Существует естественная биекция между множествами { g : G1 →* G3 | f.ker ≤ g.ker } и G2 →* G3, задаваемая подъемом вдоль f с правым обратным.
LaTeX
$$$ { g : G1 \\to* G3 // f.ker \\le g.ker } \\ \\xrightarrow{\\sim} (G2 \\to* G3) $$$
Lean4
/-- Auxiliary definition used to define `liftOfRightInverse` -/
@[to_additive /-- Auxiliary definition used to define `liftOfRightInverse` -/
]
def liftOfRightInverseAux (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) : G₂ →* G₃
where
toFun b := g (f_inv b)
map_one' := hg (hf 1)
map_mul' := by
intro x y
rw [← g.map_mul, ← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]
apply hg
rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one, f.map_mul]
simp only [hf _]
