English
If A is a commutative semiring and an R-algebra, then the free algebra FreeAlgebra A X carries a natural structure of an R-algebra.
Русский
Если A — коммутативное полукольцо и A обладает структурой R-алгебры, то свободная алгебра FreeAlgebra A X естественно является R-алгеброй.
LaTeX
$$$\mathrm{FreeAlgebra}(A,X)$ carries an $R$-algebra structure.$$
Lean4
instance instAlgebra {A} [CommSemiring A] [Algebra R A] : Algebra R (FreeAlgebra A X)
where
algebraMap :=
({ toFun := fun r => Quot.mk _ r
map_one' := rfl
map_mul' := fun _ _ => Quot.sound Rel.mul_scalar
map_zero' := rfl
map_add' := fun _ _ => Quot.sound Rel.add_scalar } : A →+* FreeAlgebra A X).comp (algebraMap R A)
commutes'
_ := by
rintro ⟨⟩
exact Quot.sound Rel.central_scalar
smul_def' _ _ := rfl
