Cofiltered systems #
This file deals with properties of cofiltered (and inverse) systems.
Main definitions #
Given a functor
F : J ⥤ Type v:
j : J,
F.eventualRange jis the intersections of all ranges of morphisms
F.IsMittagLefflerstates that the functor
Fsatisfies the Mittag-Leffler condition: the ranges of morphisms
F.toEventualRangesis the subfunctor of
Fobtained by restriction to
F.toPreimagesrestricts a functor to preimages of a given set in some
F.obj i. If
Jis cofiltered, then it is Mittag-Leffler if
Main statements #
nonempty_sections_of_finite_cofiltered_systemshows that if
Jis cofiltered and each
F.obj jis nonempty and finite,
nonempty_sections_of_finite_inverse_systemis a specialization of the above to
Jbeing a directed set (and
F : Jᵒᵖ ⥤ Type v).
isMittagLeffler_of_exists_finite_rangeshows that if
Jis cofiltered and for all
j, there exists some
f : i ⟶ jsuch that the range of
F.map fis finite, then
surjective_toEventualRangesshows that if
Fis Mittag-Leffler, then
F.toEventualRangeshas all morphisms
- Prove Stacks: Lemma 0597
Mittag-Leffler, surjective, eventual range, inverse system,
nonempty_sections_of_finite_inverse_system. In this version,
F functor is between categories of the same universe, and it is an easy
The cofiltered limit of nonempty finite types is nonempty.
nonempty_sections_of_finite_inverse_system for a specialization to inverse limits.
The inverse limit of nonempty finite types is nonempty.
nonempty_sections_of_finite_cofiltered_system for a generalization to cofiltered limits.
That version applies in almost all cases, and the only difference is that this version
J to be empty.
This may be regarded as a generalization of Kőnig's lemma.
To specialize: given a locally finite connected graph, take
Jᵒᵖ to be
F j to be length-
j paths that start from an arbitrary fixed vertex.
F.sections can be read off as infinite rays in the graph.
The eventual range of the functor
F : J ⥤ Type v at index
j : J is the intersection
of the ranges of all maps
F.map f with
i : J and
f : i ⟶ j.
F : J ⥤ Type v satisfies the Mittag-Leffler condition if for all
j : J,
there exists some
i : J and
f : i ⟶ j such that for all
k : J and
g : k ⟶ j, the range
F.map f is contained in that of
in other words (see
isMittagLeffler_iff_eventualRange), the eventual range at
j is attained
f : i ⟶ j.
The subfunctor of
F obtained by restricting to the eventual range at each index.
The sections of the functor
F : J ⥤ Type v are in bijection with the sections of
F satisfies the Mittag-Leffler condition, its restriction to eventual ranges is a
F is nonempty at each index and Mittag-Leffler, then so is
F has all arrows surjective, then it "factors through a poset".