Graded units for bimodule tensor composition

The regular bimodule of a graded algebra is the unit for balanced tensor composition. Its carrier is lifted so that it lies in the same universe as the modules being tensored. The grading is transported from the algebra; no internal shift is introduced.

The construction uses Bimodule.of, InternalGrading.map, and the balanced homogeneous lift. The unit identities are the graded enveloping-module versions of BalancedTensorProduct.lid and BalancedTensorProduct.rid.

Both unit isomorphisms have public evaluation and insertion formulas. Their evaluation maps are natural in graded bimodule maps; on the tensor of two regular bimodules, left and right evaluation agree.

The unit complex of the graded bimodule setting of Ξ, the regular graded bimodule in cohomological degree zero, is gradedBimoduleUnitComplex.

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

The universe-lifted regular graded bimodule of A.

def TauCeti.GradedModuleCat.bimoduleUnitEquiv {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] : A ≃ₗ[k] (bimoduleUnit Γ).carrier

The unit bimodule has the same ground-ring module as the algebra.

theorem TauCeti.GradedModuleCat.bimoduleUnitEquiv_apply {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (a : A) : (bimoduleUnitEquiv Γ) a = { down := (Bimodule.of (AlgHom.id k A)) a }

The algebra element in the concrete lifted regular-bimodule carrier.

theorem TauCeti.GradedModuleCat.bimoduleUnitEquiv_symm_apply {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (x : (bimoduleUnit Γ).carrier) : (bimoduleUnitEquiv Γ).symm x = (Bimodule.of (AlgHom.id k A)).symm x.down

Read the algebra element from the concrete lifted regular-bimodule carrier.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleUnitEquiv_symm_smul {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (a : A) (b : Aᵐᵒᵖ) (x : (bimoduleUnit Γ).carrier) : (bimoduleUnitEquiv Γ).symm (a ⊗ₜ[k] b • x) = a * (bimoduleUnitEquiv Γ).symm x * MulOpposite.unop b

@[simp]

theorem TauCeti.GradedModuleCat.tmul_smul_bimoduleUnitEquiv {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (a : A) (b : Aᵐᵒᵖ) (x : A) : a ⊗ₜ[k] b • (bimoduleUnitEquiv Γ) x = (bimoduleUnitEquiv Γ) (a * x * MulOpposite.unop b)

@[simp]

theorem TauCeti.GradedModuleCat.mem_bimoduleUnit_piece_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] (p : ℤ) (x : (bimoduleUnit Γ).carrier) : x ∈ (bimoduleUnit Γ).grading.piece ℤ p ↔ (bimoduleUnitEquiv Γ).symm x ∈ Γ.piece ℤ p

Homogeneous membership in the regular bimodule is membership in the algebra grading.

@[instance_reducible]

def TauCeti.GradedModuleCat.instModuleCarrierTensorProductMulOpposite_1 {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : Module A M.carrier

Restrict the envelope action to the left algebra factor.

theorem TauCeti.GradedModuleCat.instIsScalarTowerCarrierTensorProductMulOpposite_1 {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : IsScalarTower k A M.carrier

The restricted left action respects the ground-ring action.

@[instance_reducible]

def TauCeti.GradedModuleCat.instModuleMulOppositeCarrierTensorProduct_1 {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : Module Bᵐᵒᵖ M.carrier

Restrict the envelope action to the right algebra factor.

theorem TauCeti.GradedModuleCat.instSMulCommClassMulOppositeCarrierTensorProduct_1 {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : SMulCommClass A Bᵐᵒᵖ M.carrier

The restricted left and right actions commute.

noncomputable def TauCeti.GradedModuleCat.bimoduleTensorLeftUnitorHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : bimoduleTensorObj Γ Γ Δ (bimoduleUnit Γ) M ⟶ M

Evaluate the regular left tensor factor by its action on the second factor.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorLeftUnitorHom_tmul {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (x : (bimoduleUnit Γ).carrier) (m : M.carrier) : (bimoduleTensorLeftUnitorHom Γ Δ M).hom (bimoduleTensorTmul Γ Γ Δ (bimoduleUnit Γ) M x m) = (bimoduleUnitEquiv Γ).symm x ⊗ₜ[k] 1 • m

noncomputable def TauCeti.GradedModuleCat.bimoduleTensorLeftUnitorInv {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : M ⟶ bimoduleTensorObj Γ Γ Δ (bimoduleUnit Γ) M

Insert 1 in the regular left tensor factor, as a degree-zero bimodule map.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorLeftUnitorInv_apply {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (m : M.carrier) : (bimoduleTensorLeftUnitorInv Γ Δ M).hom m = bimoduleTensorTmul Γ Γ Δ (bimoduleUnit Γ) M ((bimoduleUnitEquiv Γ) 1) m

noncomputable def TauCeti.GradedModuleCat.bimoduleTensorLeftUnitor {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : bimoduleTensorObj Γ Γ Δ (bimoduleUnit Γ) M ≅ M

The regular graded bimodule is a left unit for balanced tensor composition.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorLeftUnitor_hom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : (bimoduleTensorLeftUnitor Γ Δ M).hom = bimoduleTensorLeftUnitorHom Γ Δ M

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorLeftUnitor_inv {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : (bimoduleTensorLeftUnitor Γ Δ M).inv = bimoduleTensorLeftUnitorInv Γ Δ M

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorLeftUnitorHom_naturality {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) {N : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Γ Δ (CategoryTheory.CategoryStruct.id (bimoduleUnit Γ)) f) (bimoduleTensorLeftUnitorHom Γ Δ N) = CategoryTheory.CategoryStruct.comp (bimoduleTensorLeftUnitorHom Γ Δ M) f

Evaluation of a left unit commutes with every graded bimodule map.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorLeftUnitorHom_naturality_assoc {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) {N : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} (f : M ⟶ N) {Z : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Γ Δ (CategoryTheory.CategoryStruct.id (bimoduleUnit Γ)) f) (CategoryTheory.CategoryStruct.comp (bimoduleTensorLeftUnitorHom Γ Δ N) h) = CategoryTheory.CategoryStruct.comp (bimoduleTensorLeftUnitorHom Γ Δ M) (CategoryTheory.CategoryStruct.comp f h)

Evaluation of a left unit commutes with every graded bimodule map.

@[instance_reducible]

def TauCeti.GradedModuleCat.instModuleCarrierTensorProductMulOpposite_2 {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : Module A M.carrier

Restrict the envelope action to the left algebra factor.

@[instance_reducible]

def TauCeti.GradedModuleCat.instModuleMulOppositeCarrierTensorProduct_2 {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : Module Bᵐᵒᵖ M.carrier

Restrict the envelope action to the right algebra factor.

theorem TauCeti.GradedModuleCat.instIsScalarTowerMulOppositeCarrierTensorProduct_1 {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : IsScalarTower k Bᵐᵒᵖ M.carrier

The restricted right action respects the ground-ring action.

theorem TauCeti.GradedModuleCat.instSMulCommClassMulOppositeCarrierTensorProduct_2 {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : SMulCommClass A Bᵐᵒᵖ M.carrier

The restricted left and right actions commute.

noncomputable def TauCeti.GradedModuleCat.bimoduleTensorRightUnitorHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : bimoduleTensorObj Γ Δ Δ M (bimoduleUnit Δ) ⟶ M

Evaluate the regular right tensor factor by its right action on the first factor.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorRightUnitorHom_tmul {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (m : M.carrier) (x : (bimoduleUnit Δ).carrier) : (bimoduleTensorRightUnitorHom Γ Δ M).hom (bimoduleTensorTmul Γ Δ Δ M (bimoduleUnit Δ) m x) = 1 ⊗ₜ[k] MulOpposite.op ((bimoduleUnitEquiv Δ).symm x) • m

noncomputable def TauCeti.GradedModuleCat.bimoduleTensorRightUnitorInv {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : M ⟶ bimoduleTensorObj Γ Δ Δ M (bimoduleUnit Δ)

Insert 1 in the regular right tensor factor, as a degree-zero bimodule map.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorRightUnitorInv_apply {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (m : M.carrier) : (bimoduleTensorRightUnitorInv Γ Δ M).hom m = bimoduleTensorTmul Γ Δ Δ M (bimoduleUnit Δ) m ((bimoduleUnitEquiv Δ) 1)

noncomputable def TauCeti.GradedModuleCat.bimoduleTensorRightUnitor {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : bimoduleTensorObj Γ Δ Δ M (bimoduleUnit Δ) ≅ M

The regular graded bimodule is a right unit for balanced tensor composition.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorRightUnitor_hom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : (bimoduleTensorRightUnitor Γ Δ M).hom = bimoduleTensorRightUnitorHom Γ Δ M

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorRightUnitor_inv {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : (bimoduleTensorRightUnitor Γ Δ M).inv = bimoduleTensorRightUnitorInv Γ Δ M

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorRightUnitorHom_naturality {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) {N : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Δ Δ f (CategoryTheory.CategoryStruct.id (bimoduleUnit Δ))) (bimoduleTensorRightUnitorHom Γ Δ N) = CategoryTheory.CategoryStruct.comp (bimoduleTensorRightUnitorHom Γ Δ M) f

Evaluation of a right unit commutes with every graded bimodule map.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorRightUnitorHom_naturality_assoc {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] {B : Type uB} [Ring B] [Algebra k B] (Δ : InternalGrading k B ℤ) [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) {N : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} (f : M ⟶ N) {Z : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Δ Δ f (CategoryTheory.CategoryStruct.id (bimoduleUnit Δ))) (CategoryTheory.CategoryStruct.comp (bimoduleTensorRightUnitorHom Γ Δ N) h) = CategoryTheory.CategoryStruct.comp (bimoduleTensorRightUnitorHom Γ Δ M) (CategoryTheory.CategoryStruct.comp f h)

Evaluation of a right unit commutes with every graded bimodule map.

theorem TauCeti.GradedModuleCat.bimoduleTensorUnitHom_eq {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] : bimoduleTensorLeftUnitorHom Γ Γ (bimoduleUnit Γ) = bimoduleTensorRightUnitorHom Γ Γ (bimoduleUnit Γ)

Left and right evaluation agree on the tensor of two regular graded bimodules.

@[reducible, inline]

noncomputable abbrev TauCeti.gradedBimoduleUnitComplex (k : Type w) [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (Ξ : InternalGrading k A ℤ) [GradedAlgebra (Ξ.piece ℤ)] : HomologicalComplex (GradedBimoduleCat k Ξ) (ComplexShape.up ℤ)

The unit complex of the graded bimodule setting of Ξ: the regular graded bimodule GradedModuleCat.bimoduleUnit Ξ placed in cohomological degree zero.