The regular bimodule acts as the identity on graded left modules

Evaluation identifies the balanced tensor of the regular graded bimodule with a graded left module with that module. Its inverse inserts the unit element. Both maps preserve the internal grading, and evaluation is natural in graded module maps.

The construction adapts bimoduleTensorLeftUnitor from TauCeti.Algebra.Category.GradedModuleCat.BimoduleTensor.Unit, using the left-module analogue of its supporting bimoduleTensorLift from TauCeti.Algebra.Category.GradedModuleCat.BimoduleTensor.Basic.

This is the unit comparison for the graded bimodule action on left modules. The module universe contains the algebra universe, as in the selected graded endobimodule monoidal category.

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitorHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) : bimoduleModuleTensorObj Γ Γ (bimoduleUnit Γ) N ⟶ N

Evaluate a regular-bimodule element by its left action on a graded module.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitorHom_tmul {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) (x : (bimoduleUnit Γ).carrier) (n : N.carrier) : (bimoduleModuleTensorLeftUnitorHom Γ N).hom (bimoduleModuleTensorTmul Γ Γ (bimoduleUnit Γ) N x n) = (bimoduleUnitEquiv Γ).symm x • n

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorTmul_unit_smul {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) (a : A) (n : N.carrier) : bimoduleModuleTensorTmul Γ Γ (bimoduleUnit Γ) N ((bimoduleUnitEquiv Γ) 1) (a • n) = bimoduleModuleTensorTmul Γ Γ (bimoduleUnit Γ) N ((bimoduleUnitEquiv Γ) a) n

Balancing transfers a module scalar to the regular bimodule's unit element.

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitorInv {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) : N ⟶ bimoduleModuleTensorObj Γ Γ (bimoduleUnit Γ) N

Insert the regular bimodule's unit element in the first tensor factor.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitorInv_apply {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) (n : N.carrier) : (bimoduleModuleTensorLeftUnitorInv Γ N).hom n = bimoduleModuleTensorTmul Γ Γ (bimoduleUnit Γ) N ((bimoduleUnitEquiv Γ) 1) n

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitor {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) : bimoduleModuleTensorObj Γ Γ (bimoduleUnit Γ) N ≅ N

Tensoring the regular graded bimodule with a left module returns that left module.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitor_hom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) : (bimoduleModuleTensorLeftUnitor Γ N).hom = bimoduleModuleTensorLeftUnitorHom Γ N

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitor_inv {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) : (bimoduleModuleTensorLeftUnitor Γ N).inv = bimoduleModuleTensorLeftUnitorInv Γ N

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitorHom_naturality {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) {N' : GradedModuleCat (Γ.piece ℤ)} (f : N ⟶ N') : CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorMap Γ Γ (CategoryTheory.CategoryStruct.id (bimoduleUnit Γ)) f) (bimoduleModuleTensorLeftUnitorHom Γ N') = CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorLeftUnitorHom Γ N) f

Evaluation of a left unit commutes with every graded left-module map.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitorHom_naturality_assoc {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) {N' : GradedModuleCat (Γ.piece ℤ)} (f : N ⟶ N') {Z : GradedModuleCat (Γ.piece ℤ)} (h : N' ⟶ Z) : CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorMap Γ Γ (CategoryTheory.CategoryStruct.id (bimoduleUnit Γ)) f) (CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorLeftUnitorHom Γ N') h) = CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorLeftUnitorHom Γ N) (CategoryTheory.CategoryStruct.comp f h)

Evaluation of a left unit commutes with every graded left-module map.

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitorNatIso {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] : (bimoduleModuleTensor Γ Γ).obj (bimoduleUnit Γ) ≅ CategoryTheory.Functor.id (GradedModuleCat (Γ.piece ℤ))

The regular bimodule acts as the identity functor on graded left modules.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitorNatIso_hom_app {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) : (bimoduleModuleTensorLeftUnitorNatIso Γ).hom.app N = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (bimoduleModuleTensorLeftUnitor Γ N).hom

The forward natural comparison is evaluation after the public object transport.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitorNatIso_hom_app_assoc {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) {Z : GradedModuleCat (Γ.piece ℤ)} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp ((bimoduleModuleTensorLeftUnitorNatIso Γ).hom.app N) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorLeftUnitor Γ N).hom h)

The forward natural comparison is evaluation after the public object transport.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitorNatIso_inv_app {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) : (bimoduleModuleTensorLeftUnitorNatIso Γ).inv.app N = CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorLeftUnitor Γ N).inv (CategoryTheory.eqToHom ⋯)

The inverse natural comparison inserts the unit before the inverse object transport.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorLeftUnitorNatIso_inv_app_assoc {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (N : GradedModuleCat (Γ.piece ℤ)) {Z : GradedModuleCat (Γ.piece ℤ)} (h : ((bimoduleModuleTensor Γ Γ).obj (bimoduleUnit Γ)).obj N ⟶ Z) : CategoryTheory.CategoryStruct.comp ((bimoduleModuleTensorLeftUnitorNatIso Γ).inv.app N) h = CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorLeftUnitor Γ N).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

The inverse natural comparison inserts the unit before the inverse object transport.