limMap_π — Mathlib

English

For a natural transformation α: F ⟶ G between J-shaped functors, the limMap α map between limits commutes with projections: limMap α ≫ limit.π G j = limit.π F j ≫ α.app j.

Русский

Для натурального перехода α: F ⟶ G между функтор-образами J, лимитный переход limMap α commute с π_j: limMap α ≫ limit.π G j = limit.π F j ≫ α.app j.

LaTeX

$$$\\mathrm{limMap} \\alpha \\;\\circ\\; \\mathrm{limit}.\\pi G j = \\mathrm{limit}.\\pi F j \\;\\circ\\; \\alpha.app j$$$

Lean4

@[reassoc (attr := simp)]
theorem limMap_π {F G : J ⥤ C} [HasLimit F] [HasLimit G] (α : F ⟶ G) (j : J) :
    limMap α ≫ limit.π G j = limit.π F j ≫ α.app j :=
  limit.lift_π _ j

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