English
In CostructuredArrow, the map₂ construction with identity on T and S is initial under cofiltro conditions.
Русский
В CostructuredArrow конструирование map₂ с идентичностью на T и S начально при cofiltro-условиях.
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 T d ⥤ CostructuredArrow (T ⋙ S) e` that `u : S.obj d ⟶ e`
induces via `CostructuredArrow.map₂` is initial, if `T` and `S` are initial and the domain of `T` is
filtered. -/
instance initial_map₂_id [IsCofiltered C] {E : Type u₃} [Category.{v₃} E] (T : C ⥤ D) [T.Initial] (S : D ⥤ E)
[S.Initial] (d : D) (e : E) (u : S.obj d ⟶ e) : Initial (map₂ (F := 𝟭 _) (U := T ⋙ S) (𝟙 (T ⋙ S)) u) :=
by
have := (T ⋙ S).initial_iff_isCofiltered_costructuredArrow.mp inferInstance e
apply initial_of_natIso (map₂IsoPreEquivalenceInverseCompProj T S d e u).symm
