The differential on a balanced tensor product of DG modules

For a right DG module M and a left DG module N over the same DG algebra A, the ordinary balanced tensor product carries the differential d (m ⊗ n) = dM m ⊗ n + (-1)^|m| m ⊗ dN n. The two module Leibniz rules make this formula balanced even when the algebra differential is nonzero. Its square vanishes by cancellation of the mixed terms.

This file constructs that endomorphism over an arbitrary commutative ground ring and proves compatibility with tensoring DG module morphisms and with the regular-module unit identifications. It supplies the differential on the underlying balanced module; a grading on the quotient and outer bimodule actions are separate constructions.

References

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

noncomputable def TauCeti.BalancedTensorProduct.differential {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {dA : A →ₗ[R] A} {hA : IsDGAlgebra 𝒜 dA} {ℳ : ℤ → Submodule R M} {ℳN : ℤ → Submodule R N} [DirectSum.Decomposition ℳ] [DirectSum.Decomposition ℳN] [SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ] [SetLike.GradedSMul 𝒜 ℳN] {dM : M →ₗ[R] M} {dN : N →ₗ[R] N} (hM : IsDGRightModule hA ℳ dM) (hN : IsDGLeftModule hA ℳN dN) : Module.End R (BalancedTensorProduct R A M N)

The signed tensor differential on the ordinary balanced tensor product of a right and a left DG module. No flatness assumption is needed for this underived construction.

Equations

• TauCeti.BalancedTensorProduct.differential hM hN = TauCeti.BalancedTensorProduct.lift TauCeti.BalancedTensorProduct.differentialBilinear✝ ⋯

@[simp]

theorem TauCeti.BalancedTensorProduct.differential_tmul {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {dA : A →ₗ[R] A} {hA : IsDGAlgebra 𝒜 dA} {ℳ : ℤ → Submodule R M} {ℳN : ℤ → Submodule R N} [DirectSum.Decomposition ℳ] [DirectSum.Decomposition ℳN] [SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ] [SetLike.GradedSMul 𝒜 ℳN] {dM : M →ₗ[R] M} {dN : N →ₗ[R] N} (hM : IsDGRightModule hA ℳ dM) (hN : IsDGLeftModule hA ℳN dN) (m : M) (n : N) : (differential hM hN) (tmul R A m n) = tmul R A (dM m) n + tmul R A (((InternalGrading.ofDecomposition ℳ).koszulTwist 1) m) (dN n)

On arbitrary pure tensors, the sign is represented by the grading's Koszul twist.

theorem TauCeti.BalancedTensorProduct.differential_tmul_of_mem {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {dA : A →ₗ[R] A} {hA : IsDGAlgebra 𝒜 dA} {ℳ : ℤ → Submodule R M} {ℳN : ℤ → Submodule R N} [DirectSum.Decomposition ℳ] [DirectSum.Decomposition ℳN] [SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ] [SetLike.GradedSMul 𝒜 ℳN] {dM : M →ₗ[R] M} {dN : N →ₗ[R] N} (hM : IsDGRightModule hA ℳ dM) (hN : IsDGLeftModule hA ℳN dN) {q : ℤ} {m : M} (hm : m ∈ ℳ q) (n : N) : (differential hM hN) (tmul R A m n) = tmul R A (dM m) n + ↑↑q.negOnePow • tmul R A m (dN n)

The tensor differential has the usual sign on a homogeneous left factor.

@[simp]

theorem TauCeti.BalancedTensorProduct.differential_comp_self {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {dA : A →ₗ[R] A} {hA : IsDGAlgebra 𝒜 dA} {ℳ : ℤ → Submodule R M} {ℳN : ℤ → Submodule R N} [DirectSum.Decomposition ℳ] [DirectSum.Decomposition ℳN] [SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ] [SetLike.GradedSMul 𝒜 ℳN] {dM : M →ₗ[R] M} {dN : N →ₗ[R] N} (hM : IsDGRightModule hA ℳ dM) (hN : IsDGLeftModule hA ℳN dN) : differential hM hN ∘ₗ differential hM hN = 0

The differential on the balanced tensor product squares to zero.

@[simp]

theorem TauCeti.BalancedTensorProduct.differential_sq_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {dA : A →ₗ[R] A} {hA : IsDGAlgebra 𝒜 dA} {ℳ : ℤ → Submodule R M} {ℳN : ℤ → Submodule R N} [DirectSum.Decomposition ℳ] [DirectSum.Decomposition ℳN] [SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ] [SetLike.GradedSMul 𝒜 ℳN] {dM : M →ₗ[R] M} {dN : N →ₗ[R] N} (hM : IsDGRightModule hA ℳ dM) (hN : IsDGLeftModule hA ℳN dN) (z : BalancedTensorProduct R A M N) : (differential hM hN) ((differential hM hN) z) = 0

Applying the tensor differential twice gives zero.

theorem TauCeti.BalancedTensorProduct.differential_naturality {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {dA : A →ₗ[R] A} {hA : IsDGAlgebra 𝒜 dA} {ℳ : ℤ → Submodule R M} {ℳN : ℤ → Submodule R N} [DirectSum.Decomposition ℳ] [DirectSum.Decomposition ℳN] [SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ] [SetLike.GradedSMul 𝒜 ℳN] {dM : M →ₗ[R] M} {dN : N →ₗ[R] N} {M' : Type u_5} {N' : Type u_6} [AddCommGroup M'] [Module R M'] [Module Aᵐᵒᵖ M'] [IsScalarTower R Aᵐᵒᵖ M'] [AddCommGroup N'] [Module R N'] [Module A N'] [IsScalarTower R A N'] {ℳ' : ℤ → Submodule R M'} {ℳN' : ℤ → Submodule R N'} [DirectSum.Decomposition ℳ'] [DirectSum.Decomposition ℳN'] [SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ'] [SetLike.GradedSMul 𝒜 ℳN'] {dM' : M' →ₗ[R] M'} {dN' : N' →ₗ[R] N'} (hM : IsDGRightModule hA ℳ dM) (hN : IsDGLeftModule hA ℳN dN) (hM' : IsDGRightModule hA ℳ' dM') (hN' : IsDGLeftModule hA ℳN' dN') (f : M →ₗ[R] M') (g : N →ₗ[R] N') (hf : ∀ (a : A) (m : M), f (MulOpposite.op a • m) = MulOpposite.op a • f m) (hg : ∀ (a : A) (n : N), g (a • n) = a • g n) (hf₀ : LinearMap.IsHomogeneous f ℳ ℳ' 0) (hfd : dM' ∘ₗ f = f ∘ₗ dM) (hgd : dN' ∘ₗ g = g ∘ₗ dN) : differential hM' hN' ∘ₗ map f g hf hg = map f g hf hg ∘ₗ differential hM hN

Tensoring equivariant chain maps, with the first map of degree zero, commutes with the balanced tensor differential. Only the first map's degree is needed for this differential identity.

@[simp]

theorem TauCeti.BalancedTensorProduct.lid_comp_differential {R : Type u_1} {A : Type u_2} {N : Type u_4} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {dA : A →ₗ[R] A} {ℳN : ℤ → Submodule R N} [DirectSum.Decomposition ℳN] [SetLike.GradedSMul 𝒜 ℳN] {dN : N →ₗ[R] N} (hA : IsDGAlgebra 𝒜 dA) (hN : IsDGLeftModule hA ℳN dN) : ↑(lid R A N) ∘ₗ differential ⋯ hN = dN ∘ₗ ↑(lid R A N)

The left regular-module unit identification commutes with the tensor differential.

@[simp]

theorem TauCeti.BalancedTensorProduct.rid_comp_differential {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {dA : A →ₗ[R] A} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ] {dM : M →ₗ[R] M} (hA : IsDGAlgebra 𝒜 dA) (hM : IsDGRightModule hA ℳ dM) : ↑(rid R A M) ∘ₗ differential hM ⋯ = dM ∘ₗ ↑(rid R A M)

The right regular-module unit identification commutes with the tensor differential.