English
For H: C ⥤ D, if there are limits for F, G, and H, then the two-step post composition identity holds: map H of limit.post F G composed with limit.post (F ⋙ G) H equals limit.post F (G ⋙ H).
Русский
Для H: C ⥤ D существует равенство для пост-композиции пределов: H.map (limit.post F G) ≫ limit.post (F ⋙ G) H = limit.post F (G ⋙ H).
LaTeX
$$$H.map (\\operatorname{limit.post} F G) \\gg \\operatorname{limit.post} (F \\cdot G) H = \\operatorname{limit.post} F (G \\cdot H)$$$
Lean4
@[simp]
theorem post_post {E : Type u''} [Category.{v''} E] (H : D ⥤ E) [h : HasLimit ((F ⋙ G) ⋙ H)] :
-- H G (limit F) ⟶ H (limit (F ⋙ G)) ⟶ limit ((F ⋙ G) ⋙ H) equals
-- H G (limit F) ⟶ limit (F ⋙ (G ⋙ H))
haveI : HasLimit (F ⋙ G ⋙ H) := h
H.map (limit.post F G) ≫ limit.post (F ⋙ G) H = limit.post F (G ⋙ H) :=
by
haveI : HasLimit (F ⋙ G ⋙ H) := h
ext; erw [assoc, limit.post_π, ← H.map_comp, limit.post_π, limit.post_π]; rfl
