Cofiltered systems

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

Main definitions

Given a functor F : J ⥤ Type v:

• For j : J, F.eventualRange j is the intersections of all ranges of morphisms F.map f where f has codomain j.
• F.IsMittagLeffler 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.toEventualRanges is the subfunctor of F obtained by restriction to F.eventualRange.
• F.toPreimages 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 IsMittagLeffler.toPreimages.

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).
• isMittagLeffler_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.
• surjective_toEventualRanges shows that if F is Mittag-Leffler, then F.toEventualRanges 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,

theorem nonempty_sections_of_finite_cofiltered_system.init {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofilteredOrEmpty J] (F : CategoryTheory.Functor J (Type u)) [hf : ∀ (j : J), Finite (F.toPrefunctor.obj j)] [hne : ∀ (j : J), Nonempty (F.toPrefunctor.obj j)] : Set.Nonempty (CategoryTheory.Functor.sections F)

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 TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.

theorem nonempty_sections_of_finite_cofiltered_system {J : Type u} [CategoryTheory.Category.{w, u} J] [CategoryTheory.IsCofilteredOrEmpty J] (F : CategoryTheory.Functor J (Type v)) [∀ (j : J), Finite (F.toPrefunctor.obj j)] [∀ (j : J), Nonempty (F.toPrefunctor.obj j)] : Set.Nonempty (CategoryTheory.Functor.sections F)

The cofiltered limit of nonempty finite types is nonempty.

See nonempty_sections_of_finite_inverse_system for a specialization to inverse limits.

theorem nonempty_sections_of_finite_inverse_system {J : Type u} [Preorder J] [IsDirected J fun (x x_1 : J) => x ≤ x_1] (F : CategoryTheory.Functor Jᵒᵖ (Type v)) [∀ (j : Jᵒᵖ), Finite (F.toPrefunctor.obj j)] [∀ (j : Jᵒᵖ), Nonempty (F.toPrefunctor.obj j)] : Set.Nonempty (CategoryTheory.Functor.sections F)

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.

def CategoryTheory.Functor.eventualRange {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) (j : J) : Set (F.toPrefunctor.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

• CategoryTheory.Functor.eventualRange F j = ⋂ (i : J), ⋂ (f : i ⟶ j), Set.range (F.toPrefunctor.map f)

theorem CategoryTheory.Functor.mem_eventualRange_iff {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {j : J} {x : F.toPrefunctor.obj j} : x ∈ CategoryTheory.Functor.eventualRange F j ↔ ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ Set.range (F.toPrefunctor.map f)

def CategoryTheory.Functor.IsMittagLeffler {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor 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 isMittagLeffler_iff_eventualRange), the eventual range at j is attained by some f : i ⟶ j.

Equations

• CategoryTheory.Functor.IsMittagLeffler F = ∀ (j : J), ∃ (i : J) (f : i ⟶ j), ∀ ⦃k : J⦄ (g : k ⟶ j), Set.range (F.toPrefunctor.map f) ⊆ Set.range (F.toPrefunctor.map g)

theorem CategoryTheory.Functor.isMittagLeffler_iff_eventualRange {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) : CategoryTheory.Functor.IsMittagLeffler F ↔ ∀ (j : J), ∃ (i : J) (f : i ⟶ j), CategoryTheory.Functor.eventualRange F j = Set.range (F.toPrefunctor.map f)

theorem CategoryTheory.Functor.IsMittagLeffler.subset_image_eventualRange {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} {j : J} (h : CategoryTheory.Functor.IsMittagLeffler F) (f : j ⟶ i) : CategoryTheory.Functor.eventualRange F i ⊆ F.toPrefunctor.map f '' CategoryTheory.Functor.eventualRange F j

theorem CategoryTheory.Functor.eventualRange_eq_range_precomp {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} {j : J} {k : J} (f : i ⟶ j) (g : j ⟶ k) (h : CategoryTheory.Functor.eventualRange F k = Set.range (F.toPrefunctor.map g)) : CategoryTheory.Functor.eventualRange F k = Set.range (F.toPrefunctor.map (CategoryTheory.CategoryStruct.comp f g))

theorem CategoryTheory.Functor.isMittagLeffler_of_surjective {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) (h : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.toPrefunctor.map f)) : CategoryTheory.Functor.IsMittagLeffler F

@[simp]

theorem CategoryTheory.Functor.toPreimages_obj {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} (s : Set (F.toPrefunctor.obj i)) (j : J) : (CategoryTheory.Functor.toPreimages F s).toPrefunctor.obj j = ↑(⋂ (f : j ⟶ i), F.toPrefunctor.map f ⁻¹' s)

@[simp]

theorem CategoryTheory.Functor.toPreimages_map {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} (s : Set (F.toPrefunctor.obj i)) : ∀ {X Y : J} (g : X ⟶ Y) (a : ↑(⋂ (f : X ⟶ i), F.toPrefunctor.map f ⁻¹' s)), (CategoryTheory.Functor.toPreimages F s).toPrefunctor.map g a = Set.MapsTo.restrict (F.toPrefunctor.map g) (⋂ (f : X ⟶ i), F.toPrefunctor.map f ⁻¹' s) (⋂ (f : Y ⟶ i), F.toPrefunctor.map f ⁻¹' s) (_ : ∀ x ∈ ⋂ (f : X ⟶ i), F.toPrefunctor.map f ⁻¹' s, F.toPrefunctor.map g x ∈ ⋂ (f : Y ⟶ i), F.toPrefunctor.map f ⁻¹' s) a

def CategoryTheory.Functor.toPreimages {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} (s : Set (F.toPrefunctor.obj i)) : CategoryTheory.Functor J (Type v)

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

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Functor.toPreimages_finite {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} (s : Set (F.toPrefunctor.obj i)) [∀ (j : J), Finite (F.toPrefunctor.obj j)] (j : J) : Finite ((CategoryTheory.Functor.toPreimages F s).toPrefunctor.obj j)

Equations

• (_ : Finite ((CategoryTheory.Functor.toPreimages F s).toPrefunctor.obj x)) = (_ : Finite { x_1 : F.toPrefunctor.obj x // x_1 ∈ ⋂ (f : x ⟶ i), F.toPrefunctor.map f ⁻¹' s })

theorem CategoryTheory.Functor.eventualRange_mapsTo {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} {j : J} [CategoryTheory.IsCofilteredOrEmpty J] (f : j ⟶ i) : Set.MapsTo (F.toPrefunctor.map f) (CategoryTheory.Functor.eventualRange F j) (CategoryTheory.Functor.eventualRange F i)

theorem CategoryTheory.Functor.IsMittagLeffler.eq_image_eventualRange {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} {j : J} [CategoryTheory.IsCofilteredOrEmpty J] (h : CategoryTheory.Functor.IsMittagLeffler F) (f : j ⟶ i) : CategoryTheory.Functor.eventualRange F i = F.toPrefunctor.map f '' CategoryTheory.Functor.eventualRange F j

theorem CategoryTheory.Functor.eventualRange_eq_iff {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} {j : J} [CategoryTheory.IsCofilteredOrEmpty J] {f : i ⟶ j} : CategoryTheory.Functor.eventualRange F j = Set.range (F.toPrefunctor.map f) ↔ ∀ ⦃k : J⦄ (g : k ⟶ i), Set.range (F.toPrefunctor.map f) ⊆ Set.range (F.toPrefunctor.map (CategoryTheory.CategoryStruct.comp g f))

theorem CategoryTheory.Functor.isMittagLeffler_iff_subset_range_comp {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] : CategoryTheory.Functor.IsMittagLeffler F ↔ ∀ (j : J), ∃ (i : J) (f : i ⟶ j), ∀ ⦃k : J⦄ (g : k ⟶ i), Set.range (F.toPrefunctor.map f) ⊆ Set.range (F.toPrefunctor.map (CategoryTheory.CategoryStruct.comp g f))

theorem CategoryTheory.Functor.IsMittagLeffler.toPreimages {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} (s : Set (F.toPrefunctor.obj i)) [CategoryTheory.IsCofilteredOrEmpty J] (h : CategoryTheory.Functor.IsMittagLeffler F) : CategoryTheory.Functor.IsMittagLeffler (CategoryTheory.Functor.toPreimages F s)

theorem CategoryTheory.Functor.isMittagLeffler_of_exists_finite_range {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] (h : ∀ (j : J), ∃ (i : J) (f : i ⟶ j), Set.Finite (Set.range (F.toPrefunctor.map f))) : CategoryTheory.Functor.IsMittagLeffler F

@[simp]

theorem CategoryTheory.Functor.toEventualRanges_map {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] : ∀ {X Y : J} (f : X ⟶ Y) (a : ↑(CategoryTheory.Functor.eventualRange F X)), (CategoryTheory.Functor.toEventualRanges F).toPrefunctor.map f a = Set.MapsTo.restrict (F.toPrefunctor.map f) (CategoryTheory.Functor.eventualRange F X) (CategoryTheory.Functor.eventualRange F Y) (_ : Set.MapsTo (F.toPrefunctor.map f) (CategoryTheory.Functor.eventualRange F X) (CategoryTheory.Functor.eventualRange F Y)) a

@[simp]

theorem CategoryTheory.Functor.toEventualRanges_obj {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] (j : J) : (CategoryTheory.Functor.toEventualRanges F).toPrefunctor.obj j = ↑(CategoryTheory.Functor.eventualRange F j)

def CategoryTheory.Functor.toEventualRanges {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] : CategoryTheory.Functor J (Type v)

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

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Functor.toEventualRanges_finite {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Finite (F.toPrefunctor.obj j)] (j : J) : Finite ((CategoryTheory.Functor.toEventualRanges F).toPrefunctor.obj j)

Equations

• (_ : Finite ((CategoryTheory.Functor.toEventualRanges F).toPrefunctor.obj x)) = (_ : Finite { x_1 : F.toPrefunctor.obj x // x_1 ∈ CategoryTheory.Functor.eventualRange F x })

def CategoryTheory.Functor.toEventualRangesSectionsEquiv {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] : ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.toEventualRanges F)) ≃ ↑(CategoryTheory.Functor.sections F)

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Functor.surjective_toEventualRanges {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] (h : CategoryTheory.Functor.IsMittagLeffler F) ⦃i : J⦄ ⦃j : J⦄ (f : i ⟶ j) : Function.Surjective ((CategoryTheory.Functor.toEventualRanges F).toPrefunctor.map f)

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

theorem CategoryTheory.Functor.toEventualRanges_nonempty {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] (h : CategoryTheory.Functor.IsMittagLeffler F) [∀ (j : J), Nonempty (F.toPrefunctor.obj j)] (j : J) : Nonempty ((CategoryTheory.Functor.toEventualRanges F).toPrefunctor.obj j)

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

theorem CategoryTheory.Functor.thin_diagram_of_surjective {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] (Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.toPrefunctor.map f)) {i : J} {j : J} (f : i ⟶ j) (g : i ⟶ j) : F.toPrefunctor.map f = F.toPrefunctor.map g

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

theorem CategoryTheory.Functor.toPreimages_nonempty_of_surjective {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} (s : Set (F.toPrefunctor.obj i)) [CategoryTheory.IsCofilteredOrEmpty J] [hFn : ∀ (j : J), Nonempty (F.toPrefunctor.obj j)] (Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.toPrefunctor.map f)) (hs : Set.Nonempty s) (j : J) : Nonempty ((CategoryTheory.Functor.toPreimages F s).toPrefunctor.obj j)

theorem CategoryTheory.Functor.eval_section_injective_of_eventually_injective {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] {j : J} (Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.toPrefunctor.map f)) (i : J) (f : i ⟶ j) : Function.Injective fun (s : ↑(CategoryTheory.Functor.sections F)) => ↑s j

theorem CategoryTheory.Functor.eval_section_surjective_of_surjective {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Nonempty (F.toPrefunctor.obj j)] [∀ (j : J), Finite (F.toPrefunctor.obj j)] (Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.toPrefunctor.map f)) (i : J) : Function.Surjective fun (s : ↑(CategoryTheory.Functor.sections F)) => ↑s i

theorem CategoryTheory.Functor.eventually_injective {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Nonempty (F.toPrefunctor.obj j)] [∀ (j : J), Finite (F.toPrefunctor.obj j)] (Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.toPrefunctor.map f)) [Nonempty J] [Finite ↑(CategoryTheory.Functor.sections F)] : ∃ (j : J), ∀ (i : J) (f : i ⟶ j), Function.Injective (F.toPrefunctor.map f)