Linear

📁 Source: Mathlib/Algebra/Lie/Weights/Linear.lean

Statistics

Metric	Count
Definitions LinearWeights, instCoeLinearMap, ker, toLinear, shiftedGenWeightSpace, instLieRingModuleSubtypeMemLieSubmodule, shift	7
Theorems map_add, map_lie, map_smul, apply_lie, coe_coe, coe_toLinear_eq_zero_iff, coe_toLinear_ne_zero_iff, instLinearMapClass, toLinear_apply, exists_forall_lie_eq_smul, exists_nontrivial_weightSpace_of_isNilpotent, instLinearWeightsOfCharZero, instLinearWeightsOfIsLieAbelian, coe_lie_shiftedGenWeightSpace_apply, instIsNilpotentSubtypeMemLieSubmoduleOfIsNoetherian, instSubtypeMemLieSubmodule, shift_apply, shift_symm_apply, toEnd_eq, trace_comp_toEnd_genWeightSpace_eq, zero_lt_finrank_genWeightSpace	21
Total	28

LieModule

Definitions

Name	Category	Theorems
LinearWeights 📖	CompData	2 math math: instLinearWeightsOfCharZero, instLinearWeightsOfIsLieAbelian
shiftedGenWeightSpace 📖	CompOp	6 math math: shiftedGenWeightSpace.shift_apply, shiftedGenWeightSpace.instSubtypeMemLieSubmodule, shiftedGenWeightSpace.toEnd_eq, shiftedGenWeightSpace.coe_lie_shiftedGenWeightSpace_apply, shiftedGenWeightSpace.instIsNilpotentSubtypeMemLieSubmoduleOfIsNoetherian, shiftedGenWeightSpace.shift_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_forall_lie_eq_smul 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid DFunLike.coe Weight Weight.instFunLike	—	LieSubmodule.nontrivial_iff_ne_bot Weight.genWeightSpace_ne_bot LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass shiftedGenWeightSpace.instSubtypeMemLieSubmodule AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass exists_ne nontrivial_max_triv_of_isNilpotent shiftedGenWeightSpace.instIsNilpotentSubtypeMemLieSubmoduleOfIsNoetherian sub_eq_zero shiftedGenWeightSpace.coe_lie_shiftedGenWeightSpace_apply
exists_nontrivial_weightSpace_of_isNilpotent 📖	mathematical	—	Nontrivial LieSubmodule EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubmodule.instSetLike weightSpace DFunLike.coe Module.Dual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id	—	iSup_of_empty LieSubmodule.instNontrivial iSup_genWeightSpace_eq_top' exists_forall_lie_eq_smul isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule
instLinearWeightsOfCharZero 📖	mathematical	—	LinearWeights	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass IsAddTorsionFree.to_isTorsionFree_nat IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero Nat.instIsCancelMulZero LT.lt.ne' zero_lt_finrank_genWeightSpace smul_add Pi.smul_apply smulCommClass_self RingHomCompTriple.ids IsScalarTower.left LieSubmodule.instLieModule trace_comp_toEnd_genWeightSpace_eq map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass SMulCommClass.smul_comm Algebra.to_smulCommClass map_smul SemilinearMapClass.toMulActionSemiHomClass nsmul_zero LinearMap.comp_apply LieHom.coe_toLinearMap LieHom.map_lie Ring.lie_def map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.trace_mul_comm sub_self
instLinearWeightsOfIsLieAbelian 📖	mathematical	—	LinearWeights trivialIsNilpotent LieRing.toAddCommGroup lieRingSelfModule	—	trivialIsNilpotent smulCommClass_self IsScalarTower.left commute_iff_lie_eq LieHom.map_lie trivial_lie_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieHom.instLinearMapClass Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass LieSubmodule.iInf_toSubmodule Module.End.map_smul_of_iInf_genEigenspace_ne_bot SemilinearMapClass.toMulActionSemiHomClass AddRightCancelSemigroup.toIsRightCancelAdd zero_add
trace_comp_toEnd_genWeightSpace_eq 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LieAlgebra.toModule Semiring.toModule LinearMap.instFunLike LinearMap.comp LieSubmodule SetLike.instMembership LieSubmodule.instSetLike genWeightSpace AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomCompTriple.ids LinearMap.trace LieHom.toLinearMap Module.End LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra CommRing.toCommMonoid Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero toEnd LieSubmodule.instLieRingModuleSubtypeMem LieSubmodule.instLieModule AddMonoid.toNatSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.finrank	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass smulCommClass_self RingHomCompTriple.ids IsScalarTower.left LieSubmodule.instLieModule trace_toEnd_genWeightSpace nsmul_eq_mul
zero_lt_finrank_genWeightSpace 📖	mathematical	—	Module.finrank LieSubmodule SetLike.instMembership LieSubmodule.instSetLike genWeightSpace CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass Nat.cast_pos Cardinal.isOrderedRing Cardinal.instNontrivial Module.finrank_eq_rank commRing_strongRankCondition IsDomain.toNontrivial Module.IsNoetherian.finite LieSubmodule.instIsNoetherianSubtypeMem isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing rank_pos_iff_nontrivial LieSubmodule.instIsTorsionFreeSubtypeMem Module.IsReflexive.to_isTorsionFree Module.instIsReflexiveOfFiniteOfProjective Module.Projective.of_free LieSubmodule.nontrivial_iff_ne_bot

LieModule.LinearWeights

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_add 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
map_lie 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
map_smul 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid LieAlgebra.toModule Algebra.toSMul Algebra.id	—	—

LieModule.Weight

Definitions

Name	Category	Theorems
instCoeLinearMap 📖	CompOp	—
ker 📖	CompOp	4 math math: LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker
toLinear 📖	CompOp	17 math math: LieAlgebra.IsKilling.restrict_killingForm_eq_sum, LieModule.traceForm_eq_sum_finrank_nsmul', coe_coe, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', coe_toLinear_eq_zero_iff, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, LieModule.traceForm_eq_sum_finrank_nsmul, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.IsKilling.span_weight_eq_top, toLinear_neg, LieModule.range_traceForm_le_span_weight, LieAlgebra.IsKilling.rootSystem_root_apply, toLinear_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_lie 📖	mathematical	—	DFunLike.coe LieModule.Weight instFunLike Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	LieModule.LinearWeights.map_lie genWeightSpace_ne_bot
coe_coe 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id LinearMap.instFunLike toLinear LieModule.Weight instFunLike	—	—
coe_toLinear_eq_zero_iff 📖	mathematical	—	toLinear LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id LinearMap.instZero IsZero	—	LinearMap.congr_fun LinearMap.ext IsZero.eq
coe_toLinear_ne_zero_iff 📖	mathematical	—	IsNonZero	—	—
instLinearMapClass 📖	mathematical	—	LinearMapClass LieModule.Weight CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id instFunLike	—	LieModule.LinearWeights.map_add genWeightSpace_ne_bot LieModule.LinearWeights.map_smul
toLinear_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id LinearMap.instFunLike toLinear LieModule.Weight instFunLike	—	—

LieModule.shiftedGenWeightSpace

Definitions

Name	Category	Theorems
instLieRingModuleSubtypeMemLieSubmodule 📖	CompOp	4 math math: instSubtypeMemLieSubmodule, toEnd_eq, coe_lie_shiftedGenWeightSpace_apply, instIsNilpotentSubtypeMemLieSubmoduleOfIsNoetherian
shift 📖	CompOp	3 math math: shift_apply, toEnd_eq, shift_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_lie_shiftedGenWeightSpace_apply 📖	mathematical	—	LieSubmodule SetLike.instMembership LieSubmodule.instSetLike LieModule.shiftedGenWeightSpace Bracket.bracket LieRingModule.toBracket AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass instLieRingModuleSubtypeMemLieSubmodule SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	LieSubmodule.instAddSubgroupClass
instIsNilpotentSubtypeMemLieSubmoduleOfIsNoetherian 📖	mathematical	—	LieModule.IsNilpotent LieSubmodule SetLike.instMembership LieSubmodule.instSetLike LieModule.shiftedGenWeightSpace AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass instLieRingModuleSubtypeMemLieSubmodule	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass smulCommClass_self IsScalarTower.left instSubtypeMemLieSubmodule LieModule.isNilpotent_iff_forall' LieSubmodule.instIsNoetherianSubtypeMem LieModule.isNilpotent_toEnd_sub_algebraMap
instSubtypeMemLieSubmodule 📖	mathematical	—	LieModule LieSubmodule SetLike.instMembership LieSubmodule.instSetLike LieModule.shiftedGenWeightSpace AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass instLieRingModuleSubtypeMemLieSubmodule	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass trivial_lie_zero LieModule.instIsTrivialOfSubsingleton' smul_zero coe_lie_shiftedGenWeightSpace_apply smul_lie LieModule.LinearWeights.map_smul smul_assoc IsScalarTower.left smul_sub lie_smul SMulCommClass.smul_comm smulCommClass_self
shift_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LieSubmodule SetLike.instMembership LieSubmodule.instSetLike LieModule.genWeightSpace LieModule.shiftedGenWeightSpace AddCommGroup.toAddCommMonoid AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass EquivLike.toFunLike LinearEquiv.instEquivLike shift	—	RingHomInvPair.ids LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass
shift_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LieSubmodule SetLike.instMembership LieSubmodule.instSetLike LieModule.shiftedGenWeightSpace LieModule.genWeightSpace AddCommGroup.toAddCommMonoid AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm shift	—	RingHomInvPair.ids LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass
toEnd_eq 📖	mathematical	—	DFunLike.coe LieHom Module.End LieSubmodule SetLike.instMembership LieSubmodule.instSetLike LieModule.shiftedGenWeightSpace CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieModule.toEnd instLieRingModuleSubtypeMemLieSubmodule instSubtypeMemLieSubmodule LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LieModule.genWeightSpace LinearMap.addCommMonoid LinearMap.module CommSemiring.toCommMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.conj shift LinearMap.instSub LieSubmodule.instLieRingModuleSubtypeMem LieSubmodule.instLieModule LinearMap LinearMap.instSMul DistribMulAction.toDistribSMul LinearMap.id	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass smulCommClass_self IsScalarTower.left instSubtypeMemLieSubmodule

---

← Back to Index