Pulling back filteredness along representably flat functors

We show that if F : C ⥤ D is a representably coflat functor between two categories, filteredness of D implies filteredness of C. Dually, if F is representably flat, cofilteredness of D implies cofilteredness of C.

Transferring (co)filteredness along representably (co)flat functors is given by IsFiltered.of_final and its dual, since every representably flat functor is final and every representably coflat functor is initial.

theorem CategoryTheory.isFiltered_of_representablyCoflat {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [IsFiltered D] [RepresentablyCoflat F] : IsFiltered C

theorem CategoryTheory.isCofiltered_of_representablyFlat {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [IsCofiltered D] [RepresentablyFlat F] : IsCofiltered C