English
For A, B in Ind C and a morphism f: A ⟶ B, there exists a representation of f as an arrow between two diagrams that become isomorphic after passing to Ind-limits.
Русский
Для объектов A, B в Ind C и морфизма f: A ⟶ B существует представление f как стрелы между диаграммами, которые после перехода к Ind-пределам становятся изоморфны.
LaTeX
$$$\\exists (I) (F G : I ⥤ C) (\\varphi : F ⟶ G), \\text{Nonempty}(Arrow.mk f \\cong Arrow.mk ((Ind.lim _).map \\varphi))$$$
Lean4
/-- A way to understand morphisms in `Ind C`: every morphism is induced by a natural transformation
of diagrams. -/
theorem exists_nonempty_arrow_mk_iso_ind_lim {A B : Ind C} {f : A ⟶ B} :
∃ (I : Type v) (_ : SmallCategory I) (_ : IsFiltered I) (F G : I ⥤ C) (φ : F ⟶ G),
Nonempty (Arrow.mk f ≅ Arrow.mk ((Ind.lim _).map φ)) :=
by
obtain ⟨P⟩ := nonempty_indParallelPairPresentation A.2 B.2 (Ind.inclusion _ |>.map f) (Ind.inclusion _ |>.map f)
refine ⟨P.I, inferInstance, inferInstance, P.F₁, P.F₂, P.φ, ⟨Arrow.isoMk ?_ ?_ ?_⟩⟩
· exact P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.zero
· exact P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.one
· simpa using (P.parallelPairIsoParallelPairCompIndYoneda.hom.naturality WalkingParallelPairHom.left).symm
