English
The functor functorExtension₂ is an equivalence when the target is idempotent complete.
Русский
Функтор functorExtension₂ является эквивалентностью при идемпотентно-дополенной цели.
LaTeX
$$(functorExtension₂ C D).IsEquivalence$$
Lean4
instance : ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).IsEquivalence :=
by
have :
((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C) ⋙
(whiskeringRight C D (Karoubi D)).obj (toKaroubi D) ⋙
(whiskeringRight C (Karoubi D) D).obj (Functor.inv (toKaroubi D))).IsEquivalence :=
by
change (karoubiUniversal C D).inverse.IsEquivalence
infer_instance
exact
Functor.isEquivalence_of_comp_right _
((whiskeringRight C _ _).obj (toKaroubi D) ⋙ (whiskeringRight C (Karoubi D) D).obj (Functor.inv (toKaroubi D)))
