initial_proj_of_isCofiltered — Mathlib

English

In CostructuredArrow, if C is cofiltred, T: C ⥤ D is initial, S: D ⥤ E is initial, and d,e, u as stated, then the functor map₂ is initial.

Русский

В CostructuredArrow, если C кофильтрована, T: C ⥤ D начален, S: D ⥤ E начален, и даны соответствующие объекты, то функтор map₂ начален.

LaTeX

$$[IsCofiltered(C)] (T: C ⥤ D) [T.Initial] (S: D ⥤ E) [S.Initial] (d : D) (e : E) (u : S.obj d ⟶ e) : Initial (map₂ (F := 𝟭 _) (U := T \circ S) (\text{id}_{T \circ S}) u)$$

Lean4

/-- The functor `CostructuredArrow.proj : CostructuredArrow Y T ⥤ C` is initial if `T : C ⥤ D` is
initial and `C` is cofiltered. -/
instance initial_proj_of_isCofiltered [IsCofilteredOrEmpty C] (T : C ⥤ D) [Initial T] (Y : D) :
    Initial (CostructuredArrow.proj T Y) := by
  refine ⟨fun X => ?_⟩
  rw [isConnected_iff_of_equivalence (ofCostructuredArrowProjEquivalence T Y X)]
  exact (initial_comp (Over.forget X) T).out _

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