whiskeringLeft — Mathlib

Lean4
/-- Whiskering an exact functor by an exact functor yields an 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 _ _, by dsimp; exact comp_preservesFiniteColimits _ _⟩)
  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
Похожие утверждения