English
The composition of the functor from the base category to Karoubi, followed by the embedding into a functor category of Karoubi objects, equals the Whiskering construction with toKaroubi on C.
Русский
Композиция отображения к Кароуби и вложения в категорию функторов Карауби-объектов равна операции восподобления правого взведённого whiskering с toKaroubi на C.
LaTeX
$$toKaroubi_\\{\\} \\circ karoubiFunctorCategoryEmbedding_{J,C} = (\\mathrm{Functor.whiskeringRight}_{J} C (\\mathrm{Karoubi} C)).\\mathrm{obj} (toKaroubi C)$$
Lean4
instance functor_category_isIdempotentComplete [IsIdempotentComplete C] : IsIdempotentComplete (J ⥤ C) :=
by
refine ⟨fun F p hp => ?_⟩
have hC := (isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent C).mp inferInstance
haveI : ∀ j : J, HasEqualizer (𝟙 _) (p.app j) := fun j =>
hC _ _
(congr_app hp j)
/- We construct the direct factor `Y` associated to `p : F ⟶ F` by computing
the equalizer of the identity and `p.app j` on each object `(j : J)`. -/
let Y : J ⥤ C :=
{ obj := fun j => Limits.equalizer (𝟙 _) (p.app j)
map := fun {j j'} φ =>
equalizer.lift (Limits.equalizer.ι (𝟙 _) (p.app j) ≫ F.map φ)
(by rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id]) }
let i : Y ⟶ F :=
{ app := fun j => equalizer.ι _ _
naturality := fun _ _ _ => by rw [equalizer.lift_ι] }
let e : F ⟶ Y :=
{ app := fun j => equalizer.lift (p.app j) (by simpa only [comp_id] using (congr_app hp j).symm)
naturality := fun j j' φ => equalizer.hom_ext (by simp [Y]) }
use Y, i, e
constructor
· ext j
dsimp
rw [assoc, equalizer.lift_ι, ← equalizer.condition, id_comp, comp_id]
· ext j
simp [Y, i, e]
