English
The underlying map of a composite equals the composite of the underlying maps under forget₂.
Русский
Базовое отображение композиции равно композиции базовых отображений для forget₂.
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 ≫ 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] {FC : C → C → Type*} {CC : C → Type w}
[∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory.{w} C FC] [Category.{v'} D] {FD : D → D → Type*}
{CD : D → Type w} [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory.{w} D FD] [HasForget₂ C D] {X Y Z : C}
(f : X ⟶ Y) (g : Y ⟶ Z) (x : ToType ((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, ConcreteCategory.comp_apply]
