Cones along initial functors

For an initial functor F : C ⥤ D, Mathlib's CategoryTheory.Functor.Initial.conesEquiv identifies the category of cones over G : D ⥤ E with the category of cones over F ⋙ G, and both of its unit and counit are the identity on cone points. This file records the resulting bijection between natural transformations const X ⟶ G and const X ⟶ F ⋙ G for a fixed apex X, given by whiskering along F. It is the form in which initiality is used to compare constant presheaves on two sites.

CategoryTheory.Limits.IsLimit.whiskerOfCofinal combines Mathlib's Monotone.final_functor_iff with Functor.Initial.isLimitWhiskerEquiv: a limit cone over an inverse system remains a limit after restriction along a cofinal monotone map from a directed preorder.

noncomputable def CategoryTheory.Functor.Initial.constHomEquiv {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {E : Type u_3} [Category.{v_3, u_3} E] (F : Functor C D) [F.Initial] (G : Functor D E) (X : E) : ((const D).obj X ⟶ G) ≃ ((const C).obj X ⟶ F.comp G)

For an initial functor F : C ⥤ D, whiskering along F identifies cones with apex X over G : D ⥤ E with cones with apex X over F ⋙ G; the inverse is Initial.extendCone.

@[simp]

theorem CategoryTheory.Functor.Initial.constHomEquiv_apply {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {E : Type u_3} [Category.{v_3, u_3} E] (F : Functor C D) [F.Initial] (G : Functor D E) (X : E) (π : (const D).obj X ⟶ G) : (constHomEquiv F G X) π = F.whiskerLeft π

noncomputable def CategoryTheory.Limits.IsLimit.whiskerOfCofinal {J : Type u_1} {K : Type u_2} {C : Type u_3} [Preorder J] [Preorder K] [IsDirectedOrder J] [Category.{v_1, u_3} C] {F : Functor Kᵒᵖ C} {c : Cone F} (hc : IsLimit c) (φ : J →o K) (hφ : ∀ (k : K), ∃ (j : J), k ≤ φ j) : IsLimit (Cone.whisker ⋯.functor.op c)

Restriction along a cofinal monotone map from a directed preorder preserves a limit cone over an inverse system.