Whiskering homogeneous dg natural transformations

A homogeneous dg natural transformation can be precomposed with a dg functor on the source side and postcomposed with one on the target side. Both operations keep the degree, and neither introduces a sign.

Where the Koszul sign is, and where it is not

It is tempting to expect a sign in whiskerRight, because it applies a functor to a morphism of degree n. There is none: a DGFunctor preserves the graded composition on the nose (DGFunctor.map_comp carries no sign), so transporting η's graded naturality through K transports the sign unchanged. Likewise whiskerLeft is naturality of η evaluated at F.map p f, again with η's own sign and no other.

The sign appears one level up, in the interchange law. For α : F ⟶ F' of degree n and β : G ⟶ G' of degree m the two ways of reading the horizontal composite differ by (-1)^(m * n):

(α ◁ G) ≫ (F' ▷ β) = (-1)^(m n) • ((F ▷ β) ≫ (α ◁ G')).

That is exactly graded naturality of β evaluated at the degree-n morphism α X, which is why the sign is β's degree times α's and not something new. The two horizontal composites agree on the nose exactly when m * n is even.

Degrees

Whiskering does not change the degree, so both operations are additive in the transformation and are packaged as AddMonoidHoms. Vertical composition is where degrees add, and whiskerLeft_composition and whiskerRight_composition say whiskering is a homomorphism for it in every result degree.

Left whiskering

def CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerLeft {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) {G H : DGFunctor D E} {n : ℤ} (η : ↥(G.HomogeneousNatTrans H n)) : ↥((F.comp G).HomogeneousNatTrans (F.comp H) n)

Precomposition with a dg functor.

The component at X is η's component at F.obj X, and graded naturality is η's own, evaluated at F.map p f.

Equations

• CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerLeft F η = ⟨fun (X : C) => CategoryTheory.DGFunctor.HomogeneousNatTrans.app η (F.obj X), ⋯⟩

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerLeft_app {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) {G H : DGFunctor D E} {n : ℤ} (η : ↥(G.HomogeneousNatTrans H n)) (X : C) : app (whiskerLeft F η) X = app η (F.obj X)

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerLeft_zero {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) {G H : DGFunctor D E} {n : ℤ} : whiskerLeft F 0 = 0

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerLeft_add {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) {G H : DGFunctor D E} {n : ℤ} (η θ : ↥(G.HomogeneousNatTrans H n)) : whiskerLeft F (η + θ) = whiskerLeft F η + whiskerLeft F θ

def CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerLeftHom {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) (G H : DGFunctor D E) (n : ℤ) : ↥(G.HomogeneousNatTrans H n) →+ ↥((F.comp G).HomogeneousNatTrans (F.comp H) n)

Left whiskering as an additive map.

Equations

• CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerLeftHom F G H n = AddMonoidHom.mk' (CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerLeft F) ⋯

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerLeftHom_apply {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) {G H : DGFunctor D E} {n : ℤ} (η : ↥(G.HomogeneousNatTrans H n)) : (whiskerLeftHom F G H n) η = whiskerLeft F η

@[simp]

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

Left whiskering takes the identity transformation to the identity.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerLeft_composition {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) {G H I : DGFunctor D E} {n m : ℤ} (η : ↥(G.HomogeneousNatTrans H n)) (θ : ↥(H.HomogeneousNatTrans I m)) (r : ℤ) (h : n + m = r) : whiskerLeft F (((composition G H I n m r h) η) θ) = ((composition (F.comp G) (F.comp H) (F.comp I) n m r h) (whiskerLeft F η)) (whiskerLeft F θ)

Left whiskering is a homomorphism for vertical composition, in every result degree.

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerLeft_differential {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) {G H : DGFunctor D E} {n : ℤ} (η : ↥(G.HomogeneousNatTrans H n)) : differential (whiskerLeft F η) = whiskerLeft F (differential η)

Left whiskering commutes with the pointwise differential.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.IsClosed.whiskerLeft {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) {G H : DGFunctor D E} {n : ℤ} {η : ↥(G.HomogeneousNatTrans H n)} (hη : IsClosed η) : IsClosed (HomogeneousNatTrans.whiskerLeft F η)

A whiskered closed transformation is closed.

Right whiskering

def CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerRight {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) (K : DGFunctor D E) : ↥((F.comp K).HomogeneousNatTrans (G.comp K) n)

Postcomposition with a dg functor.

The component at X is K applied to η's component, in the same degree n. No sign appears: K preserves the graded composition on the nose, so it carries η's naturality equation across sign and all.

Equations

• CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerRight η K = ⟨fun (X : C) => (K.map n) (CategoryTheory.DGFunctor.HomogeneousNatTrans.app η X), ⋯⟩

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerRight_app {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) (K : DGFunctor D E) (X : C) : app (whiskerRight η K) X = (K.map n) (app η X)

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerRight_zero {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F G : DGFunctor C D} {n : ℤ} (K : DGFunctor D E) : whiskerRight 0 K = 0

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerRight_add {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F G : DGFunctor C D} {n : ℤ} (η θ : ↥(F.HomogeneousNatTrans G n)) (K : DGFunctor D E) : whiskerRight (η + θ) K = whiskerRight η K + whiskerRight θ K

def CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerRightHom {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F G : DGFunctor C D) (n : ℤ) (K : DGFunctor D E) : ↥(F.HomogeneousNatTrans G n) →+ ↥((F.comp K).HomogeneousNatTrans (G.comp K) n)

Right whiskering as an additive map.

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerRightHom_apply {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) (K : DGFunctor D E) : (whiskerRightHom F G n K) η = whiskerRight η K

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerRight_id {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) (K : DGFunctor D E) : whiskerRight (id F) K = id (F.comp K)

Right whiskering takes the identity transformation to the identity. This is DGFunctor.map_id, and it is the one place where right whiskering needs more than additivity of K.map.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerRight_composition {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F G H : DGFunctor C D} {n m : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) (θ : ↥(G.HomogeneousNatTrans H m)) (r : ℤ) (h : n + m = r) (K : DGFunctor D E) : whiskerRight (((composition F G H n m r h) η) θ) K = ((composition (F.comp K) (G.comp K) (H.comp K) n m r h) (whiskerRight η K)) (whiskerRight θ K)

Right whiskering is a homomorphism for vertical composition, in every result degree. This is DGFunctor.map_comp.

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerRight_differential {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) (K : DGFunctor D E) : differential (whiskerRight η K) = whiskerRight (differential η) K

Right whiskering commutes with the pointwise differential. This is DGFunctor.map_d.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.IsClosed.whiskerRight {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F G : DGFunctor C D} {n : ℤ} {η : ↥(F.HomogeneousNatTrans G n)} (hη : IsClosed η) (K : DGFunctor D E) : IsClosed (HomogeneousNatTrans.whiskerRight η K)

A whiskered closed transformation is closed.

Whiskering by a composite

All three laws hold by rfl, because DGFunctor.comp composes the object maps and the AddMonoidHoms directly. They are what makes horizontal composition of dg natural transformations strictly associative.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerRight_whiskerRight {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} {n : ℤ} (α : ↥(F.HomogeneousNatTrans F' n)) (G : DGFunctor D E) (K : DGFunctor E B) : whiskerRight (whiskerRight α G) K = whiskerRight α (G.comp K)

Whiskering twice on the right is whiskering by the composite.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerLeft_whiskerLeft {C : Type u} {D : Type u'} {E : Type u''} {B : Type u'''} [DGCategory C] [DGCategory D] [DGCategory E] [DGCategory B] {n : ℤ} (F : DGFunctor C D) (G : DGFunctor D E) {K K' : DGFunctor E B} (β : ↥(K.HomogeneousNatTrans K' n)) : whiskerLeft F (whiskerLeft G β) = whiskerLeft (F.comp G) β

Whiskering twice on the left is whiskering by the composite.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.whiskerRight_whiskerLeft {C : Type u} {D : Type u'} {E : Type u''} {B : Type u'''} [DGCategory C] [DGCategory D] [DGCategory E] [DGCategory B] {G G' : DGFunctor D E} {m : ℤ} (F : DGFunctor C D) (β : ↥(G.HomogeneousNatTrans G' m)) (K : DGFunctor E B) : whiskerRight (whiskerLeft F β) K = whiskerLeft F (whiskerRight β K)

Whiskering on the two sides commutes.

The interchange law

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.interchange_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 : ℤ) (hnm : n + m = r) (hmn : m + n = r) (X : C) : ((DGCategoryStruct.dgComp n m r hnm) ((G.map n) (app α X))) (app β (F'.obj X)) = (m * n).negOnePow • ((DGCategoryStruct.dgComp m n r hmn) (app β (F.obj X))) ((G'.map n) (app α X))

The Godement interchange law, componentwise.

Reading the horizontal composite of α and β in the two possible orders differs by (-1)^(m * n). The identity is nothing but graded naturality of β evaluated at the degree-n morphism α X, which is why the sign is β's degree times α's and not something new.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.interchange {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 : ℤ) (hnm : n + m = r) (hmn : m + n = r) : ((composition (F.comp G) (F'.comp G) (F'.comp G') n m r hnm) (whiskerRight α G)) (whiskerLeft F' β) = (m * n).negOnePow • ((composition (F.comp G) (F.comp G') (F'.comp G') m n r hmn) (whiskerLeft F β)) (whiskerRight α G')

The Godement interchange law.

(α ◁ G) ≫ (F' ▷ β) = (-1)^(m n) • ((F ▷ β) ≫ (α ◁ G')), with n the degree of α and m the degree of β. Both sides are transformations F ⋙ G ⟶ F' ⋙ G' of degree r; the two vertical composites are taken in the two orders, which is why r comes with both n + m = r and m + n = r.