Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-21 14:25 5bc18a9e

View on Github →

feat(topology/category/limits): Generalize Topological Kőnig's lemma (#7982) This PR generalizes the Topological Kőnig's lemma to work with limits over cofiltered categories (as opposed to just directed orders). Along the way, we also prove some more API for the category instance on ulift C, and provide an as_small C construction for a category C. Coauthored with @kmill

Estimated changes

Modified src/category_theory/category/ulift.lean

added def category_theory.as_small.down

added def category_theory.as_small.equiv

added def category_theory.as_small.up

added theorem category_theory.obj_down_obj_up

added theorem category_theory.obj_up_obj_down

modified def category_theory.ulift.down

modified def category_theory.ulift.equivalence

modified def category_theory.ulift.up

added def category_theory.ulift_hom.down

added def category_theory.ulift_hom.equiv

added def category_theory.ulift_hom.obj_down

added def category_theory.ulift_hom.obj_up

added def category_theory.ulift_hom.up

added def category_theory.{w

Modified src/category_theory/filtered.lean

Modified src/topology/category/Top/limits.lean

added theorem Top.nonempty_limit_cone_of_compact_t2_cofiltered_system

deleted theorem Top.nonempty_limit_cone_of_compact_t2_inverse_system

modified theorem Top.partial_sections.closed

modified theorem Top.partial_sections.directed

modified theorem Top.partial_sections.nonempty

modified def Top.partial_sections

added theorem nonempty_sections_of_fintype_cofiltered_system.init

added theorem nonempty_sections_of_fintype_cofiltered_system

deleted theorem nonempty_sections_of_fintype_inverse_system.init

deleted def ulift.directed_order