Commit 2024-08-17 15:02 aae0e915

View on Github →

chore(Algebra/Lie): rename weightSpace to genWeightspace (#15911) There are two variants of the concept of weight space, similar to the two concepts of eigenspace and generalized eigenspace. This PR renames weightSpace to genWeightSpace so that the name weightSpace can be reused for the version of weight spaces using non-generalized eigenspaces. Moves:

  • coe_lie_shiftedWeightSpace_apply -> coe_lie_shiftedgenWeightSpace_apply
  • coe_weightSpaceOf_zero -> coe_genWeightSpaceOf_zero
  • coe_weightSpace_of_top -> coe_genWeightSpace_of_top
  • comap_weightSpace_eq_of_injective -> comap_genWeightSpace_eq_of_injective
  • disjoint_weightSpace -> disjoint_genWeightSpace
  • disjoint_weightSpaceOf -> disjoint_genWeightSpaceOf
  • eq_zero_of_mem_weightSpace_mem_posFitting -> eq_zero_of_mem_genWeightSpace_mem_posFitting
  • eventually_weightSpace_smul_add_eq_bot -> eventually_genWeightSpace_smul_add_eq_bot
  • exists_weightSpace_le_ker_of_isNoetherian -> exists_genWeightSpace_le_ker_of_isNoetherian
  • exists_weightSpace_smul_add_eq_bot -> exists_genWeightSpace_smul_add_eq_bot
  • exists_weightSpace_zero_le_ker_of_isNoetherian -> exists_genWeightSpace_zero_le_ker_of_isNoetherian
  • exists₂_weightSpace_smul_add_eq_bot -> exists₂_genWeightSpace_smul_add_eq_bot
  • finite_weightSpaceOf_ne_bot -> finite_genWeightSpaceOf_ne_bot
  • finite_weightSpace_ne_bot -> finite_genWeightSpace_ne_bot
  • iSup_ucs_eq_weightSpace_zero -> iSup_ucs_eq_genWeightSpace_zero
  • iSup_ucs_le_weightSpace_zero -> iSup_ucs_le_genWeightSpace_zero
  • iSup_weightSpaceOf_eq_top -> iSup_genWeightSpaceOf_eq_top
  • iSup_weightSpace_eq_top -> iSup_genWeightSpace_eq_top
  • iSup_weightSpace_eq_top' -> iSup_genWeightSpace_eq_top'
  • independent_weightSpace -> independent_genWeightSpace
  • independent_weightSpace' -> independent_genWeightSpace'
  • independent_weightSpaceOf -> independent_genWeightSpaceOf
  • injOn_weightSpace -> injOn_genWeightSpace
  • isCompl_weightSpaceOf_zero_posFittingCompOf -> isCompl_genWeightSpaceOf_zero_posFittingCompOf
  • isCompl_weightSpace_zero_posFittingComp -> isCompl_genWeightSpace_zero_posFittingComp
  • isNilpotent_toEnd_weightSpace_zero -> isNilpotent_toEnd_genWeightSpace_zero
  • lie_mem_weightSpaceChain_of_weightSpace_eq_bot_left -> lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left
  • lie_mem_weightSpaceChain_of_weightSpace_eq_bot_right -> lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right
  • lie_mem_weightSpace_of_mem_weightSpace -> lie_mem_genWeightSpace_of_mem_genWeightSpace
  • map_weightSpace_eq -> map_genWeightSpace_eq
  • map_weightSpace_eq_of_injective -> map_genWeightSpace_eq_of_injective
  • map_weightSpace_le -> map_genWeightSpace_le
  • mapsTo_toEnd_weightSpace_add_of_mem_rootSpace -> mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace
  • mem_weightSpace -> mem_genWeightSpace
  • mem_weightSpaceOf -> mem_genWeightSpaceOf
  • rootSpace_comap_eq_weightSpace -> rootSpace_comap_eq_genWeightSpace
  • shiftedWeightSpace -> shiftedgenWeightSpace
  • traceForm_eq_sum_weightSpaceOf -> traceForm_eq_sum_genWeightSpaceOf
  • traceForm_weightSpace_eq -> traceForm_genWeightSpace_eq
  • trace_comp_toEnd_weightSpace_eq -> trace_comp_toEnd_genWeightSpace_eq
  • trace_toEnd_weightSpace -> trace_toEnd_genWeightSpace
  • trace_toEnd_weightSpaceChain_eq_zero -> trace_toEnd_genWeightSpaceChain_eq_zero
  • weightSpace -> genWeightSpace
  • weightSpaceChain -> genWeightSpaceChain
  • weightSpaceChain_def -> genWeightSpaceChain_def
  • weightSpaceChain_def' -> genWeightSpaceChain_def'
  • weightSpaceChain_neg -> genWeightSpaceChain_neg
  • weightSpaceOf -> genWeightSpaceOf
  • weightSpaceOf_ne_bot -> genWeightSpaceOf_ne_bot
  • weightSpace_add_chainTop -> genWeightSpace_add_chainTop
  • weightSpace_chainBotCoeff_sub_one_zsmul_sub -> genWeightSpace_chainBotCoeff_sub_one_zsmul_sub
  • weightSpace_chainTopCoeff_add_one_nsmul_add -> genWeightSpace_chainTopCoeff_add_one_nsmul_add
  • weightSpace_chainTopCoeff_add_one_zsmul_add -> genWeightSpace_chainTopCoeff_add_one_zsmul_add
  • weightSpace_le_weightSpaceChain -> genWeightSpace_le_genWeightSpaceChain
  • weightSpace_le_weightSpaceOf -> genWeightSpace_le_genWeightSpaceOf
  • weightSpace_ne_bot -> genWeightSpace_ne_bot
  • weightSpace_neg_add_chainBot -> genWeightSpace_neg_add_chainBot
  • weightSpace_neg_zsmul_add_ne_bot -> genWeightSpace_neg_zsmul_add_ne_bot
  • weightSpace_nsmul_add_ne_bot_of_le -> genWeightSpace_nsmul_add_ne_bot_of_le
  • weightSpace_weightSpaceOf_map_incl -> genWeightSpace_genWeightSpaceOf_map_incl
  • weightSpace_zero_normalizer_eq_self -> genWeightSpace_zero_normalizer_eq_self
  • weightSpace_zsmul_add_ne_bot -> genWeightSpace_zsmul_add_ne_bot
  • zero_lt_finrank_weightSpace -> zero_lt_finrank_genWeightSpace
  • zero_weightSpace_eq_top_of_nilpotent -> zero_genWeightSpace_eq_top_of_nilpotent
  • zero_weightSpace_eq_top_of_nilpotent' -> zero_genWeightSpace_eq_top_of_nilpotent'

Estimated changes

modified theorem LieModule.Weight.coe_zero
modified theorem LieModule.Weight.zero_apply
deleted theorem LieModule.mem_weightSpace