Products of internally graded modules

The product of two internally graded modules has the componentwise grading. This supplies the grading on finite biproducts and mapping cones of curved differential graded modules. The two inclusions into the product have degree zero.

noncomputable def TauCeti.InternalGrading.prod {R : Type u} [Semiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) : InternalGrading R (M × N) ℤ

The componentwise internal grading on a product of modules.

@[simp]

theorem TauCeti.InternalGrading.prod_piece {R : Type u} [Semiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) (p : ℤ) : (G.prod H).piece ℤ p = (G.piece ℤ p).prod (H.piece ℤ p)

The degree-p piece of the product is the product of the degree-p pieces.

theorem TauCeti.InternalGrading.isHomogeneous_inl {R : Type u} [Semiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) : LinearMap.IsHomogeneous (LinearMap.inl R M N) (G.piece ℤ) ((G.prod H).piece ℤ) 0

The first inclusion into the product has degree zero.

theorem TauCeti.InternalGrading.isHomogeneous_inr {R : Type u} [Semiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) : LinearMap.IsHomogeneous (LinearMap.inr R M N) (H.piece ℤ) ((G.prod H).piece ℤ) 0

The second inclusion into the product has degree zero.