Commit 2021-05-29 02:32 1ac49b0e

View on Github →

chore(category_theory): dualize filtered categories to cofiltered categories (#7731) Per request on zulip. I have not attempted to dualize "filtered colimits commute with finite limits", as I've never heard of that being used.

Estimated changes

Modified src/category_theory/filtered.lean

added theorem category_theory.is_cofiltered.cone_nonempty

added theorem category_theory.is_cofiltered.eq_condition

added def category_theory.is_cofiltered.inf

added theorem category_theory.is_cofiltered.inf_exists

added theorem category_theory.is_cofiltered.inf_objs_exists

added def category_theory.is_cofiltered.inf_to

added theorem category_theory.is_cofiltered.inf_to_commutes

added theorem category_theory.is_cofiltered.of_equivalence

added theorem category_theory.is_cofiltered.of_is_left_adjoint

added theorem category_theory.is_cofiltered.of_left_adjoint