English
The functor map₂ is final if T and S are final and the domain of T is filtered.
Русский
Функтор map₂ финален, если T и S финальны, и область определения T фильтрована.
LaTeX
$$∧[T.Final] ∧ [S.Final] ∧ [IsFiltered(C)] ⇒ Final (StructuredArrow.map₂ (u) (α))$$
Lean4
/-- The functor `StructuredArrow d T ⥤ StructuredArrow e (T ⋙ S)` that `u : e ⟶ S.obj d`
induces via `StructuredArrow.map₂` is final, if `T` and `S` are final and the domain of `T` is
filtered. -/
instance final_map₂_id [IsFiltered C] {E : Type u₃} [Category.{v₃} E] {T : C ⥤ D} [T.Final] {S : D ⥤ E} [S.Final]
{T' : C ⥤ E} {d : D} {e : E} (u : e ⟶ S.obj d) (α : T ⋙ S ⟶ T') [IsIso α] : Final (map₂ (F := 𝟭 _) u α) :=
by
haveI : IsFiltered (StructuredArrow e (T ⋙ S)) := (T ⋙ S).final_iff_isFiltered_structuredArrow.mp inferInstance e
apply final_of_natIso (map₂IsoPreEquivalenceInverseCompProj d e u α).symm
