Theorems · Definition · nonassociative algebras
LieDerivation.ad
(R : Type u_1) → (L : Type u_2) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → L →ₗ⁅R⁆ LieDerivation R L L
The adjoint action of a Lie algebra L on itself, seen as a morphism of Lie algebras from
L to its derivations.
Note the minus sign: this is chosen to so that ad ⁅x, y⁆ = ⁅ad x, ad y⁆.
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingLieRingLieAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idproof · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- LinearMapproof · cited by 10,215
- LieRingstatement and proof · cited by 1,548
- LieAlgebrastatement and proof · cited by 1,246
- LieHomstatement · cited by 382
- LieDerivationstatement and proof · cited by 95
- LieDerivation.innerproof · cited by 1
Cited by20
Results whose statement or proof uses this declaration.
- LieDerivation.ad_apply_applystatement · cited by 3
- LieDerivation.ad_ker_eq_centerstatement and proof · cited by 3
- LieDerivation.IsKilling.killingForm_restrict_range_adstatement and proof · cited by 2
- LieDerivation.IsKilling.rangeAdOrthogonalproof · cited by 2
- LieDerivation.ad_isIdealMorphismstatement and proof · cited by 2
- LieDerivation.coe_ad_apply_eq_ad_applystatement · cited by 1
- LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebraproof · cited by 1
- LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonalstatement and proof · cited by 1
- LieDerivation.IsKilling.ad_mem_orthogonal_of_mem_orthogonalstatement and proof · cited by 1
- LieDerivation.IsKilling.exists_eq_adstatement · cited by 1
- LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegeneratestatement and proof · cited by 1
- LieDerivation.IsKilling.range_ad_eq_topstatement and proof · cited by 1