Total degree and balanced reassociation #
The balanced associator preserves total degree for a right B-module, a (B,C)-bimodule,
and a left C-module. Neither endpoint needs a second action. Consequently reassociation
restricts to each homogeneous piece, as required for tensor composition of DG modules.
The carrier map is BalancedTensorProduct.assoc; no new associator is constructed here.
The grading convention follows B. Keller, Deriving DG categories, Section 6.1.
theorem
TauCeti.BalancedTensorProduct.isHomogeneous_assoc
{R : Type u_1}
{B : Type u_2}
{C : Type u_3}
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[CommRing R]
[Semiring B]
[Semiring C]
[Module R B]
[Module R C]
[AddCommGroup M]
[Module R M]
[Module Bᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module B N]
[Module Cᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module C P]
[SMulCommClass B R N]
[SMulCommClass Cᵐᵒᵖ R N]
[SMulCommClass B Cᵐᵒᵖ N]
{ℬ : ℤ → Submodule R B}
{𝒞 : ℤ → Submodule R C}
[DirectSum.Decomposition ℬ]
[DirectSum.Decomposition 𝒞]
(G : InternalGrading R M ℤ)
(H : InternalGrading R N ℤ)
(I : InternalGrading R P ℤ)
[SetLike.GradedSMul ((InternalGrading.ofDecomposition ℬ).opposite.piece ℤ) (G.piece ℤ)]
[SetLike.GradedSMul ℬ (H.piece ℤ)]
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒞).opposite.piece ℤ) (H.piece ℤ)]
[SetLike.GradedSMul 𝒞 (I.piece ℤ)]
:
Balanced reassociation preserves the sum of the three input degrees.
theorem
TauCeti.BalancedTensorProduct.isHomogeneous_assoc_symm
{R : Type u_1}
{B : Type u_2}
{C : Type u_3}
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[CommRing R]
[Semiring B]
[Semiring C]
[Module R B]
[Module R C]
[AddCommGroup M]
[Module R M]
[Module Bᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module B N]
[Module Cᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module C P]
[SMulCommClass B R N]
[SMulCommClass Cᵐᵒᵖ R N]
[SMulCommClass B Cᵐᵒᵖ N]
{ℬ : ℤ → Submodule R B}
{𝒞 : ℤ → Submodule R C}
[DirectSum.Decomposition ℬ]
[DirectSum.Decomposition 𝒞]
(G : InternalGrading R M ℤ)
(H : InternalGrading R N ℤ)
(I : InternalGrading R P ℤ)
[SetLike.GradedSMul ((InternalGrading.ofDecomposition ℬ).opposite.piece ℤ) (G.piece ℤ)]
[SetLike.GradedSMul ℬ (H.piece ℤ)]
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒞).opposite.piece ℤ) (H.piece ℤ)]
[SetLike.GradedSMul 𝒞 (I.piece ℤ)]
:
The inverse balanced associator also preserves total degree.
theorem
TauCeti.BalancedTensorProduct.map_assoc_grading_piece
{R : Type u_1}
{B : Type u_2}
{C : Type u_3}
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[CommRing R]
[Semiring B]
[Semiring C]
[Module R B]
[Module R C]
[AddCommGroup M]
[Module R M]
[Module Bᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module B N]
[Module Cᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module C P]
[SMulCommClass B R N]
[SMulCommClass Cᵐᵒᵖ R N]
[SMulCommClass B Cᵐᵒᵖ N]
{ℬ : ℤ → Submodule R B}
{𝒞 : ℤ → Submodule R C}
[DirectSum.Decomposition ℬ]
[DirectSum.Decomposition 𝒞]
(G : InternalGrading R M ℤ)
(H : InternalGrading R N ℤ)
(I : InternalGrading R P ℤ)
[SetLike.GradedSMul ((InternalGrading.ofDecomposition ℬ).opposite.piece ℤ) (G.piece ℤ)]
[SetLike.GradedSMul ℬ (H.piece ℤ)]
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒞).opposite.piece ℤ) (H.piece ℤ)]
[SetLike.GradedSMul 𝒞 (I.piece ℤ)]
(p : ℤ)
:
Reassociation maps each total-degree piece onto the piece of the same degree.
This is not a simp lemma, since grading_piece already rewrites its left-hand side.