whiskeringLeft — Mathlib

Lean4
/-- Whiskering a left exact functor by a left exact functor yields a left exact functor. -/
@[simps! obj_obj obj_map map_app_app]
def whiskeringLeft : (C ⥤ₗ D) ⥤ (D ⥤ₗ E) ⥤ (C ⥤ₗ E)
    where
  obj
    F :=
    ObjectProperty.lift _ (forget _ _ ⋙ (Functor.whiskeringLeft C D E).obj F.obj)
      (fun G => by dsimp; exact comp_preservesFiniteLimits _ _)
  map {F G}
    η :=
    { app := fun H => ((Functor.whiskeringLeft C D E).map η).app H.obj
      naturality := fun _ _ f => ((Functor.whiskeringLeft C D E).map η).naturality f }
  map_id
    X := by
    rw [ObjectProperty.FullSubcategory.id_def]
    cat_disch
  map_comp f
    g := by
    rw [ObjectProperty.FullSubcategory.comp_def]
    cat_disch
Похожие утверждения