Naturality of the preserved-colimit comparison

The canonical comparison from a functor applied to a colimit to the colimit of its image is natural also in the preserving functor. Mathlib's preservesColimitNatIso records naturality in the diagram; this file records the other variable.

theorem CategoryTheory.preservesColimitIso_naturality {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Limits.HasColimitsOfShape J D] {H H' : Functor C D} (α : H ⟶ H') (F : Functor J C) [Limits.HasColimit F] [Limits.PreservesColimit F H] [Limits.PreservesColimit F H'] : CategoryStruct.comp (α.app (Limits.colimit F)) (preservesColimitIso H' F).hom = CategoryStruct.comp (preservesColimitIso H F).hom (Limits.colim.map (F.whiskerLeft α))

Naturality in the preserving functor complements Mathlib's diagram naturality for preservesColimitIso. Compare both sides on each colimit injection.

theorem CategoryTheory.preservesColimitIso_naturality_assoc {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Limits.HasColimitsOfShape J D] {H H' : Functor C D} (α : H ⟶ H') (F : Functor J C) [Limits.HasColimit F] [Limits.PreservesColimit F H] [Limits.PreservesColimit F H'] {Z : D} (h : Limits.colimit (F.comp H') ⟶ Z) : CategoryStruct.comp (α.app (Limits.colimit F)) (CategoryStruct.comp (preservesColimitIso H' F).hom h) = CategoryStruct.comp (preservesColimitIso H F).hom (CategoryStruct.comp (Limits.colim.map (F.whiskerLeft α)) h)

Naturality in the preserving functor complements Mathlib's diagram naturality for preservesColimitIso. Compare both sides on each colimit injection.