Graded pieces of an algebra tensored on the right with an algebra

For a family of submodules 𝒜 i of an R-module A and an R-module H, Mathlib's DirectSum.decomposeTensor 𝒜 H i is the image of 𝒜 i ⊗[R] H in A ⊗[R] H; it is a decomposition of A ⊗[R] H when 𝒜 is one of A. When A and H are R-algebras and 𝒜 is a graded monoid, these pieces multiply according to the grading of A: A ⊗[R] H is graded with H in degree zero.

This is the right-handed companion of Mathlib's GradedAlgebra.baseChange, which grades S ⊗[R] A by the pieces (𝒜 i).baseChange S. The right-handed form is the one met by coactions V →ₗ[R] V ⊗[R] H of comodules: an algebra homomorphism A →ₐ[R] A ⊗[R] H sending generators of degree one into the degree-one piece preserves every degree.

Main results

• TauCeti.DirectSum.tmul_mem_decomposeTensor: a pure tensor with homogeneous left factor is homogeneous of the same degree.
• TauCeti.DirectSum.decomposeTensor.gradedOne and TauCeti.DirectSum.decomposeTensor.gradedMul: tensoring preserves the unit and multiplication grading separately, without requiring a decomposition into a direct sum.
• TauCeti.DirectSum.decomposeTensor.gradedMonoid: the pieces decomposeTensor 𝒜 H i form a graded monoid.

theorem TauCeti.DirectSum.tmul_mem_decomposeTensor {ι : Type u_1} {R : Type u_2} {A : Type u_3} {H : Type u_4} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid H] [Module R H] {𝒜 : ι → Submodule R A} {i : ι} {a : A} (ha : a ∈ 𝒜 i) (h : H) : a ⊗ₜ[R] h ∈ DirectSum.decomposeTensor 𝒜 H i

A pure tensor whose left factor lies in 𝒜 i lies in the i-th piece of A ⊗[R] H.

instance TauCeti.DirectSum.decomposeTensor.gradedOne {ι : Type u_1} {R : Type u_2} {A : Type u_3} {H : Type u_4} [CommSemiring R] [AddCommMonoidWithOne A] [Module R A] [AddCommMonoidWithOne H] [Module R H] (𝒜 : ι → Submodule R A) [Zero ι] [SetLike.GradedOne 𝒜] : SetLike.GradedOne (DirectSum.decomposeTensor 𝒜 H)

If 1 : A has degree zero, so does 1 : A ⊗[R] H.

instance TauCeti.DirectSum.decomposeTensor.gradedMul {ι : Type u_1} {R : Type u_2} {A : Type u_3} {H : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring H] [Algebra R H] (𝒜 : ι → Submodule R A) [Add ι] [SetLike.GradedMul 𝒜] : SetLike.GradedMul (DirectSum.decomposeTensor 𝒜 H)

Tensoring on the right preserves graded multiplication; the index type only needs addition.

instance TauCeti.DirectSum.decomposeTensor.gradedMonoid {ι : Type u_1} {R : Type u_2} {A : Type u_3} {H : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring H] [Algebra R H] (𝒜 : ι → Submodule R A) [AddMonoid ι] [SetLike.GradedMonoid 𝒜] : SetLike.GradedMonoid (DirectSum.decomposeTensor 𝒜 H)

The pieces of A ⊗[R] H induced by a graded monoid 𝒜 on A form a graded monoid, with the right tensor factor H in degree zero.