instAlgebraOfPolynomial — Mathlib

English

There is an algebra structure on RatFunc K induced from R-algebra structures, enabling scalar actions and compatibility with algebra maps.

Русский

Для RatFunc K существует структура алгебры, порождаемая структурами на R, обеспечивающая скалярное действие и совместимость с алгебраическими отображениями.

LaTeX

$$$\\text{RatFunc } K \\text{ inherits an } R\\text{-algebra structure from } R[X]\\text{ via localization}$$$

Lean4

instance (R : Type*) [CommSemiring R] [Algebra R K[X]] : Algebra R (RatFunc K)
    where
  algebraMap :=
    { toFun x := RatFunc.mk (algebraMap _ _ x) 1
      map_add' x y := by simp only [mk_one', RingHom.map_add, ofFractionRing_add]
      map_mul' x y := by simp only [mk_one', RingHom.map_mul, ofFractionRing_mul]
      map_one' := by simp only [mk_one', RingHom.map_one, ofFractionRing_one]
      map_zero' := by simp only [mk_one', RingHom.map_zero, ofFractionRing_zero] }
  smul := (· • ·)
  smul_def' c
    x :=
    by
    induction x using RatFunc.induction_on' with
    | _ p q hq
    rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, mk_one', ← mk_smul, mk_def_of_ne (c • p) hq, mk_def_of_ne p hq,
      ← ofFractionRing_mul, IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def]
  commutes' _ _ := mul_comm _ _

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