feat(RingTheory/Derivation/Basic): define lifting a derivation via an algebra homomorphism

Mathlib/RingTheory/Derivation/Basic.lean

@@ -336,6 +336,70 @@ end RestrictScalars
 
 end
 
+section Lift
+
+variable {R : Type*} {A : Type*} {M : Type*}
+variable [CommSemiring R] [CommRing A] [CommRing M]
+variable [Algebra R A] [Algebra R M]
+variable {F : Type*} [FunLike F A M] [AlgHomClass F R A M]
+
+/--
+Lift a derivation via an algebra homomorphism `f` with a right inverse. This gives the derivation
+`f ∘ d ∘ f⁻¹`.
+-/
+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
+    simp only [← map_add]
+    rw [← sub_eq_zero, ← map_sub, ← map_sub]
+    apply hd
+    simp [hf _]
+  map_smul' x y := by
+    simp only [RingHom.id_apply, ← _root_.map_smul, ← map_smul]
+    rw [← sub_eq_zero, ← map_sub, ← map_sub]
+    apply hd
+    simp [hf _]
+  map_one_eq_zero' := by
+    simp only [LinearMap.coe_mk, AddHom.coe_mk]
+    convert_to f (d (f_inv 1 - 1)) = 0
+    · simp
+    apply hd
+    simp [hf _, map_one]
+  leibniz' x y := by
+    simp only [LinearMap.coe_mk, AddHom.coe_mk, smul_eq_mul]
+    convert_to _ = f (f_inv x * d (f_inv y)) + f (f_inv y * d (f_inv x)) using 2
+    · simp [hf _]
+    · simp [hf _]
+    convert_to _ = f (d (f_inv x * f_inv y))
+    · simp
+    rw [← sub_eq_zero, ← map_sub, ← map_sub]
+    apply hd
+    simp [hf _]
+
+@[simp]
+lemma 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 f f_inv hf d hd (f x) = f (d x) := by
+  unfold liftOfRightInverse
+  simp only [mk_coe, LinearMap.coe_mk, AddHom.coe_mk]
+  rw [← sub_eq_zero, ← map_sub, ← map_sub]
+  apply hd
+  simp [hf _]
+
+/--
+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 f (Function.surjInv hf) (Function.rightInverse_surjInv hf) hd
+
+lemma liftOfSurjective_apply (f : F) (hf : Function.Surjective f)
+    (d : Derivation R A A) (hd : ∀ x, f x = 0 → f (d x) = 0) (x : A) :
+    Derivation.liftOfSurjective f hf d hd (f x) = f (d x) := by simp
+
+end Lift
+
 section Cancel
 
 variable {R : Type*} [CommSemiring R] {A : Type*} [CommSemiring A] [Algebra R A] {M : Type*}