functoriality — Mathlib

Lean4
/-- A functor `G : C ⥤ D` sends bicones over `F` to bicones over `G.obj ∘ F` functorially. -/
@[simps]
def functoriality (G : C ⥤ D) [Functor.PreservesZeroMorphisms G] : Bicone F ⥤ Bicone (G.obj ∘ F)
    where
  obj
    A :=
    { pt := G.obj A.pt
      π := fun j => G.map (A.π j)
      ι := fun j => G.map (A.ι j)
      ι_π := fun i j =>
        (Functor.map_comp _ _ _).symm.trans <| by
          rw [A.ι_π]
          cat_disch }
  map
    f :=
    { hom := G.map f.hom
      wπ := fun j => by simp [-BiconeMorphism.wπ, ← f.wπ j]
      wι := fun j => by simp [-BiconeMorphism.wι, ← f.wι j] }
Похожие утверждения