map_aeval — Mathlib

English

For a map g: σ → S1 and an algebra hom φ: S1 → B, the action φ on aeval_g(p) can be expressed as a₂ = eval₂Hom with φ ∘ algebraMap and φ(g(i)).

Русский

Для отображения g: σ → S1 и алгебра-гомоморфизма φ: S1 → B выполняется равенство φ(aeval_g(p)) = eval₂Hom(φ ∘ algebraMap, i ↦ φ(g(i)))(p).

LaTeX

$$$$ \phi( \mathrm{aeval}_g(p) ) = \mathrm{eval_2Hom}( \phi \circ \mathrm{algebraMap}, i \mapsto \phi(g(i)) )(p) $$$$

Lean4

@[simp]
theorem map_aeval {B : Type*} [CommSemiring B] (g : σ → S₁) (φ : S₁ →+* B) (p : MvPolynomial σ R) :
    φ (aeval g p) = eval₂Hom (φ.comp (algebraMap R S₁)) (fun i => φ (g i)) p :=
  by
  rw [← comp_eval₂Hom]
  rfl

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