ι — Mathlib · SciLib

English

Naturality of ι with respect to maps: coend.ι F j ≫ coend.map f = (f.app(op j)).app j ≫ coend.ι F' j.

Русский

Натуральность ι относительно отображений: coend.ι F j ≫ coend.map f = (f.app(op j)).app j ≫ coend.ι F' j.

LaTeX

$$$coend.ι F j \;≫\; coend.map f = (f.app (op j)).app j \;≫\; coend.ι F' j$$$

Lean4

/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this is the inclusion `(F.obj (op j)).obj j ⟶ coend F`
for any `j : J`. -/
noncomputable def ι (j : J) : (F.obj (op j)).obj j ⟶ coend F :=
  Multicoequalizer.π (multispanIndexCoend F) _

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