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:

For j : J, F.eventual_range j is the intersections of all ranges of morphisms F.map f where f has codomain j.
F.is_mittag_leffler states that the functor F satisfies the Mittag-Leffler condition: the ranges of morphisms F.map f (with f having codomain j) stabilize.
If J is cofiltered F.to_eventual_ranges is the subfunctor of F obtained by restriction to F.eventual_range.
F.to_preimages restricts a functor to preimages of a given set in some F.obj i. If J is cofiltered, then it is Mittag-Leffler if F is, see is_mittag_leffler.to_preimages.

Main statements #

nonempty_sections_of_finite_cofiltered_system shows that if J is cofiltered and each F.obj j is nonempty and finite, F.sections is nonempty.
nonempty_sections_of_finite_inverse_system is a specialization of the above to J being a directed set (and F : Jᵒᵖ ⥤ Type v).
is_mittag_leffler_of_exists_finite_range shows that if J is cofiltered and for all j, there exists some i and f : i ⟶ j such that the range of F.map f is finite, then F is Mittag-Leffler.
to_eventual_ranges_surjective shows that if F is Mittag-Leffler, then F.to_eventual_ranges has all morphisms F.map f surjective.

Todo #

Prove Stacks: Lemma 0597

References #

Stacks: Mittag-Leffler systems

Tags #

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

source

theorem nonempty_sections_of_finite_cofiltered_system.init {J : Type u} [category_theory.small_category J] [category_theory.is_cofiltered_or_empty J] (F : J ⥤ Type u) [hf : ∀ (j : J), finite (F.obj j)] [hne : ∀ (j : J), nonempty (F.obj j)] :

F.sections.nonempty

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.

source

theorem nonempty_sections_of_finite_cofiltered_system {J : Type u} [category_theory.category J] [category_theory.is_cofiltered_or_empty J] (F : J ⥤ Type v) [∀ (j : J), finite (F.obj j)] [∀ (j : J), nonempty (F.obj j)] :

F.sections.nonempty

The cofiltered limit of nonempty finite types is nonempty.

See nonempty_sections_of_finite_inverse_system for a specialization to inverse limits.

source

theorem nonempty_sections_of_finite_inverse_system {J : Type u} [preorder J] [is_directed J has_le.le] (F : Jᵒᵖ ⥤ Type v) [∀ (j : Jᵒᵖ), finite (F.obj j)] [∀ (j : Jᵒᵖ), nonempty (F.obj j)] :

F.sections.nonempty

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.

source

def category_theory.functor.eventual_range {J : Type u} [category_theory.category J] (F : J ⥤ Type v) (j : J) :

set (F.obj j)

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

F.eventual_range j = ⋂ (i : J) (f : i ⟶ j), set.range (F.map f)

source

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)

source

def category_theory.functor.is_mittag_leffler {J : Type u} [category_theory.category J] (F : J ⥤ Type v) :

Prop

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

F.is_mittag_leffler = ∀ (j : J), ∃ (i : J) (f : i ⟶ j), ∀ ⦃k : J⦄ (g : k ⟶ j), set.range (F.map f) ⊆ set.range (F.map g)

source

theorem category_theory.functor.is_mittag_leffler_iff_eventual_range {J : Type u} [category_theory.category J] (F : J ⥤ Type v) :

F.is_mittag_leffler ↔ ∀ (j : J), ∃ (i : J) (f : i ⟶ j), F.eventual_range j = set.range (F.map f)

source

theorem category_theory.functor.is_mittag_leffler.subset_image_eventual_range {J : Type u} [category_theory.category J] (F : J ⥤ Type v) {i j : J} (h : F.is_mittag_leffler) (f : j ⟶ i) :

F.eventual_range i ⊆ F.map f '' F.eventual_range j

source

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)) :

F.eventual_range k = set.range (F.map (f ≫ g))

source

theorem category_theory.functor.is_mittag_leffler_of_surjective {J : Type u} [category_theory.category J] (F : J ⥤ Type v) (h : ∀ ⦃i j : J⦄ (f : i ⟶ j), function.surjective (F.map f)) :

F.is_mittag_leffler

source

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

F.to_preimages s = {obj := λ (j : J), ↥⋂ (f : j ⟶ i), F.map f ⁻¹' s, map := λ (j k : J) (g : j ⟶ k), set.maps_to.restrict (F.map g) (⋂ (f : j ⟶ i), F.map f ⁻¹' s) (⋂ (f : k ⟶ i), F.map f ⁻¹' s) _, map_id' := _, map_comp' := _}

source

@[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) _ ᾰ

source

@[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

source

@[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) :

finite ((F.to_preimages s).obj j)

source

theorem category_theory.functor.eventual_range_maps_to {J : Type u} [category_theory.category J] (F : J ⥤ Type v) {i j : J} [category_theory.is_cofiltered_or_empty J] (f : j ⟶ i) :

set.maps_to (F.map f) (F.eventual_range j) (F.eventual_range i)

source

theorem category_theory.functor.is_mittag_leffler.eq_image_eventual_range {J : Type u} [category_theory.category J] (F : J ⥤ Type v) {i j : J} [category_theory.is_cofiltered_or_empty J] (h : F.is_mittag_leffler) (f : j ⟶ i) :

F.eventual_range i = F.map f '' F.eventual_range j

source

theorem category_theory.functor.eventual_range_eq_iff {J : Type u} [category_theory.category J] (F : J ⥤ Type v) {i j : J} [category_theory.is_cofiltered_or_empty J] {f : i ⟶ j} :

F.eventual_range j = set.range (F.map f) ↔ ∀ ⦃k : J⦄ (g : k ⟶ i), set.range (F.map f) ⊆ set.range (F.map (g ≫ f))

source

theorem category_theory.functor.is_mittag_leffler_iff_subset_range_comp {J : Type u} [category_theory.category J] (F : J ⥤ Type v) [category_theory.is_cofiltered_or_empty J] :

F.is_mittag_leffler ↔ ∀ (j : J), ∃ (i : J) (f : i ⟶ j), ∀ ⦃k : J⦄ (g : k ⟶ i), set.range (F.map f) ⊆ set.range (F.map (g ≫ f))

source

theorem category_theory.functor.is_mittag_leffler.to_preimages {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] (h : F.is_mittag_leffler) :

(F.to_preimages s).is_mittag_leffler

source

theorem category_theory.functor.is_mittag_leffler_of_exists_finite_range {J : Type u} [category_theory.category J] (F : J ⥤ Type v) [category_theory.is_cofiltered_or_empty J] (h : ∀ (j : J), ∃ (i : J) (f : i ⟶ j), (set.range (F.map f)).finite) :

F.is_mittag_leffler

source

@[simp]

theorem category_theory.functor.to_eventual_ranges_obj {J : Type u} [category_theory.category J] (F : J ⥤ Type v) [category_theory.is_cofiltered_or_empty J] (j : J) :

F.to_eventual_ranges.obj j = ↥(F.eventual_range j)

source

@[simp]

theorem category_theory.functor.to_eventual_ranges_map {J : Type u} [category_theory.category J] (F : J ⥤ Type v) [category_theory.is_cofiltered_or_empty J] (i j : J) (f : i ⟶ j) (ᾰ : ↥(F.eventual_range i)) :

F.to_eventual_ranges.map f ᾰ = set.maps_to.restrict (F.map f) (F.eventual_range i) (F.eventual_range j) _ ᾰ

source

def category_theory.functor.to_eventual_ranges {J : Type u} [category_theory.category J] (F : J ⥤ Type v) [category_theory.is_cofiltered_or_empty J] :

J ⥤ Type v

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

Equations

F.to_eventual_ranges = {obj := λ (j : J), ↥(F.eventual_range j), map := λ (i j : J) (f : i ⟶ j), set.maps_to.restrict (F.map f) (F.eventual_range i) (F.eventual_range j) _, map_id' := _, map_comp' := _}

source

@[protected, instance]

def category_theory.functor.to_eventual_ranges_finite {J : Type u} [category_theory.category J] (F : J ⥤ Type v) [category_theory.is_cofiltered_or_empty J] [∀ (j : J), finite (F.obj j)] (j : J) :

finite (F.to_eventual_ranges.obj j)

source

def category_theory.functor.to_eventual_ranges_sections_equiv {J : Type u} [category_theory.category J] (F : J ⥤ Type v) [category_theory.is_cofiltered_or_empty J] :

↥(F.to_eventual_ranges.sections) ≃ ↥(F.sections)

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

Equations

F.to_eventual_ranges_sections_equiv = {to_fun := λ (s : ↥(F.to_eventual_ranges.sections)), ⟨λ (i : J), ↑(↑s i), _⟩, inv_fun := λ (s : ↥(F.sections)), ⟨λ (j : J), ⟨↑s j, _⟩, _⟩, left_inv := _, right_inv := _}

source

theorem category_theory.functor.surjective_to_eventual_ranges {J : Type u} [category_theory.category J] (F : J ⥤ Type v) [category_theory.is_cofiltered_or_empty J] (h : F.is_mittag_leffler) ⦃i j : J⦄ (f : i ⟶ j) :

function.surjective (F.to_eventual_ranges.map f)

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

source

theorem category_theory.functor.to_eventual_ranges_nonempty {J : Type u} [category_theory.category J] (F : J ⥤ Type v) [category_theory.is_cofiltered_or_empty J] (h : F.is_mittag_leffler) [∀ (j : J), nonempty (F.obj j)] (j : J) :

nonempty (F.to_eventual_ranges.obj j)

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

source

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".

source

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) :

nonempty ((F.to_preimages s).obj j)

source

theorem category_theory.functor.eval_section_injective_of_eventually_injective {J : Type u} [category_theory.category J] (F : J ⥤ Type v) [category_theory.is_cofiltered_or_empty J] {j : J} (Finj : ∀ (i : J) (f : i ⟶ j), function.injective (F.map f)) (i : J) (f : i ⟶ j) :

function.injective (λ (s : ↥(F.sections)), s.val j)

source

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)

source

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)