English
For HasLimitsOfShape, a morphism α, and H: C ⥤ D, we have H.map (limMap α) ≫ limit.post G H = limit.post F H ≫ limMap (whiskerRight α H).
Русский
Для ограниченного предела: H.map (limMap α) ≫ limit.post G H = limit.post F H ≫ limMap (whiskerRight α H).
LaTeX
$$$H.map (\\limMap \\alpha) \\gg \\operatorname{limit.post} G H = \\operatorname{limit.post} F H \\gg \\limMap (\\mathrm{whiskerRight} \\alpha H)$$$
Lean4
theorem map_post {D : Type u'} [Category.{v'} D] [HasLimitsOfShape J D] (H : C ⥤ D) :
/- H (limit F) ⟶ H (limit G) ⟶ limit (G ⋙ H) vs
H (limit F) ⟶ limit (F ⋙ H) ⟶ limit (G ⋙ H) -/
H.map (limMap α) ≫ limit.post G H = limit.post F H ≫ limMap (whiskerRight α H) :=
by
ext
simp only [whiskerRight_app, limMap_π, assoc, limit.post_π_assoc, limit.post_π, ← H.map_comp]
