algebraPi — Mathlib

English

There is an algebra structure on the function space S → T extending the Pi-action via (p, f) ↦ (x ↦ algebraMap_S_T (aeval x p) · f x).

Русский

Существует структура алгебры на пространстве функций S → T, расширяющая действие Pi через (p, f) → (x ↦ algebraMap_S_T (aeval x p) · f x).

LaTeX

$$$$\text{algebraPi} : \text{Algebra } R[X] (S \to T) \text{ with } (p,f) \mapsto (x \mapsto \operatorname{algebraMap}_S^T(\operatorname{aeval}(x,p)) \cdot f(x)). $$$$

Lean4

/-- This is not an instance for the same reasons as `Polynomial.hasSMulPi'`. -/
noncomputable def algebraPi : Algebra R[X] (S → T)
    where
  __ := Polynomial.hasSMulPi' R S T
  algebraMap :=
    { toFun p z := algebraMap S T (aeval z p)
      map_one' := funext fun z => by simp only [Pi.one_apply, map_one]
      map_mul' _ _ := funext fun z => by simp only [Pi.mul_apply, map_mul]
      map_zero' := funext fun z => by simp only [Pi.zero_apply, map_zero]
      map_add' _ _ := funext fun z => by simp only [Pi.add_apply, map_add] }
  commutes' _ _ := funext fun z => by exact mul_comm _ _
  smul_def' _
    _ :=
    funext fun z => by
      simp only [polynomial_smul_apply', Algebra.algebraMap_eq_smul_one, RingHom.coe_mk, MonoidHom.coe_mk,
        OneHom.coe_mk, Pi.mul_apply, Algebra.smul_mul_assoc, one_mul]

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