English
Let f_inv be a right inverse of a homomorphism f, and let d be a derivation on A. If fx = 0 implies f(d x) = 0 for all x ∈ A, then the lifted derivation on M satisfies (liftOfRightInverse hf hd)(f x) = f(d x) for all x ∈ A.
Русский
Пусть f_inv является правым обратным к гомоморфизму f, а d — выводом на A. Если для каждого x ∈ A выполняется f x = 0 ⇒ f(d x) = 0, то полученный через подъем по правому обратному переходу вывод на M удовлетворяет (liftOfRightInverse hf hd)(f x) = f(d x) для всех x ∈ A.
LaTeX
$$$\displaystyle \forall x \in A,\quad \operatorname{liftOfRightInverse}(hf, hd)(f(x)) = f(d(x)),$$$
Lean4
@[simp]
theorem liftOfRightInverse_apply {f : F} {f_inv : M → A} (hf : Function.RightInverse f_inv f) {d : Derivation R A A}
(hd : ∀ x, f x = 0 → f (d x) = 0) (x : A) : Derivation.liftOfRightInverse hf hd (f x) = f (d x) :=
by
suffices f (d (f_inv (f x) - x)) = 0 by simpa [sub_eq_zero]
apply hd
simp [hf _]
