Horizontal composition of homogeneous dg natural transformations

The Godement product of α : F ⟶ F' of degree n and β : G ⟶ G' of degree m is a transformation F ⋙ G ⟶ F' ⋙ G' of degree n + m. Whiskering supplies the two halves and HomogeneousNatTrans.interchange says the two possible readings differ by (-1)^(m * n), so a choice has to be made.

The choice, and what it costs

hcomp is the reading that whiskers α first:

α ⋆ β := (α ◁ G) ≫ (F' ▷ β).

Nothing forces this over the other order, and hcomp_eq_smul_swap records the price of swapping. What the choice buys is that the two unit laws come out as the two whiskerings with no sign at all (id_hcomp, hcomp_id), and that the Leibniz rule below has its sign on the term where the repository's dgComp convention already puts it.

The Leibniz rule is the point

hcomp is vertical composition in the dg category of dg functors, applied to two whiskerings, and whiskering commutes with the differential. So the differential of a Godement product obeys the graded Leibniz rule of that dg category:

δ (α ⋆ β) = α ⋆ δβ + (-1)^m • (δα ⋆ β).

That is differential_hcomp, and it is what makes horizontal composition a dg-level operation rather than a bookkeeping convenience: it says the product of two closed transformations is closed (IsClosed.hcomp) and that a homotopy in either argument produces a homotopy of the product.

Strictness

Dg functors compose strictly (DGFunctor.comp_assoc, DGFunctor.id_comp, DGFunctor.comp_id, all rfl), so hcomp_assoc is an equation between transformations of the same type rather than a coherence isomorphism, and the unit laws need no comparison either. Only the degrees have to be threaded, which is why every statement below carries its result degree explicitly, as HomogeneousNatTrans.composition does.

def CategoryTheory.DGFunctor.HomogeneousNatTrans.hcomp {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F F' : DGFunctor C D} {G G' : DGFunctor D E} {n m : ℤ} (α : ↥(F.HomogeneousNatTrans F' n)) (β : ↥(G.HomogeneousNatTrans G' m)) (r : ℤ) (h : n + m = r) : ↥((F.comp G).HomogeneousNatTrans (F'.comp G') r)

The Godement product.

α is whiskered on the right by G, β on the left by F', and the two are composed vertically in the result degree r. See hcomp_eq_smul_swap for the other reading.

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.hcomp_app {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F F' : DGFunctor C D} {G G' : DGFunctor D E} {n m : ℤ} (α : ↥(F.HomogeneousNatTrans F' n)) (β : ↥(G.HomogeneousNatTrans G' m)) (r : ℤ) (h : n + m = r) (X : C) : app (hcomp α β r h) X = ((DGCategoryStruct.dgComp n m r h) ((G.map n) (app α X))) (app β (F'.obj X))

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.hcomp_eq_smul_swap {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F F' : DGFunctor C D} {G G' : DGFunctor D E} {n m : ℤ} (α : ↥(F.HomogeneousNatTrans F' n)) (β : ↥(G.HomogeneousNatTrans G' m)) (r : ℤ) (h : n + m = r) (h' : m + n = r) : hcomp α β r h = (m * n).negOnePow • ((composition (F.comp G) (F.comp G') (F'.comp G') m n r h') (whiskerLeft F β)) (whiskerRight α G')

Swapping the order of the product costs (-1)^(m * n).

This is interchange, read as a statement about hcomp. The sign is graded naturality of β evaluated at the degree-n component of α, so it is not a convention: whichever reading is taken as the definition, the other one carries that factor.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.hcomp_app_swap {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F F' : DGFunctor C D} {G G' : DGFunctor D E} {n m : ℤ} (α : ↥(F.HomogeneousNatTrans F' n)) (β : ↥(G.HomogeneousNatTrans G' m)) (r : ℤ) (h : n + m = r) (h' : m + n = r) (X : C) : app (hcomp α β r h) X = (m * n).negOnePow • ((DGCategoryStruct.dgComp m n r h') (app β (F.obj X))) ((G'.map n) (app α X))

The componentwise form of hcomp_eq_smul_swap.

Additivity in each argument

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.hcomp_zero_left {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F F' : DGFunctor C D} {G G' : DGFunctor D E} {n m : ℤ} (β : ↥(G.HomogeneousNatTrans G' m)) (r : ℤ) (h : n + m = r) : hcomp 0 β r h = 0

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.hcomp_zero_right {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F F' : DGFunctor C D} {G G' : DGFunctor D E} {n m : ℤ} (α : ↥(F.HomogeneousNatTrans F' n)) (r : ℤ) (h : n + m = r) : hcomp α 0 r h = 0

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.hcomp_add_left {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F F' : DGFunctor C D} {G G' : DGFunctor D E} {n m : ℤ} (α α' : ↥(F.HomogeneousNatTrans F' n)) (β : ↥(G.HomogeneousNatTrans G' m)) (r : ℤ) (h : n + m = r) : hcomp (α + α') β r h = hcomp α β r h + hcomp α' β r h

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.hcomp_add_right {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F F' : DGFunctor C D} {G G' : DGFunctor D E} {n m : ℤ} (α : ↥(F.HomogeneousNatTrans F' n)) (β β' : ↥(G.HomogeneousNatTrans G' m)) (r : ℤ) (h : n + m = r) : hcomp α (β + β') r h = hcomp α β r h + hcomp α β' r h

def CategoryTheory.DGFunctor.HomogeneousNatTrans.horizontalComposition {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F F' : DGFunctor C D) (G G' : DGFunctor D E) (n m r : ℤ) (h : n + m = r) : ↥(F.HomogeneousNatTrans F' n) →+ ↥(G.HomogeneousNatTrans G' m) →+ ↥((F.comp G).HomogeneousNatTrans (F'.comp G') r)

Horizontal composition as a biadditive map, in a fixed result degree.

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.horizontalComposition_apply {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F F' : DGFunctor C D} {G G' : DGFunctor D E} {n m : ℤ} (α : ↥(F.HomogeneousNatTrans F' n)) (β : ↥(G.HomogeneousNatTrans G' m)) (r : ℤ) (h : n + m = r) : ((horizontalComposition F F' G G' n m r h) α) β = hcomp α β r h

Units

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.id_hcomp {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {G G' : DGFunctor D E} {m : ℤ} (F : DGFunctor C D) (β : ↥(G.HomogeneousNatTrans G' m)) : hcomp (id F) β m ⋯ = whiskerLeft F β

Horizontally composing with an identity on the left is left whiskering. No sign appears, which is one reason to take this order as the definition.

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.hcomp_id {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F F' : DGFunctor C D} {n : ℤ} (α : ↥(F.HomogeneousNatTrans F' n)) (G : DGFunctor D E) : hcomp α (id G) n ⋯ = whiskerRight α G

Horizontally composing with an identity on the right is right whiskering.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.id_hcomp_id {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) (G : DGFunctor D E) : hcomp (id F) (id G) 0 ⋯ = id (F.comp G)

The differential

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.differential_hcomp {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F F' : DGFunctor C D} {G G' : DGFunctor D E} {n m : ℤ} (α : ↥(F.HomogeneousNatTrans F' n)) (β : ↥(G.HomogeneousNatTrans G' m)) (r : ℤ) (h : n + m = r) : differential (hcomp α β r h) = hcomp α (differential β) (r + 1) ⋯ + m.negOnePow • hcomp (differential α) β (r + 1) ⋯

The graded Leibniz rule for the Godement product.

δ (α ⋆ β) = α ⋆ δβ + (-1)^m • (δα ⋆ β), with m the degree of β. Both whiskerings commute with the differential, so this is the Leibniz rule of the dg category of dg functors applied to the vertical composite that defines hcomp; the sign is the repository's dgComp convention and nothing more.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.IsClosed.hcomp {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F F' : DGFunctor C D} {G G' : DGFunctor D E} {n m : ℤ} {α : ↥(F.HomogeneousNatTrans F' n)} {β : ↥(G.HomogeneousNatTrans G' m)} (hα : IsClosed α) (hβ : IsClosed β) (r : ℤ) (h : n + m = r) : IsClosed (HomogeneousNatTrans.hcomp α β r h)

The Godement product of two closed transformations is closed.

Associativity

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.hcomp_assoc {C : Type u} {D : Type u'} {E : Type u''} {B : Type u'''} [DGCategory C] [DGCategory D] [DGCategory E] [DGCategory B] {F F' : DGFunctor C D} {G G' : DGFunctor D E} {H H' : DGFunctor E B} {n m k : ℤ} (α : ↥(F.HomogeneousNatTrans F' n)) (β : ↥(G.HomogeneousNatTrans G' m)) (γ : ↥(H.HomogeneousNatTrans H' k)) (nm mk s : ℤ) (hnm : n + m = nm) (hmk : m + k = mk) (hs : nm + k = s) (hs' : n + mk = s) : hcomp (hcomp α β nm hnm) γ s hs = hcomp α (hcomp β γ mk hmk) s hs'

The Godement product is strictly associative.

Dg functors compose strictly, so both sides are transformations F ⋙ G ⋙ H ⟶ F' ⋙ G' ⋙ H' of the same degree and the statement needs no comparison isomorphism. The proof is DGFunctor.map_comp for H, then associativity of the graded composition.