Lean4
/-- (Implementation) The isomorphism that proves that `A` preserves finite limits. -/
noncomputable def iso [IsFiltered (CostructuredArrow yoneda A)] : A.obj (limit K) ≅ limit (K ⋙ A) :=
calc
A.obj (limit K) ≅ (colimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).obj (limit K) :=
(IsColimit.coconePointUniqueUpToIso (Presheaf.isColimitTautologicalCocone A) (colimit.isColimit _)).app _
_ ≅ colimit (((CostructuredArrow.proj yoneda A) ⋙ yoneda) ⋙ (evaluation _ _).obj (limit K)) :=
(colimitObjIsoColimitCompEvaluation _ _)
_ ≅ colimit ((CostructuredArrow.proj yoneda A) ⋙ yoneda ⋙ (evaluation _ _).obj (limit K)) :=
(HasColimit.isoOfNatIso (Functor.associator _ _ _))
_ ≅ colimit ((coyoneda ⋙ (whiskeringLeft _ _ _).obj (CostructuredArrow.proj yoneda A)).obj (limit K)) :=
(HasColimit.isoOfNatIso (isoAux A K))
_ ≅ colimit (limit (K ⋙ (coyoneda ⋙ (whiskeringLeft _ _ _).obj (CostructuredArrow.proj _ _)))) :=
(HasColimit.isoOfNatIso (preservesLimitIso _ _))
_ ≅ colimit (limit (functorToInterchange A K)) :=
(HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm))
_ ≅ limit (colimit (functorToInterchange A K).flip) := (colimitLimitIso _)
_ ≅ limit (colimit ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ (whiskeringLeft _ _ _).obj K)) :=
(HasLimit.isoOfNatIso (HasColimit.isoOfNatIso (flipFunctorToInterchange A K)))
_ ≅ limit (K ⋙ colimit (CostructuredArrow.proj yoneda A ⋙ yoneda)) :=
(HasLimit.isoOfNatIso (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K))
_ ≅ limit (K ⋙ A) :=
HasLimit.isoOfNatIso
(isoWhiskerLeft _
(IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (Presheaf.isColimitTautologicalCocone A)))
