Composition of cochains as a morphism of R-linear Hom complexes

Composition of cochains is R-bilinear and satisfies the Leibniz rule

δ (z₁.comp z₂) = z₁.comp (δ z₂) + (-1)^{|z₂|} • (δ z₁).comp z₂

(Mathlib's CochainComplex.HomComplex.δ_comp; Cochain.comp is written in diagrammatic order, so z₁ : Cochain F G n₁ comes first and z₂ : Cochain G K n₂ second). Together these say exactly that composition is a closed degree-zero map of R-linear Hom complexes, that is, a morphism

linearHomComplex R G K ⊗ linearHomComplex R F G ⟶ linearHomComplex R F K

in CochainComplex (ModuleCat R) ℤ. The order of the two tensor factors is forced by the Koszul sign rule: a morphism φ out of a tensor product of complexes is a chain map exactly when d (φ (x ⊗ y)) = φ (d x ⊗ y) + (-1)^{|x|} φ (x ⊗ d y), so the sign is carried by the term whose differential hits the second factor. In δ_comp the sign is carried by (δ z₁).comp z₂, the term differentiating z₁; hence z₁ must be the second tensor factor and z₂ the first. This is Keller's m₂ (g, f) = g ∘ f convention.

Mathlib's CategoryTheory.EnrichedCategory instead asks for Hom(X, Y) ⊗ Hom(Y, Z) ⟶ Hom(X, Z); converting between the two orders is exactly the Koszul braiding of CochainComplex (ModuleCat R) ℤ, built in TauCeti/Algebra/Homology/Monoidal/Braiding.lean and imported here. The EnrichedCategory instance and its associativity and unit axioms in Mathlib's factor order are constructed in TauCeti/Algebra/Homology/LinearHomComplex/Enrichment.lean.

The monoidal structure used here is Mathlib's HomologicalComplex.monoidalCategory at ComplexShape.up ℤ; nothing is re-totalized. The component equations for the whiskerings, the unitors and the associator, which Mathlib does not state, are taken from TauCeti/Algebra/Homology/Monoidal/Summand.lean rather than repeated here. Its colimit-preservation hypotheses are discharged by Mathlib's instances for a braided monoidal closed category, so Mathlib.CategoryTheory.Monoidal.Closed.Braided, which that file imports, is what makes the tensor product of cochain complexes exist at all. Note that ModuleCat.{v} R is monoidal only for a commutative R : Type v, so this file, unlike TauCeti/Algebra/Homology/LinearHomComplex/Basic.lean, requires CommRing R and ties the ring to the morphism universe of C.

Main definitions

• TauCeti.linearHomComplexComp: composition, as a morphism of R-linear Hom complexes out of the tensor product.
• TauCeti.linearHomComplexOfHom: a morphism of cochain complexes, as a degree-zero cocycle in the corresponding R-linear Hom complex.
• TauCeti.linearHomComplexUnit: the identity cochain, as a morphism from the tensor unit.

Main results

• TauCeti.ι_linearHomComplexComp: the degree-j component restricted to a bidegree summand is TauCeti.cochainCompTensor; TauCeti.cochainCompTensor_tmul gives its pure-tensor formula.
• TauCeti.linearHomComplexComp_naturality_source and TauCeti.linearHomComplexComp_naturality_target: composition is natural in the source and in the target cochain complex.
• TauCeti.linearHomComplexComp_dinaturality_middle: composition is dinatural in the middle cochain complex.
• TauCeti.linearHomComplexComp_assoc, TauCeti.linearHomComplexOfHom_comp, and TauCeti.linearHomComplexComp_ofHom: composition is associative and composing with a degree-zero cocycle recovers postcomposition or precomposition; the unit laws are their identity specializations.
• TauCeti.linearHomComplexOfHom_f_zero_apply: a morphism of complexes gives its associated cochain in degree zero.

This advances TauCetiRoadmap/DGAInfinity/README.md, Layer 0, item "signed graded multilinear and tensor-coalgebra infrastructure", specifically "construct the k-linear Hom complex, its signed differential ..., closed composition map, and the enrichment". The stage that bullet orders first, the complex-level Koszul braiding, is TauCeti/Algebra/Homology/Monoidal/Braiding.lean. No formalization is vendored: the Leibniz rule δ_comp and the totalized monoidal structure are Mathlib's.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 3.1.
• B. Keller, Deriving DG categories, Section 1.
• Joël Riou's Mathlib cochain/δ and totalization API, together with the totalized HomologicalComplex.monoidalCategory of Joël Riou and Kim Morrison in Mathlib/Algebra/Homology/Monoidal.lean. This file assembles Riou's δ_comp and the totalization API into the ModuleCat R-valued composition map, inheriting their sign convention.

noncomputable def TauCeti.cochainCompTensor (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G K : CochainComplex C ℤ) (p q j : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = j) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((linearHomComplex R G K).X p) ((linearHomComplex R F G).X q) ⟶ (linearHomComplex R F K).X j

Composition of a degree-p cochain from G to K with a degree-q cochain from F to G, as a map out of the tensor product of the two cochain modules. This is the bidegree-(p, q) component of TauCeti.linearHomComplexComp.

Equations

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

@[simp]

theorem TauCeti.cochainCompTensor_tmul (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G K : CochainComplex C ℤ) (p q j : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = j) (z₂ : ↑↧(CochainComplex.HomComplex.Cochain G K p)) (z₁ : ↑↧(CochainComplex.HomComplex.Cochain F G q)) : (ModuleCat.Hom.hom (cochainCompTensor R F G K p q j h)) (z₂ ⊗ₜ[R] z₁) = CochainComplex.HomComplex.Cochain.comp z₁ z₂ ⋯

On a pure tensor, cochainCompTensor sends z₂ ⊗ₜ z₁ to the composite z₁.comp z₂.

noncomputable def TauCeti.linearHomComplexComp (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G K : CochainComplex C ℤ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (linearHomComplex R G K) (linearHomComplex R F G) ⟶ linearHomComplex R F K

Composition of cochains is a closed degree-zero map. It assembles into a morphism of cochain complexes of R-modules out of the tensor product; the differential of a composite is computed by the Leibniz rule, which is precisely the condition for this to be a chain map.

Equations

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

@[simp]

theorem TauCeti.ι_linearHomComplexComp (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G K : CochainComplex C ℤ) (p q j : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = j) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (linearHomComplex R G K) (linearHomComplex R F G) (CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)) (ComplexShape.up ℤ) p q j h) ((linearHomComplexComp R F G K).f j) = cochainCompTensor R F G K p q j h

The degree-j component of composition restricted to the bidegree-(p, q) summand is cochainCompTensor; see cochainCompTensor_tmul for its value on pure tensors.

@[simp]

theorem TauCeti.ι_linearHomComplexComp_assoc (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G K : CochainComplex C ℤ) (p q j : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = j) {Z : ModuleCat R} (h✝ : (linearHomComplex R F K).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (linearHomComplex R G K) (linearHomComplex R F G) (CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)) (ComplexShape.up ℤ) p q j h) (CategoryTheory.CategoryStruct.comp ((linearHomComplexComp R F G K).f j) h✝) = CategoryTheory.CategoryStruct.comp (cochainCompTensor R F G K p q j h) h✝

The degree-j component of composition restricted to the bidegree-(p, q) summand is cochainCompTensor; see cochainCompTensor_tmul for its value on pure tensors.

noncomputable def TauCeti.linearHomComplexOfHom (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CochainComplex (ModuleCat R) ℤ) ⟶ linearHomComplex R F G

A morphism of cochain complexes, regarded as a degree-zero cocycle in the corresponding R-linear Hom complex.

Equations

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

theorem TauCeti.linearHomComplexOfHom_f_zero (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) : (linearHomComplexOfHom R φ).f 0 = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))).hom (ModuleCat.ofHom (LinearMap.toSpanSingleton R (CochainComplex.HomComplex.Cochain F G 0) (CochainComplex.HomComplex.Cochain.ofHom φ)))

The degree-zero component of linearHomComplexOfHom as a morphism in ModuleCat.

@[simp]

theorem TauCeti.linearHomComplexOfHom_f_zero_apply (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) (r : R) : (ModuleCat.Hom.hom ((linearHomComplexOfHom R φ).f 0)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))).inv) r) = r • CochainComplex.HomComplex.Cochain.ofHom φ

The degree-zero component of linearHomComplexOfHom sends a scalar to that scalar multiple of the associated cochain.

noncomputable def TauCeti.linearHomComplexUnit (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F : CochainComplex C ℤ) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CochainComplex (ModuleCat R) ℤ) ⟶ linearHomComplex R F F

The identity cochain of F, as a morphism from the tensor unit to the R-linear Hom complex of F with itself.

Equations

• TauCeti.linearHomComplexUnit R F = TauCeti.linearHomComplexOfHom R (CategoryTheory.CategoryStruct.id F)

theorem TauCeti.linearHomComplexUnit_def (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F : CochainComplex C ℤ) : linearHomComplexUnit R F = linearHomComplexOfHom R (CategoryTheory.CategoryStruct.id F)

The unit is the degree-zero cocycle associated to the identity morphism.

@[simp]

theorem TauCeti.linearHomComplexUnit_f_zero_apply (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F : CochainComplex C ℤ) (r : R) : (ModuleCat.Hom.hom ((linearHomComplexUnit R F).f 0)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))).inv) r) = r • CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id F)

The degree-zero component of the unit sends a scalar to the corresponding scalar multiple of the identity cochain.

theorem TauCeti.linearHomComplexComp_naturality_source (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F₁ F₂ : CochainComplex C ℤ} (φ : F₁ ⟶ F₂) (G K : CochainComplex C ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (linearHomComplex R G K) (linearHomComplexPrecomp R φ G)) (linearHomComplexComp R F₁ G K) = CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F₂ G K) (linearHomComplexPrecomp R φ K)

Composition is natural in the source: composing after precomposition by φ is the same as precomposing the composite by φ. This is associativity of Cochain.comp with the degree-zero cochain Cochain.ofHom φ in the first (diagrammatic) argument.

theorem TauCeti.linearHomComplexComp_naturality_source_assoc (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F₁ F₂ : CochainComplex C ℤ} (φ : F₁ ⟶ F₂) (G K : CochainComplex C ℤ) {Z : CochainComplex (ModuleCat R) ℤ} (h : linearHomComplex R F₁ K ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (linearHomComplex R G K) (linearHomComplexPrecomp R φ G)) (CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F₁ G K) h) = CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F₂ G K) (CategoryTheory.CategoryStruct.comp (linearHomComplexPrecomp R φ K) h)

Composition is natural in the source: composing after precomposition by φ is the same as precomposing the composite by φ. This is associativity of Cochain.comp with the degree-zero cochain Cochain.ofHom φ in the first (diagrammatic) argument.

theorem TauCeti.linearHomComplexComp_naturality_target (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {K₁ K₂ : CochainComplex C ℤ} (ψ : K₁ ⟶ K₂) (F G : CochainComplex C ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (linearHomComplexPostcomp R G ψ) (linearHomComplex R F G)) (linearHomComplexComp R F G K₂) = CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F G K₁) (linearHomComplexPostcomp R F ψ)

Composition is natural in the target: composing after postcomposition by ψ is the same as postcomposing the composite by ψ. This is associativity of Cochain.comp with the degree-zero cochain Cochain.ofHom ψ in the last (diagrammatic) argument.

theorem TauCeti.linearHomComplexComp_naturality_target_assoc (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {K₁ K₂ : CochainComplex C ℤ} (ψ : K₁ ⟶ K₂) (F G : CochainComplex C ℤ) {Z : CochainComplex (ModuleCat R) ℤ} (h : linearHomComplex R F K₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (linearHomComplexPostcomp R G ψ) (linearHomComplex R F G)) (CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F G K₂) h) = CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F G K₁) (CategoryTheory.CategoryStruct.comp (linearHomComplexPostcomp R F ψ) h)

Composition is natural in the target: composing after postcomposition by ψ is the same as postcomposing the composite by ψ. This is associativity of Cochain.comp with the degree-zero cochain Cochain.ofHom ψ in the last (diagrammatic) argument.

theorem TauCeti.linearHomComplexComp_dinaturality_middle (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {G₁ G₂ : CochainComplex C ℤ} (ψ : G₁ ⟶ G₂) (F K : CochainComplex C ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (linearHomComplexPrecomp R ψ K) (linearHomComplex R F G₁)) (linearHomComplexComp R F G₁ K) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (linearHomComplex R G₂ K) (linearHomComplexPostcomp R F ψ)) (linearHomComplexComp R F G₂ K)

Composition is dinatural in the middle object: precomposition in the first Hom complex agrees with postcomposition in the second Hom complex.

theorem TauCeti.linearHomComplexComp_dinaturality_middle_assoc (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {G₁ G₂ : CochainComplex C ℤ} (ψ : G₁ ⟶ G₂) (F K : CochainComplex C ℤ) {Z : CochainComplex (ModuleCat R) ℤ} (h : linearHomComplex R F K ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (linearHomComplexPrecomp R ψ K) (linearHomComplex R F G₁)) (CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F G₁ K) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (linearHomComplex R G₂ K) (linearHomComplexPostcomp R F ψ)) (CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F G₂ K) h)

Composition is dinatural in the middle object: precomposition in the first Hom complex agrees with postcomposition in the second Hom complex.

@[simp]

theorem TauCeti.linearHomComplexComp_assoc (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G K : CochainComplex C ℤ} (L : CochainComplex C ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (linearHomComplexComp R G K L) (linearHomComplex R F G)) (linearHomComplexComp R F G L) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (linearHomComplex R K L) (linearHomComplex R G K) (linearHomComplex R F G)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (linearHomComplex R K L) (linearHomComplexComp R F G K)) (linearHomComplexComp R F K L))

Composition of cochains is associative, with the tensor products identified by the monoidal associator.

@[simp]

theorem TauCeti.linearHomComplexComp_assoc_assoc (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G K : CochainComplex C ℤ} (L : CochainComplex C ℤ) {Z : CochainComplex (ModuleCat R) ℤ} (h : linearHomComplex R F L ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (linearHomComplexComp R G K L) (linearHomComplex R F G)) (CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F G L) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (linearHomComplex R K L) (linearHomComplex R G K) (linearHomComplex R F G)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (linearHomComplex R K L) (linearHomComplexComp R F G K)) (CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F K L) h))

Composition of cochains is associative, with the tensor products identified by the monoidal associator.

theorem TauCeti.linearHomComplexOfHom_comp (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G K : CochainComplex C ℤ} (ψ : G ⟶ K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (linearHomComplexOfHom R ψ) (linearHomComplex R F G)) (linearHomComplexComp R F G K) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (linearHomComplex R F G)).hom (linearHomComplexPostcomp R F ψ)

Composing with the degree-zero cocycle associated to ψ is postcomposition by ψ.

theorem TauCeti.linearHomComplexOfHom_comp_assoc (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G K : CochainComplex C ℤ} (ψ : G ⟶ K) {Z : CochainComplex (ModuleCat R) ℤ} (h : linearHomComplex R F K ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (linearHomComplexOfHom R ψ) (linearHomComplex R F G)) (CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F G K) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (linearHomComplex R F G)).hom (CategoryTheory.CategoryStruct.comp (linearHomComplexPostcomp R F ψ) h)

Composing with the degree-zero cocycle associated to ψ is postcomposition by ψ.

@[simp]

theorem TauCeti.linearHomComplexUnit_comp (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (linearHomComplexUnit R G) (linearHomComplex R F G)) (linearHomComplexComp R F G G) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (linearHomComplex R F G)).hom

The identity cochain is a left unit for composition.

@[simp]

theorem TauCeti.linearHomComplexUnit_comp_assoc (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {Z : CochainComplex (ModuleCat R) ℤ} (h : linearHomComplex R F G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (linearHomComplexUnit R G) (linearHomComplex R F G)) (CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F G G) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (linearHomComplex R F G)).hom h

The identity cochain is a left unit for composition.

theorem TauCeti.linearHomComplexComp_ofHom (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G F' : CochainComplex C ℤ} (φ : F' ⟶ F) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (linearHomComplex R F G) (linearHomComplexOfHom R φ)) (linearHomComplexComp R F' F G) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (linearHomComplex R F G)).hom (linearHomComplexPrecomp R φ G)

Composing with the degree-zero cocycle associated to φ is precomposition by φ.

theorem TauCeti.linearHomComplexComp_ofHom_assoc (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G F' : CochainComplex C ℤ} (φ : F' ⟶ F) {Z : CochainComplex (ModuleCat R) ℤ} (h : linearHomComplex R F' G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (linearHomComplex R F G) (linearHomComplexOfHom R φ)) (CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F' F G) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (linearHomComplex R F G)).hom (CategoryTheory.CategoryStruct.comp (linearHomComplexPrecomp R φ G) h)

Composing with the degree-zero cocycle associated to φ is precomposition by φ.

@[simp]

theorem TauCeti.linearHomComplexComp_unit (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (linearHomComplex R F G) (linearHomComplexUnit R F)) (linearHomComplexComp R F F G) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (linearHomComplex R F G)).hom

The identity cochain is a right unit for composition.

@[simp]

theorem TauCeti.linearHomComplexComp_unit_assoc (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {Z : CochainComplex (ModuleCat R) ℤ} (h : linearHomComplex R F G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (linearHomComplex R F G) (linearHomComplexUnit R F)) (CategoryTheory.CategoryStruct.comp (linearHomComplexComp R F F G) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (linearHomComplex R F G)).hom h

The identity cochain is a right unit for composition.