hcomp_id_app — Mathlib

English

Horizontal composition of a natural transformation α with the identity on H yields, at each X, the action of H on α.app X: (α ◫ 𝟙 H).app X = H.map (α.app X).

Русский

Горизонтальное композиции натурального преобразования α с единичным преобразованием на H на каждом X даёт H.map(α.app X).

LaTeX

$$$ (\alpha \;◫\; 𝟙 H).app X = H.map (\alpha.app X). $$$

Lean4

theorem hcomp_id_app {H : D ⥤ E} (α : F ⟶ G) (X : C) : (α ◫ 𝟙 H).app X = H.map (α.app X) := by simp

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