Coherence for graded bimodule tensor composition

The associator of graded bimodule composition satisfies the pentagon, including heterogeneous composition over five graded algebras. With the regular bimodule as unit, it also satisfies the triangle. Both equations follow from pure-tensor extensionality; the triangle is precisely the balancing relation.

For endobimodules these identities package the existing tensor maps, associator, and unitors into bimoduleMonoidalCategory. The structure is chosen explicitly so its factor grading and carrier universe remain visible. Its curried tensor functor is the existing bimoduleTensor.

The module also provides GradedBimoduleMonoidalDatum, the pointwise homotopy-monoidal datum of a functor on complexes of graded bimodules: for every pair of source complexes X and Y, a homotopy equivalence comparing the target tensor product of the image complexes with the image of the source tensor product. It is the monoidal compatibility data that such a functor has to supply.

theorem TauCeti.GradedModuleCat.bimoduleTensorAssociator_pentagon {k : Type uk} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} {E : Type uE} [CommRing k] [Ring A] [Ring B] [Ring C] [Ring D] [Ring E] [Algebra k A] [Algebra k B] [Algebra k C] [Algebra k D] [Algebra k E] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) (Ψ : InternalGrading k D ℤ) (Ω : InternalGrading k E ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] [GradedAlgebra (Ψ.piece ℤ)] [GradedAlgebra (Ω.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (P : GradedModuleCat ((Θ.tensorProduct Ψ.opposite).piece ℤ)) (Q : GradedModuleCat ((Ψ.tensorProduct Ω.opposite).piece ℤ)) : CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Ψ Ω (bimoduleTensorAssociator Γ Δ Θ Ψ M N P).hom (CategoryTheory.CategoryStruct.id Q)) (CategoryTheory.CategoryStruct.comp (bimoduleTensorAssociator Γ Δ Ψ Ω M (bimoduleTensorObj Δ Θ Ψ N P) Q).hom (bimoduleTensorMap Γ Δ Ω (CategoryTheory.CategoryStruct.id M) (bimoduleTensorAssociator Δ Θ Ψ Ω N P Q).hom)) = CategoryTheory.CategoryStruct.comp (bimoduleTensorAssociator Γ Θ Ψ Ω (bimoduleTensorObj Γ Δ Θ M N) P Q).hom (bimoduleTensorAssociator Γ Δ Θ Ω M N (bimoduleTensorObj Θ Ψ Ω P Q)).hom

Reassociation of four graded bimodules satisfies the pentagon.

theorem TauCeti.GradedModuleCat.bimoduleTensorAssociator_pentagon_assoc {k : Type uk} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} {E : Type uE} [CommRing k] [Ring A] [Ring B] [Ring C] [Ring D] [Ring E] [Algebra k A] [Algebra k B] [Algebra k C] [Algebra k D] [Algebra k E] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) (Ψ : InternalGrading k D ℤ) (Ω : InternalGrading k E ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] [GradedAlgebra (Ψ.piece ℤ)] [GradedAlgebra (Ω.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (P : GradedModuleCat ((Θ.tensorProduct Ψ.opposite).piece ℤ)) (Q : GradedModuleCat ((Ψ.tensorProduct Ω.opposite).piece ℤ)) {Z : GradedModuleCat ((Γ.tensorProduct Ω.opposite).piece ℤ)} (h : bimoduleTensorObj Γ Δ Ω M (bimoduleTensorObj Δ Θ Ω N (bimoduleTensorObj Θ Ψ Ω P Q)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Ψ Ω (bimoduleTensorAssociator Γ Δ Θ Ψ M N P).hom (CategoryTheory.CategoryStruct.id Q)) (CategoryTheory.CategoryStruct.comp (bimoduleTensorAssociator Γ Δ Ψ Ω M (bimoduleTensorObj Δ Θ Ψ N P) Q).hom (CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Δ Ω (CategoryTheory.CategoryStruct.id M) (bimoduleTensorAssociator Δ Θ Ψ Ω N P Q).hom) h)) = CategoryTheory.CategoryStruct.comp (bimoduleTensorAssociator Γ Θ Ψ Ω (bimoduleTensorObj Γ Δ Θ M N) P Q).hom (CategoryTheory.CategoryStruct.comp (bimoduleTensorAssociator Γ Δ Θ Ω M N (bimoduleTensorObj Θ Ψ Ω P Q)).hom h)

Reassociation of four graded bimodules satisfies the pentagon.

theorem TauCeti.GradedModuleCat.bimoduleTensorAssociator_triangle {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 ℤ)) : CategoryTheory.CategoryStruct.comp (bimoduleTensorAssociator Γ Δ Δ Θ M (bimoduleUnit Δ) N).hom (bimoduleTensorMap Γ Δ Θ (CategoryTheory.CategoryStruct.id M) (bimoduleTensorLeftUnitor Δ Θ N).hom) = bimoduleTensorMap Γ Δ Θ (bimoduleTensorRightUnitor Γ Δ M).hom (CategoryTheory.CategoryStruct.id N)

Evaluation of the middle regular bimodule is compatible with reassociation.

theorem TauCeti.GradedModuleCat.bimoduleTensorAssociator_triangle_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 ℤ)) {Z : GradedModuleCat ((Γ.tensorProduct Θ.opposite).piece ℤ)} (h : bimoduleTensorObj Γ Δ Θ M N ⟶ Z) : CategoryTheory.CategoryStruct.comp (bimoduleTensorAssociator Γ Δ Δ Θ M (bimoduleUnit Δ) N).hom (CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Δ Θ (CategoryTheory.CategoryStruct.id M) (bimoduleTensorLeftUnitor Δ Θ N).hom) h) = CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Δ Θ (bimoduleTensorRightUnitor Γ Δ M).hom (CategoryTheory.CategoryStruct.id N)) h

Evaluation of the middle regular bimodule is compatible with reassociation.

@[instance_reducible]

noncomputable def TauCeti.GradedModuleCat.bimoduleMonoidalCategory {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] : CategoryTheory.MonoidalCategory (GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ))

The chosen monoidal structure on graded endobimodules, with regular bimodule unit.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleMonoidalCategory_tensorObj {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (M N : GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) : have x := bimoduleMonoidalCategory Γ; CategoryTheory.MonoidalCategoryStruct.tensorObj M N = bimoduleTensorObj Γ Γ Γ M N

The chosen tensor object is balanced graded bimodule composition.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleMonoidalCategory_tensorHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (M N P Q : GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) (f : M ⟶ N) (g : P ⟶ Q) : let x := bimoduleMonoidalCategory Γ; CategoryTheory.MonoidalCategoryStruct.tensorHom f g = bimoduleTensorMap Γ Γ Γ f g

The chosen tensor morphism is the map induced on the balanced tensor product.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleMonoidalCategory_whiskerLeft {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (M N P : GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) (f : N ⟶ P) : let x := bimoduleMonoidalCategory Γ; CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f = bimoduleTensorMap Γ Γ Γ (CategoryTheory.CategoryStruct.id M) f

Left whiskering maps the second balanced tensor factor.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleMonoidalCategory_whiskerRight {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (M N P : GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) (f : M ⟶ N) : let x := bimoduleMonoidalCategory Γ; CategoryTheory.MonoidalCategoryStruct.whiskerRight f P = bimoduleTensorMap Γ Γ Γ f (CategoryTheory.CategoryStruct.id P)

Right whiskering maps the first balanced tensor factor.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleMonoidalCategory_associator {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (M N P : GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) : let x := bimoduleMonoidalCategory Γ; CategoryTheory.MonoidalCategoryStruct.associator M N P = bimoduleTensorAssociator Γ Γ Γ Γ M N P

The chosen associator is graded balanced-tensor reassociation.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleMonoidalCategory_leftUnitor {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) : let x := bimoduleMonoidalCategory Γ; CategoryTheory.MonoidalCategoryStruct.leftUnitor M = bimoduleTensorLeftUnitor Γ Γ M

The chosen left unitor evaluates the regular left factor.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleMonoidalCategory_rightUnitor {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) : let x := bimoduleMonoidalCategory Γ; CategoryTheory.MonoidalCategoryStruct.rightUnitor M = bimoduleTensorRightUnitor Γ Γ M

The chosen right unitor evaluates the regular right factor.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleMonoidalCategory_tensorUnit {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] : have x := bimoduleMonoidalCategory Γ; CategoryTheory.MonoidalCategoryStruct.tensorUnit (GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) = bimoduleUnit Γ

The chosen tensor unit is the universe-lifted regular graded bimodule.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleMonoidalCategory_curriedTensor {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] : have x := bimoduleMonoidalCategory Γ; CategoryTheory.MonoidalCategory.curriedTensor (GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) = bimoduleTensor Γ Γ Γ

The chosen monoidal tensor functor is the canonical balanced bimodule bifunctor.

@[reducible, inline]

abbrev TauCeti.GradedBimoduleMonoidalDatum (k : Type w) [CommRing k] {A₁ : Type uA} [Ring A₁] [Algebra k A₁] {A₂ : Type uB} [Ring A₂] [Algebra k A₂] (Ξ₁ : InternalGrading k A₁ ℤ) [GradedAlgebra (Ξ₁.piece ℤ)] (Ξ₂ : InternalGrading k A₂ ℤ) [GradedAlgebra (Ξ₂.piece ℤ)] (Φ : CategoryTheory.Functor (HomologicalComplex (GradedBimoduleCat k Ξ₁) (ComplexShape.up ℤ)) (HomologicalComplex (GradedBimoduleCat k Ξ₂) (ComplexShape.up ℤ))) : Type (max (max (max (max (max (max (max (uA + 1) (w + 1)) uA w) 0) (uA + 1) (w + 1)) uA w) 0) uB w)

The pointwise homotopy-monoidal datum of the functor Φ on complexes of graded bimodules between the source and the target graded bimodule setting: for every pair of source complexes X and Y, a homotopy equivalence comparing the target tensor product of the image complexes with the image of the source tensor product.