Monoid algebras commute with base change #

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

TODO #

Additivise

noncomputable def AddMonoidAlgebra.tensorEquiv.invFun {R : Type u_1} {M : Type u_2} {A : Type u_4} {B : Type u_5} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] :

AddMonoidAlgebra (TensorProduct R A B) M →ₐ[A] TensorProduct R A (AddMonoidAlgebra B M)

Implementation detail.

Equations

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

Instances For

source

def MonoidAlgebra.tensorEquiv.invFun {R : Type u_1} {M : Type u_2} {A : Type u_4} {B : Type u_5} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [CommMonoid M] :

MonoidAlgebra (TensorProduct R A B) M →ₐ[A] TensorProduct R A (MonoidAlgebra B M)

Implementation detail.

Equations

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

Instances For

source

@[simp]

theorem AddMonoidAlgebra.tensorEquiv.invFun_tmul (R : Type u_1) {M : Type u_2} (A : Type u_4) (B : Type u_5) [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] (a : A) (m : M) (b : B) :

invFun (MonoidAlgebra.single m (a ⊗ₜ[R] b)) = a ⊗ₜ[R] MonoidAlgebra.single m b

source

@[simp]

theorem MonoidAlgebra.tensorEquiv.invFun_tmul {R : Type u_1} {M : Type u_2} {A : Type u_4} {B : Type u_5} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [CommMonoid M] (a : A) (m : M) (b : B) :

invFun (single m (a ⊗ₜ[R] b)) = a ⊗ₜ[R] single m b

source

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

TensorProduct R A (MonoidAlgebra B M) ≃ₐ[A] MonoidAlgebra (TensorProduct R A B) M

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

Equations

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

Instances For

source

noncomputable def AddMonoidAlgebra.tensorEquiv (R : Type u_1) {M : Type u_2} (A : Type u_4) (B : Type u_5) [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] :

TensorProduct R A (AddMonoidAlgebra B M) ≃ₐ[A] AddMonoidAlgebra (TensorProduct R A B) M

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

Equations

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

Instances For

source

@[simp]

theorem MonoidAlgebra.tensorEquiv_tmul {R : Type u_1} {M : Type u_2} {A : Type u_4} {B : Type u_5} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [CommMonoid M] (a : A) (p : MonoidAlgebra B M) :

(tensorEquiv R A B) (a ⊗ₜ[R] p) = a • (mapRangeAlgHom M Algebra.TensorProduct.includeRight) p

source

@[simp]

theorem AddMonoidAlgebra.tensorEquiv_tmul {R : Type u_1} {M : Type u_2} {A : Type u_4} {B : Type u_5} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] (a : A) (p : AddMonoidAlgebra B M) :

(tensorEquiv R A B) (a ⊗ₜ[R] p) = a • (mapRangeAlgHom M Algebra.TensorProduct.includeRight) p

source

@[simp]

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

(tensorEquiv R A B).symm (single m (a ⊗ₜ[R] b)) = a ⊗ₜ[R] single m b

source

@[simp]

theorem AddMonoidAlgebra.tensorEquiv_symm_single {R : Type u_1} {M : Type u_2} {A : Type u_4} {B : Type u_5} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] (m : M) (a : A) (b : B) :

(tensorEquiv R A B).symm (single m (a ⊗ₜ[R] b)) = a ⊗ₜ[R] single m b

source

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

TensorProduct R A (MonoidAlgebra R M) ≃ₐ[A] MonoidAlgebra A M

The base change of R[M] to an R-algebra A is isomorphic to 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))

Instances For

source

noncomputable def AddMonoidAlgebra.scalarTensorEquiv (R : Type u_1) {M : Type u_2} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] :

TensorProduct R A (AddMonoidAlgebra R M) ≃ₐ[A] AddMonoidAlgebra A M

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

Equations

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

Instances For

source

@[simp]

theorem MonoidAlgebra.scalarTensorEquiv_tmul {R : Type u_1} {M : Type u_2} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommMonoid M] (a : A) (p : MonoidAlgebra R M) :

(scalarTensorEquiv R A) (a ⊗ₜ[R] p) = a • (mapRangeAlgHom M (Algebra.ofId R A)) p

source

@[simp]

theorem AddMonoidAlgebra.scalarTensorEquiv_tmul {R : Type u_1} {M : Type u_2} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] (a : A) (p : AddMonoidAlgebra R M) :

(scalarTensorEquiv R A) (a ⊗ₜ[R] p) = a • (mapRangeAlgHom M (Algebra.ofId R A)) p

source

@[simp]

theorem MonoidAlgebra.scalarTensorEquiv_symm_single {R : Type u_1} {M : Type u_2} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommMonoid M] (m : M) (a : A) :

(scalarTensorEquiv R A).symm (single m a) = a ⊗ₜ[R] single m 1

source

@[simp]

theorem AddMonoidAlgebra.scalarTensorEquiv_symm_single {R : Type u_1} {M : Type u_2} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] (m : M) (a : A) :

(scalarTensorEquiv R A).symm (single m a) = a ⊗ₜ[R] single m 1

source

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] [CommSemiring A] [CommSemiring B] [Algebra R S] [Algebra R A] [CommMonoid M] [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)

source

instance AddMonoidAlgebra.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] [CommSemiring A] [CommSemiring B] [Algebra R S] [Algebra R A] [AddCommMonoid M] [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 (AddMonoidAlgebra A M) (AddMonoidAlgebra B M)

source

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] [CommSemiring A] [CommSemiring B] [Algebra R S] [Algebra R A] [CommMonoid M] [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)

source

instance AddMonoidAlgebra.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] [CommSemiring A] [CommSemiring B] [Algebra R S] [Algebra R A] [AddCommMonoid M] [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 (AddMonoidAlgebra A M) S (AddMonoidAlgebra B M)

Documentation

Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Monoid algebras commute with base change #

TODO #