instRepresentablyCoflatIndYoneda — Mathlib

English

The Ind Yoneda embedding is representably coflat.

Русский

Встроенная Яно́да для Ind является представимо ко-флатной.

LaTeX

$$$\operatorname{RepresentablyCoflat}(\mathrm{Ind.yoneda})$$$

Lean4

instance : RepresentablyCoflat (Ind.yoneda (C := C)) :=
  by
  refine ⟨fun X => ?_⟩
  suffices IsFiltered (CostructuredArrow yoneda ((Ind.inclusion C).obj X)) from
    IsFiltered.of_equivalence
      ((CostructuredArrow.post Ind.yoneda (Ind.inclusion C) X).asEquivalence.trans
          (CostructuredArrow.mapNatIso Ind.yonedaCompInclusion)).symm
  exact ((isIndObject_iff _).1 (Ind.isIndObject_inclusion_obj X)).1

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