English
Same as 181025: the coordinate-wise formula for the direct-sum decomposition of weighted homogeneous components.
Русский
То же, что и 181025: покоординатное формула разложения по прямой сумме взвешенных однородных компонент.
LaTeX
$$$weightedHomogeneousComponent\, w\, m\, ((DirectSum.coeLinearMap\, w)\, x) = x\, m$$$
Lean4
theorem weightedHomogeneousComponent_directSum [DecidableEq M]
(x : DirectSum M fun i : M => ↥(weightedHomogeneousSubmodule R w i)) (m : M) :
(weightedHomogeneousComponent w m) ((DirectSum.coeLinearMap fun i : M => weightedHomogeneousSubmodule R w i) x) =
x m :=
by
classical
rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, map_sum]
convert @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _
· rw [IsWeightedHomogeneous.weightedHomogeneousComponent_same (x m).prop]
· intro n _ hmn
exact IsWeightedHomogeneous.weightedHomogeneousComponent_ne m (x n).prop hmn.symm
· rw [DFinsupp.notMem_support_iff]
intro hm; rw [hm, Submodule.coe_zero, map_zero]
