Skip to content

Commit 11fa0b4

Browse files
jano-woljano-wol
committed
feat: add Ad.lean for collecting adjoint action properties (#36628)
Add Ad.lean for collecting adjoint action properties Co-authored-by: Janos Wolosz <janos.wolosz@gmail.com>
1 parent 7a0d2c9 commit 11fa0b4

File tree

7 files changed

+92
-29
lines changed

7 files changed

+92
-29
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -683,6 +683,8 @@ public import Mathlib.Algebra.Homology.TotalComplexSymmetry
683683
public import Mathlib.Algebra.IsPrimePow
684684
public import Mathlib.Algebra.Jordan.Basic
685685
public import Mathlib.Algebra.Lie.Abelian
686+
public import Mathlib.Algebra.Lie.AdjointAction.Basic
687+
public import Mathlib.Algebra.Lie.AdjointAction.Derivation
686688
public import Mathlib.Algebra.Lie.BaseChange
687689
public import Mathlib.Algebra.Lie.Basic
688690
public import Mathlib.Algebra.Lie.CartanExists
@@ -691,7 +693,6 @@ public import Mathlib.Algebra.Lie.CartanSubalgebra
691693
public import Mathlib.Algebra.Lie.Character
692694
public import Mathlib.Algebra.Lie.Classical
693695
public import Mathlib.Algebra.Lie.Cochain
694-
public import Mathlib.Algebra.Lie.Derivation.AdjointAction
695696
public import Mathlib.Algebra.Lie.Derivation.Basic
696697
public import Mathlib.Algebra.Lie.Derivation.Killing
697698
public import Mathlib.Algebra.Lie.DirectSum

‎Mathlib/Algebra/Lie/AdjointAction/Basic.lean‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
/-
2+
Copyright (c) 2026 Janos Wolosz. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Janos Wolosz
5+
-/
6+
module
7+
8+
public import Mathlib.Algebra.Algebra.Bilinear
9+
public import Mathlib.Algebra.Lie.OfAssociative
10+
public import Mathlib.LinearAlgebra.Semisimple
11+
public import Mathlib.RingTheory.Nilpotent.Lemmas
12+
13+
/-!
14+
# Properties of the adjoint action
15+
16+
Theorems about the adjoint action `LieAlgebra.ad` on associative algebras.
17+
18+
## Main results
19+
20+
* `LieAlgebra.commute_ad_of_commute`: commuting elements have commuting adjoints.
21+
* `LieAlgebra.ad_nilpotent_of_nilpotent`: the adjoint of a nilpotent element is nilpotent.
22+
* `LieAlgebra.ad_isSemisimple_of_isSemisimple`: the adjoint of a semisimple element is semisimple.
23+
-/
24+
25+
@[expose] public section
26+
27+
section CommRing
28+
29+
variable {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
30+
31+
/-- Commuting elements have commuting adjoint actions. -/
32+
theorem LieAlgebra.commute_ad_of_commute {a b : A} (h : Commute a b) :
33+
Commute (LieAlgebra.ad R A a) (LieAlgebra.ad R A b) := by
34+
rw [Commute, SemiconjBy, ← sub_eq_zero, ← Ring.lie_def,
35+
← (LieAlgebra.ad R A).map_lie, Ring.lie_def, sub_eq_zero.mpr h, map_zero]
36+
37+
/-- The adjoint of a nilpotent element is nilpotent. -/
38+
theorem LieAlgebra.ad_nilpotent_of_nilpotent {a : A} (h : IsNilpotent a) :
39+
IsNilpotent (LieAlgebra.ad R A a) := by
40+
rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]
41+
have hl : IsNilpotent (LinearMap.mulLeft R a) := by rwa [LinearMap.isNilpotent_mulLeft_iff]
42+
have hr : IsNilpotent (LinearMap.mulRight R a) := by rwa [LinearMap.isNilpotent_mulRight_iff]
43+
exact (LinearMap.commute_mulLeft_right a a).isNilpotent_sub hl hr
44+
45+
theorem LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad {L : Type*} [LieRing L] [LieAlgebra R L]
46+
(K : LieSubalgebra R L) {x : K} (h : IsNilpotent (LieAlgebra.ad R L ↑x)) :
47+
IsNilpotent (LieAlgebra.ad R K x) := by
48+
obtain ⟨n, hn⟩ := h
49+
use n
50+
exact Module.End.submodule_pow_eq_zero_of_pow_eq_zero (K.ad_comp_incl_eq x) hn
51+
52+
theorem LieAlgebra.isNilpotent_ad_of_isNilpotent
53+
{L : LieSubalgebra R A} {x : L} (h : IsNilpotent (x : A)) :
54+
IsNilpotent (LieAlgebra.ad R L x) :=
55+
L.isNilpotent_ad_of_isNilpotent_ad <| LieAlgebra.ad_nilpotent_of_nilpotent h
56+
57+
end CommRing
58+
59+
section Field
60+
61+
variable {K V : Type*} [Field K] [PerfectField K] [AddCommGroup V] [Module K V]
62+
variable [FiniteDimensional K V]
63+
64+
/-- The adjoint of a semisimple element is semisimple. -/
65+
theorem LieAlgebra.ad_isSemisimple_of_isSemisimple {a : Module.End K V} (ha : a.IsSemisimple) :
66+
(LieAlgebra.ad K (Module.End K V) a).IsSemisimple := by
67+
rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]
68+
have hl : Module.End.IsSemisimple (LinearMap.mulLeft K a) := by
69+
apply Module.End.isSemisimple_of_squarefree_aeval_eq_zero ha.minpoly_squarefree
70+
have : Polynomial.aeval (Algebra.lmul K (Module.End K V) a) (minpoly K a) = 0 := by
71+
rw [Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]
72+
simpa using this
73+
have hr : Module.End.IsSemisimple (LinearMap.mulRight K a) := by
74+
apply Module.End.isSemisimple_of_squarefree_aeval_eq_zero ha.minpoly_squarefree
75+
have hrw : LinearMap.mulRight K a =
76+
(Algebra.lsmul (A := (Module.End K V)ᵐᵒᵖ) K K (Module.End K V)) (.op a) := by
77+
ext; simp [Algebra.lsmul]
78+
rw [hrw, Polynomial.aeval_algHom_apply, Polynomial.aeval_op_apply, minpoly.aeval,
79+
MulOpposite.op_zero, map_zero]
80+
exact hl.sub_of_commute (LinearMap.commute_mulLeft_right a a) hr
81+
82+
end Field

Mathlib/Algebra/Lie/Derivation/AdjointAction.lean renamed to Mathlib/Algebra/Lie/AdjointAction/Derivation.lean

File renamed without changes.

‎Mathlib/Algebra/Lie/Derivation/Killing.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Frédéric Marbach
55
-/
66
module
77

8-
public import Mathlib.Algebra.Lie.Derivation.AdjointAction
8+
public import Mathlib.Algebra.Lie.AdjointAction.Derivation
99
public import Mathlib.Algebra.Lie.Killing
1010
public import Mathlib.LinearAlgebra.BilinearForm.Orthogonal
1111

‎Mathlib/Algebra/Lie/Engel.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Oliver Nash
55
-/
66
module
77

8+
public import Mathlib.Algebra.Lie.AdjointAction.Basic
89
public import Mathlib.Algebra.Lie.Nilpotent
910
public import Mathlib.Algebra.Lie.Normalizer
1011

‎Mathlib/Algebra/Lie/Nilpotent.lean‎

Lines changed: 0 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -923,33 +923,6 @@ instance [IsNilpotent L I] : LieRing.IsNilpotent I := by
923923

924924
end LieIdeal
925925

926-
section OfAssociative
927-
928-
variable (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A]
929-
930-
theorem _root_.LieAlgebra.ad_nilpotent_of_nilpotent {a : A} (h : IsNilpotent a) :
931-
IsNilpotent (LieAlgebra.ad R A a) := by
932-
rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]
933-
have hl : IsNilpotent (LinearMap.mulLeft R a) := by rwa [LinearMap.isNilpotent_mulLeft_iff]
934-
have hr : IsNilpotent (LinearMap.mulRight R a) := by rwa [LinearMap.isNilpotent_mulRight_iff]
935-
have := @LinearMap.commute_mulLeft_right R A _ _ _ _ _ a a
936-
exact this.isNilpotent_sub hl hr
937-
938-
variable {R}
939-
940-
theorem _root_.LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad {L : Type v} [LieRing L]
941-
[LieAlgebra R L] (K : LieSubalgebra R L) {x : K} (h : IsNilpotent (LieAlgebra.ad R L ↑x)) :
942-
IsNilpotent (LieAlgebra.ad R K x) := by
943-
obtain ⟨n, hn⟩ := h
944-
use n
945-
exact Module.End.submodule_pow_eq_zero_of_pow_eq_zero (K.ad_comp_incl_eq x) hn
946-
947-
theorem _root_.LieAlgebra.isNilpotent_ad_of_isNilpotent {L : LieSubalgebra R A} {x : L}
948-
(h : IsNilpotent (x : A)) : IsNilpotent (LieAlgebra.ad R L x) :=
949-
L.isNilpotent_ad_of_isNilpotent_ad <| LieAlgebra.ad_nilpotent_of_nilpotent R h
950-
951-
end OfAssociative
952-
953926
section ExtendScalars
954927

955928
open LieModule TensorProduct

‎Mathlib/Algebra/Polynomial/AlgebraMap.lean‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -413,6 +413,12 @@ theorem aeval_algHom_apply {F : Type*} [FunLike F A B] [AlgHomClass F R A B]
413413
(by simp [AlgHomClass.commutes])
414414
rw [map_add, hp, hq, ← map_add, ← map_add]
415415

416+
theorem aeval_op_apply (x : A) (p : R[X]) :
417+
aeval (MulOpposite.op x) p = MulOpposite.op (aeval x p) := by
418+
induction p using Polynomial.induction_on' with
419+
| add p q hp hq => simp [map_add, hp, hq]
420+
| monomial n c => simp [aeval_monomial, MulOpposite.op_pow, Algebra.commutes]
421+
416422
theorem aeval_smul (f : R[X]) {G : Type*} [Monoid G] [MulSemiringAction G A] [SMulCommClass G R A]
417423
(g : G) (x : A) : f.aeval (g • x) = g • (f.aeval x) := by
418424
rw [← MulSemiringAction.toAlgHom_apply R, aeval_algHom_apply, MulSemiringAction.toAlgHom_apply]

0 commit comments

Comments
 (0)