createsLimitsOfShapeOfEquiv — Mathlib

Lean4
/-- If `F` creates limits of shape `J` and `J ≌ J'`, then `F` creates limits of shape `J'`. -/
def createsLimitsOfShapeOfEquiv {J' : Type w₁} [Category.{w'₁} J'] (e : J ≌ J') (F : C ⥤ D) [CreatesLimitsOfShape J F] :
    CreatesLimitsOfShape J' F where
  CreatesLimit
    {K} :=
    { lifts c
        hc := by
        refine ⟨(Cones.whiskeringEquivalence e).inverse.obj (liftLimit (hc.whiskerEquivalence e)), ?_⟩
        letI inner :=
          (Cones.whiskeringEquivalence (F := K ⋙ F) e).inverse.mapIso
            (liftedLimitMapsToOriginal (K := e.functor ⋙ K) (hc.whiskerEquivalence e))
        refine ?_ ≪≫ inner ≪≫ ((Cones.whiskeringEquivalence e).unitIso.app c).symm
        exact Cones.ext (Iso.refl _)
      toReflectsLimit :=
        have := reflectsLimitsOfShape_of_equiv e F;
        inferInstance }
Похожие утверждения