feat(ring_theory/derivation): support non-commutative rings (via bimo…

…dules)

src/ring_theory/derivation.lean

@@ -32,17 +32,19 @@ This file defines derivation. A derivation `D` from the `R`-algebra `A` to the `
 open algebra
 open_locale big_operators
 
+open mul_opposite
+
 /-- `D : derivation R A M` is an `R`-linear map from `A` to `M` that satisfies the `leibniz`
 equality. We also require that `D 1 = 0`. See `derivation.mk'` for a constructor that deduces this
 assumption from the Leibniz rule when `M` is cancellative.
 
 TODO: update this when bimodules are defined. -/
 @[protect_proj]
-structure derivation (R : Type*) (A : Type*) [comm_semiring R] [comm_semiring A]
-  [algebra R A] (M : Type*) [add_comm_monoid M] [module A M] [module R M]
+structure derivation (R : Type*) (A : Type*) [comm_semiring R] [semiring A]
+  [algebra R A] (M : Type*) [add_comm_monoid M] [module A M] [module Aᵐᵒᵖ M] [module R M]
   extends A →ₗ[R] M :=
 (map_one_eq_zero' : to_linear_map 1 = 0)
-(leibniz' (a b : A) : to_linear_map (a * b) = a • to_linear_map b + b • to_linear_map a)
+(leibniz' (a b : A) : to_linear_map (a * b) = a • to_linear_map b + op b • to_linear_map a)
 
 /-- The `linear_map` underlying a `derivation`. -/
 add_decl_doc derivation.to_linear_map
@@ -52,8 +54,8 @@ namespace derivation
 section
 
 variables {R : Type*} [comm_semiring R]
-variables {A : Type*} [comm_semiring A] [algebra R A]
-variables {M : Type*} [add_comm_monoid M] [module A M] [module R M]
+variables {A : Type*} [semiring A] [algebra R A]
+variables {M : Type*} [add_comm_monoid M] [module A M] [module Aᵐᵒᵖ M] [module R M]
 variables (D : derivation R A M) {D1 D2 : derivation R A M} (r : R) (a b : A)
 
 instance : add_monoid_hom_class (derivation R A M) A M :=
@@ -91,7 +93,7 @@ lemma congr_fun (h : D1 = D2) (a : A) : D1 a = D2 a := fun_like.congr_fun h a
 protected lemma map_add : D (a + b) = D a + D b := map_add D a b
 protected lemma map_zero : D 0 = 0 := map_zero D
 @[simp] lemma map_smul : D (r • a) = r • D a := D.to_linear_map.map_smul r a
-@[simp] lemma leibniz : D (a * b) = a • D b + b • D a := D.leibniz' _ _
+@[simp] lemma leibniz : D (a * b) = a • D b + op b • D a := D.leibniz' _ _
 
 lemma map_sum {ι : Type*} (s : finset ι) (f : ι → A) : D (∑ i in s, f i) = ∑ i in s, D (f i) :=
 D.to_linear_map.map_sum
@@ -110,15 +112,15 @@ by rw [←mul_one r, ring_hom.map_mul, ring_hom.map_one, ←smul_def, map_smul,
 @[simp] lemma map_coe_nat (n : ℕ) : D (n : A) = 0 :=
 by rw [← nsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
 
-@[simp] lemma leibniz_pow (n : ℕ) : D (a ^ n) = n • a ^ (n - 1) • D a :=
+@[simp] lemma leibniz_pow [is_central_scalar A M] (n : ℕ) : D (a ^ n) = n • a ^ (n - 1) • D a :=
 begin
   induction n with n ihn,
   { rw [pow_zero, map_one_eq_zero, zero_smul] },
   { rcases (zero_le n).eq_or_lt with (rfl|hpos),
     { rw [pow_one, one_smul, pow_zero, one_smul] },
     { have : a * a ^ (n - 1) = a ^ n, by rw [← pow_succ, nat.sub_add_cancel hpos],
       simp only [pow_succ, leibniz, ihn, smul_comm a n, smul_smul a, add_smul, this,
-        nat.succ_eq_add_one, nat.add_succ_sub_one, add_zero, one_nsmul] } }
+        nat.succ_eq_add_one, nat.add_succ_sub_one, add_zero, one_nsmul, op_smul_eq_smul] } }
 end
 
 lemma eq_on_adjoin {s : set A} (h : set.eq_on D1 D2 s) : set.eq_on D1 D2 (adjoin R s) :=
@@ -160,7 +162,7 @@ instance : inhabited (derivation R A M) := ⟨0⟩
 section scalar
 
 variables {S : Type*} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M]
-  [smul_comm_class S A M]
+  [smul_comm_class S A M] [smul_comm_class S Aᵐᵒᵖ M]
 
 @[priority 100]
 instance : has_smul S (derivation R A M) :=
@@ -193,17 +195,20 @@ instance [distrib_mul_action Sᵐᵒᵖ M] [is_central_scalar S M] :
 end scalar
 
 @[priority 100]
-instance {S : Type*} [semiring S] [module S M] [smul_comm_class R S M] [smul_comm_class S A M] :
+instance {S : Type*} [semiring S] [module S M] [smul_comm_class R S M]
+  [smul_comm_class S A M] [smul_comm_class S Aᵐᵒᵖ M] :
   module S (derivation R A M) :=
 function.injective.module S coe_fn_add_monoid_hom coe_injective coe_smul
 
-instance [is_scalar_tower R A M] : is_scalar_tower R A (derivation R A M) :=
+instance [is_scalar_tower R A M] [smul_comm_class R Aᵐᵒᵖ M]
+  [smul_comm_class A Aᵐᵒᵖ M] :
+  is_scalar_tower R A (derivation R A M) :=
 ⟨λ x y z, ext (λ a, smul_assoc _ _ _)⟩
 
 section push_forward
 
-variables {N : Type*} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M]
-  [is_scalar_tower R A N]
+variables {N : Type*} [add_comm_monoid N] [module A N] [module Aᵐᵒᵖ N] [module R N]
+  [is_scalar_tower R A M] [is_scalar_tower R Aᵐᵒᵖ M] [is_scalar_tower R A N] [is_scalar_tower R Aᵐᵒᵖ N]
 variables (f : M →ₗ[A] N) (e : M ≃ₗ[A] N)
 
 /-- We can push forward derivations using linear maps, i.e., the composition of a derivation with a