isIndObject_of_isFiltered_of_finallySmall

English

An object A is Ind if the CostructuredArrow yoneda A is filtered and finally small.

Русский

Объект A является Ind, если CostructuredArrow yoneda A фильтрован и finally small.

LaTeX

$$$\mathrm{IsIndObject}(A) \\iff \\left( \mathrm{IsFiltered}(\mathrm{CostructuredArrow}(\mathrm{yoneda},A)) \land \mathrm{FinallySmall}(\mathrm{CostructuredArrow}(\mathrm{yoneda},A)) \right)$$$

Lean4

theorem isIndObject_of_isFiltered_of_finallySmall (A : Cᵒᵖ ⥤ Type v) [IsFiltered (CostructuredArrow yoneda A)]
    [FinallySmall.{v} (CostructuredArrow yoneda A)] : IsIndObject A :=
  by
  have h₁ :
    (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
        inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final :=
    Functor.final_of_natIso (factoringCompInclusion (fromFinalModel <| CostructuredArrow yoneda A)).symm
  have h₂ : Functor.Final (inclusion (fromFinalModel (CostructuredArrow yoneda A))) :=
    Functor.final_of_comp_full_faithful' (factoring _) (inclusion _)
  let c := (Presheaf.tautologicalCocone A).whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
  let hc : IsColimit c := (Functor.Final.isColimitWhiskerEquiv _ _).symm (Presheaf.isColimitTautologicalCocone A)
  have hq : Nonempty (FinalModel (CostructuredArrow yoneda A)) :=
    Nonempty.map (Functor.Final.lift (fromFinalModel (CostructuredArrow yoneda A))) IsFiltered.nonempty
  exact ⟨_, inclusion (fromFinalModel _) ⋙ CostructuredArrow.proj yoneda A, c.ι, hc⟩

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