Koszul braiding for nonnegative chain complexes

On the summand of bidegree (p, q), interchange of tensor factors carries the sign (-1)^(p*q) to commute with the differential. TauCeti.NatChainComplex.koszulBraidingHom constructs this chain map in any braided preadditive monoidal category, assuming only that the two tensor complexes exist. It is an isomorphism in a braided category; in a symmetric category, its inverse is the same construction with the factors swapped.

The tensor-cochain formula is the chain-level interchange needed to compare the Alexander–Whitney diagonal with its transpose, and hence to prove graded commutativity of cup products. The cup formulas give signed interchange along a transposed diagonal, with the braided coefficient pairing. No commutativity is asserted for the Alexander–Whitney diagonal itself.

Main definitions and results

• TauCeti.NatChainComplex.koszulBraidingHom: the signed interchange chain map.
• TauCeti.NatChainComplex.ιTensorObj_koszulBraidingHom_f: its value on each bidegree summand.
• TauCeti.NatChainComplex.koszulBraidingHom_naturality: naturality in both chain complexes.
• TauCeti.NatChainComplex.koszulBraiding: the signed interchange isomorphism.
• TauCeti.NatChainComplex.inv_koszulBraidingHom: the inverse of the signed interchange map.
• TauCeti.NatChainComplex.ιTensorObj_koszulBraiding_inv_f: its inverse on each summand.
• TauCeti.NatChainComplex.koszulBraidingHom_comp: interchanging twice is the identity in a symmetric category.
• TauCeti.NatChainComplex.koszulBraidingHom_f_comp_tensorCochain: signed tensor-cochain interchange in every output degree.
• TauCeti.NatChainComplex.cupCochain_koszulBraidingHom: signed cup-cochain interchange.
• TauCeti.NatChainComplex.cup_koszulBraidingHom: signed interchange on cohomology.

Implementation notes

The TauCeti.NatChainComplex namespace distinguishes this construction from the integer-indexed cochain braiding. The tensor-cochain and cup formulas use the existing API in TauCeti.ChainComplex.

The construction follows the signed tensor differential in Mathlib's HomologicalComplex.tensorObj, and the summand method of TauCeti.koszulBraidingHom for integer-indexed cochain complexes. The differential out of degree zero vanishes, so one Leibniz term drops in bidegrees with a zero index. The construction requires no monoidal structure on the entire category of complexes. The inverse uses the inverse coefficient braiding, lifted by HomologicalComplex.Hom.isoOfComponents.

References

• A. Hatcher, Algebraic Topology, Section 3.2, for the graded-commutativity sign.
• C. Weibel, An Introduction to Homological Algebra, Section 2.7, for tensor complexes.

noncomputable def TauCeti.NatChainComplex.koszulBraidingHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] : HomologicalComplex.tensorObj A B ⟶ HomologicalComplex.tensorObj B A

Interchange the factors of a tensor product of nonnegative chain complexes, with the Koszul sign (-1)^(p*q) on its bidegree-(p, q) summand.

Equations

• TauCeti.NatChainComplex.koszulBraidingHom A B = { f := TauCeti.NatChainComplex.koszulBraidingX✝ A B, comm' := ⋯ }

@[simp]

theorem TauCeti.NatChainComplex.ιTensorObj_koszulBraidingHom_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] (p q n : ℕ) (h : p + q = n) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj A B p q n h) ((koszulBraidingHom A B).f n) = (-1) ^ (p * q) • CategoryTheory.CategoryStruct.comp (β_ (A.X p) (B.X q)).hom (HomologicalComplex.ιTensorObj B A q p n ⋯)

On the bidegree-(p, q) summand, interchange is the coefficient braiding multiplied by (-1)^(p*q), followed by the inclusion of the swapped summand.

@[simp]

theorem TauCeti.NatChainComplex.ιTensorObj_koszulBraidingHom_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] (p q n : ℕ) (h : p + q = n) {Z : C} (h✝ : (HomologicalComplex.tensorObj B A).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj A B p q n h) (CategoryTheory.CategoryStruct.comp ((koszulBraidingHom A B).f n) h✝) = CategoryTheory.CategoryStruct.comp ((-1) ^ (p * q) • CategoryTheory.CategoryStruct.comp (β_ (A.X p) (B.X q)).hom (HomologicalComplex.ιTensorObj B A q p n ⋯)) h✝

On the bidegree-(p, q) summand, interchange is the coefficient braiding multiplied by (-1)^(p*q), followed by the inclusion of the swapped summand.

theorem TauCeti.NatChainComplex.koszulBraidingHom_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] {A' B' : ChainComplex C ℕ} [HomologicalComplex.HasTensor A' B'] [HomologicalComplex.HasTensor B' A'] (f : A ⟶ A') (g : B ⟶ B') : CategoryTheory.CategoryStruct.comp (HomologicalComplex.tensorHom f g) (koszulBraidingHom A' B') = CategoryTheory.CategoryStruct.comp (koszulBraidingHom A B) (HomologicalComplex.tensorHom g f)

Koszul interchange is natural in both chain complexes.

theorem TauCeti.NatChainComplex.koszulBraidingHom_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] {A' B' : ChainComplex C ℕ} [HomologicalComplex.HasTensor A' B'] [HomologicalComplex.HasTensor B' A'] (f : A ⟶ A') (g : B ⟶ B') {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : HomologicalComplex.tensorObj B' A' ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.tensorHom f g) (CategoryTheory.CategoryStruct.comp (koszulBraidingHom A' B') h) = CategoryTheory.CategoryStruct.comp (koszulBraidingHom A B) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.tensorHom g f) h)

Koszul interchange is natural in both chain complexes.

noncomputable def TauCeti.NatChainComplex.koszulBraiding {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] : HomologicalComplex.tensorObj A B ≅ HomologicalComplex.tensorObj B A

The signed interchange isomorphism of tensor complexes in a braided coefficient category.

Equations

• TauCeti.NatChainComplex.koszulBraiding A B = HomologicalComplex.Hom.isoOfComponents (TauCeti.NatChainComplex.koszulBraidingXIso✝ A B) ⋯

@[simp]

theorem TauCeti.NatChainComplex.koszulBraiding_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] : (koszulBraiding A B).hom = koszulBraidingHom A B

The forward map of signed interchange is koszulBraidingHom.

instance TauCeti.NatChainComplex.instIsIsoHomologicalComplexNatDownKoszulBraidingHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] : CategoryTheory.IsIso (koszulBraidingHom A B)

@[simp]

theorem TauCeti.NatChainComplex.inv_koszulBraidingHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] : CategoryTheory.inv (koszulBraidingHom A B) = (koszulBraiding A B).inv

The categorical inverse of signed interchange is the inverse of koszulBraiding.

@[simp]

theorem TauCeti.NatChainComplex.koszulBraidingHom_comp_koszulBraiding_inv {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] : CategoryTheory.CategoryStruct.comp (koszulBraidingHom A B) (koszulBraiding A B).inv = CategoryTheory.CategoryStruct.id (HomologicalComplex.tensorObj A B)

Signed interchange followed by its inverse is the identity chain map.

@[simp]

theorem TauCeti.NatChainComplex.koszulBraidingHom_comp_koszulBraiding_inv_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : HomologicalComplex.tensorObj A B ⟶ Z) : CategoryTheory.CategoryStruct.comp (koszulBraidingHom A B) (CategoryTheory.CategoryStruct.comp (koszulBraiding A B).inv h) = h

Signed interchange followed by its inverse is the identity chain map.

@[simp]

theorem TauCeti.NatChainComplex.koszulBraiding_inv_comp_koszulBraidingHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] : CategoryTheory.CategoryStruct.comp (koszulBraiding A B).inv (koszulBraidingHom A B) = CategoryTheory.CategoryStruct.id (HomologicalComplex.tensorObj B A)

The inverse of signed interchange followed by the forward map is the identity chain map.

@[simp]

theorem TauCeti.NatChainComplex.koszulBraiding_inv_comp_koszulBraidingHom_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : HomologicalComplex.tensorObj B A ⟶ Z) : CategoryTheory.CategoryStruct.comp (koszulBraiding A B).inv (CategoryTheory.CategoryStruct.comp (koszulBraidingHom A B) h) = h

The inverse of signed interchange followed by the forward map is the identity chain map.

@[simp]

theorem TauCeti.NatChainComplex.ιTensorObj_koszulBraiding_inv_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] (p q n : ℕ) (h : q + p = n) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj B A q p n h) ((koszulBraiding A B).inv.f n) = (-1) ^ (p * q) • CategoryTheory.CategoryStruct.comp (β_ (A.X p) (B.X q)).inv (HomologicalComplex.ιTensorObj A B p q n ⋯)

On the bidegree-(q, p) summand, inverse interchange is the inverse coefficient braiding multiplied by (-1)^(p*q), followed by the inclusion of the swapped summand.

@[simp]

theorem TauCeti.NatChainComplex.ιTensorObj_koszulBraiding_inv_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] (p q n : ℕ) (h : q + p = n) {Z : C} (h✝ : (HomologicalComplex.tensorObj A B).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj B A q p n h) (CategoryTheory.CategoryStruct.comp ((koszulBraiding A B).inv.f n) h✝) = CategoryTheory.CategoryStruct.comp ((-1) ^ (p * q) • CategoryTheory.CategoryStruct.comp (β_ (A.X p) (B.X q)).inv (HomologicalComplex.ιTensorObj A B p q n ⋯)) h✝

On the bidegree-(q, p) summand, inverse interchange is the inverse coefficient braiding multiplied by (-1)^(p*q), followed by the inclusion of the swapped summand.

@[simp]

theorem TauCeti.NatChainComplex.koszulBraidingHom_comp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.SymmetricCategory C] : CategoryTheory.CategoryStruct.comp (koszulBraidingHom A B) (koszulBraidingHom B A) = CategoryTheory.CategoryStruct.id (HomologicalComplex.tensorObj A B)

In a symmetric category, interchanging tensor factors twice is the identity chain map.

@[simp]

theorem TauCeti.NatChainComplex.koszulBraidingHom_comp_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.SymmetricCategory C] {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : HomologicalComplex.tensorObj A B ⟶ Z) : CategoryTheory.CategoryStruct.comp (koszulBraidingHom A B) (CategoryTheory.CategoryStruct.comp (koszulBraidingHom B A) h) = h

In a symmetric category, interchanging tensor factors twice is the identity chain map.

@[simp]

theorem TauCeti.NatChainComplex.koszulBraiding_inv {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.SymmetricCategory C] : (koszulBraiding A B).inv = koszulBraidingHom B A

The inverse of signed interchange swaps the factors in the opposite order.

theorem TauCeti.NatChainComplex.koszulBraidingHom_f_comp_tensorCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj N M ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((koszulBraidingHom A B).f n) (ChainComplex.tensorCochain μ ψ φ n) = (-1) ^ (p * q) • ChainComplex.tensorCochain (CategoryTheory.CategoryStruct.comp (β_ M N).hom μ) φ ψ n

Precomposing a tensor product of cochains with Koszul interchange swaps the cochains and braids their coefficient pairing, with sign (-1)^(p*q). This holds in every output degree, including n ≠ p + q, where both sides are zero.

theorem TauCeti.NatChainComplex.koszulBraidingHom_f_comp_tensorCochain_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj N M ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) {Z : C} (h : P ⟶ Z) : CategoryTheory.CategoryStruct.comp ((koszulBraidingHom A B).f n) (CategoryTheory.CategoryStruct.comp (ChainComplex.tensorCochain μ ψ φ n) h) = CategoryTheory.CategoryStruct.comp ((-1) ^ (p * q) • ChainComplex.tensorCochain (CategoryTheory.CategoryStruct.comp (β_ M N).hom μ) φ ψ n) h

Precomposing a tensor product of cochains with Koszul interchange swaps the cochains and braids their coefficient pairing, with sign (-1)^(p*q). This holds in every output degree, including n ≠ p + q, where both sides are zero.

theorem TauCeti.NatChainComplex.cupCochain_koszulBraidingHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] [CategoryTheory.BraidedCategory C] {E : ChainComplex C ℕ} {M N P : C} (k : Type u_2) [CommSemiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj N M ⟶ P) {p q n : ℕ} (h : p + q = n) (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) : ((ChainComplex.cupCochain k (CategoryTheory.CategoryStruct.comp D (koszulBraidingHom A B)) μ q p n ⋯) ψ) φ = (-1) ^ (p * q) • ((ChainComplex.cupCochain k D (CategoryTheory.CategoryStruct.comp (β_ M N).hom μ) p q n h) φ) ψ

Transposing a diagonal swaps its cup product of cochains, braids the pairing, and introduces the Koszul sign.

theorem TauCeti.NatChainComplex.cup_koszulBraidingHom {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.BraidedCategory C] (A B : ChainComplex C ℕ) [HomologicalComplex.HasTensor A B] [HomologicalComplex.HasTensor B A] {E : ChainComplex C ℕ} {M N P : C} (k : Type u_3) [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj N M ⟶ P) {p q n : ℕ} (h : p + q = n) (a : ↑(HomologicalComplex.homology (A.linearYonedaObj k M) p)) (b : ↑(HomologicalComplex.homology (B.linearYonedaObj k N) q)) : ((ChainComplex.cup k (CategoryTheory.CategoryStruct.comp D (koszulBraidingHom A B)) μ q p n ⋯) b) a = (-1) ^ (p * q) • ((ChainComplex.cup k D (CategoryTheory.CategoryStruct.comp (β_ M N).hom μ) p q n h) a) b

Transposing a diagonal swaps the cup product on cohomology, with the Koszul sign and the braided coefficient pairing.