isCofiltered_of_representablyFlat

English

If D is cofiltered and F: C ⥤ D is representably flat, then C is cofiltered.

Русский

Если D кофильтрована, а F: C ⥤ D представимо плоская, то C кофильтрована.

LaTeX

$$$[IsCofiltered(D)] \land [RepresentablyFlat(F)] \Rightarrow IsCofiltered(C)$$$

Lean4

theorem isCofiltered_of_representablyFlat [IsCofiltered D] [RepresentablyFlat F] : IsCofiltered C :=
  by
  have := isFiltered_of_representablyCoflat F.op
  exact isCofiltered_of_isFiltered_op C

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