English
Let C and D be categories with forgetful functors. For morphisms f: X → Y and g: Y → Z in C, the underlying map of the composite f ≫ g is the composition of the underlying maps: (forget₂ C D).map (f ≫ g) = (forget₂ C D).map g ∘ (forget₂ C D).map f.
Русский
Пусть C и D — категории с забывающими функторaми. Морфизмы f: X → Y и g: Y → Z в C, представленные через забывающий функтор, удовлетворяют: (forget₂ C D).map (f ≫ g) = (forget₂ C D).map g ∘ (forget₂ C D).map f.
LaTeX
$$$\forall {X Y Z : C} (f : X \to Y) (g : Y \to Z) (x : (forget₂ C D).obj X), ((forget₂ C D).map (f \gg g)\ x) = (forget₂ C D).map g ((forget₂ C D).map f\ x)$$$
Lean4
theorem forget₂_comp_apply {C : Type u} {D : Type u'} [Category.{v} C] [HasForget.{w} C] [Category.{v'} D]
[HasForget.{w} D] [HasForget₂ C D] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : (forget₂ C D).obj X) :
((forget₂ C D).map (f ≫ g) x) = (forget₂ C D).map g ((forget₂ C D).map f x) := by rw [Functor.map_comp, comp_apply]
