map_π — Mathlib

English

In a limit diagram, the map IsLimit.map c hd α satisfies the identity: IsLimit.map c hd α ≫ d.π.app j = c.π.app j ≫ α.app j for every j.

Русский

В предельной диаграмме отображение IsLimit.map c hd α удовлетворяет тождеству: IsLimit.map c hd α ≫ d.π.app j = c.π.app j ≫ α.app j для каждого j.

LaTeX

$$$\\text{IsLimit.map } c \\; hd \\; \\alpha \\; j = d.π.app j \\; \\; \\text{relation}: \\; hd.map c α ≫ d.π.app j = c.π.app j ≫ α.app j$$$

Lean4

@[reassoc (attr := simp)]
theorem map_π {F G : J ⥤ C} (c : Cone F) {d : Cone G} (hd : IsLimit d) (α : F ⟶ G) (j : J) :
    hd.map c α ≫ d.π.app j = c.π.app j ≫ α.app j :=
  fac _ _ _

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