English
For F: J ⥤ C, E: K ⥤ J, G: C ⥤ D with appropriate limits, we have: G.map (limit.pre F E) ≫ limit.post (E ⋙ F) G = limit.post F G ≫ limit.pre (F ⋙ G) E.
Русский
Для F: J ⥤ C, E: K ⥤ J, G: C ⥤ D с нужными пределами выполняется: G.map (limit.pre F E) ≫ limit.post (E ⋙ F) G = limit.post F G ≫ limit.pre (F ⋙ G) E.
LaTeX
$$$G.map (\\operatorname{limit.pre} F E) \\gg \\operatorname{limit.post} (E \\cdot F) G = \\operatorname{limit.post} F G \\gg \\operatorname{limit.pre} (F \\cdot G) E$$$
Lean4
theorem pre_post {D : Type u'} [Category.{v'} D] (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D) [HasLimit F] [HasLimit (E ⋙ F)]
[HasLimit (F ⋙ G)] [h : HasLimit ((E ⋙ F) ⋙ G)] : -- G (limit F) ⟶ G (limit (E ⋙ F)) ⟶ limit ((E ⋙ F) ⋙ G) vs
-- G (limit F) ⟶ limit F ⋙ G ⟶ limit (E ⋙ (F ⋙ G)) or
haveI : HasLimit (E ⋙ F ⋙ G) := h
G.map (limit.pre F E) ≫ limit.post (E ⋙ F) G = limit.post F G ≫ limit.pre (F ⋙ G) E :=
by
haveI : HasLimit (E ⋙ F ⋙ G) := h
ext; erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]
