English
Given a right inverse f_inv of a map f with a suitable restriction property, we can lift a derivation d: A → A to a derivation M → M by composing with f and f_inv, preserving Leibniz.
Русский
Дано отображение f и его право-обратное f_inv, удовлетворяющее свойству; можно возвести деривацию d на M → M, используя композицию f ∘ d ∘ f_inv, сохраняя Leibniz.
LaTeX
$$$\mathrm{liftOfRightInverse} : (f \circ d \circ f^{-1}) \in \mathrm{Derivation}(R,M,M)$$$
Lean4
/-- Lift a derivation via an algebra homomorphism `f` with a right inverse such that
`f(x) = 0 → f(d(x)) = 0`. This gives the derivation `f ∘ d ∘ f⁻¹`.
This is needed for an argument in [Rosenlicht, M. Integration in finite terms][Rosenlicht_1972].
-/
def liftOfRightInverse {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) : Derivation R M M
where
toFun x := f (d (f_inv x))
map_add' x
y := by
suffices f (d (f_inv (x + y) - (f_inv x + f_inv y))) = 0 by simpa [sub_eq_zero]
apply hd
simp [hf _]
map_smul' x
y := by
suffices f (d (f_inv (x • y) - x • f_inv y)) = 0 by simpa [sub_eq_zero]
apply hd
simp [hf _]
map_one_eq_zero' := by
suffices f (d (f_inv 1 - 1)) = 0 by simpa [sub_eq_zero]
apply hd
simp [hf _]
leibniz' x
y := by
suffices f (d (f_inv (x * y) - f_inv x * f_inv y)) = 0 by simpa [sub_eq_zero, hf _]
apply hd
simp [hf _]
