createsColimitsOfShapeOfEquiv — Mathlib

Lean4
/-- If `F` creates colimits of shape `J` and `J ≌ J'`, then `F` creates colimits of shape `J'`. -/
def createsColimitsOfShapeOfEquiv {J' : Type w₁} [Category.{w'₁} J'] (e : J ≌ J') (F : C ⥤ D)
    [CreatesColimitsOfShape J F] : CreatesColimitsOfShape J' F where
  CreatesColimit
    {K} :=
    { lifts c
        hc :=
        by
        refine ⟨(Cocones.whiskeringEquivalence e).inverse.obj (liftColimit (hc.whiskerEquivalence e)), ?_⟩
        letI inner :=
          (Cocones.whiskeringEquivalence (F := K ⋙ F) e).inverse.mapIso
            (liftedColimitMapsToOriginal (K := e.functor ⋙ K) (hc.whiskerEquivalence e))
        refine ?_ ≪≫ inner ≪≫ ((Cocones.whiskeringEquivalence e).unitIso.app c).symm
        exact Cocones.ext (Iso.refl _)
      toReflectsColimit :=
        have := reflectsColimitsOfShape_of_equiv e F;
        inferInstance }
      -- For the inhabited linter later.
Похожие утверждения