Structures · Algebra
LieSubalgebra.IsCartanSubalgebra
A Cartan subalgebra is a nilpotent, self-normalizing subalgebra.
A _splitting_ Cartan subalgebra can be defined by mixing in LieModule.IsTriangularizable R H L.
- Defined in
- Mathlib.Algebra.Lie.CartanSubalgebra
- Shape
- One type argument · adds nilpotent, self_normalizing
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by149
- LieAlgebra.IsKilling.coroot
- LieSubalgebra.root
- LieAlgebra.IsKilling.rootSystem
- LieAlgebra.corootSpace
- LieAlgebra.IsKilling.chainLength
- LieAlgebra.IsKilling.cartanEquivDual
- LieAlgebra.IsKilling.root_apply_coroot
- LieIdeal.rootSet
- LieAlgebra.IsKilling.sl2SubmoduleOfRoot
- LieAlgebra.rootSpace_zero_eq
- LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace
- LieAlgebra.IsKilling.invtSubmoduleToLieIdeal
- LieAlgebra.IsKilling.corootSubmodule
- LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton
- LieAlgebra.IsKilling.coroot_eq_zero_iff
- LieAlgebra.IsKilling.finrank_rootSpace_eq_one
- LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff
- LieModule.Weight.IsNonZero.neg
- LieModule.Weight.coe_neg
- LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero
- LieAlgebra.IsKilling.apply_coroot_eq_cast'
- LieSubalgebra.isNonZero_coe_root
- IsSl2Triple.h_eq_coroot
- LieIdeal.corootSubmodule_le
- LieAlgebra.mem_corootSpace
- LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg
- LieAlgebra.IsKilling.chainTopCoeff_zero_right
- LieAlgebra.IsKilling.root_apply_cartanEquivDual_symm_ne_zero
- LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace
- LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt
- LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup
- LieIdeal.rootSpan
- LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff
- LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg
- LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff
- LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra
- LieSubalgebra.IsCartanSubalgebra.self_normalizing
- LieAlgebra.IsKilling.sl2SubalgebraOfRoot
- LieAlgebra.IsKilling.chainLength_of_isZero
- LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra
- LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_le
- LieAlgebra.IsKilling.chainLength_smul
- LieAlgebra.IsKilling.biSup_corootSpace_eq_top
- LieIdeal.root_apply_eq_zero_of_notMem_rootSet
- LieModule.Weight.IsZero.neg
- LieAlgebra.IsKilling.iInf_ker_weight_eq_bot
- LieAlgebra.IsKilling.coe_coroot_mem_corootSubmodule
- LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker
- LieIdeal.toInvtRootSubmodule
- LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal
Ancestors0
No ancestors.