Balanced tensor composition of graded bimodules

For graded algebras A, B, and C, this file constructs the composition

(A,B)-bimodules × (B,C)-bimodules → (A,C)-bimodules,

balanced over B. Each bimodule is an object of GradedModuleCat over its enveloping algebra, with the tensor-product internal grading. Restricting the enveloping action supplies the actions used to balance. The quotient has the sum internal grading and the two outer actions.

The construction uses the existing balanced quotient, grading, map, and lift APIs. Its internal grading introduces no Koszul sign. Cohomological tensor signs come from Mathlib's totalization when this bifunctor is applied to cochain complexes. Taking all three algebras and gradings equal gives tensor composition of endobimodules; heterogeneous composition also supplies the tensors needed for transfer through a supplied Morita equivalence.

bimoduleModuleTensor gives the corresponding action on graded left modules: an (A,B)-bimodule tensored over B with a left B-module is a left A-module. Both constructions are linear in each variable.

GradedBimoduleCat is the category of graded bimodules of a graded algebra with an internal grading, and GradedModuleCat.bimoduleTensor is the balanced bimodule tensor of that setting.

References

• B. Keller, Deriving DG categories, Section 6.1.

@[instance_reducible]

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

The left action obtained by restricting the envelope action to its first factor.

@[instance_reducible]

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

The right action obtained by restricting the envelope action to its second factor.

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

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

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

theorem TauCeti.GradedModuleCat.leftGradedSMul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [SetLike.GradedOne (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : SetLike.GradedSMul (Γ.piece ℤ) (M.grading.piece ℤ)

theorem TauCeti.GradedModuleCat.rightGradedSMul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [DirectSum.Decomposition (Δ.piece ℤ)] [SetLike.GradedOne (Γ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) : SetLike.GradedSMul ((InternalGrading.ofDecomposition (Δ.piece ℤ)).opposite.piece ℤ) (M.grading.piece ℤ)

@[instance_reducible]

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

The output left action is induced from the bimodule's first factor.

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

theorem TauCeti.GradedModuleCat.instGradedSMulIntSubmoduleBalancedTensorProductCarrierTensorProductMulOppositePieceGradingGrading {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) : SetLike.GradedSMul (Γ.piece ℤ) ((BalancedTensorProduct.grading M.grading N.grading).piece ℤ)

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

An internally graded bimodule acts on a graded left module by balanced tensor product.

def TauCeti.GradedModuleCat.bimoduleModuleTensorTmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) (m : M.carrier) (n : N.carrier) : (bimoduleModuleTensorObj Γ Δ M N).carrier

The pure tensor of a bimodule element and a left-module element.

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorMk {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) : M.carrier →ₗ[k] N.carrier →ₗ[k] (bimoduleModuleTensorObj Γ Δ M N).carrier

The pure tensor as a bilinear map over the ground ring.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorMk_apply {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) (m : M.carrier) (n : N.carrier) : ((bimoduleModuleTensorMk Γ Δ M N) m) n = bimoduleModuleTensorTmul Γ Δ M N m n

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorUnderlyingEquiv {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) : (bimoduleModuleTensorObj Γ Δ M N).carrier ≃ₗ[k] BalancedTensorProduct k B M.carrier N.carrier

Forgetting the output grading identifies the left-module tensor carrier with the balanced quotient.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorUnderlyingEquiv_tmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) (m : M.carrier) (n : N.carrier) : (bimoduleModuleTensorUnderlyingEquiv Γ Δ M N) (bimoduleModuleTensorTmul Γ Δ M N m n) = BalancedTensorProduct.tmul k B m n

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorUnderlyingEquiv_symm_tmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) (m : M.carrier) (n : N.carrier) : (bimoduleModuleTensorUnderlyingEquiv Γ Δ M N).symm (BalancedTensorProduct.tmul k B m n) = bimoduleModuleTensorTmul Γ Δ M N m n

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorUnderlyingEquiv_smul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) (a : A) (z : (bimoduleModuleTensorObj Γ Δ M N).carrier) : (bimoduleModuleTensorUnderlyingEquiv Γ Δ M N) (a • z) = a • (bimoduleModuleTensorUnderlyingEquiv Γ Δ M N) z

The carrier identification preserves the output left action.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorUnderlyingEquiv_mem_iff {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) {p : ℤ} {z : (bimoduleModuleTensorObj Γ Δ M N).carrier} : (bimoduleModuleTensorUnderlyingEquiv Γ Δ M N) z ∈ (BalancedTensorProduct.grading M.grading N.grading).piece ℤ p ↔ z ∈ (bimoduleModuleTensorObj Γ Δ M N).grading.piece ℤ p

The carrier identification preserves membership in each internal degree piece.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorUnderlyingEquiv_isHomogeneous {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) : LinearMap.IsHomogeneous (↑(bimoduleModuleTensorUnderlyingEquiv Γ Δ M N)) ((bimoduleModuleTensorObj Γ Δ M N).grading.piece ℤ) ((BalancedTensorProduct.grading M.grading N.grading).piece ℤ) 0

The left-module tensor carrier identification is homogeneous of degree zero.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorTmul_balance {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) (b : B) (m : M.carrier) (n : N.carrier) : bimoduleModuleTensorTmul Γ Δ M N (1 ⊗ₜ[k] MulOpposite.op b • m) n = bimoduleModuleTensorTmul Γ Δ M N m (b • n)

Balancing transfers the right action on the bimodule to the left module.

@[simp]

theorem TauCeti.GradedModuleCat.smul_bimoduleModuleTensorTmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) (a : A) (m : M.carrier) (n : N.carrier) : a • bimoduleModuleTensorTmul Γ Δ M N m n = bimoduleModuleTensorTmul Γ Δ M N (a ⊗ₜ[k] 1 • m) n

The output left action acts on the first tensor factor.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorTmul_mem {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) {p q : ℤ} {m : M.carrier} {n : N.carrier} (hm : m ∈ M.grading.piece ℤ p) (hn : n ∈ N.grading.piece ℤ q) : bimoduleModuleTensorTmul Γ Δ M N m n ∈ (bimoduleModuleTensorObj Γ Δ M N).grading.piece ℤ (p + q)

The internal degrees of the two factors add.

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorMkQ {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) : TensorProduct k M.carrier N.carrier →ₗ[k] (bimoduleModuleTensorObj Γ Δ M N).carrier

The quotient map from the ground-ring tensor product to the left-module tensor product.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorMkQ_tmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) (m : M.carrier) (n : N.carrier) : (bimoduleModuleTensorMkQ Γ Δ M N) (m ⊗ₜ[k] n) = bimoduleModuleTensorTmul Γ Δ M N m n

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorObj_grading_piece {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) (p : ℤ) : (bimoduleModuleTensorObj Γ Δ M N).grading.piece ℤ p = Submodule.map (bimoduleModuleTensorMkQ Γ Δ M N) ((M.grading.tensorProduct N.grading).piece ℤ p)

The internal degree piece is the image of the ground-ring tensor degree piece.

theorem TauCeti.GradedModuleCat.mem_bimoduleModuleTensorObj_piece_iff {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) {p : ℤ} {z : (bimoduleModuleTensorObj Γ Δ M N).carrier} : z ∈ (bimoduleModuleTensorObj Γ Δ M N).grading.piece ℤ p ↔ ∃ x ∈ (M.grading.tensorProduct N.grading).piece ℤ p, (bimoduleModuleTensorMkQ Γ Δ M N) x = z

Membership in a degree piece has a homogeneous ground-ring tensor representative.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorObj_map_mem_of_tmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat (Δ.piece ℤ)) {Q : Type u_1} [AddCommGroup Q] [Module k Q] (H : InternalGrading k Q ℤ) (f : (bimoduleModuleTensorObj Γ Δ M N).carrier →ₗ[k] Q) (s : ℤ) (hf : ∀ {p q : ℤ} {m : M.carrier} {n : N.carrier}, m ∈ M.grading.piece ℤ p → n ∈ N.grading.piece ℤ q → f (bimoduleModuleTensorTmul Γ Δ M N m n) ∈ H.piece ℤ (p + q + s)) {p : ℤ} {z : (bimoduleModuleTensorObj Γ Δ M N).carrier} (hz : z ∈ (bimoduleModuleTensorObj Γ Δ M N).grading.piece ℤ p) : f z ∈ H.piece ℤ (p + s)

A linear map shifts internal degrees if it does so on homogeneous pure left-module tensors.

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorMap {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N' : GradedModuleCat (Δ.piece ℤ)} (f : M ⟶ M') (g : N ⟶ N') : bimoduleModuleTensorObj Γ Δ M N ⟶ bimoduleModuleTensorObj Γ Δ M' N'

Tensor a graded bimodule map with a graded left-module map.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorMap_tmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N' : GradedModuleCat (Δ.piece ℤ)} (f : M ⟶ M') (g : N ⟶ N') (m : M.carrier) (n : N.carrier) : (bimoduleModuleTensorMap Γ Δ f g).hom (bimoduleModuleTensorTmul Γ Δ M N m n) = bimoduleModuleTensorTmul Γ Δ M' N' (f.hom m) (g.hom n)

theorem TauCeti.GradedModuleCat.bimoduleModuleTensor_hom_ext {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {P : GradedModuleCat (Γ.piece ℤ)} {f g : bimoduleModuleTensorObj Γ Δ M N ⟶ P} (h : ∀ (m : M.carrier) (n : N.carrier), f.hom (bimoduleModuleTensorTmul Γ Δ M N m n) = g.hom (bimoduleModuleTensorTmul Γ Δ M N m n)) : f = g

Maps from a bimodule-module tensor are determined by their values on pure tensors.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensor_hom_ext_iff {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] {Γ : InternalGrading k A ℤ} {Δ : InternalGrading k B ℤ} [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {P : GradedModuleCat (Γ.piece ℤ)} {f g : bimoduleModuleTensorObj Γ Δ M N ⟶ P} : f = g ↔ ∀ (m : M.carrier) (n : N.carrier), f.hom (bimoduleModuleTensorTmul Γ Δ M N m n) = g.hom (bimoduleModuleTensorTmul Γ Δ M N m n)

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorLift {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {P : GradedModuleCat (Γ.piece ℤ)} (f : M.carrier →ₗ[k] N.carrier →ₗ[k] P.carrier) (hbalance : ∀ (b : B) (m : M.carrier) (n : N.carrier), (f (1 ⊗ₜ[k] MulOpposite.op b • m)) n = (f m) (b • n)) (hleft : ∀ (a : A) (m : M.carrier) (n : N.carrier), (f (a ⊗ₜ[k] 1 • m)) n = a • (f m) n) (hdegree : ∀ {p q : ℤ} {m : M.carrier} {n : N.carrier}, m ∈ M.grading.piece ℤ p → n ∈ N.grading.piece ℤ q → (f m) n ∈ P.grading.piece ℤ (p + q)) : bimoduleModuleTensorObj Γ Δ M N ⟶ P

Lift a balanced bilinear map respecting the left action and total internal degree.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorLift_tmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {P : GradedModuleCat (Γ.piece ℤ)} (f : M.carrier →ₗ[k] N.carrier →ₗ[k] P.carrier) (hbalance : ∀ (b : B) (m : M.carrier) (n : N.carrier), (f (1 ⊗ₜ[k] MulOpposite.op b • m)) n = (f m) (b • n)) (hleft : ∀ (a : A) (m : M.carrier) (n : N.carrier), (f (a ⊗ₜ[k] 1 • m)) n = a • (f m) n) (hdegree : ∀ {p q : ℤ} {m : M.carrier} {n : N.carrier}, m ∈ M.grading.piece ℤ p → n ∈ N.grading.piece ℤ q → (f m) n ∈ P.grading.piece ℤ (p + q)) (m : M.carrier) (n : N.carrier) : (bimoduleModuleTensorLift Γ Δ f hbalance hleft ⋯).hom (bimoduleModuleTensorTmul Γ Δ M N m n) = (f m) n

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorLift_unique {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {P : GradedModuleCat (Γ.piece ℤ)} (f : M.carrier →ₗ[k] N.carrier →ₗ[k] P.carrier) (hbalance : ∀ (b : B) (m : M.carrier) (n : N.carrier), (f (1 ⊗ₜ[k] MulOpposite.op b • m)) n = (f m) (b • n)) (hleft : ∀ (a : A) (m : M.carrier) (n : N.carrier), (f (a ⊗ₜ[k] 1 • m)) n = a • (f m) n) (hdegree : ∀ {p q : ℤ} {m : M.carrier} {n : N.carrier}, m ∈ M.grading.piece ℤ p → n ∈ N.grading.piece ℤ q → (f m) n ∈ P.grading.piece ℤ (p + q)) (g : bimoduleModuleTensorObj Γ Δ M N ⟶ P) (h : ∀ (m : M.carrier) (n : N.carrier), g.hom (bimoduleModuleTensorTmul Γ Δ M N m n) = (f m) n) : g = bimoduleModuleTensorLift Γ Δ f hbalance hleft ⋯

A homogeneous balanced left-module lift is determined by its pure-tensor values.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorMap_id {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} : bimoduleModuleTensorMap Γ Δ (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (bimoduleModuleTensorObj Γ Δ M N)

@[simp]

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

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorMap_add_left {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N' : GradedModuleCat (Δ.piece ℤ)} (f f' : M ⟶ M') (g : N ⟶ N') : bimoduleModuleTensorMap Γ Δ (f + f') g = bimoduleModuleTensorMap Γ Δ f g + bimoduleModuleTensorMap Γ Δ f' g

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorMap_add_right {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N' : GradedModuleCat (Δ.piece ℤ)} (f : M ⟶ M') (g g' : N ⟶ N') : bimoduleModuleTensorMap Γ Δ f (g + g') = bimoduleModuleTensorMap Γ Δ f g + bimoduleModuleTensorMap Γ Δ f g'

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorMap_smul_left {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N' : GradedModuleCat (Δ.piece ℤ)} (c : k) (f : M ⟶ M') (g : N ⟶ N') : bimoduleModuleTensorMap Γ Δ (c • f) g = c • bimoduleModuleTensorMap Γ Δ f g

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorMap_smul_right {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N' : GradedModuleCat (Δ.piece ℤ)} (c : k) (f : M ⟶ M') (g : N ⟶ N') : bimoduleModuleTensorMap Γ Δ f (c • g) = c • bimoduleModuleTensorMap Γ Δ f g

@[implicit_reducible]

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

Balanced tensor action of graded bimodules on graded left modules.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensor_obj_obj {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} : ((bimoduleModuleTensor Γ Δ).obj M).obj N = bimoduleModuleTensorObj Γ Δ M N

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensor_obj_map {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N N' : GradedModuleCat (Δ.piece ℤ)} (g : N ⟶ N') : ((bimoduleModuleTensor Γ Δ).obj M).map g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorMap Γ Δ (CategoryTheory.CategoryStruct.id M) g) (CategoryTheory.eqToHom ⋯))

theorem TauCeti.GradedModuleCat.bimoduleModuleTensor_obj_map_assoc {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N N' : GradedModuleCat (Δ.piece ℤ)} (g : N ⟶ N') {Z : GradedModuleCat (Γ.piece ℤ)} (h : ((bimoduleModuleTensor Γ Δ).obj M).obj N' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((bimoduleModuleTensor Γ Δ).obj M).map g) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorMap Γ Δ (CategoryTheory.CategoryStruct.id M) g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h))

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensor_map_app {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} (f : M ⟶ M') : ((bimoduleModuleTensor Γ Δ).map f).app N = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorMap Γ Δ f (CategoryTheory.CategoryStruct.id N)) (CategoryTheory.eqToHom ⋯))

theorem TauCeti.GradedModuleCat.bimoduleModuleTensor_map_app_assoc {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat (Δ.piece ℤ)} {M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} (f : M ⟶ M') {Z : GradedModuleCat (Γ.piece ℤ)} (h : ((bimoduleModuleTensor Γ Δ).obj M').obj N ⟶ Z) : CategoryTheory.CategoryStruct.comp (((bimoduleModuleTensor Γ Δ).map f).app N) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (bimoduleModuleTensorMap Γ Δ f (CategoryTheory.CategoryStruct.id N)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h))

instance TauCeti.GradedModuleCat.instAdditivePieceIntObjTensorProductMulOppositeTensorProductOppositeFunctorBimoduleModuleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} : ((bimoduleModuleTensor Γ Δ).obj M).Additive

instance TauCeti.GradedModuleCat.instAdditiveTensorProductMulOppositePieceIntTensorProductOppositeObjFunctorFlipBimoduleModuleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {N : GradedModuleCat (Δ.piece ℤ)} : ((bimoduleModuleTensor Γ Δ).flip.obj N).Additive

instance TauCeti.GradedModuleCat.instAdditiveTensorProductMulOppositePieceIntTensorProductOppositeFunctorBimoduleModuleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] : (bimoduleModuleTensor Γ Δ).Additive

instance TauCeti.GradedModuleCat.instAdditivePieceIntFunctorTensorProductMulOppositeTensorProductOppositeFlipBimoduleModuleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] : (bimoduleModuleTensor Γ Δ).flip.Additive

instance TauCeti.GradedModuleCat.instLinearPieceIntObjTensorProductMulOppositeTensorProductOppositeFunctorBimoduleModuleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} : CategoryTheory.Functor.Linear k ((bimoduleModuleTensor Γ Δ).obj M)

instance TauCeti.GradedModuleCat.instLinearTensorProductMulOppositePieceIntTensorProductOppositeObjFunctorFlipBimoduleModuleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] {N : GradedModuleCat (Δ.piece ℤ)} : CategoryTheory.Functor.Linear k ((bimoduleModuleTensor Γ Δ).flip.obj N)

instance TauCeti.GradedModuleCat.instLinearTensorProductMulOppositePieceIntTensorProductOppositeFunctorBimoduleModuleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] : CategoryTheory.Functor.Linear k (bimoduleModuleTensor Γ Δ)

instance TauCeti.GradedModuleCat.instLinearPieceIntFunctorTensorProductMulOppositeTensorProductOppositeFlipBimoduleModuleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] : CategoryTheory.Functor.Linear k (bimoduleModuleTensor Γ Δ).flip

@[instance_reducible]

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

The left outer action on the balanced tensor quotient.

@[instance_reducible]

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

The right outer action on the balanced tensor quotient.

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

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

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

@[instance_reducible]

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

The commuting outer actions combine into an action of the output envelope.

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

theorem TauCeti.GradedModuleCat.instGradedSMulIntSubmoduleBalancedTensorProductCarrierTensorProductMulOppositePieceGradingGrading_1 {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) : SetLike.GradedSMul (Γ.piece ℤ) ((BalancedTensorProduct.grading M.grading N.grading).piece ℤ)

theorem TauCeti.GradedModuleCat.instGradedSMulIntSubmoduleMulOppositeBalancedTensorProductCarrierTensorProductPieceOppositeOfDecompositionGradingGrading {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) : SetLike.GradedSMul ((InternalGrading.ofDecomposition (Θ.piece ℤ)).opposite.piece ℤ) ((BalancedTensorProduct.grading M.grading N.grading).piece ℤ)

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

The graded (A,C)-bimodule obtained by balancing over B.

def TauCeti.GradedModuleCat.bimoduleTensorTmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (m : M.carrier) (n : N.carrier) : (bimoduleTensorObj Γ Δ Θ M N).carrier

The pure tensor in the graded bimodule tensor product.

noncomputable def TauCeti.GradedModuleCat.bimoduleTensorUnderlyingEquiv {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) : (bimoduleTensorObj Γ Δ Θ M N).carrier ≃ₗ[k] BalancedTensorProduct k B M.carrier N.carrier

Forgetting the output grading identifies the tensor carrier with the balanced quotient. The factor actions in this quotient are the restrictions of the enveloping actions.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorUnderlyingEquiv_tmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (m : M.carrier) (n : N.carrier) : (bimoduleTensorUnderlyingEquiv Γ Δ Θ M N) (bimoduleTensorTmul Γ Δ Θ M N m n) = BalancedTensorProduct.tmul k B m n

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorUnderlyingEquiv_symm_tmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (m : M.carrier) (n : N.carrier) : (bimoduleTensorUnderlyingEquiv Γ Δ Θ M N).symm (BalancedTensorProduct.tmul k B m n) = bimoduleTensorTmul Γ Δ Θ M N m n

theorem TauCeti.GradedModuleCat.bimoduleTensorUnderlyingEquiv_mem_iff {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) {p : ℤ} {z : (bimoduleTensorObj Γ Δ Θ M N).carrier} : (bimoduleTensorUnderlyingEquiv Γ Δ Θ M N) z ∈ (BalancedTensorProduct.grading M.grading N.grading).piece ℤ p ↔ z ∈ (bimoduleTensorObj Γ Δ Θ M N).grading.piece ℤ p

The bimodule carrier identification preserves every internal degree piece.

theorem TauCeti.GradedModuleCat.bimoduleTensorUnderlyingEquiv_isHomogeneous {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) : LinearMap.IsHomogeneous (↑(bimoduleTensorUnderlyingEquiv Γ Δ Θ M N)) ((bimoduleTensorObj Γ Δ Θ M N).grading.piece ℤ) ((BalancedTensorProduct.grading M.grading N.grading).piece ℤ) 0

The bimodule tensor carrier identification is homogeneous of degree zero.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorTmul_zero_left {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (n : N.carrier) : bimoduleTensorTmul Γ Δ Θ M N 0 n = 0

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorTmul_zero_right {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (m : M.carrier) : bimoduleTensorTmul Γ Δ Θ M N m 0 = 0

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorTmul_add_left {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (m m' : M.carrier) (n : N.carrier) : bimoduleTensorTmul Γ Δ Θ M N (m + m') n = bimoduleTensorTmul Γ Δ Θ M N m n + bimoduleTensorTmul Γ Δ Θ M N m' n

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorTmul_add_right {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (m : M.carrier) (n n' : N.carrier) : bimoduleTensorTmul Γ Δ Θ M N m (n + n') = bimoduleTensorTmul Γ Δ Θ M N m n + bimoduleTensorTmul Γ Δ Θ M N m n'

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorTmul_smul_left {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (r : k) (m : M.carrier) (n : N.carrier) : bimoduleTensorTmul Γ Δ Θ M N (r • m) n = r • bimoduleTensorTmul Γ Δ Θ M N m n

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorTmul_smul_right {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (r : k) (m : M.carrier) (n : N.carrier) : bimoduleTensorTmul Γ Δ Θ M N m (r • n) = r • bimoduleTensorTmul Γ Δ Θ M N m n

theorem TauCeti.GradedModuleCat.bimoduleTensorTmul_mem {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) {p q : ℤ} {m : M.carrier} {n : N.carrier} (hm : m ∈ M.grading.piece ℤ p) (hn : n ∈ N.grading.piece ℤ q) : bimoduleTensorTmul Γ Δ Θ M N m n ∈ (bimoduleTensorObj Γ Δ Θ M N).grading.piece ℤ (p + q)

Internal degrees add on pure bimodule tensors.

theorem TauCeti.GradedModuleCat.bimoduleTensor_induction_on {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) {P : (bimoduleTensorObj Γ Δ Θ M N).carrier → Prop} (z : (bimoduleTensorObj Γ Δ Θ M N).carrier) (ht : ∀ (m : M.carrier) (n : N.carrier), P (bimoduleTensorTmul Γ Δ Θ M N m n)) (ha : ∀ (x y : (bimoduleTensorObj Γ Δ Θ M N).carrier), P x → P y → P (x + y)) : P z

Every bimodule tensor is a sum of pure tensors.

noncomputable def TauCeti.GradedModuleCat.bimoduleTensorMkQ {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) : TensorProduct k M.carrier N.carrier →ₗ[k] (bimoduleTensorObj Γ Δ Θ M N).carrier

The quotient map from the ground-ring tensor product.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorMkQ_tmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (m : M.carrier) (n : N.carrier) : (bimoduleTensorMkQ Γ Δ Θ M N) (m ⊗ₜ[k] n) = bimoduleTensorTmul Γ Δ Θ M N m n

theorem TauCeti.GradedModuleCat.bimoduleTensorObj_grading_piece {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (p : ℤ) : (bimoduleTensorObj Γ Δ Θ M N).grading.piece ℤ p = Submodule.map (bimoduleTensorMkQ Γ Δ Θ M N) ((M.grading.tensorProduct N.grading).piece ℤ p)

The internal degree piece is the image of the ground-ring tensor degree piece.

theorem TauCeti.GradedModuleCat.mem_bimoduleTensorObj_piece_iff {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) {p : ℤ} {z : (bimoduleTensorObj Γ Δ Θ M N).carrier} : z ∈ (bimoduleTensorObj Γ Δ Θ M N).grading.piece ℤ p ↔ ∃ x ∈ (M.grading.tensorProduct N.grading).piece ℤ p, (bimoduleTensorMkQ Γ Δ Θ M N) x = z

A homogeneous balanced tensor has a homogeneous ground-ring representative.

theorem TauCeti.GradedModuleCat.bimoduleTensorObj_map_mem_of_tmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) {Q : Type u_1} [AddCommGroup Q] [Module k Q] (H : InternalGrading k Q ℤ) (f : (bimoduleTensorObj Γ Δ Θ M N).carrier →ₗ[k] Q) (s : ℤ) (hf : ∀ {p q : ℤ} {m : M.carrier} {n : N.carrier}, m ∈ M.grading.piece ℤ p → n ∈ N.grading.piece ℤ q → f (bimoduleTensorTmul Γ Δ Θ M N m n) ∈ H.piece ℤ (p + q + s)) {p : ℤ} {z : (bimoduleTensorObj Γ Δ Θ M N).carrier} (hz : z ∈ (bimoduleTensorObj Γ Δ Θ M N).grading.piece ℤ p) : f z ∈ H.piece ℤ (p + s)

A linear map shifts the degree of every tensor if it does so on homogeneous pure tensors.

theorem TauCeti.GradedModuleCat.bimoduleTensorTmul_balance {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (b : B) (m : M.carrier) (n : N.carrier) : bimoduleTensorTmul Γ Δ Θ M N (1 ⊗ₜ[k] MulOpposite.op b • m) n = bimoduleTensorTmul Γ Δ Θ M N m (b ⊗ₜ[k] 1 • n)

Balancing moves the right B-action to the left B-action.

@[simp]

theorem TauCeti.GradedModuleCat.tmul_smul_bimoduleTensorTmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (a : A) (c : Cᵐᵒᵖ) (m : M.carrier) (n : N.carrier) : a ⊗ₜ[k] c • bimoduleTensorTmul Γ Δ Θ M N m n = bimoduleTensorTmul Γ Δ Θ M N (a ⊗ₜ[k] 1 • m) (1 ⊗ₜ[k] c • n)

A pure output enveloping scalar acts on the two outer factors.

theorem TauCeti.GradedModuleCat.bimoduleTensorUnderlyingEquiv_smul_left {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (a : A) (x : (bimoduleTensorObj Γ Δ Θ M N).carrier) : (bimoduleTensorUnderlyingEquiv Γ Δ Θ M N) (a • x) = a • (bimoduleTensorUnderlyingEquiv Γ Δ Θ M N) x

The underlying carrier identification preserves the restricted left outer action.

theorem TauCeti.GradedModuleCat.bimoduleTensorUnderlyingEquiv_smul_right {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (c : Cᵐᵒᵖ) (x : (bimoduleTensorObj Γ Δ Θ M N).carrier) : (bimoduleTensorUnderlyingEquiv Γ Δ Θ M N) (c • x) = c • (bimoduleTensorUnderlyingEquiv Γ Δ Θ M N) x

The underlying carrier identification preserves the restricted right outer action.

noncomputable def TauCeti.GradedModuleCat.bimoduleTensorMap {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : 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 ℤ)} (f : M ⟶ M') (g : N ⟶ N') : bimoduleTensorObj Γ Δ Θ M N ⟶ bimoduleTensorObj Γ Δ Θ M' N'

Tensor the degree-zero bimodule maps in both factors.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorMap_tmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : 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 ℤ)} (f : M ⟶ M') (g : N ⟶ N') (m : M.carrier) (n : N.carrier) : (bimoduleTensorMap Γ Δ Θ f g).hom (bimoduleTensorTmul Γ Δ Θ M N m n) = bimoduleTensorTmul Γ Δ Θ M' N' (f.hom m) (g.hom n)

theorem TauCeti.GradedModuleCat.bimoduleTensor_hom_ext {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} {P : GradedModuleCat ((Γ.tensorProduct Θ.opposite).piece ℤ)} {f g : bimoduleTensorObj Γ Δ Θ M N ⟶ P} (h : ∀ (m : M.carrier) (n : N.carrier), f.hom (bimoduleTensorTmul Γ Δ Θ M N m n) = g.hom (bimoduleTensorTmul Γ Δ Θ M N m n)) : f = g

Morphisms out of a bimodule tensor product agree if they agree on pure tensors.

theorem TauCeti.GradedModuleCat.bimoduleTensor_hom_ext_iff {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] {Γ : InternalGrading k A ℤ} {Δ : InternalGrading k B ℤ} {C : Type uC} [Ring C] [Algebra k C] {Θ : InternalGrading k C ℤ} [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} {P : GradedModuleCat ((Γ.tensorProduct Θ.opposite).piece ℤ)} {f g : bimoduleTensorObj Γ Δ Θ M N ⟶ P} : f = g ↔ ∀ (m : M.carrier) (n : N.carrier), f.hom (bimoduleTensorTmul Γ Δ Θ M N m n) = g.hom (bimoduleTensorTmul Γ Δ Θ M N m n)

noncomputable def TauCeti.GradedModuleCat.bimoduleTensorLift {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} {P : GradedModuleCat ((Γ.tensorProduct Θ.opposite).piece ℤ)} (f : M.carrier →ₗ[k] N.carrier →ₗ[k] P.carrier) (hbalance : ∀ (b : B) (m : M.carrier) (n : N.carrier), (f (1 ⊗ₜ[k] MulOpposite.op b • m)) n = (f m) (b ⊗ₜ[k] 1 • n)) (hleft : ∀ (a : A) (m : M.carrier) (n : N.carrier), (f (a ⊗ₜ[k] 1 • m)) n = a ⊗ₜ[k] 1 • (f m) n) (hright : ∀ (c : Cᵐᵒᵖ) (m : M.carrier) (n : N.carrier), (f m) (1 ⊗ₜ[k] c • n) = 1 ⊗ₜ[k] c • (f m) n) (hdegree : ∀ {p q : ℤ} {m : M.carrier} {n : N.carrier}, m ∈ M.grading.piece ℤ p → n ∈ N.grading.piece ℤ q → (f m) n ∈ P.grading.piece ℤ (p + q)) : bimoduleTensorObj Γ Δ Θ M N ⟶ P

Lift a balanced bilinear map that respects the two outer actions and internal degrees.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorLift_tmul {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} {P : GradedModuleCat ((Γ.tensorProduct Θ.opposite).piece ℤ)} (f : M.carrier →ₗ[k] N.carrier →ₗ[k] P.carrier) (hbalance : ∀ (b : B) (m : M.carrier) (n : N.carrier), (f (1 ⊗ₜ[k] MulOpposite.op b • m)) n = (f m) (b ⊗ₜ[k] 1 • n)) (hleft : ∀ (a : A) (m : M.carrier) (n : N.carrier), (f (a ⊗ₜ[k] 1 • m)) n = a ⊗ₜ[k] 1 • (f m) n) (hright : ∀ (c : Cᵐᵒᵖ) (m : M.carrier) (n : N.carrier), (f m) (1 ⊗ₜ[k] c • n) = 1 ⊗ₜ[k] c • (f m) n) (hdegree : ∀ {p q : ℤ} {m : M.carrier} {n : N.carrier}, m ∈ M.grading.piece ℤ p → n ∈ N.grading.piece ℤ q → (f m) n ∈ P.grading.piece ℤ (p + q)) (m : M.carrier) (n : N.carrier) : (bimoduleTensorLift Γ Δ Θ f hbalance hleft hright ⋯).hom (bimoduleTensorTmul Γ Δ Θ M N m n) = (f m) n

theorem TauCeti.GradedModuleCat.bimoduleTensorLift_unique {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} {P : GradedModuleCat ((Γ.tensorProduct Θ.opposite).piece ℤ)} (f : M.carrier →ₗ[k] N.carrier →ₗ[k] P.carrier) (hbalance : ∀ (b : B) (m : M.carrier) (n : N.carrier), (f (1 ⊗ₜ[k] MulOpposite.op b • m)) n = (f m) (b ⊗ₜ[k] 1 • n)) (hleft : ∀ (a : A) (m : M.carrier) (n : N.carrier), (f (a ⊗ₜ[k] 1 • m)) n = a ⊗ₜ[k] 1 • (f m) n) (hright : ∀ (c : Cᵐᵒᵖ) (m : M.carrier) (n : N.carrier), (f m) (1 ⊗ₜ[k] c • n) = 1 ⊗ₜ[k] c • (f m) n) (hdegree : ∀ {p q : ℤ} {m : M.carrier} {n : N.carrier}, m ∈ M.grading.piece ℤ p → n ∈ N.grading.piece ℤ q → (f m) n ∈ P.grading.piece ℤ (p + q)) (g : bimoduleTensorObj Γ Δ Θ M N ⟶ P) (h : ∀ (m : M.carrier) (n : N.carrier), g.hom (bimoduleTensorTmul Γ Δ Θ M N m n) = (f m) n) : g = bimoduleTensorLift Γ Δ Θ f hbalance hleft hright ⋯

The homogeneous balanced lift is uniquely determined by its pure-tensor values.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorMap_id {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} : bimoduleTensorMap Γ Δ Θ (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (bimoduleTensorObj Γ Δ Θ M N)

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorMap_comp {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} {M' M'' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N' N'' : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} (f : M ⟶ M') (g : N ⟶ N') (f' : M' ⟶ M'') (g' : N' ⟶ N'') : bimoduleTensorMap Γ Δ Θ (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (bimoduleTensorMap Γ Δ Θ f g) (bimoduleTensorMap Γ Δ Θ f' g')

Tensoring bimodule maps respects composition.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorMap_add_left {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : 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 ℤ)} (f f' : M ⟶ M') (g : N ⟶ N') : bimoduleTensorMap Γ Δ Θ (f + f') g = bimoduleTensorMap Γ Δ Θ f g + bimoduleTensorMap Γ Δ Θ f' g

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorMap_add_right {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : 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 ℤ)} (f : M ⟶ M') (g g' : N ⟶ N') : bimoduleTensorMap Γ Δ Θ f (g + g') = bimoduleTensorMap Γ Δ Θ f g + bimoduleTensorMap Γ Δ Θ f g'

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorMap_smul_left {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : 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 ℤ)} (c : k) (f : M ⟶ M') (g : N ⟶ N') : bimoduleTensorMap Γ Δ Θ (c • f) g = c • bimoduleTensorMap Γ Δ Θ f g

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensorMap_smul_right {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : 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 ℤ)} (c : k) (f : M ⟶ M') (g : N ⟶ N') : bimoduleTensorMap Γ Δ Θ f (c • g) = c • bimoduleTensorMap Γ Δ Θ f g

@[implicit_reducible]

noncomputable def TauCeti.GradedModuleCat.bimoduleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] : CategoryTheory.Functor (GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (CategoryTheory.Functor (GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (GradedModuleCat ((Γ.tensorProduct Θ.opposite).piece ℤ)))

Balanced tensor composition of internally graded bimodules.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensor_obj_obj {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} : ((bimoduleTensor Γ Δ Θ).obj M).obj N = bimoduleTensorObj Γ Δ Θ M N

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensor_obj_map {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N N' : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} (g : N ⟶ N') : ((bimoduleTensor Γ Δ Θ).obj M).map g = bimoduleTensorMap Γ Δ Θ (CategoryTheory.CategoryStruct.id M) g

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleTensor_map_app {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} {N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} {M' : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} (f : M ⟶ M') : ((bimoduleTensor Γ Δ Θ).map f).app N = bimoduleTensorMap Γ Δ Θ f (CategoryTheory.CategoryStruct.id N)

instance TauCeti.GradedModuleCat.instAdditiveTensorProductMulOppositePieceIntTensorProductOppositeObjFunctorBimoduleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} : ((bimoduleTensor Γ Δ Θ).obj M).Additive

instance TauCeti.GradedModuleCat.instAdditiveTensorProductMulOppositePieceIntTensorProductOppositeObjFunctorFlipBimoduleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} : ((bimoduleTensor Γ Δ Θ).flip.obj N).Additive

instance TauCeti.GradedModuleCat.instAdditiveTensorProductMulOppositePieceIntTensorProductOppositeFunctorBimoduleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] : (bimoduleTensor Γ Δ Θ).Additive

instance TauCeti.GradedModuleCat.instAdditiveTensorProductMulOppositePieceIntTensorProductOppositeFunctorFlipBimoduleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] : (bimoduleTensor Γ Δ Θ).flip.Additive

instance TauCeti.GradedModuleCat.instLinearTensorProductMulOppositePieceIntTensorProductOppositeObjFunctorBimoduleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {M : GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)} : CategoryTheory.Functor.Linear k ((bimoduleTensor Γ Δ Θ).obj M)

instance TauCeti.GradedModuleCat.instLinearTensorProductMulOppositePieceIntTensorProductOppositeObjFunctorFlipBimoduleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] {N : GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)} : CategoryTheory.Functor.Linear k ((bimoduleTensor Γ Δ Θ).flip.obj N)

instance TauCeti.GradedModuleCat.instLinearTensorProductMulOppositePieceIntTensorProductOppositeFunctorBimoduleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] : CategoryTheory.Functor.Linear k (bimoduleTensor Γ Δ Θ)

instance TauCeti.GradedModuleCat.instLinearTensorProductMulOppositePieceIntTensorProductOppositeFunctorFlipBimoduleTensor {k : Type uk} {A : Type uA} {B : Type uB} [CommRing k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) {C : Type uC} [Ring C] [Algebra k C] (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] : CategoryTheory.Functor.Linear k (bimoduleTensor Γ Δ Θ).flip

@[reducible, inline]

abbrev TauCeti.GradedBimoduleCat (k : Type w) [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (Ξ : InternalGrading k A ℤ) : Type (max (max uA w) ((max uA w) + 1))

The category of graded bimodules over the graded algebra A with internal grading Ξ: the graded modules over the enveloping grading Ξ.tensorProduct Ξ.opposite.