mathlib3 documentation

category_theory.cofiltered_system

Cofiltered systems #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file deals with properties of cofiltered (and inverse) systems.

Main definitions #

Given a functor F : J ⥤ Type v:

Main statements #

Todo #

References #

Tags #

Mittag-Leffler, surjective, eventual range, inverse system,

This bootstraps nonempty_sections_of_finite_inverse_system. In this version, the F functor is between categories of the same universe, and it is an easy corollary to Top.nonempty_limit_cone_of_compact_t2_inverse_system.

The cofiltered limit of nonempty finite types is nonempty.

See nonempty_sections_of_finite_inverse_system for a specialization to inverse limits.

The inverse limit of nonempty finite types is nonempty.

See 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 allows 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 and F j to be length-j paths that start from an arbitrary fixed vertex. Elements of 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.

Equations
theorem category_theory.functor.mem_eventual_range_iff {J : Type u} [category_theory.category J] (F : J Type v) {j : J} {x : F.obj j} :
x F.eventual_range j ⦃i : J⦄ (f : i j), x set.range (F.map f)

The functor 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 of F.map f is contained in that of F.map g; in other words (see is_mittag_leffler_iff_eventual_range), the eventual range at j is attained by some f : i ⟶ j.

Equations
theorem category_theory.functor.eventual_range_eq_range_precomp {J : Type u} [category_theory.category J] (F : J Type v) {i j k : J} (f : i j) (g : j k) (h : F.eventual_range k = set.range (F.map g)) :
def category_theory.functor.to_preimages {J : Type u} [category_theory.category J] (F : J Type v) {i : J} (s : set (F.obj i)) :
J Type v

The subfunctor of F obtained by restricting to the preimages of a set s ∈ F.obj i.

Equations
@[simp]
theorem category_theory.functor.to_preimages_map {J : Type u} [category_theory.category J] (F : J Type v) {i : J} (s : set (F.obj i)) (j k : J) (g : j k) (ᾰ : (f : j i), F.map f ⁻¹' s) :
(F.to_preimages s).map g = set.maps_to.restrict (F.map g) ( (f : j i), F.map f ⁻¹' s) ( (f : k i), F.map f ⁻¹' s) _
@[simp]
theorem category_theory.functor.to_preimages_obj {J : Type u} [category_theory.category J] (F : J Type v) {i : J} (s : set (F.obj i)) (j : J) :
(F.to_preimages s).obj j = (f : j i), F.map f ⁻¹' s
@[protected, instance]
def category_theory.functor.to_preimages_finite {J : Type u} [category_theory.category J] (F : J Type v) {i : J} (s : set (F.obj i)) [ (j : J), finite (F.obj j)] (j : J) :

The subfunctor of F obtained by restricting to the eventual range at each index.

Equations

The sections of the functor F : J ⥤ Type v are in bijection with the sections of F.eventual_ranges.

Equations

If F satisfies the Mittag-Leffler condition, its restriction to eventual ranges is a surjective functor.

If F is nonempty at each index and Mittag-Leffler, then so is F.to_eventual_ranges.

theorem category_theory.functor.thin_diagram_of_surjective {J : Type u} [category_theory.category J] (F : J Type v) [category_theory.is_cofiltered_or_empty J] (Fsur : ⦃i j : J⦄ (f : i j), function.surjective (F.map f)) {i j : J} (f g : i j) :
F.map f = F.map g

If F has all arrows surjective, then it "factors through a poset".

theorem category_theory.functor.to_preimages_nonempty_of_surjective {J : Type u} [category_theory.category J] (F : J Type v) {i : J} (s : set (F.obj i)) [category_theory.is_cofiltered_or_empty J] [hFn : (j : J), nonempty (F.obj j)] (Fsur : ⦃i j : J⦄ (f : i j), function.surjective (F.map f)) (hs : s.nonempty) (j : J) :
theorem category_theory.functor.eval_section_surjective_of_surjective {J : Type u} [category_theory.category J] (F : J Type v) [category_theory.is_cofiltered_or_empty J] [ (j : J), nonempty (F.obj j)] [ (j : J), finite (F.obj j)] (Fsur : ⦃i j : J⦄ (f : i j), function.surjective (F.map f)) (i : J) :
function.surjective (λ (s : (F.sections)), s.val i)
theorem category_theory.functor.eventually_injective {J : Type u} [category_theory.category J] (F : J Type v) [category_theory.is_cofiltered_or_empty J] [ (j : J), nonempty (F.obj j)] [ (j : J), finite (F.obj j)] (Fsur : ⦃i j : J⦄ (f : i j), function.surjective (F.map f)) [nonempty J] [finite (F.sections)] :
(j : J), (i : J) (f : i j), function.injective (F.map f)