w — Mathlib · SciLib

English

For a cone c over a diagram F, the naturality condition on the cone maps ensures c.π.app j ≫ F.map f = c.π.app j' for every morphism f: j → j' in J.

Русский

Для конуса c над диаграммой F естественность мап конуса обеспечивает c.π.app j ≫ F.map f = c.π.app j' для каждого морфизма f: j → j' в J.

LaTeX

$$$$ c.\pi_{j} \; \; \; \; \; \; \; \; \; \; F.map f = c.\pi_{j'} $$$$

Lean4

@[reassoc (attr := simp)]
theorem w {F : J ⥤ C} (c : Cone F) {j j' : J} (f : j ⟶ j') : c.π.app j ≫ F.map f = c.π.app j' :=
  by
  rw [← c.π.naturality f]
  apply id_comp

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