From d43978d8598f6bd10470f95c1f828c34b39faba2 Mon Sep 17 00:00:00 2001
From: Oliver Nash <github@olivernash.org>
Date: Thu, 15 Feb 2024 11:58:43 +0000
Subject: [PATCH] feat: add lemma `LinearMap.trace_lie` and move `Bracket`
 instance (#10584)

It is useful to have access to this bracket definition without having to import a bunch of Lie algebra theory.
---
 Mathlib/Algebra/Lie/OfAssociative.lean | 21 ---------------
 Mathlib/Algebra/Ring/Commute.lean      | 22 ++++++++++++++++
 Mathlib/LinearAlgebra/Trace.lean       |  6 +++++
 test/NoncommRing.lean                  | 36 ++++++++++++--------------
 4 files changed, 45 insertions(+), 40 deletions(-)

diff --git a/Mathlib/Algebra/Lie/OfAssociative.lean b/Mathlib/Algebra/Lie/OfAssociative.lean
index fa0fdb4c28991..efca45b4673c9 100644
--- a/Mathlib/Algebra/Lie/OfAssociative.lean
+++ b/Mathlib/Algebra/Lie/OfAssociative.lean
@@ -41,27 +41,6 @@ section OfAssociative
 
 variable {A : Type v} [Ring A]
 
-namespace Ring
-
-/-- The bracket operation for rings is the ring commutator, which captures the extent to which a
-ring is commutative. It is identically zero exactly when the ring is commutative. -/
-instance (priority := 100) instBracket : Bracket A A :=
-  ⟨fun x y => x * y - y * x⟩
-
-theorem lie_def (x y : A) : ⁅x, y⁆ = x * y - y * x :=
-  rfl
-#align ring.lie_def Ring.lie_def
-
-end Ring
-
-theorem commute_iff_lie_eq {x y : A} : Commute x y ↔ ⁅x, y⁆ = 0 :=
-  sub_eq_zero.symm
-#align commute_iff_lie_eq commute_iff_lie_eq
-
-theorem Commute.lie_eq {x y : A} (h : Commute x y) : ⁅x, y⁆ = 0 :=
-  sub_eq_zero_of_eq h
-#align commute.lie_eq Commute.lie_eq
-
 namespace LieRing
 
 /-- An associative ring gives rise to a Lie ring by taking the bracket to be the ring commutator. -/
diff --git a/Mathlib/Algebra/Ring/Commute.lean b/Mathlib/Algebra/Ring/Commute.lean
index 17965603b53f0..4167143e2720a 100644
--- a/Mathlib/Algebra/Ring/Commute.lean
+++ b/Mathlib/Algebra/Ring/Commute.lean
@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Ne
 import Mathlib.Algebra.Ring.Semiconj
 import Mathlib.Algebra.Ring.Units
 import Mathlib.Algebra.Group.Commute.Defs
+import Mathlib.Data.Bracket
 
 #align_import algebra.ring.commute from "leanprover-community/mathlib"@"70d50ecfd4900dd6d328da39ab7ebd516abe4025"
 
@@ -175,3 +176,24 @@ theorem inv_eq_self_iff [Ring R] [NoZeroDivisors R] (u : Rˣ) : u⁻¹ = u ↔ u
 #align units.inv_eq_self_iff Units.inv_eq_self_iff
 
 end Units
+
+section Bracket
+
+variable [NonUnitalNonAssocRing R]
+
+namespace Ring
+
+instance (priority := 100) instBracket : Bracket R R := ⟨fun x y => x * y - y * x⟩
+
+theorem lie_def (x y : R) : ⁅x, y⁆ = x * y - y * x := rfl
+#align ring.lie_def Ring.lie_def
+
+end Ring
+
+theorem commute_iff_lie_eq {x y : R} : Commute x y ↔ ⁅x, y⁆ = 0 := sub_eq_zero.symm
+#align commute_iff_lie_eq commute_iff_lie_eq
+
+theorem Commute.lie_eq {x y : R} (h : Commute x y) : ⁅x, y⁆ = 0 := sub_eq_zero_of_eq h
+#align commute.lie_eq Commute.lie_eq
+
+end Bracket
diff --git a/Mathlib/LinearAlgebra/Trace.lean b/Mathlib/LinearAlgebra/Trace.lean
index 9cc4c2ef28a19..4247dce29f38a 100644
--- a/Mathlib/LinearAlgebra/Trace.lean
+++ b/Mathlib/LinearAlgebra/Trace.lean
@@ -123,6 +123,12 @@ theorem trace_conj (g : M →ₗ[R] M) (f : (M →ₗ[R] M)ˣ) :
   simp
 #align linear_map.trace_conj LinearMap.trace_conj
 
+@[simp]
+lemma trace_lie {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (f g : Module.End R M) :
+    trace R M ⁅f, g⁆ = 0 := by
+  rw [Ring.lie_def, map_sub, trace_mul_comm]
+  exact sub_self _
+
 end
 
 section
diff --git a/test/NoncommRing.lean b/test/NoncommRing.lean
index f0b388483a78e..053a44e35975a 100644
--- a/test/NoncommRing.lean
+++ b/test/NoncommRing.lean
@@ -1,9 +1,6 @@
 import Mathlib.GroupTheory.GroupAction.Ring
 import Mathlib.Tactic.NoncommRing
 
-local notation (name := commutator) "⁅"a", "b"⁆" => a * b - b * a
-
-set_option quotPrecheck false
 local infix:70 " ⚬ " => fun a b => a * b + b * a
 
 variable {R : Type _} [Ring R]
@@ -33,19 +30,19 @@ example : (a - b)^2 = a^2 - a*b - b*a + b^2 := by noncomm_ring
 example : (a + b)^3 = a^3 + a^2*b + a*b*a + a*b^2 + b*a^2 + b*a*b + b^2*a + b^3 := by noncomm_ring
 example : (a - b)^3 = a^3 - a^2*b - a*b*a + a*b^2 - b*a^2 + b*a*b + b^2*a - b^3 := by noncomm_ring
 
-example : ⁅a, a⁆ = 0 := by noncomm_ring
-example : ⁅a, b⁆ = -⁅b, a⁆ := by noncomm_ring
-example : ⁅a + b, c⁆ = ⁅a, c⁆ + ⁅b, c⁆ := by noncomm_ring
-example : ⁅a, b + c⁆ = ⁅a, b⁆ + ⁅a, c⁆ := by noncomm_ring
-example : ⁅a, ⁅b, c⁆⁆ + ⁅b, ⁅c, a⁆⁆ + ⁅c, ⁅a, b⁆⁆ = 0 := by noncomm_ring
-example : ⁅⁅a, b⁆, c⁆ + ⁅⁅b, c⁆, a⁆ + ⁅⁅c, a⁆, b⁆ = 0 := by noncomm_ring
-example : ⁅a, ⁅b, c⁆⁆ = ⁅⁅a, b⁆, c⁆ + ⁅b, ⁅a, c⁆⁆ := by noncomm_ring
-example : ⁅⁅a, b⁆, c⁆ = ⁅⁅a, c⁆, b⁆ + ⁅a, ⁅b, c⁆⁆ := by noncomm_ring
-example : ⁅a * b, c⁆ = a * ⁅b, c⁆ + ⁅a, c⁆ * b := by noncomm_ring
-example : ⁅a, b * c⁆ = ⁅a, b⁆ * c + b * ⁅a, c⁆ := by noncomm_ring
-example : ⁅3 * a, a⁆ = 0 := by noncomm_ring
-example : ⁅a * -5, a⁆ = 0 := by noncomm_ring
-example : ⁅a^3, a⁆ = 0 := by noncomm_ring
+example : ⁅a, a⁆ = 0 := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅a, b⁆ = -⁅b, a⁆ := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅a + b, c⁆ = ⁅a, c⁆ + ⁅b, c⁆ := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅a, b + c⁆ = ⁅a, b⁆ + ⁅a, c⁆ := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅a, ⁅b, c⁆⁆ + ⁅b, ⁅c, a⁆⁆ + ⁅c, ⁅a, b⁆⁆ = 0 := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅⁅a, b⁆, c⁆ + ⁅⁅b, c⁆, a⁆ + ⁅⁅c, a⁆, b⁆ = 0 := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅a, ⁅b, c⁆⁆ = ⁅⁅a, b⁆, c⁆ + ⁅b, ⁅a, c⁆⁆ := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅⁅a, b⁆, c⁆ = ⁅⁅a, c⁆, b⁆ + ⁅a, ⁅b, c⁆⁆ := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅a * b, c⁆ = a * ⁅b, c⁆ + ⁅a, c⁆ * b := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅a, b * c⁆ = ⁅a, b⁆ * c + b * ⁅a, c⁆ := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅3 * a, a⁆ = 0 := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅a * -5, a⁆ = 0 := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅a^3, a⁆ = 0 := by simp only [Ring.lie_def]; noncomm_ring
 
 example : a ⚬ a = 2*a^2 := by noncomm_ring
 example : (2 * a) ⚬ a = 4*a^2 := by noncomm_ring
@@ -54,9 +51,10 @@ example : a ⚬ (b + c) = a ⚬ b + a ⚬ c := by noncomm_ring
 example : (a + b) ⚬ c = a ⚬ c + b ⚬ c := by noncomm_ring
 example : (a ⚬ b) ⚬ (a ⚬ a) = a ⚬ (b ⚬ (a ⚬ a)) := by noncomm_ring
 
-example : ⁅a, b ⚬ c⁆ = ⁅a, b⁆ ⚬ c + b ⚬ ⁅a, c⁆ := by noncomm_ring
-example : ⁅a ⚬ b, c⁆ = a ⚬ ⁅b, c⁆ + ⁅a, c⁆ ⚬ b := by noncomm_ring
-example : (a ⚬ b) ⚬ c - a ⚬ (b ⚬ c) = -⁅⁅a, b⁆, c⁆ + ⁅a, ⁅b, c⁆⁆ := by noncomm_ring
+example : ⁅a, b ⚬ c⁆ = ⁅a, b⁆ ⚬ c + b ⚬ ⁅a, c⁆ := by simp only [Ring.lie_def]; noncomm_ring
+example : ⁅a ⚬ b, c⁆ = a ⚬ ⁅b, c⁆ + ⁅a, c⁆ ⚬ b := by simp only [Ring.lie_def]; noncomm_ring
+example : (a ⚬ b) ⚬ c - a ⚬ (b ⚬ c) = -⁅⁅a, b⁆, c⁆ + ⁅a, ⁅b, c⁆⁆ := by
+  simp only [Ring.lie_def]; noncomm_ring
 
 example : a + -b = -b + a := by
   -- This should print "`noncomm_ring` simp lemmas don't apply; try `abel` instead"