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

theorem nonempty_sections_of_finite_inverse_system {J : Type u} [Preorder J] [IsDirected J fun (x1 x2 : J) => x1 ≤ x2] (F : CategoryTheory.Functor 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.

def CategoryTheory.Functor.eventualRange {J : Type u} [Category.{u_1, u} J] (F : Functor 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.eventualRange j = ⋂ (i : J), ⋂ (f : i ⟶ j), Set.range (F.map f)

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

def CategoryTheory.Functor.IsMittagLeffler {J : Type u} [Category.{u_1, u} J] (F : 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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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} [Category.{u_1, u} J] (F : Functor J (Type v)) [IsCofilteredOrEmpty J] (h : F.IsMittagLeffler) ⦃i j : J⦄ (f : i ⟶ j) : Function.Surjective (F.toEventualRanges.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} [Category.{u_1, u} J] (F : Functor J (Type v)) [IsCofilteredOrEmpty J] (h : F.IsMittagLeffler) [∀ (j : J), Nonempty (F.obj j)] (j : J) : Nonempty (F.toEventualRanges.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} [Category.{u_1, u} J] (F : Functor J (Type v)) [IsCofilteredOrEmpty 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 CategoryTheory.Functor.toPreimages_nonempty_of_surjective {J : Type u} [Category.{u_1, u} J] (F : Functor J (Type v)) {i : J} (s : Set (F.obj i)) [IsCofilteredOrEmpty 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.toPreimages s).obj j)

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

theorem CategoryTheory.Functor.eval_section_surjective_of_surjective {J : Type u} [Category.{u_1, u} J] (F : Functor J (Type v)) [IsCofilteredOrEmpty 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 fun (s : ↑F.sections) => ↑s i

theorem CategoryTheory.Functor.eventually_injective {J : Type u} [Category.{u_1, u} J] (F : Functor J (Type v)) [IsCofilteredOrEmpty 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)