Associativity of graded bimodule tensor composition #
For graded algebras A, B, C, and D, tensor composition identifies
(M tensor_B N) tensor_C P with M tensor_B (N tensor_C P) as graded
(A,D)-bimodules. The construction transports the balanced carrier associator
through the public underlying equivalences. Transport is equivariant for the
middle actions, and the output map respects both outer actions and the sum
internal grading.
The public associator and its inverse compute on pure tensors. Naturality in all three factors packages the comparison as an isomorphism of trifunctors, ready for Mathlib's totalization associator. No internal Koszul sign is introduced; cohomological signs belong to the complex totalization.
noncomputable def
TauCeti.GradedModuleCat.bimoduleTensorAssociator
{k : Type uk}
{A : Type uA}
{B : Type uB}
{C : Type uC}
{D : Type uD}
[CommRing k]
[Ring A]
[Ring B]
[Ring C]
[Ring D]
[Algebra k A]
[Algebra k B]
[Algebra k C]
[Algebra k D]
(Γ : InternalGrading k A ℤ)
(Δ : InternalGrading k B ℤ)
(Θ : InternalGrading k C ℤ)
(Ψ : InternalGrading k D ℤ)
[GradedAlgebra (Γ.piece ℤ)]
[GradedAlgebra (Δ.piece ℤ)]
[GradedAlgebra (Θ.piece ℤ)]
[GradedAlgebra (Ψ.piece ℤ)]
(M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ))
(N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ))
(P : GradedModuleCat ((Θ.tensorProduct Ψ.opposite).piece ℤ))
:
bimoduleTensorObj Γ Θ Ψ (bimoduleTensorObj Γ Δ Θ M N) P ≅ bimoduleTensorObj Γ Δ Ψ M (bimoduleTensorObj Δ Θ Ψ N P)
Reassociation of graded bimodule tensors, balanced over the two middle algebras.
Instances For
@[simp]
theorem
TauCeti.GradedModuleCat.bimoduleTensorAssociator_hom_tmul
{k : Type uk}
{A : Type uA}
{B : Type uB}
{C : Type uC}
{D : Type uD}
[CommRing k]
[Ring A]
[Ring B]
[Ring C]
[Ring D]
[Algebra k A]
[Algebra k B]
[Algebra k C]
[Algebra k D]
(Γ : InternalGrading k A ℤ)
(Δ : InternalGrading k B ℤ)
(Θ : InternalGrading k C ℤ)
(Ψ : InternalGrading k D ℤ)
[GradedAlgebra (Γ.piece ℤ)]
[GradedAlgebra (Δ.piece ℤ)]
[GradedAlgebra (Θ.piece ℤ)]
[GradedAlgebra (Ψ.piece ℤ)]
(M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ))
(N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ))
(P : GradedModuleCat ((Θ.tensorProduct Ψ.opposite).piece ℤ))
(m : M.carrier)
(n : N.carrier)
(p : P.carrier)
:
(bimoduleTensorAssociator Γ Δ Θ Ψ M N P).hom.hom
(bimoduleTensorTmul Γ Θ Ψ (bimoduleTensorObj Γ Δ Θ M N) P (bimoduleTensorTmul Γ Δ Θ M N m n) p) = bimoduleTensorTmul Γ Δ Ψ M (bimoduleTensorObj Δ Θ Ψ N P) m (bimoduleTensorTmul Δ Θ Ψ N P n p)
The graded associator changes only the parentheses of a nested pure tensor.
@[simp]
theorem
TauCeti.GradedModuleCat.bimoduleTensorAssociator_inv_tmul
{k : Type uk}
{A : Type uA}
{B : Type uB}
{C : Type uC}
{D : Type uD}
[CommRing k]
[Ring A]
[Ring B]
[Ring C]
[Ring D]
[Algebra k A]
[Algebra k B]
[Algebra k C]
[Algebra k D]
(Γ : InternalGrading k A ℤ)
(Δ : InternalGrading k B ℤ)
(Θ : InternalGrading k C ℤ)
(Ψ : InternalGrading k D ℤ)
[GradedAlgebra (Γ.piece ℤ)]
[GradedAlgebra (Δ.piece ℤ)]
[GradedAlgebra (Θ.piece ℤ)]
[GradedAlgebra (Ψ.piece ℤ)]
(M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ))
(N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ))
(P : GradedModuleCat ((Θ.tensorProduct Ψ.opposite).piece ℤ))
(m : M.carrier)
(n : N.carrier)
(p : P.carrier)
:
(bimoduleTensorAssociator Γ Δ Θ Ψ M N P).inv.hom
(bimoduleTensorTmul Γ Δ Ψ M (bimoduleTensorObj Δ Θ Ψ N P) m (bimoduleTensorTmul Δ Θ Ψ N P n p)) = bimoduleTensorTmul Γ Θ Ψ (bimoduleTensorObj Γ Δ Θ M N) P (bimoduleTensorTmul Γ Δ Θ M N m n) p
The inverse graded associator restores the original nested pure tensor.
theorem
TauCeti.GradedModuleCat.bimoduleTensorAssociator_naturality
{k : Type uk}
{A : Type uA}
{B : Type uB}
{C : Type uC}
{D : Type uD}
[CommRing k]
[Ring A]
[Ring B]
[Ring C]
[Ring D]
[Algebra k A]
[Algebra k B]
[Algebra k C]
[Algebra k D]
(Γ : InternalGrading k A ℤ)
(Δ : InternalGrading k B ℤ)
(Θ : InternalGrading k C ℤ)
(Ψ : InternalGrading k D ℤ)
[GradedAlgebra (Γ.piece ℤ)]
[GradedAlgebra (Δ.piece ℤ)]
[GradedAlgebra (Θ.piece ℤ)]
[GradedAlgebra (Ψ.piece ℤ)]
(M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ))
(N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ))
(P : GradedModuleCat ((Θ.tensorProduct Ψ.opposite).piece ℤ))
{M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)}
{N' : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)}
{P' : GradedModuleCat ((Θ.tensorProduct Ψ.opposite).piece ℤ)}
(f : M ⟶ M')
(g : N ⟶ N')
(h : P ⟶ P')
:
CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Θ Ψ (bimoduleTensorMap Γ Δ Θ f g) h)
(bimoduleTensorAssociator Γ Δ Θ Ψ M' N' P').hom = CategoryTheory.CategoryStruct.comp (bimoduleTensorAssociator Γ Δ Θ Ψ M N P).hom
(bimoduleTensorMap Γ Δ Ψ f (bimoduleTensorMap Δ Θ Ψ g h))
Reassociation is natural in each of the three bimodule maps.
theorem
TauCeti.GradedModuleCat.bimoduleTensorAssociator_naturality_assoc
{k : Type uk}
{A : Type uA}
{B : Type uB}
{C : Type uC}
{D : Type uD}
[CommRing k]
[Ring A]
[Ring B]
[Ring C]
[Ring D]
[Algebra k A]
[Algebra k B]
[Algebra k C]
[Algebra k D]
(Γ : InternalGrading k A ℤ)
(Δ : InternalGrading k B ℤ)
(Θ : InternalGrading k C ℤ)
(Ψ : InternalGrading k D ℤ)
[GradedAlgebra (Γ.piece ℤ)]
[GradedAlgebra (Δ.piece ℤ)]
[GradedAlgebra (Θ.piece ℤ)]
[GradedAlgebra (Ψ.piece ℤ)]
(M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ))
(N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ))
(P : GradedModuleCat ((Θ.tensorProduct Ψ.opposite).piece ℤ))
{M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)}
{N' : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)}
{P' : GradedModuleCat ((Θ.tensorProduct Ψ.opposite).piece ℤ)}
(f : M ⟶ M')
(g : N ⟶ N')
(h : P ⟶ P')
{Z : GradedModuleCat ((Γ.tensorProduct Ψ.opposite).piece ℤ)}
(h✝ : bimoduleTensorObj Γ Δ Ψ M' (bimoduleTensorObj Δ Θ Ψ N' P') ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Θ Ψ (bimoduleTensorMap Γ Δ Θ f g) h)
(CategoryTheory.CategoryStruct.comp (bimoduleTensorAssociator Γ Δ Θ Ψ M' N' P').hom h✝) = CategoryTheory.CategoryStruct.comp (bimoduleTensorAssociator Γ Δ Θ Ψ M N P).hom
(CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Δ Ψ f (bimoduleTensorMap Δ Θ Ψ g h)) h✝)
Reassociation is natural in each of the three bimodule maps.
noncomputable def
TauCeti.GradedModuleCat.bimoduleTensorAssociatorNatIso
{k : Type uk}
{A : Type uA}
{B : Type uB}
{C : Type uC}
{D : Type uD}
[CommRing k]
[Ring A]
[Ring B]
[Ring C]
[Ring D]
[Algebra k A]
[Algebra k B]
[Algebra k C]
[Algebra k D]
(Γ : InternalGrading k A ℤ)
(Δ : InternalGrading k B ℤ)
(Θ : InternalGrading k C ℤ)
(Ψ : InternalGrading k D ℤ)
[GradedAlgebra (Γ.piece ℤ)]
[GradedAlgebra (Δ.piece ℤ)]
[GradedAlgebra (Θ.piece ℤ)]
[GradedAlgebra (Ψ.piece ℤ)]
:
CategoryTheory.bifunctorComp₁₂ (bimoduleTensor Γ Δ Θ) (bimoduleTensor Γ Θ Ψ) ≅ CategoryTheory.bifunctorComp₂₃ (bimoduleTensor Γ Δ Ψ) (bimoduleTensor Δ Θ Ψ)
The graded associator as an isomorphism between the two tensor trifunctors.
Instances For
@[simp]
theorem
TauCeti.GradedModuleCat.bimoduleTensorAssociatorNatIso_hom_app
{k : Type uk}
{A : Type uA}
{B : Type uB}
{C : Type uC}
{D : Type uD}
[CommRing k]
[Ring A]
[Ring B]
[Ring C]
[Ring D]
[Algebra k A]
[Algebra k B]
[Algebra k C]
[Algebra k D]
(Γ : InternalGrading k A ℤ)
(Δ : InternalGrading k B ℤ)
(Θ : InternalGrading k C ℤ)
(Ψ : InternalGrading k D ℤ)
[GradedAlgebra (Γ.piece ℤ)]
[GradedAlgebra (Δ.piece ℤ)]
[GradedAlgebra (Θ.piece ℤ)]
[GradedAlgebra (Ψ.piece ℤ)]
(M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ))
(N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ))
(P : GradedModuleCat ((Θ.tensorProduct Ψ.opposite).piece ℤ))
:
(((bimoduleTensorAssociatorNatIso Γ Δ Θ Ψ).hom.app M).app N).app P = (bimoduleTensorAssociator Γ Δ Θ Ψ M N P).hom
The forward trifunctor comparison has the graded associator as each component.
@[simp]
theorem
TauCeti.GradedModuleCat.bimoduleTensorAssociatorNatIso_inv_app
{k : Type uk}
{A : Type uA}
{B : Type uB}
{C : Type uC}
{D : Type uD}
[CommRing k]
[Ring A]
[Ring B]
[Ring C]
[Ring D]
[Algebra k A]
[Algebra k B]
[Algebra k C]
[Algebra k D]
(Γ : InternalGrading k A ℤ)
(Δ : InternalGrading k B ℤ)
(Θ : InternalGrading k C ℤ)
(Ψ : InternalGrading k D ℤ)
[GradedAlgebra (Γ.piece ℤ)]
[GradedAlgebra (Δ.piece ℤ)]
[GradedAlgebra (Θ.piece ℤ)]
[GradedAlgebra (Ψ.piece ℤ)]
(M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ))
(N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ))
(P : GradedModuleCat ((Θ.tensorProduct Ψ.opposite).piece ℤ))
:
(((bimoduleTensorAssociatorNatIso Γ Δ Θ Ψ).inv.app M).app N).app P = (bimoduleTensorAssociator Γ Δ Θ Ψ M N P).inv
The reverse trifunctor comparison has the inverse graded associator as each component.