Commit 2020-09-03 14:47 8b277a95

View on Github →

feat(category_theory/filtered): finite diagrams in filtered categories admit cocones (#4026) This is only step towards eventual results about filtered colimits commuting with finite limits, forget CommRing preserving filtered colimits, and applications to Scheme.

Estimated changes

Modified src/category_theory/filtered.lean

added theorem category_theory.is_filtered.cocone_nonempty

added theorem category_theory.is_filtered.coeq_condition

added def category_theory.is_filtered.sup

added theorem category_theory.is_filtered.sup_exists'

added theorem category_theory.is_filtered.sup_exists

added theorem category_theory.is_filtered.sup_objs_exists

added def category_theory.is_filtered.to_sup

added theorem category_theory.is_filtered.to_sup_commutes

Created src/category_theory/fin_category.lean

Modified src/category_theory/limits/shapes/finite_limits.lean

Modified src/linear_algebra/basic.lean

Modified src/logic/basic.lean

added theorem exists_apply_eq_apply'

added theorem exists_apply_eq_apply

modified theorem exists_eq'