weightedDecomposition — Mathlib

English

There exists a structured decomposition of multivariate polynomials into weight-filtered submodules, forming a DirectSum decomposition with natural projection maps given by weighted homogeneous components.

Русский

Существует структурированное разложение многочленов по весу на подмодули, образующее разложение по прямой сумме с естественными проекциями, заданными взвешенно однородными компонентами.

LaTeX

$$$\\text{WeightedDecomposition}(R,w) : \\text{DirectSum.Decomposition}(\\text{weightedHomogeneousSubmodule } R w)$$$

Lean4

/-- Given a weight `w`, the decomposition of `MvPolynomial σ R` into weighted homogeneous
submodules -/
def weightedDecomposition [DecidableEq M] : DirectSum.Decomposition (weightedHomogeneousSubmodule R w)
    where
  decompose' := decompose' R w
  left_inv
    φ := by
    classical
    conv_rhs => rw [← sum_weightedHomogeneousComponent w φ]
    rw [← DirectSum.sum_support_of (decompose' R w φ)]
    simp only [DirectSum.coeAddMonoidHom_of, map_sum, finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]
    apply Finset.sum_congr _ (fun m _ ↦ by rw [decompose'_apply])
    ext m
    simp only [DFinsupp.mem_support_toFun, ne_eq, Set.Finite.mem_toFinset, Function.mem_support, not_iff_not]
    conv_lhs => rw [← Subtype.coe_inj]
    rw [decompose'_apply, Submodule.coe_zero]
  right_inv
    x := by
    classical
    apply DFinsupp.ext
    intro m
    rw [← Subtype.coe_inj, decompose'_apply]
    exact weightedHomogeneousComponent_directSum R w x m

Похожие утверждения