cocone_naturality — Mathlib

English

For F: J ⥤ RingCat, j, j' in J, f: j ⟶ j', and x in F.obj j, the action of coconeMorphism on F.map f x equals the action of coconeMorphism on x, i.e., (coconeMorphism F j')(F.map f x) = (coconeMorphism F j)x.

Русский

Для F: J ⥤ RingCat, j, j' в J, f: j ⟶ j', и x ∈ F.obj j, действие coconeMorphism на F.map f x равно действию coconeMorphism на x.

LaTeX

$$$\forall f:\, j\to j',\; \forall x:\, F.obj j,\; (coconeMorphism F j')(F.map f\,x) = (coconeMorphism F j)\,x$$$

Lean4

@[simp]
theorem cocone_naturality {j j' : J} (f : j ⟶ j') : F.map f ≫ coconeMorphism F j' = coconeMorphism F j :=
  by
  ext
  apply Quot.sound
  apply Relation.map

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