Structures · Algebra
LieAlgebra.IsKilling
We say a Lie algebra is Killing if its Killing form is non-singular. NB: This is not standard terminology (the literature does not seem to name Lie algebras with this property).
- Defined in
- Mathlib.Algebra.Lie.Killing
- Shape
- 2 explicit arguments · adds killingCompl_top_eq_bot
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 by142
- LieAlgebra.IsKilling.coroot
- LieAlgebra.IsKilling.rootSystem
- LieAlgebra.IsKilling.chainLength
- LieAlgebra.IsKilling.cartanEquivDual
- LieAlgebra.IsKilling.root_apply_coroot
- LieAlgebra.IsKilling.sl2SubmoduleOfRoot
- LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace
- LieAlgebra.IsKilling.invtSubmoduleToLieIdeal
- LieAlgebra.IsKilling.ker_killingForm_eq_bot
- 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'
- IsSl2Triple.h_eq_coroot
- 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.Basis.baseSupportEquiv
- LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff
- LieAlgebra.IsKilling.sl2SubalgebraOfRoot
- LieAlgebra.IsKilling.chainLength_of_isZero
- LieAlgebra.Basis.base
- 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.killingCompl_top_eq_bot
- LieAlgebra.IsKilling.coe_coroot_mem_corootSubmodule
- LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker
- LieIdeal.toInvtRootSubmodule
- LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal
- LieIdeal.rootSet_apply_coroot_eq_zero_of_notMem_rootSet
- LieAlgebra.IsKilling.killingForm_nondegenerate
- LieAlgebra.IsKilling.span_weight_eq_top
- LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot
- LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux
- LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace
- LieAlgebra.IsKilling.corootSpace_zero_eq_bot
Ancestors0
No ancestors.