Monoid algebras commute with base change

In this file we show that monoid algebras are stable under pushout.

TODO

Additivise

noncomputable def MonoidAlgebra.tensorEquiv (R : Type u_1) {M : Type u_2} (A : Type u_4) (B : Type u_5) [CommSemiring R] [CommMonoid M] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] : TensorProduct R A (MonoidAlgebra B M) ≃ₐ[A] MonoidAlgebra (TensorProduct R A B) M

The base change of MonoidAlgebra B M to an R-algebra A is isomorphic to MonoidAlgebra (A ⊗[R] B) M as an A-algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MonoidAlgebra.tensorEquiv_tmul {R : Type u_1} {M : Type u_2} {A : Type u_4} {B : Type u_5} [CommSemiring R] [CommMonoid M] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] (a : A) (p : MonoidAlgebra B M) : (tensorEquiv R A B) (a ⊗ₜ[R] p) = a • (mapRangeAlgHom M Algebra.TensorProduct.includeRight) p

@[simp]

theorem MonoidAlgebra.tensorEquiv_symm_single {R : Type u_1} {M : Type u_2} {A : Type u_4} {B : Type u_5} [CommSemiring R] [CommMonoid M] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] (m : M) (a : A) (b : B) : (tensorEquiv R A B).symm (single m (a ⊗ₜ[R] b)) = a ⊗ₜ[R] single m b

noncomputable def MonoidAlgebra.scalarTensorEquiv (R : Type u_1) {M : Type u_2} (A : Type u_4) [CommSemiring R] [CommMonoid M] [CommSemiring A] [Algebra R A] : TensorProduct R A (MonoidAlgebra R M) ≃ₐ[A] MonoidAlgebra A M

The base change of MonoidAlgebra R M to an R-algebra A is isomorphic to MonoidAlgebra A M as an A-algebra.

Equations

• MonoidAlgebra.scalarTensorEquiv R A = (MonoidAlgebra.tensorEquiv R A R).trans (MonoidAlgebra.mapRangeAlgEquiv A M (Algebra.TensorProduct.rid R A A))

@[simp]

theorem MonoidAlgebra.scalarTensorEquiv_tmul {R : Type u_1} {M : Type u_2} {A : Type u_4} [CommSemiring R] [CommMonoid M] [CommSemiring A] [Algebra R A] (a : A) (p : MonoidAlgebra R M) : (scalarTensorEquiv R A) (a ⊗ₜ[R] p) = a • (mapRangeAlgHom M (Algebra.ofId R A)) p

@[simp]

theorem MonoidAlgebra.scalarTensorEquiv_symm_single {R : Type u_1} {M : Type u_2} {A : Type u_4} [CommSemiring R] [CommMonoid M] [CommSemiring A] [Algebra R A] (m : M) (a : A) : (scalarTensorEquiv R A).symm (single m a) = a ⊗ₜ[R] single m 1

instance MonoidAlgebra.instIsPushout {R : Type u_1} {M : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] [CommMonoid M] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra S B] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] : Algebra.IsPushout R S (MonoidAlgebra A M) (MonoidAlgebra B M)

instance MonoidAlgebra.instIsPushout_1 {R : Type u_1} {M : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] [CommMonoid M] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra S B] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R A S B] : Algebra.IsPushout R (MonoidAlgebra A M) S (MonoidAlgebra B M)