w — Mathlib · SciLib

English

For any cone c over F and a morphism f: j → j', the relation F.map f ; c.π.app j' = c.π.app j holds, i.e., the cone legs are natural w.r.t. morphisms in J.

Русский

Для конуса c над F и морфизма f: j → j' выполняется F.map f ; c.π.app j' = c.π.app j; т.е. ножки конуса естественны по отношению к морфизмам в J.

LaTeX

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

Lean4

@[reassoc]
theorem w {F : J ⥤ C} (c : Cocone F) {j j' : J} (f : j ⟶ j') : F.map f ≫ c.ι.app j' = c.ι.app j :=
  by
  rw [c.ι.naturality f]
  apply comp_id

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