composePath_comp — Mathlib

English

Let X, Y, Z be objects in a category C. If f is a path from X to Y and g is a path from Y to Z, then the morphism represented by the concatenated path f composed with g equals the composite of the morphisms represented by f and g.

Русский

Пусть X, Y, Z — объекты категории C. Пусть f — путь от X до Y, и g — путь от Y до Z. Тогда морфизм, соответствующий конкатенации путей f и g, равен композиции морфизмов, соответствующих f и g.

LaTeX

$$$\\operatorname{composePath}(f \\circ g) = \\operatorname{composePath}(f) \\circ \\operatorname{composePath}(g)$$$

Lean4

@[simp]
theorem composePath_comp {X Y Z : C} (f : Path X Y) (g : Path Y Z) :
    composePath (f.comp g) = composePath f ≫ composePath g := by
  induction g with
  | nil => simp
  | cons g e ih => simp [ih]

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