flip

Mathlib.CategoryTheory.Functor.Category

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.flip

Lean4

/-- Flip the arguments of a bifunctor. See also `Currying.lean`. -/
@[simps (attr := grind =) obj_obj obj_map]
protected def flip (F : C ⥤ D ⥤ E) : D ⥤ C ⥤ E
    where
  obj k := { obj := fun j => (F.obj j).obj k, map := fun f => (F.map f).app k, }
  map
    f :=
    { app := fun j => (F.obj j).map f }
      -- `@[simps]` doesn't produce a nicely stated lemma here:
      -- the implicit arguments for `app` use the definition of `flip`, rather than `flip` itself.

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

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

Разделы

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

Аффилиация

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