English
Let f be surjective with a section provided by hf, and let d be a derivation on A satisfying hd. Then there is a derivation on M obtained by lifting d along a right inverse of f, i.e., liftOfSurjective hf hd ∈ Derivation R M M.
Русский
Пусть f сюръективен, имеется секция hf, и пусть d — вывод на A, удовлетворяющий hd. Тогда существует вывод на M, получаемый подъемом вдоль правого обратного, то есть liftOfSurjective hf hd ∈ Derivation R M M.
LaTeX
$$$\exists D' \in \operatorname{Derivation} R M M \,\text{such that}\, D'(m) = d(s(m))\text{ for a right inverse } s: M\to A\text{ of } f.$$$
Lean4
/-- A noncomputable version of `liftOfRightInverse` for surjective homomorphisms.
-/
noncomputable abbrev liftOfSurjective {f : F} (hf : Function.Surjective f) ⦃d : Derivation R A A⦄
(hd : ∀ x, f x = 0 → f (d x) = 0) : Derivation R M M :=
d.liftOfRightInverse (Function.rightInverse_surjInv hf) hd
