English
If PreservesColimit₂ K1 K2 G holds, then PreservesColimit₂ K2 K1 G.flip holds.
Русский
Если PreservesColimit₂ K1 K2 G выполняется, то PreservesColimit₂ K2 K1 G.flip выполняется.
LaTeX
$$$[PreservesColimit₂ K1 K2 G] \\Rightarrow [PreservesColimit₂ K2 K1 G.flip]$$$
Lean4
theorem of_preservesColimit₂_flip : PreservesColimit₂ K₂ K₁ G.flip where
nonempty_isColimit_mapCocone₂ {c₁} hc₁ {c₂}
hc₂ := by
constructor
let E₀ :
uncurry.obj (whiskeringLeft₂ C |>.obj K₂ |>.obj K₁ |>.obj G.flip) ≅
uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G).flip :=
Iso.refl _
let E₁ :
uncurry.obj (whiskeringLeft₂ C |>.obj K₂ |>.obj K₁ |>.obj G.flip) ≅
Prod.swap _ _ ⋙ uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G) :=
E₀ ≪≫ uncurryObjFlip _
refine IsColimit.precomposeInvEquiv E₁ _ ?_
apply IsColimit.ofWhiskerEquivalence (e := Prod.braiding _ _)
refine
IsColimit.equivOfNatIsoOfIso (Iso.refl _) (G.mapCocone₂ c₂ c₁) _ ?_ |>.toFun <| isColimitOfPreserves₂ G hc₂ hc₁
exact Cocones.ext (Iso.refl _) (fun ⟨j₁, j₂⟩ ↦ by simp [E₁, E₀])
