π_comp_eqToHom — Mathlib

English

For a cone c over F with HasLimit F, the lift of c, when composed with the projection π_j, recovers the j-th leg of the cone: lift F c ≫ π_j = c.π.app j.

Русский

Для конуса c над F, имея предел F, отображение lift F c, после композиции с π_j, восстанавливает j-ю ножку конуса: lift F c ≫ π_j = c.π.app j.

LaTeX

$$$\\mathrm{limit}.lift F c \\;\\circ\\; \\mathrm{limit}.π F j = c.π.app j$$$

Lean4

@[reassoc]
theorem π_comp_eqToHom (F : J ⥤ C) [HasLimit F] {j j' : J} (hj : j = j') :
    limit.π F j ≫ eqToHom (by subst hj; rfl) = limit.π F j' :=
  by
  subst hj
  simp

Похожие утверждения