From 8fafd52412b191f64d32a5b2428062b17ffe1b6a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 3 May 2023 23:14:44 +0000 Subject: [PATCH] feat(ring_theory/derivation): support non-commutative rings (via bimodules) --- src/ring_theory/derivation.lean | 31 ++++++++++++++++++------------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/src/ring_theory/derivation.lean b/src/ring_theory/derivation.lean index 5d70b42f02def..4439072f9686e 100644 --- a/src/ring_theory/derivation.lean +++ b/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,7 +112,7 @@ 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] }, @@ -118,7 +120,7 @@ begin { 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