mkFunctor — Mathlib

English

Given functors F : C ⥤ E, G : D ⥤ E and a natural transformation α : (Prod.fst C D) ⋙ F ⟶ (Prod.snd C D) ⋙ G, one obtains a functor C ⋆ D ⥤ E.

Русский

Даны функторы F : C ⥤ E, G : D ⥤ E и натуральное преобразование α между композициями через Prod.fst и Prod.snd, образуется функтор C ⋆ D ⥤ E.

LaTeX

$$mkFunctor : (F : C ⥤ E) → (G : D ⥤ E) → (α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G) → (C ⋆ D ⥤ E)$$

Lean4

/-- A pair of functor `F : C ⥤ E, G : D ⥤ E` as well as a natural transformation
`α : (Prod.fst C D) ⋙ F ⟶ (Prod.snd C D) ⋙ G`. defines a functor out of `C ⋆ D`.
This is the main entry point to define functors out of a join of categories. -/
def mkFunctor (F : C ⥤ E) (G : D ⥤ E) (α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G) : C ⋆ D ⥤ E
    where
  obj
    X :=
    match X with
    | .left x => F.obj x
    | .right x => G.obj x
  map f := homInduction (left := fun _ _ f ↦ F.map f) (right := fun _ _ g ↦ G.map g) (edge := fun c d ↦ α.app (c, d)) f
  map_id
    x := by
    cases x
    · dsimp only [id_left, homInduction_left]
      simp
    · dsimp only [id_right, homInduction_right]
      simp
  map_comp {x y z} f
    g := by
    cases f <;> cases g
    · simp [← Functor.map_comp]
    · case left.edge f d => simpa using (α.naturality <| (Prod.sectL _ d).map f).symm
    · simp [← Functor.map_comp]
    · case edge.right c _ _ f => simpa using α.naturality <| (Prod.sectR c _).map f

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