ofComp_toAlgHom_monomial_sumElim — Mathlib

English

A refined identity expresses the compatibility of toComp with monomial maps under a sumElim decomposition.

Русский

Уточнённое тождество согласованности toComp с мономиалами через разложение sumElim.

LaTeX

$$$ (Q.ofComp P).toAlgHom (\\mathrm{monomial}(\\mathrm{Finsupp.sumElim}(v_1,v_2))\\, a) = \\mathrm{monomial}(v_1)(aeval_P(\\mathrm{monomial}(v_2)\\, a)) $$$

Lean4

theorem ofComp_toAlgHom_monomial_sumElim (Q : Generators S T ι') (P : Generators R S ι) (v₁ v₂ a) :
    (Q.ofComp P).toAlgHom (monomial (Finsupp.sumElim v₁ v₂) a) = monomial v₁ (aeval P.val (monomial v₂ a)) :=
  by
  rw [Hom.toAlgHom_monomial, monomial_eq]
  simp only [ofComp_val, aeval_monomial]
  rw [Finsupp.prod_sumElim]
  simp only [Function.comp_def, Sum.elim_inl, Sum.elim_inr, ← map_pow, ← map_finsuppProd, C_mul, Algebra.smul_def,
    MvPolynomial.algebraMap_apply, mul_assoc]
  nth_rw 2 [mul_comm]

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