ι_map — Mathlib

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

@[reassoc (attr := simp)]
theorem ι_map (j : J) : coend.ι _ _ ≫ coend.map f = (f.app (op j)).app j ≫ coend.ι _ _ := by simp [coend.map]

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