CategoryTheory.ι_preservesColimitsIso_inv

theorem CategoryTheory.ι_preservesColimitsIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesColimit F G] [inst_4 : CategoryTheory.Limits.HasColimit F] (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) j) (CategoryTheory.preservesColimitIso G F).inv = G.map (CategoryTheory.Limits.colimit.ι F j)

The theorem `CategoryTheory.ι_preservesColimitsIso_inv` states that for any category `C` and `D`, given a functor `G` from `C` to `D` and another functor `F` from a category `J` to `C`, if `G` preserves colimits of `F` and `F` has a colimit, then for any object `j` in `J`, the composition of the morphism from `F` composed with `G` to the colimit object of `F` composed with `G` and the inverse of the isomorphism induced by the preservation of colimits of `F` by `G`, is equal to the morphism induced by `G` mapping the morphism from `F` to the colimit object of `F`. In other words, this theorem asserts the commutativity of the relevant diagram in the context of category theory.

More concisely: Given functors `G: C -> D` and `F: J -> C` with `G` preserving colimits of `F` and `F` having a colimit, the diagram commutes: `(F i) ⊣ (G X) ≈ (G (F i) ∨)_∘ G (i -> X)`, where `i` is an object in `J`, `X` is the colimit of `F`, and `→` denotes the composition of morphisms.