toKaroubi_comp_karoubiFunctorCategoryEmbedding

English

The functor functorExtension₂ is an equivalence when the target is idempotent complete.

Русский

Функтор functorExtension₂ является эквивалентностью при идемпотентно-дополенной цели.

LaTeX

$$(functorExtension₂ C D).IsEquivalence$$

Lean4

/-- The composition of `(J ⥤ C) ⥤ Karoubi (J ⥤ C)` and `Karoubi (J ⥤ C) ⥤ (J ⥤ Karoubi C)`
equals the functor `(J ⥤ C) ⥤ (J ⥤ Karoubi C)` given by the composition with
`toKaroubi C : C ⥤ Karoubi C`. -/
theorem toKaroubi_comp_karoubiFunctorCategoryEmbedding :
    toKaroubi _ ⋙ karoubiFunctorCategoryEmbedding J C = (Functor.whiskeringRight J _ _).obj (toKaroubi C) :=
  by
  apply Functor.ext
  · intro X Y f
    ext j
    simp
  · intro X
    apply Functor.ext
    · intro j j' φ
      ext
      simp
    · intro j
      rfl

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