Monoid algebras commute with base change #

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

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

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

Implementation detail.

Equations

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

Instances For

source

noncomputable def MonoidAlgebra.rTensorEquivAlgEquiv.invFun {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [CommSemiring R] [CommSemiring S] [CommSemiring A] [CommSemiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] [CommMonoid M] :

MonoidAlgebra (TensorProduct R A B) M →ₐ[S] 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.rTensorEquivAlgEquiv.invFun_tmul (R : Type u_1) {M : Type u_2} {S : Type u_4} (A : Type u_5) (B : Type u_6) [CommSemiring R] [CommSemiring S] [CommSemiring A] [CommSemiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] [AddCommMonoid M] (a : A) (m : M) (b : B) :

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

source

@[simp]

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

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

source

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

TensorProduct R A (MonoidAlgebra B M) ≃ₐ[S] 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.rTensorEquivAlgEquiv (R : Type u_1) {M : Type u_2} (S : Type u_4) (A : Type u_5) (B : Type u_6) [CommSemiring R] [CommSemiring S] [CommSemiring A] [CommSemiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] [AddCommMonoid M] :

TensorProduct R A (AddMonoidAlgebra B M) ≃ₐ[S] 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.rTensorEquiv_tmulAlgEquiv {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [CommSemiring R] [CommSemiring S] [CommSemiring A] [CommSemiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] [CommMonoid M] (a : A) (p : MonoidAlgebra B M) :

(rTensorEquivAlgEquiv R S A B) (a ⊗ₜ[R] p) = a • (mapAlgHom M Algebra.TensorProduct.includeRight) p

source

@[simp]

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

(rTensorEquivAlgEquiv R S A B) (a ⊗ₜ[R] p) = a • (mapAlgHom M Algebra.TensorProduct.includeRight) p

source

@[simp]

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

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

source

@[simp]

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

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

source

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

TensorProduct R (MonoidAlgebra A M) B ≃ₐ[R] 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.lTensorAlgEquiv (R : Type u_1) {M : Type u_2} (A : Type u_5) (B : Type u_6) [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] :

TensorProduct R (AddMonoidAlgebra A M) B ≃ₐ[R] 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.lTensorAlgEquiv_symm_single {R : Type u_1} {M : Type u_2} {A : Type u_5} {B : Type u_6} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [CommMonoid M] (m : M) (a : A) (b : B) :

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

source

@[simp]

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

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

source

noncomputable def MonoidAlgebra.scalarTensorEquiv (R : Type u_1) {M : Type u_2} (A : Type u_5) [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.rTensorEquivAlgEquiv R A A R).trans (MonoidAlgebra.mapAlgEquiv 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_5) [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.rTensorEquivAlgEquiv R A A R).trans (AddMonoidAlgebra.mapAlgEquiv 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_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommMonoid M] (a : A) (p : MonoidAlgebra R M) :

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

source

@[simp]

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

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

source

@[simp]

theorem MonoidAlgebra.scalarTensorEquiv_symm_single {R : Type u_1} {M : Type u_2} {A : Type u_5} [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_5} [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_4} {A : Type u_5} {B : Type u_6} [CommSemiring R] [CommSemiring S] [CommSemiring A] [CommSemiring B] [Algebra R S] [Algebra R A] [Algebra R B] [CommMonoid M] [Algebra S B] [Algebra A 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_4} {A : Type u_5} {B : Type u_6} [CommSemiring R] [CommSemiring S] [CommSemiring A] [CommSemiring B] [Algebra R S] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Algebra S B] [Algebra A 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_4} {A : Type u_5} {B : Type u_6} [CommSemiring R] [CommSemiring S] [CommSemiring A] [CommSemiring B] [Algebra R S] [Algebra R A] [Algebra R B] [CommMonoid M] [Algebra S B] [Algebra A 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_4} {A : Type u_5} {B : Type u_6} [CommSemiring R] [CommSemiring S] [CommSemiring A] [CommSemiring B] [Algebra R S] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Algebra S B] [Algebra A 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)

source

noncomputable def MonoidAlgebra.tensorEquiv (R : Type u_1) {M : Type u_2} {N : Type u_3} [CommSemiring R] :

TensorProduct R (MonoidAlgebra R M) (MonoidAlgebra R N) ≃ₗ[R] MonoidAlgebra R (M × N)

The tensor product of two monoid algebras is the monoid algebra of their product.

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} {N : Type u_3} [CommSemiring R] :

TensorProduct R (AddMonoidAlgebra R M) (AddMonoidAlgebra R N) ≃ₗ[R] AddMonoidAlgebra R (M × N)

The tensor product of two monoid algebras is the monoid algebra of their product.

Equations

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

Instances For

source

@[simp]

theorem MonoidAlgebra.coeff_tensorEquiv_apply (R : Type u_1) {M : Type u_2} {N : Type u_3} [CommSemiring R] (x : TensorProduct R (MonoidAlgebra R M) (MonoidAlgebra R N)) :

((tensorEquiv R) x).coeff = (finsuppTensorFinsupp' R M N) ((TensorProduct.congr (coeffLinearEquiv R) (coeffLinearEquiv R)) x)

source

@[simp]

theorem AddMonoidAlgebra.coeff_tensorEquiv_apply (R : Type u_1) {M : Type u_2} {N : Type u_3} [CommSemiring R] (x : TensorProduct R (AddMonoidAlgebra R M) (AddMonoidAlgebra R N)) :

((tensorEquiv R) x).coeff = (finsuppTensorFinsupp' R M N) ((TensorProduct.congr (coeffLinearEquiv R) (coeffLinearEquiv R)) x)

source

@[simp]

theorem MonoidAlgebra.tensorEquiv_single_tmul_single {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (m : M) (r₁ : R) (n : N) (r₂ : R) :

(tensorEquiv R) (single m r₁ ⊗ₜ[R] single n r₂) = single (m, n) (r₁ * r₂)

source

@[simp]

theorem AddMonoidAlgebra.tensorEquiv_single_tmul_single {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (m : M) (r₁ : R) (n : N) (r₂ : R) :

(tensorEquiv R) (single m r₁ ⊗ₜ[R] single n r₂) = single (m, n) (r₁ * r₂)

source

theorem MonoidAlgebra.tensorEquiv_symm_single_eq_single_one_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (mn : M × N) (r : R) :

(tensorEquiv R).symm (single mn r) = single mn.1 1 ⊗ₜ[R] single mn.2 r

source

theorem AddMonoidAlgebra.tensorEquiv_symm_single_eq_single_zero_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (mn : M × N) (r : R) :

(tensorEquiv R).symm (single mn r) = single mn.1 1 ⊗ₜ[R] single mn.2 r

source

theorem MonoidAlgebra.tensorEquiv_symm_single_eq_tmul_single_one {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (mn : M × N) (r : R) :

(tensorEquiv R).symm (single mn r) = single mn.1 r ⊗ₜ[R] single mn.2 1

source

theorem AddMonoidAlgebra.tensorEquiv_symm_single_eq_tmul_single_zero {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (mn : M × N) (r : R) :

(tensorEquiv R).symm (single mn r) = single mn.1 r ⊗ₜ[R] single mn.2 1

Documentation

Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Monoid algebras commute with base change #