Total gradings on balanced tensor products

The balancing relations for a right and a left graded module are homogeneous for total cohomological degree. The quotient therefore inherits an internal grading, with |m ⊗ n| = |m| + |n|. Its degree pieces are generated by the corresponding homogeneous pure tensors. The quotient map preserves degree, and tensoring homogeneous equivariant maps adds their degrees.

This is the grading needed to equip the ordinary balanced tensor product of differential graded modules with its cochain complex. No flatness or finite-dimensionality is required. The construction reuses InternalGrading.tensorProduct and InternalGrading.quotient. Only an internal decomposition of the balancing semiring and homogeneous module actions are needed; its multiplication need not respect that decomposition, and its ground-ring module structure need not arise from an algebra structure.

References

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

theorem TauCeti.BalancedTensorProduct.isHomogeneous_relations {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Semiring A] [Module R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] {𝒜 : ℤ → Submodule R A} [DirectSum.Decomposition 𝒜] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G.piece ℤ)] [SetLike.GradedSMul 𝒜 (H.piece ℤ)] : DirectSum.SetLike.IsHomogeneous ((G.tensorProduct H).piece ℤ) (balancedTensorRelations R A M N)

Balancing relations are homogeneous for the total grading: both terms of a relation on homogeneous inputs have degree |a| + |m| + |n|.

noncomputable def TauCeti.BalancedTensorProduct.grading {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Semiring A] [Module R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] {𝒜 : ℤ → Submodule R A} [DirectSum.Decomposition 𝒜] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G.piece ℤ)] [SetLike.GradedSMul 𝒜 (H.piece ℤ)] : InternalGrading R (BalancedTensorProduct R A M N) ℤ

The total-degree grading of a tensor product balanced over homogeneous module actions.

@[simp]

theorem TauCeti.BalancedTensorProduct.grading_piece {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Semiring A] [Module R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] {𝒜 : ℤ → Submodule R A} [DirectSum.Decomposition 𝒜] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G.piece ℤ)] [SetLike.GradedSMul 𝒜 (H.piece ℤ)] (p : ℤ) : (grading G H).piece ℤ p = Submodule.map (mkQ R A) ((G.tensorProduct H).piece ℤ p)

A degree piece is the image of the corresponding ground-ring tensor degree piece.

theorem TauCeti.BalancedTensorProduct.mem_grading_piece_iff {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Semiring A] [Module R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] {𝒜 : ℤ → Submodule R A} [DirectSum.Decomposition 𝒜] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G.piece ℤ)] [SetLike.GradedSMul 𝒜 (H.piece ℤ)] {p : ℤ} {z : BalancedTensorProduct R A M N} : z ∈ (grading G H).piece ℤ p ↔ ∃ x ∈ (G.tensorProduct H).piece ℤ p, (mkQ R A) x = z

A balanced tensor is homogeneous exactly when it has a homogeneous ground-ring representative of the same degree.

theorem TauCeti.BalancedTensorProduct.grading_piece_eq_iSup {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Semiring A] [Module R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] {𝒜 : ℤ → Submodule R A} [DirectSum.Decomposition 𝒜] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G.piece ℤ)] [SetLike.GradedSMul 𝒜 (H.piece ℤ)] (p : ℤ) : (grading G H).piece ℤ p = ⨆ (q : ℤ), Submodule.map₂ (mk R A) (G.piece ℤ q) (H.piece ℤ (p - q))

The degree pieces are sums of images of homogeneous pure tensors.

theorem TauCeti.BalancedTensorProduct.tmul_mem_grading {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Semiring A] [Module R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] {𝒜 : ℤ → Submodule R A} [DirectSum.Decomposition 𝒜] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G.piece ℤ)] [SetLike.GradedSMul 𝒜 (H.piece ℤ)] {p q : ℤ} {m : M} {n : N} (hm : m ∈ G.piece ℤ p) (hn : n ∈ H.piece ℤ q) : tmul R A m n ∈ (grading G H).piece ℤ (p + q)

Degrees add on homogeneous pure balanced tensors.

theorem TauCeti.BalancedTensorProduct.map_mem_of_tmul {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Semiring A] [Module R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] {𝒜 : ℤ → Submodule R A} [DirectSum.Decomposition 𝒜] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G.piece ℤ)] [SetLike.GradedSMul 𝒜 (H.piece ℤ)] {Q : Type u_5} [AddCommMonoid Q] [Module R Q] (𝓟 : ℤ → Submodule R Q) (f : BalancedTensorProduct R A M N →ₗ[R] Q) (s : ℤ) (hf : ∀ {p q : ℤ} {m : M} {n : N}, m ∈ G.piece ℤ p → n ∈ H.piece ℤ q → f (tmul R A m n) ∈ 𝓟 (p + q + s)) {p : ℤ} {z : BalancedTensorProduct R A M N} (hz : z ∈ (grading G H).piece ℤ p) : f z ∈ 𝓟 (p + s)

A linear map shifts balanced tensor degrees if it does so on homogeneous pure tensors.

theorem TauCeti.BalancedTensorProduct.isHomogeneous_of_tmul {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Semiring A] [Module R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] {𝒜 : ℤ → Submodule R A} [DirectSum.Decomposition 𝒜] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G.piece ℤ)] [SetLike.GradedSMul 𝒜 (H.piece ℤ)] {Q : Type u_5} [AddCommMonoid Q] [Module R Q] (𝓟 : ℤ → Submodule R Q) (f : BalancedTensorProduct R A M N →ₗ[R] Q) (s : ℤ) (hf : ∀ {p q : ℤ} {m : M} {n : N}, m ∈ G.piece ℤ p → n ∈ H.piece ℤ q → f (tmul R A m n) ∈ 𝓟 (p + q + s)) : LinearMap.IsHomogeneous f ((grading G H).piece ℤ) 𝓟 s

Homogeneity of a balanced tensor map can be checked on homogeneous pure tensors.

theorem TauCeti.BalancedTensorProduct.isHomogeneous_mkQ {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Semiring A] [Module R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] {𝒜 : ℤ → Submodule R A} [DirectSum.Decomposition 𝒜] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G.piece ℤ)] [SetLike.GradedSMul 𝒜 (H.piece ℤ)] : LinearMap.IsHomogeneous (mkQ R A) ((G.tensorProduct H).piece ℤ) ((grading G H).piece ℤ) 0

The quotient map preserves total degree.

theorem TauCeti.BalancedTensorProduct.isHomogeneous_map {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Semiring A] [Module R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] {𝒜 : ℤ → Submodule R A} [DirectSum.Decomposition 𝒜] (G : InternalGrading R M ℤ) (H : InternalGrading R N ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G.piece ℤ)] [SetLike.GradedSMul 𝒜 (H.piece ℤ)] {M' : Type u_5} {N' : Type u_6} [AddCommGroup M'] [Module R M'] [Module Aᵐᵒᵖ M'] [AddCommGroup N'] [Module R N'] [Module A N'] (G' : InternalGrading R M' ℤ) (H' : InternalGrading R N' ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G'.piece ℤ)] [SetLike.GradedSMul 𝒜 (H'.piece ℤ)] (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) {r s : ℤ} (hf₀ : LinearMap.IsHomogeneous f (G.piece ℤ) (G'.piece ℤ) r) (hg₀ : LinearMap.IsHomogeneous g (H.piece ℤ) (H'.piece ℤ) s) : LinearMap.IsHomogeneous (map f g hf hg) ((grading G H).piece ℤ) ((grading G' H').piece ℤ) (r + s)

Tensoring homogeneous equivariant maps adds their degrees for the balanced total grading.

theorem TauCeti.BalancedTensorProduct.tensorGradedRight {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [Semiring A] [Module R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] {𝒜 : ℤ → Submodule R A} [DirectSum.Decomposition 𝒜] {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] : SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ((InternalGrading.ofDecomposition ℳ).piece ℤ)

theorem TauCeti.BalancedTensorProduct.tensorGradedLeft {R : Type u_1} {A : Type u_2} {N : Type u_4} [CommRing R] [Semiring A] [Module R A] [AddCommGroup N] [Module R N] [Module A N] {𝒜 : ℤ → Submodule R A} {𝒩 : ℤ → Submodule R N} [DirectSum.Decomposition 𝒩] [SetLike.GradedSMul 𝒜 𝒩] : SetLike.GradedSMul 𝒜 ((InternalGrading.ofDecomposition 𝒩).piece ℤ)

theorem TauCeti.BalancedTensorProduct.hom_ext_of_mem {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Semiring A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] {P : Type u_7} [AddCommGroup P] [Module R P] {φ ψ : BalancedTensorProduct R A M N →ₗ[R] P} (h : ∀ {q : ℤ} {m : M}, m ∈ ℳ q → ∀ (n : N), φ (tmul R A m n) = ψ (tmul R A m n)) : φ = ψ

Maps out of the balanced tensor product agree once they agree on pure tensors with a homogeneous left factor.

theorem TauCeti.BalancedTensorProduct.isHomogeneous_map_grading {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Semiring A] [Module R A] [AddCommGroup M] [Module R M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module R N] [Module A N] {𝒜 : ℤ → Submodule R A} [DirectSum.Decomposition 𝒜] {M' : Type u_5} {N' : Type u_6} [AddCommGroup M'] [Module R M'] [Module Aᵐᵒᵖ M'] [AddCommGroup N'] [Module R N'] [Module A N'] {ℳ : ℤ → Submodule R M} {𝒩 : ℤ → Submodule R N} {ℳ' : ℤ → Submodule R M'} {𝒩' : ℤ → Submodule R N'} [DirectSum.Decomposition ℳ] [DirectSum.Decomposition 𝒩] [DirectSum.Decomposition ℳ'] [DirectSum.Decomposition 𝒩'] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] [SetLike.GradedSMul 𝒜 𝒩] [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ'] [SetLike.GradedSMul 𝒜 𝒩'] (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) {r s : ℤ} (hf₀ : LinearMap.IsHomogeneous f ℳ ℳ' r) (hg₀ : LinearMap.IsHomogeneous g 𝒩 𝒩' s) : LinearMap.IsHomogeneous (map f g hf hg) ((grading (InternalGrading.ofDecomposition ℳ) (InternalGrading.ofDecomposition 𝒩)).piece ℤ) ((grading (InternalGrading.ofDecomposition ℳ') (InternalGrading.ofDecomposition 𝒩')).piece ℤ) (r + s)

Tensoring homogeneous equivariant maps adds their degrees for the total grading of the balanced tensor product of internally decomposed modules.