map_comp_eq — Mathlib

English

In the Grothendieck construction, composition of arrows maps to the composition of mapped arrows; functoriality of map is preserved under composition.

Русский

В конструкции Гротендикка композиция стрелок переходит в композицию отображенных стрелок; отображение сохраняет факторность композиции.

LaTeX

$$$map_{C}(\alpha \circ \beta) = map(\alpha) \circ map(\beta)$$$

Lean4

theorem map_comp_eq (α : F ⟶ G) (β : G ⟶ H) : map (α ≫ β) = map α ⋙ map β :=
  by
  fapply Functor.ext
  · intro X
    rfl
  · intro X Y f
    simp only [map_map, map_obj_base, NatTrans.comp_app, Cat.comp_obj, Cat.comp_map, eqToHom_refl, Functor.comp_map,
      Functor.map_comp, Category.comp_id, Category.id_comp]
    fapply Grothendieck.ext
    · rfl
    · simp

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