map₂IsoPreEquivalenceInverseCompProj

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CostructuredArrow.map₂IsoPreEquivalenceInverseCompProj

Lean4

/-- The functor `CostructuredArrow T d ⥤ CostructuredArrow (T ⋙ S) e` that `u : S.obj d ⟶ e`
induces via `CostructuredArrow.map₂` can be expressed up to isomorphism by
`CostructuredArrow.preEquivalence` and `CostructuredArrow.proj`. -/
def map₂IsoPreEquivalenceInverseCompProj (T : C ⥤ D) (S : D ⥤ E) (d : D) (e : E) (u : S.obj d ⟶ e) :
    map₂ (F := 𝟭 _) (U := T ⋙ S) (𝟙 (T ⋙ S)) u ≅ (preEquivalence T (mk u)).inverse ⋙ proj (pre T S _) (mk u) :=
  NatIso.ofComponents fun _ => isoMk (Iso.refl _)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru