English
The inverse of limitCompWhiskeringRightIsoLimitComp interacts with the projection π by the relation: (limitCompWhiskeringRightIsoLimitComp F G).inv ≫ limit.π (G ⋙ (whiskeringRight ...).obj F) j = whiskerRight (limit.π G j) F.
Русский
Обратное к limitCompWhiskeringRightIsoLimitComp взаимодействует с проекцией π по отношению: inv ≫ π = whiskerRight(π, F).
LaTeX
$$$(limitCompWhiskeringRightIsoLimitComp\\,F\\,G).inv \\;\\gg\\; \\mathrm{limit}.\\pi\\bigl(G \\!\\circ\\! (\\mathrm{whiskeringRight}\\;\\_\\;\\_\\_).\\mathrm{obj} F\bigr)\\; j = \\mathrm{whiskerRight}\\bigl(\\mathrm{limit}.\\pi\\,G\\, j\\bigr)\\; F$$$
Lean4
/-- If `Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)` preserves limits of shape `J`, so will `F`. -/
theorem preservesLimit_of_lan_preservesLimit {C D : Type u} [SmallCategory C] [SmallCategory D] (F : C ⥤ D) (J : Type u)
[SmallCategory J] [PreservesLimitsOfShape J (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u)] : PreservesLimitsOfShape J F :=
letI := preservesLimitsOfShape_of_natIso (J := J) (Presheaf.compULiftYonedaIsoULiftYonedaCompLan.{u} F).symm
preservesLimitsOfShape_of_reflects_of_preserves F uliftYoneda.{u}
