Internal shifts and balanced tensor composition #
The tensor of two internally shifted graded bimodules is the internal shift of their balanced tensor by the sum of the two shifts. The isomorphism sends each pure tensor to itself; internal degrees add and introduce no sign. Cohomological tensor signs are separate and remain those of Mathlib totalization.
The construction uses the public homogeneous balanced lift and pure-tensor extensionality. It applies to independently sized bimodules over three graded algebras. Both directions have pure-tensor formulas, and the comparison is natural in the two bimodule maps.
The shift convention is M{a}_p = M_{p-a}, as in GradedModuleCat.shiftObj.
noncomputable def
TauCeti.GradedModuleCat.bimoduleTensorShiftIso
{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 ℤ))
(a b : ℤ)
:
bimoduleTensorObj Γ Δ Θ (M.shiftObj a) (N.shiftObj b) ≅ (bimoduleTensorObj Γ Δ Θ M N).shiftObj (a + b)
Internal shifts add under balanced tensor composition of graded bimodules.
Instances For
@[simp]
theorem
TauCeti.GradedModuleCat.bimoduleTensorShiftIso_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 ℤ))
(a b : ℤ)
(m : M.carrier)
(n : N.carrier)
:
(bimoduleTensorShiftIso Γ Δ Θ M N a b).hom.hom (bimoduleTensorTmul Γ Δ Θ (M.shiftObj a) (N.shiftObj b) m n) = bimoduleTensorTmul Γ Δ Θ M N m n
@[simp]
theorem
TauCeti.GradedModuleCat.bimoduleTensorShiftIso_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 ℤ))
(a b : ℤ)
(m : M.carrier)
(n : N.carrier)
:
(bimoduleTensorShiftIso Γ Δ Θ M N a b).inv.hom (bimoduleTensorTmul Γ Δ Θ M N m n) = bimoduleTensorTmul Γ Δ Θ (M.shiftObj a) (N.shiftObj b) m n
theorem
TauCeti.GradedModuleCat.bimoduleTensorShiftIso_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 ℤ))
{M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)}
{N' : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)}
(a b : ℤ)
(f : M ⟶ M')
(g : N ⟶ N')
:
CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Δ Θ ((shiftFunctor a).map f) ((shiftFunctor b).map g))
(bimoduleTensorShiftIso Γ Δ Θ M' N' a b).hom = CategoryTheory.CategoryStruct.comp (bimoduleTensorShiftIso Γ Δ Θ M N a b).hom
((shiftFunctor (a + b)).map (bimoduleTensorMap Γ Δ Θ f g))
The tensor-shift comparison is natural in both graded bimodule maps.
theorem
TauCeti.GradedModuleCat.bimoduleTensorShiftIso_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 ℤ))
{M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)}
{N' : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)}
(a b : ℤ)
(f : M ⟶ M')
(g : N ⟶ N')
{Z : GradedModuleCat ((Γ.tensorProduct Θ.opposite).piece ℤ)}
(h : (bimoduleTensorObj Γ Δ Θ M' N').shiftObj (a + b) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Δ Θ ((shiftFunctor a).map f) ((shiftFunctor b).map g))
(CategoryTheory.CategoryStruct.comp (bimoduleTensorShiftIso Γ Δ Θ M' N' a b).hom h) = CategoryTheory.CategoryStruct.comp (bimoduleTensorShiftIso Γ Δ Θ M N a b).hom
(CategoryTheory.CategoryStruct.comp ((shiftFunctor (a + b)).map (bimoduleTensorMap Γ Δ Θ f g)) h)
The tensor-shift comparison is natural in both graded bimodule maps.