Inferring Filteredness from Filteredness of Costructured Arrow Categories

References

• M. Kashiwara, P. Schapira, Categories and Sheaves, Proposition 3.1.8

theorem CategoryTheory.isFiltered_of_isFiltered_costructuredArrow {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) [IsFiltered B] [R.Final] [∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))] : IsFiltered A

Given functors L : A ⥤ T and R : B ⥤ T with a common codomain we can conclude that A is filtered given that R is final, B is filtered and each costructured arrow category CostructuredArrow L (R.obj b) is filtered.