map_comp — Mathlib

English

The map end is functorial in the second argument: end maps compose as end(f) followed by end(g) equals end(f ∘ g).

Русский

Функциональная зависимость конца: end(f) ∘ end(g) = end(f ∘ g).

LaTeX

$$$end\_\text{map} f \; \circ\; end\_\text{map} g = end\_\text{map}(f \circ g)$$$

Lean4

@[reassoc (attr := simp)]
theorem map_comp {F'' : Jᵒᵖ ⥤ J ⥤ C} [HasEnd F''] (g : F' ⟶ F'') : end_.map f ≫ end_.map g = end_.map (f ≫ g) := by
  cat_disch

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