English
Let ι be an index set and for every i an associated finite set monoms(i) of exponent vectors. Consider the family p = (p_i) of multivariate polynomials over κ in R such that each p_i has support contained in monoms(i). Then this family is in bijection with functions from the disjoint sum Σ_i monoms(i) to R, given by reading off the coefficients of p_i. In other words, specifying all the coefficients of the p_i uniquely determines the family, and conversely.
Русский
Пусть есть множество индексов ι и для каждого i задано конечное множество monoms(i) множителей экспонент. Рассматривать семью p = (p_i) многочладов mv над κ в R таких, что поддержка p_i ⊆ monoms(i). Тогда такая семья задаётся взаимно однозначно функциями из дизъюнкции Σ_i monoms(i) в R по коэффициентам: чтение коэффициентов даёт представление семьи, и наоборот.
LaTeX
$$$\\left\\{ p : ι \\to \\mathrm{MvPolynomial}_{\\kappa,R} \\\\mid \\forall i, \\operatorname{Supp}(p(i)) \\subseteq \\operatorname{monoms}(i) \\right\\} \\cong \\bigl((\\Sigma i, \\operatorname{monoms}(i)) \\to R\\bigr)$$$
Lean4
/-- Collections of `MvPolynomial`s, `p : ι → MvPolynomial κ R` such
that `∀ i, (p i).support ⊆ monoms i` can be identified with functions
`(Σ i, monoms i) → R` by using the coefficient function -/
noncomputable def mvPolynomialSupportLEEquiv [DecidableEq κ] [CommRing R] [DecidableEq R]
(monoms : ι → Finset (κ →₀ ℕ)) :
{ p : ι → MvPolynomial κ R // ∀ i, (p i).support ⊆ monoms i } ≃ ((Σ i, monoms i) → R) :=
{ toFun := fun p i => (p.1 i.1).coeff i.2,
invFun := fun p =>
⟨fun i =>
{ toFun := fun m => if hm : m ∈ monoms i then p ⟨i, ⟨m, hm⟩⟩ else 0
support := {m ∈ monoms i | ∃ hm : m ∈ monoms i, p ⟨i, ⟨m, hm⟩⟩ ≠ 0}, mem_support_toFun := by simp }, fun i =>
Finset.filter_subset _ _⟩,
left_inv := fun p => by
ext i m
simp only [coeff, ne_eq, exists_prop, dite_eq_ite, Finsupp.coe_mk, ite_eq_left_iff]
intro hm
have : m ∉ (p.1 i).support := fun h => hm (p.2 i h)
simpa [coeff, eq_comm, MvPolynomial.mem_support_iff] using this
right_inv := fun p => by ext; simp [coeff] }
