English
If I is filtered, then a CostructuredArrow over yoneda is filtered; hence there are directed systems that cofinally map to a terminal object, enabling limits to be formed.
Русский
Если I — фильтрована, то CostructuredArrow над yoneda тоже фильтрован; следовательно, существуют направленные системы, которые все сводят к терминальному объекту, что позволяет образовывать пределы.
LaTeX
$$[IsFiltered I] ⇒ [IsFiltered (CostructuredArrow yoneda (colimit F))]$$
Lean4
theorem isFiltered [IsFiltered I] (hF : ∀ i, IsIndObject (F.obj i)) :
IsFiltered (CostructuredArrow yoneda (colimit F)) := by
-- It suffices to show that for any functor `G : J ⥤ CostructuredArrow yoneda (colimit F)` with
-- `J` finite there is some `X` such that the set
-- `lim Hom_{CostructuredArrow yoneda (colimit F)}(G·, X)` is nonempty.
refine
IsFiltered.iff_nonempty_limit.mpr
(fun {J _ _} G => ?_)
-- We begin by remarking that `lim Hom_{Over (colimit F)}(yG·, 𝟙 (colimit F))` is nonempty,
-- simply because `𝟙 (colimit F)` is the terminal object. Here `y` is the functor
-- `CostructuredArrow yoneda (colimit F) ⥤ Over (colimit F)` induced by `yoneda`.
have h₁ : Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver _ _).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F))))) :=
⟨Types.Limit.mk _ (fun j => Over.mkIdTerminal.from _) (by simp)⟩
-- `𝟙 (colimit F)` is the colimit of the diagram in `Over (colimit F)` given by the arrows of
-- the form `Fi ⟶ colimit F`. Thus, pulling the colimit out of the hom functor and commuting
-- the finite limit with the filtered colimit, we obtain
-- `lim_j Hom_{Over (colimit F)}(yGj, 𝟙 (colimit F)) ≅`
-- `colim_i lim_j Hom_{Over (colimit F)}(yGj, colimit.ι F i)`, and so we find `i` such that
-- the limit is non-empty.
obtain ⟨i, hi⟩ := exists_nonempty_limit_obj_of_isColimit F G _ (colimit.isColimitToOver F) _ (Iso.refl _) h₁
obtain ⟨⟨P⟩⟩ := hF i
let hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
isColimitOfPreserves (Over.map _)
(Over.isColimitToOver P.coconeIsColimit)
-- Again, we pull the colimit out of the hom functor and commute limit and colimit to obtain
-- `lim_j Hom_{Over (colimit F)}(yGj, colimit.ι F i) ≅`
-- `colim_k lim_j Hom_{Over (colimit F)}(yGj, yHk)`, and so we find `k` such that the limit
-- is non-empty.
obtain ⟨k, hk⟩ :
∃ k,
Nonempty
(limit
(G.op ⋙
(CostructuredArrow.toOver yoneda (colimit F)).op ⋙
yoneda.obj
((CostructuredArrow.toOver yoneda (colimit F)).obj <|
(CostructuredArrow.pre P.F yoneda (colimit F)).obj <| (map (colimit.ι F i)).obj <| mk _))) :=
exists_nonempty_limit_obj_of_isColimit F G _ hc _ (Iso.refl _) hi
have htO : (CostructuredArrow.toOver yoneda (colimit F)).FullyFaithful :=
.ofFullyFaithful
_
-- Since the inclusion `y : CostructuredArrow yoneda (colimit F) ⥤ Over (colimit F)` is fully
-- faithful, `lim_j Hom_{Over (colimit F)}(yGj, yHk) ≅`
-- `lim_j Hom_{CostructuredArrow yoneda (colimit F)}(Gj, Hk)` and so `Hk` is the object we're
-- looking for.
let q := htO.homNatIsoMaxRight
obtain ⟨t'⟩ := Nonempty.map (limMap (isoWhiskerLeft G.op (q _)).hom) hk
exact ⟨_, ⟨((preservesLimitIso uliftFunctor.{u, v} _).inv t').down⟩⟩
