Associativity of the graded bimodule action on left modules

For graded algebras A, B, and C, tensor composition and the left-module action identify (M tensor_B N) tensor_C P with M tensor_B (N tensor_C P), where M and N are graded bimodules and P is a graded left C-module. The comparison transports the existing balanced carrier associator and preserves the output left A-action and total internal grading.

The graded construction adapts TauCeti.Algebra.Category.GradedModuleCat.BimoduleTensor.Associator to left modules. The degree-preservation argument reuses the homogeneous balanced associator in TauCeti.LinearAlgebra.TensorProduct.Balanced.Grading.Associator.

Both directions compute on nested pure tensors, and reassociation is natural in all three maps. The trifunctor comparison supplies the associator for complex totalization; any cohomological Koszul signs come from totalization, rather than the internal grading.

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorAssociator {k : Type uk} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing k] [Ring A] [Ring B] [Ring C] [Algebra k A] [Algebra k B] [Algebra k C] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (P : GradedModuleCat (Θ.piece ℤ)) : bimoduleModuleTensorObj Γ Θ (bimoduleTensorObj Γ Δ Θ M N) P ≅ bimoduleModuleTensorObj Γ Δ M (bimoduleModuleTensorObj Δ Θ N P)

Reassociate two graded bimodules acting on a graded left module.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorAssociator_hom_tmul {k : Type uk} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing k] [Ring A] [Ring B] [Ring C] [Algebra k A] [Algebra k B] [Algebra k C] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (P : GradedModuleCat (Θ.piece ℤ)) (m : M.carrier) (n : N.carrier) (p : P.carrier) : (bimoduleModuleTensorAssociator Γ Δ Θ M N P).hom.hom (bimoduleModuleTensorTmul Γ Θ (bimoduleTensorObj Γ Δ Θ M N) P (bimoduleTensorTmul Γ Δ Θ M N m n) p) = bimoduleModuleTensorTmul Γ Δ M (bimoduleModuleTensorObj Δ Θ N P) m (bimoduleModuleTensorTmul Δ Θ N P n p)

Reassociation changes only the parentheses of a nested pure tensor.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorAssociator_inv_tmul {k : Type uk} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing k] [Ring A] [Ring B] [Ring C] [Algebra k A] [Algebra k B] [Algebra k C] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (P : GradedModuleCat (Θ.piece ℤ)) (m : M.carrier) (n : N.carrier) (p : P.carrier) : (bimoduleModuleTensorAssociator Γ Δ Θ M N P).inv.hom (bimoduleModuleTensorTmul Γ Δ M (bimoduleModuleTensorObj Δ Θ N P) m (bimoduleModuleTensorTmul Δ Θ N P n p)) = bimoduleModuleTensorTmul Γ Θ (bimoduleTensorObj Γ Δ Θ M N) P (bimoduleTensorTmul Γ Δ Θ M N m n) p

The inverse associator restores the original nested pure tensor.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorAssociator_naturality {k : Type uk} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing k] [Ring A] [Ring B] [Ring C] [Algebra k A] [Algebra k B] [Algebra k C] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (P : GradedModuleCat (Θ.piece ℤ)) {M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N' : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} {P' : GradedModuleCat (Θ.piece ℤ)} (f : M ⟶ M') (g : N ⟶ N') (h : P ⟶ P') : CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorMap Γ Θ (bimoduleTensorMap Γ Δ Θ f g) h) (bimoduleModuleTensorAssociator Γ Δ Θ M' N' P').hom = CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorAssociator Γ Δ Θ M N P).hom (bimoduleModuleTensorMap Γ Δ f (bimoduleModuleTensorMap Δ Θ g h))

Reassociation is natural in each bimodule and the left module.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorAssociator_naturality_assoc {k : Type uk} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing k] [Ring A] [Ring B] [Ring C] [Algebra k A] [Algebra k B] [Algebra k C] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (P : GradedModuleCat (Θ.piece ℤ)) {M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N' : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} {P' : GradedModuleCat (Θ.piece ℤ)} (f : M ⟶ M') (g : N ⟶ N') (h : P ⟶ P') {Z : GradedModuleCat (Γ.piece ℤ)} (h✝ : bimoduleModuleTensorObj Γ Δ M' (bimoduleModuleTensorObj Δ Θ N' P') ⟶ Z) : CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorMap Γ Θ (bimoduleTensorMap Γ Δ Θ f g) h) (CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorAssociator Γ Δ Θ M' N' P').hom h✝) = CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorAssociator Γ Δ Θ M N P).hom (CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorMap Γ Δ f (bimoduleModuleTensorMap Δ Θ g h)) h✝)

Reassociation is natural in each bimodule and the left module.

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorAssociatorNatIso {k : Type uk} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing k] [Ring A] [Ring B] [Ring C] [Algebra k A] [Algebra k B] [Algebra k C] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] : CategoryTheory.bifunctorComp₁₂ (bimoduleTensor Γ Δ Θ) (bimoduleModuleTensor Γ Θ) ≅ CategoryTheory.bifunctorComp₂₃ (bimoduleModuleTensor Γ Δ) (bimoduleModuleTensor Δ Θ)

The action associator as an isomorphism between the two tensor trifunctors.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorAssociatorNatIso_hom_app {k : Type uk} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing k] [Ring A] [Ring B] [Ring C] [Algebra k A] [Algebra k B] [Algebra k C] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (P : GradedModuleCat (Θ.piece ℤ)) : (((bimoduleModuleTensorAssociatorNatIso Γ Δ Θ).hom.app M).app N).app P = (bimoduleModuleTensorAssociator Γ Δ Θ M N P).hom

Each forward trifunctor component is the graded associator.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorAssociatorNatIso_hom_app_assoc {k : Type uk} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing k] [Ring A] [Ring B] [Ring C] [Algebra k A] [Algebra k B] [Algebra k C] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (P : GradedModuleCat (Θ.piece ℤ)) {Z : GradedModuleCat (Γ.piece ℤ)} (h : (((CategoryTheory.bifunctorComp₂₃ (bimoduleModuleTensor Γ Δ) (bimoduleModuleTensor Δ Θ)).obj M).obj N).obj P ⟶ Z) : CategoryTheory.CategoryStruct.comp ((((bimoduleModuleTensorAssociatorNatIso Γ Δ Θ).hom.app M).app N).app P) h = CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorAssociator Γ Δ Θ M N P).hom h

Each forward trifunctor component is the graded associator.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorAssociatorNatIso_inv_app {k : Type uk} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing k] [Ring A] [Ring B] [Ring C] [Algebra k A] [Algebra k B] [Algebra k C] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (P : GradedModuleCat (Θ.piece ℤ)) : (((bimoduleModuleTensorAssociatorNatIso Γ Δ Θ).inv.app M).app N).app P = (bimoduleModuleTensorAssociator Γ Δ Θ M N P).inv

Each reverse trifunctor component is the inverse graded associator.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorAssociatorNatIso_inv_app_assoc {k : Type uk} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing k] [Ring A] [Ring B] [Ring C] [Algebra k A] [Algebra k B] [Algebra k C] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (P : GradedModuleCat (Θ.piece ℤ)) {Z : GradedModuleCat (Γ.piece ℤ)} (h : (((CategoryTheory.bifunctorComp₁₂ (bimoduleTensor Γ Δ Θ) (bimoduleModuleTensor Γ Θ)).obj M).obj N).obj P ⟶ Z) : CategoryTheory.CategoryStruct.comp ((((bimoduleModuleTensorAssociatorNatIso Γ Δ Θ).inv.app M).app N).app P) h = CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorAssociator Γ Δ Θ M N P).inv h

Each reverse trifunctor component is the inverse graded associator.