coe_comp — Mathlib

English

The forgetful functor preserves composition: forgetting the composite equals the composite of forgetful images.

Русский

Forgetful-функтор сохраняет композицию: забывая композицию, получаем композицию забытых морфизмов.

LaTeX

$$$\mathrm{forget}(f \circ g) = (\mathrm{forget} g) \circ (\mathrm{forget} f)$$$

Lean4

theorem coe_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g : X → Z) = g ∘ f :=
  (forget _).map_comp f g

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