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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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 #