Monomial-valued substitutions

A substitution sending every variable to a coefficient-one monomial sends each source monomial to one coefficient-one monomial. Product enrichment is the main instance: the eliminated variable is sent to X left * X right, and all previous variables remain variables.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.MonomialSubstitution.substitution {SourceVar : Type u} {TargetVar : Type v} (basis : SourceVar → TargetVar →₀ ℕ) (source : SourceVar) : MvPolynomial TargetVar ℕ

Substitute the coefficient-one monomial specified by basis for each source variable.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.MonomialSubstitution.substitution basis source = (MvPolynomial.monomial (basis source)) 1

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.MonomialSubstitution.exponentMap {SourceVar : Type u} {TargetVar : Type v} (basis : SourceVar → TargetVar →₀ ℕ) : (SourceVar →₀ ℕ) →ₗ[ℕ] TargetVar →₀ ℕ

Additive extension of the exponent images of the source variables.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.MonomialSubstitution.exponentMap basis = Finsupp.linearCombination ℕ basis

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.MonomialSubstitution.monomialExpansion_eq {SourceVar : Type u} {TargetVar : Type v} (basis : SourceVar → TargetVar →₀ ℕ) (exponent : SourceVar →₀ ℕ) : Expansion.monomialExpansion (substitution basis) exponent = (MvPolynomial.monomial ((exponentMap basis) exponent)) 1

A monomial-valued substitution expands a monomial to the monomial whose exponent vector is the linear extension of basis.

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.MonomialSubstitution.support_monomialExpansion {SourceVar : Type u} {TargetVar : Type v} (basis : SourceVar → TargetVar →₀ ℕ) (exponent : SourceVar →₀ ℕ) : (Expansion.monomialExpansion (substitution basis) exponent).support = {(exponentMap basis) exponent}

Every monomial expansion under a monomial-valued substitution has singleton support.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.MonomialSubstitution.productBasis {variableCount : ℕ} (left right : Fin variableCount) : Fin (variableCount + 1) → Fin variableCount →₀ ℕ

Exponent image for reverse substitution of the last variable by X left * X right.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.MonomialSubstitution.product_substitution_eq {variableCount : ℕ} (left right : Fin variableCount) : (fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left * MvPolynomial.X right) MvPolynomial.X i) = substitution (productBasis left right)

Reverse product substitution as a monomial-valued substitution.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.MonomialSubstitution.product_support_monomialExpansion {variableCount : ℕ} (left right : Fin variableCount) (exponent : Fin (variableCount + 1) →₀ ℕ) : (Expansion.monomialExpansion (fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left * MvPolynomial.X right) MvPolynomial.X i) exponent).support = {(exponentMap (productBasis left right)) exponent}

Product enrichment gives every source monomial exactly one expansion neighbor.