Exactness of a finite-projective graded bimodule tensor action

A graded (A,B)-bimodule finite projective as a right B-module acts on graded left B-modules by an exact functor to graded left A-modules. Its underlying balanced tensor carrier is naturally the ground-ring linear Hom module out of its opposite dual. Opposite-dual reflexivity and finite projectivity supply this identification, and projective lifting proves exactness on underlying modules. The existing graded exactness criterion then gives preservation of homology.

Only finiteness over the balancing algebra on the right is needed. Neither algebra nor the bimodule is required to be finite over the commutative ground ring. The carrier equivalence is not asserted to preserve the internal grading or the outer left action. The two module carrier universes are independent.

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorHomEquiv {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 ℤ)) [Module.Finite Bᵐᵒᵖ M.carrier] [Module.Projective Bᵐᵒᵖ M.carrier] (N : GradedModuleCat (Δ.piece ℤ)) : (bimoduleModuleTensorObj Γ Δ M N).carrier ≃ₗ[k] (M.carrier →ₗ[Bᵐᵒᵖ] B) →ₗ[B] N.carrier

The underlying tensor carrier is Hom from the opposite dual of a finite projective right module. This equivalence is linear over the ground ring.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorHomEquiv_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 ℤ)) [Module.Finite Bᵐᵒᵖ M.carrier] [Module.Projective Bᵐᵒᵖ M.carrier] (N : GradedModuleCat (Δ.piece ℤ)) (m : M.carrier) (n : N.carrier) (p : M.carrier →ₗ[Bᵐᵒᵖ] B) : ((bimoduleModuleTensorHomEquiv Γ Δ M N) (bimoduleModuleTensorTmul Γ Δ M N m n)) p = p m • n

The tensor–Hom equivalence evaluates a pure tensor by applying the functional.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorHomEquiv_naturality {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 ℤ)) [Module.Finite Bᵐᵒᵖ M.carrier] [Module.Projective Bᵐᵒᵖ M.carrier] {N N' : GradedModuleCat (Δ.piece ℤ)} (f : N ⟶ N') : LinearMap.compRight k f.hom ∘ₗ ↑(bimoduleModuleTensorHomEquiv Γ Δ M N) = ↑(bimoduleModuleTensorHomEquiv Γ Δ M N') ∘ₗ ↑k (((bimoduleModuleTensor Γ Δ).obj M).map f).hom

The tensor–Hom equivalence is natural in the graded left-module argument.

theorem TauCeti.GradedModuleCat.bimoduleModuleTensor_preservesHomology {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 ℤ)) [Module.Finite Bᵐᵒᵖ M.carrier] [Module.Projective Bᵐᵒᵖ M.carrier] : ((bimoduleModuleTensor Γ Δ).obj M).PreservesHomology

A graded bimodule finite projective over the balancing algebra on the right acts by a functor preserving homology of graded left modules.