Documentation

Mathlib.CategoryTheory.CofilteredSystem

Cofiltered systems #

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,

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 (x x_1 : J) => x x_1] (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.

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)
Instances For
    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.obj j} :
    x F.eventualRange 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 isMittagLeffler_iff_eventualRange), the eventual range at j is attained by some f : i ⟶ j.

    Equations
    Instances For
      theorem CategoryTheory.Functor.isMittagLeffler_iff_eventualRange {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.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} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} {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} [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 : F.eventualRange k = Set.range (F.map g)) :
      F.eventualRange k = Set.range (F.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.map f)) :
      F.IsMittagLeffler
      @[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.obj i)) (j : J) :
      (F.toPreimages s).obj j = (⋂ (f : j i), F.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.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

      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.
      Instances For
        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.obj i)) [∀ (j : J), Finite (F.obj j)] (j : J) :
        Finite ((F.toPreimages s).obj j)
        Equations
        • =
        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.map f) (F.eventualRange j) (F.eventualRange 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 : F.IsMittagLeffler) (f : j i) :
        F.eventualRange i = F.map f '' F.eventualRange 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} :
        F.eventualRange j = Set.range (F.map f) ∀ ⦃k : J⦄ (g : k i), Set.range (F.map f) Set.range (F.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] :
        F.IsMittagLeffler ∀ (j : J), ∃ (i : J) (f : i j), ∀ ⦃k : J⦄ (g : k i), Set.range (F.map f) Set.range (F.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.obj i)) [CategoryTheory.IsCofilteredOrEmpty J] (h : F.IsMittagLeffler) :
        (F.toPreimages s).IsMittagLeffler
        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.range (F.map f)).Finite) :
        F.IsMittagLeffler
        @[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 : (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} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] (j : J) :
        F.toEventualRanges.obj j = (F.eventualRange j)

        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.
        Instances For
          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.obj j)] (j : J) :
          Finite (F.toEventualRanges.obj j)
          Equations
          • =

          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.
          Instances For
            theorem CategoryTheory.Functor.surjective_toEventualRanges {J : Type u} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] (h : F.IsMittagLeffler) ⦃i : J ⦃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} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.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} [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.map f)) {i : J} {j : J} (f : i j) (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} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} (s : Set (F.obj i)) [CategoryTheory.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} [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.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} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.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} [CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.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)