@[reducible, inline]

noncomputable abbrev MonoidAlgebra.algebraMonoidAlgebra {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] : Algebra (MonoidAlgebra R M) (MonoidAlgebra S M)

If S is an R-algebra, then MonoidAlgebra S σ is a MonoidAlgebra R σ algebra.

Warning: This produces a diamond for Algebra (MonoidAlgebra R σ) (MonoidAlgebra (MonoidAlgebra S σ) σ). That's why it is not a global instance.

Equations

• MonoidAlgebra.algebraMonoidAlgebra = (MonoidAlgebra.mapRangeRingHom M (algebraMap R S)).toAlgebra

@[simp]

theorem MonoidAlgebra.algebraMap_def {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] : algebraMap (MonoidAlgebra R M) (MonoidAlgebra S M) = mapRangeRingHom M (algebraMap R S)

instance MonoidAlgebra.instIsScalarTower_toric {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] {T : Type u_4} [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] : IsScalarTower R (MonoidAlgebra S M) (MonoidAlgebra T M)