English
Another formulation asserting that flipping the bifunctor arguments preserves the two-variable limit preservation property.
Русский
Другая формулировка, утверждающая, что разворот аргументов бифунктора сохраняет свойство сохранения пределов по двум переменным.
LaTeX
$$$\\text{PreservesLimit₂ K_2 K_1 G.flip}$$$
Lean4
theorem of_preservesLimit₂_flip : PreservesLimit₂ K₂ K₁ G.flip where
nonempty_isLimit_mapCone₂ {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 IsLimit.postcomposeHomEquiv E₁ _ ?_
apply IsLimit.ofWhiskerEquivalence (e := Prod.braiding _ _)
refine IsLimit.equivOfNatIsoOfIso (Iso.refl _) (G.mapCone₂ c₂ c₁) _ ?_ |>.toFun <| isLimitOfPreserves₂ G hc₂ hc₁
exact Cones.ext (Iso.refl _) (fun ⟨j₁, j₂⟩ ↦ by simp [E₁, E₀])
