The Koszul braiding on cochain complexes of modules

Mathlib's HomologicalComplex.monoidalCategory, instantiated at ComplexShape.up ℤ and its ComplexShape.TensorSigns, makes CochainComplex (ModuleCat R) ℤ monoidal by totalizing the degreewise tensor product. It does not make it braided: Mathlib's GradedObject.braidedCategory uses the braiding of the base category on each summand with no sign, and that map does not commute with the totalized differential.

This file supplies the missing sign. On the bidegree-(p, q) summand of X ⊗ Y the braiding is (-1)^{p * q} times the braiding of ModuleCat R, that is, x ⊗ y ↦ (-1)^{|x| * |y|} y ⊗ x on homogeneous elements. The sign is forced: the totalized differential carries ComplexShape.up ℤ's tensor signs ε₁ = 1 and ε₂ (p, q) = (-1)^p, and the two Leibniz terms match after transposing exactly when the summand map is scaled by (-1)^{p * q}.

Main definitions

• TauCeti.koszulBraidingSummand: the bidegree component of the braiding.
• TauCeti.koszulBraidingHom, TauCeti.koszulBraiding: the braiding X ⊗ Y ⟶ Y ⊗ X of cochain complexes and the isomorphism it underlies.
• TauCeti.koszulBraidedCategory and TauCeti.koszulSymmetricCategory: the BraidedCategory and SymmetricCategory instances on CochainComplex (ModuleCat R) ℤ.

Main results

• TauCeti.koszulBraidingHom_naturality_left and TauCeti.koszulBraidingHom_naturality_right: the braiding is natural in each factor.
• TauCeti.koszulBraidingHom_hexagon_forward and TauCeti.koszulBraidingHom_hexagon_reverse: the two hexagon identities.
• TauCeti.koszulBraidingHom_comp: the braiding is symmetric.
• TauCeti.ι_tensorμ: on a homogeneous summand, the middle-four interchange MonoidalCategory.tensorμ of cochain complexes is that of ModuleCat R, with the Koszul sign of the two factors it exchanges.

The two auxiliary equations HomologicalComplex.whiskerLeft_eq_mapBifunctorMap and HomologicalComplex.whiskerRight_eq_mapBifunctorMap of TauCeti/Algebra/Homology/Monoidal/Summand.lean, which record that the whiskerings of CochainComplex (ModuleCat R) ℤ are HomologicalComplex.mapBifunctorMap, are used throughout.

This advances TauCetiRoadmap/DGAInfinity/README.md, Layer 0, item "signed graded multilinear and tensor-coalgebra infrastructure", specifically "Complete the symmetric monoidal structure on unbounded CochainComplex (ModuleCat k) ℤ ... What has to be added is the braiding: transport GradedObject.braidedCategory through the totalization, supply the Koszul sign x ⊗ y ↦ (-1)^{|x||y|} y ⊗ x on the degreewise summands, and prove the hexagon and symmetry axioms at complex level." It is the prerequisite, in the roadmap's own order, of the R-linear Hom complex and its composition map built in TauCeti/Algebra/Homology/LinearHomComplex/.

Implementation notes

Mathlib.CategoryTheory.Monoidal.Closed.Braided is imported for the colimit-preservation instances that make the tensor product of cochain complexes exist at all, exactly as in TauCeti/Algebra/Homology/LinearHomComplex/Composition.lean.

The hexagon proofs restrict both sides to a tridegree summand with HomologicalComplex.mapBifunctor₁₂.hom_ext and then reduce to the corresponding hexagon of ModuleCat R; the second hexagon is deduced from the first by inverting every isomorphism involved, which is legitimate because the braiding is symmetric.

References

• The totalized monoidal structure HomologicalComplex.monoidalCategory in Mathlib/Algebra/Homology/Monoidal.lean, by Joël Riou and Kim Morrison, and the unsigned GradedObject.Monoidal.braiding of Mathlib/CategoryTheory/GradedObject/Braiding.lean, by Joël Riou. This file adds the Koszul sign and the complex-level axioms; nothing is vendored.
• B. Keller, Introduction to A-infinity algebras and modules, Section 3.1, for the sign convention.

noncomputable def TauCeti.koszulBraidingSummand (R : Type v) [CommRing R] (X Y : CochainComplex (ModuleCat R) ℤ) (p q j : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = j) : CategoryTheory.MonoidalCategoryStruct.tensorObj (X.X p) (Y.X q) ⟶ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X).X j

The bidegree-(p, q) component of the Koszul braiding X ⊗ Y ⟶ Y ⊗ X: the braiding of ModuleCat R on the summand X.X p ⊗ Y.X q, carrying the Koszul sign (-1)^{p * q}.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.koszulBraidingSummand_def (R : Type v) [CommRing R] (X Y : CochainComplex (ModuleCat R) ℤ) (p q j : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = j) : koszulBraidingSummand R X Y p q j h = (p * q).negOnePow • CategoryTheory.CategoryStruct.comp (β_ (X.X p) (Y.X q)).hom (HomologicalComplex.ιMapBifunctor Y X (CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)) (ComplexShape.up ℤ) q p j ⋯)

The bidegree component of the Koszul braiding is the ordinary module braiding, followed by the inclusion of the swapped summand, and scaled by (-1)^(p*q).

noncomputable def TauCeti.koszulBraidingHom (R : Type v) [CommRing R] (X Y : CochainComplex (ModuleCat R) ℤ) : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X

The Koszul braiding X ⊗ Y ⟶ Y ⊗ X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ι_koszulBraidingHom (R : Type v) [CommRing R] (X Y : CochainComplex (ModuleCat R) ℤ) (p q j : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = j) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor X Y (CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)) (ComplexShape.up ℤ) p q j h) ((koszulBraidingHom R X Y).f j) = koszulBraidingSummand R X Y p q j h

@[simp]

theorem TauCeti.ι_koszulBraidingHom_assoc (R : Type v) [CommRing R] (X Y : CochainComplex (ModuleCat R) ℤ) (p q j : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = j) {Z : ModuleCat R} (h✝ : (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor X Y (CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)) (ComplexShape.up ℤ) p q j h) (CategoryTheory.CategoryStruct.comp ((koszulBraidingHom R X Y).f j) h✝) = CategoryTheory.CategoryStruct.comp (koszulBraidingSummand R X Y p q j h) h✝

theorem TauCeti.koszulBraidingHom_comp (R : Type v) [CommRing R] (X Y : CochainComplex (ModuleCat R) ℤ) : CategoryTheory.CategoryStruct.comp (koszulBraidingHom R X Y) (koszulBraidingHom R Y X) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

Composing the Koszul braiding with the braiding of the swapped factors is the identity.

theorem TauCeti.koszulBraidingHom_naturality_left (R : Type v) [CommRing R] {X Y : CochainComplex (ModuleCat R) ℤ} (f : X ⟶ Y) (Z : CochainComplex (ModuleCat R) ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (koszulBraidingHom R Y Z) = CategoryTheory.CategoryStruct.comp (koszulBraidingHom R X Z) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)

The Koszul braiding is natural in the left-hand factor.

theorem TauCeti.koszulBraidingHom_naturality_right (R : Type v) [CommRing R] (X : CochainComplex (ModuleCat R) ℤ) {Y Z : CochainComplex (ModuleCat R) ℤ} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (koszulBraidingHom R X Z) = CategoryTheory.CategoryStruct.comp (koszulBraidingHom R X Y) (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)

The Koszul braiding is natural in the right-hand factor.

theorem TauCeti.koszulBraidingHom_hexagon_forward (R : Type v) [CommRing R] (X Y Z : CochainComplex (ModuleCat R) ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (koszulBraidingHom R X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (koszulBraidingHom R X Y) Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (koszulBraidingHom R X Z)))

The first hexagon identity for the Koszul braiding.

noncomputable def TauCeti.koszulBraiding (R : Type v) [CommRing R] (X Y : CochainComplex (ModuleCat R) ℤ) : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X

The Koszul braiding of two cochain complexes of R-modules, as an isomorphism. It is its own inverse up to swapping the factors, since ModuleCat R is symmetric and the Koszul sign is.

Equations

• TauCeti.koszulBraiding R X Y = { hom := TauCeti.koszulBraidingHom R X Y, inv := TauCeti.koszulBraidingHom R Y X, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem TauCeti.koszulBraidingHom_hexagon_reverse (R : Type v) [CommRing R] (X Y Z : CochainComplex (ModuleCat R) ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (koszulBraidingHom R (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (koszulBraidingHom R Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (koszulBraidingHom R X Z) Y))

The second hexagon identity for the Koszul braiding. It follows from the first one applied to Z, X, Y by inverting every isomorphism involved, because the braiding is symmetric.

@[simp]

theorem TauCeti.koszulBraiding_hom (R : Type v) [CommRing R] (X Y : CochainComplex (ModuleCat R) ℤ) : (koszulBraiding R X Y).hom = koszulBraidingHom R X Y

The forward direction of the Koszul braiding isomorphism.

@[simp]

theorem TauCeti.koszulBraiding_inv (R : Type v) [CommRing R] (X Y : CochainComplex (ModuleCat R) ℤ) : (koszulBraiding R X Y).inv = koszulBraidingHom R Y X

The inverse of the Koszul braiding isomorphism is the Koszul braiding of the two complexes in the other order.

@[instance_reducible]

noncomputable instance TauCeti.koszulBraidedCategory (R : Type v) [CommRing R] : CategoryTheory.BraidedCategory (CochainComplex (ModuleCat R) ℤ)

Cochain complexes of R-modules form a braided monoidal category, with the Koszul braiding x ⊗ y ↦ (-1)^{|x| * |y|} y ⊗ x on the degreewise summands of Mathlib's totalized tensor product.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.braiding_eq_koszulBraiding (R : Type v) [CommRing R] (X Y : CochainComplex (ModuleCat R) ℤ) : β_ X Y = koszulBraiding R X Y

The braiding of the monoidal category CochainComplex (ModuleCat R) ℤ is the Koszul braiding.

@[instance_reducible]

noncomputable instance TauCeti.koszulSymmetricCategory (R : Type v) [CommRing R] : CategoryTheory.SymmetricCategory (CochainComplex (ModuleCat R) ℤ)

The Koszul braiding is symmetric.

Equations

• TauCeti.koszulSymmetricCategory R = { toBraidedCategory := TauCeti.koszulBraidedCategory R, symmetry := ⋯ }

theorem TauCeti.ι_tensorμ (R : Type v) [CommRing R] (X₁ X₂ Y₁ Y₂ : CochainComplex (ModuleCat R) ℤ) (a b c d ab cd n : ℤ) (hab : a + b = ab) (hcd : c + d = cd) (h : ab + cd = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (HomologicalComplex.ιTensorObj X₁ X₂ a b ab hab) (HomologicalComplex.ιTensorObj Y₁ Y₂ c d cd hcd)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂).ιTensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂) ab cd n h) ((CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂).f n)) = (b * c).negOnePow • CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (X₁.X a) (X₂.X b) (Y₁.X c) (Y₂.X d)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (HomologicalComplex.ιTensorObj X₁ Y₁ a c (a + c) ⋯) (HomologicalComplex.ιTensorObj X₂ Y₂ b d (b + d) ⋯)) ((CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁).ιTensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) (a + c) (b + d) n ⋯))

The middle-four interchange on a homogeneous summand. On the summand (X₁.X a ⊗ X₂.X b) ⊗ (Y₁.X c ⊗ Y₂.X d) of (X₁ ⊗ X₂) ⊗ (Y₁ ⊗ Y₂), the interchange MonoidalCategory.tensorμ of cochain complexes is the interchange of the four modules, landing in the summand (X₁.X a ⊗ Y₁.X c) ⊗ (X₂.X b ⊗ Y₂.X d), with the Koszul sign (-1)^(b * c) of moving the degree-b factor past the degree-c factor.

theorem TauCeti.ι_tensorμ_assoc (R : Type v) [CommRing R] (X₁ X₂ Y₁ Y₂ : CochainComplex (ModuleCat R) ℤ) (a b c d ab cd n : ℤ) (hab : a + b = ab) (hcd : c + d = cd) (h : ab + cd = n) {Z : ModuleCat R} (h✝ : (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (HomologicalComplex.ιTensorObj X₁ X₂ a b ab hab) (HomologicalComplex.ιTensorObj Y₁ Y₂ c d cd hcd)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂).ιTensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂) ab cd n h) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂).f n) h✝)) = CategoryTheory.CategoryStruct.comp ((b * c).negOnePow • CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (X₁.X a) (X₂.X b) (Y₁.X c) (Y₂.X d)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (HomologicalComplex.ιTensorObj X₁ Y₁ a c (a + c) ⋯) (HomologicalComplex.ιTensorObj X₂ Y₂ b d (b + d) ⋯)) ((CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁).ιTensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) (a + c) (b + d) n ⋯))) h✝

The middle-four interchange on a homogeneous summand. On the summand (X₁.X a ⊗ X₂.X b) ⊗ (Y₁.X c ⊗ Y₂.X d) of (X₁ ⊗ X₂) ⊗ (Y₁ ⊗ Y₂), the interchange MonoidalCategory.tensorμ of cochain complexes is the interchange of the four modules, landing in the summand (X₁.X a ⊗ Y₁.X c) ⊗ (X₂.X b ⊗ Y₂.X d), with the Koszul sign (-1)^(b * c) of moving the degree-b factor past the degree-c factor.