CategoryTheory.Functor.thin_diagram_of_surjective
theorem CategoryTheory.Functor.thin_diagram_of_surjective :
∀ {J : Type u} [inst : CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v))
[inst_1 : CategoryTheory.IsCofilteredOrEmpty J],
(∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)) → ∀ {i j : J} (f g : i ⟶ j), F.map f = F.map g
The theorem `CategoryTheory.Functor.thin_diagram_of_surjective` states that for any category `J` and any functor `F` from `J` to the category of types, if every arrow (morphism) in `F` is surjective, then `F` "factors through a poset". In other words, if for every object `i` and `j` in `J` and every morphism `f` from `i` to `j`, the function `F.map f` is surjective (every element in the target is the image of some element in the source), then for any two morphisms `f` and `g` from `i` to `j`, `F.map f` is equal to `F.map g`. This theorem is assuming that `J` is either cofiltered or empty, which are conditions on the morphisms of `J`.
More concisely: If `F` is a functor from a cocitempty category `J` with surjective morphisms, then `F` factors through a poset and `F.map` is constant on equal morphisms.
|
nonempty_sections_of_finite_inverse_system
theorem nonempty_sections_of_finite_inverse_system :
∀ {J : Type u} [inst : Preorder J] [inst_1 : IsDirected J fun x x_1 => x ≤ x_1]
(F : CategoryTheory.Functor Jᵒᵖ (Type v)) [inst_2 : ∀ (j : Jᵒᵖ), Finite (F.obj j)]
[inst_3 : ∀ (j : Jᵒᵖ), Nonempty (F.obj j)], F.sections.Nonempty
This theorem states that the inverse limit of nonempty finite types is also nonempty. This can be seen as a generalization of Kőnig's lemma. To put it in a specific context, consider a locally finite connected graph. If `Jᵒᵖ` is interpreted as ℕ (the set of natural numbers) and `F j` represents paths of length `j` starting from a fixed vertex, then elements of `F.sections` can be interpreted as infinite rays in the graph. The theorem is a special case of a more general result for cofiltered limits. The uniqueness of this theorem lies in the fact that it allows `J` to be empty.
More concisely: The inverse limit of a system of nonempty finite types is a nonempty type.
|
CategoryTheory.Functor.eventualRange_mapsTo
theorem CategoryTheory.Functor.eventualRange_mapsTo :
∀ {J : Type u} [inst : CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i j : J}
[inst_1 : CategoryTheory.IsCofilteredOrEmpty J] (f : j ⟶ i),
Set.MapsTo (F.map f) (F.eventualRange j) (F.eventualRange i)
This theorem states that for any category `J` and any functor `F` from `J` to some type `v`, given any two objects `i` and `j` in `J` and a morphism `f` from `j` to `i`, the map induced by `f` via the functor `F` has the property that it sends the eventual range of `F` at `j` into the eventual range of `F` at `i`.
To elaborate, the eventual range of `F` at an object `j` is defined as the intersection of the ranges of all maps `F.map f` where `f` varies over all morphisms to `j` from any object in `J`. The theorem asserts that this set at `j` is mapped into the corresponding set at `i` by `F.map f`.
This is under the assumption that `J` satisfies the condition of being cofiltered or empty, which is a kind of completeness condition for categories.
More concisely: For any cofiltered category J and functor F from J to a type, given objects i and j in J and a morphism f from j to i, the image of the eventual range of F at j under F.map f is contained in the eventual range of F at i.
|
nonempty_sections_of_finite_cofiltered_system.init
theorem nonempty_sections_of_finite_cofiltered_system.init :
∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [inst_1 : 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 theorem, `nonempty_sections_of_finite_cofiltered_system.init`, establishes that for any type `J` that is a small category and either cofiltered or empty, and for any functor `F` from `J` to the same universe, if each `F.obj j` is a finite non-empty type, then there exist nonempty sections of `F`. In other words, it assures the existence of global elements that map to an element in each of the finite nonempty sets in the image of the functor. This is a stepping stone to the more general theorem `TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system`.
More concisely: For any small cofiltered or empty category `J` and functor `F` from `J` to a universe, if each `F.obj j` is a finite non-empty type, then `F` has nonempty sections.
|
nonempty_sections_of_finite_cofiltered_system
theorem nonempty_sections_of_finite_cofiltered_system :
∀ {J : Type u} [inst : CategoryTheory.Category.{w, u} J] [inst_1 : CategoryTheory.IsCofilteredOrEmpty J]
(F : CategoryTheory.Functor J (Type v)) [inst_2 : ∀ (j : J), Finite (F.obj j)]
[inst_3 : ∀ (j : J), Nonempty (F.obj j)], F.sections.Nonempty
This theorem states that for any category `J` which is either cofiltered or empty, and any functor `F: J -> Type v` with the property that for every object `j` in `J`, the functor's image `F.obj j` is a finite and nonempty type, there exists at least one section of the functor `F`. In other words, there is at least one natural transformation from the identity functor on the category `J` to the functor `F`.
This theorem is a general statement about the existence of sections in the context of finite, cofiltered categories. The comments indicate there is a special case of this theorem for inverse limits, which can be found under the name `nonempty_sections_of_finite_inverse_system`.
More concisely: In any cofiltered or empty category `J` where every object maps to a finite and nonempty type under a functor `F`, there exists at least one section of `F`.
|
CategoryTheory.Functor.surjective_toEventualRanges
theorem CategoryTheory.Functor.surjective_toEventualRanges :
∀ {J : Type u} [inst : CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v))
[inst_1 : CategoryTheory.IsCofilteredOrEmpty J],
F.IsMittagLeffler → ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.toEventualRanges.map f)
The theorem `CategoryTheory.Functor.surjective_toEventualRanges` states that for any category `J` of type `u` and for any functor `F` from `J` to the category of types with type `v`, assuming `J` is cofiltered or empty, if `F` satisfies the Mittag-Leffler condition, then for any two objects `i` and `j` in `J` and for any morphism `f` from `i` to `j`, the function `F.toEventualRanges.map f` is surjective. In other words, for every element in the codomain there exists an element in the domain such that the function maps this element to the one in the codomain. The Mittag-Leffler condition is a property in category theory that is satisfied by certain functors, and the theorem relates this property to the concept of surjectivity when the functor is restricted to eventual ranges.
More concisely: Given a cofiltered or empty category `J`, a functor `F` from `J` to types satisfying the Mittag-Leffler condition, and morphism `f` in `J`, the function `F.toEventualRanges.map f` is surjective.
|
CategoryTheory.Functor.toEventualRanges_nonempty
theorem CategoryTheory.Functor.toEventualRanges_nonempty :
∀ {J : Type u} [inst : CategoryTheory.Category.{u_1, u} J] (F : CategoryTheory.Functor J (Type v))
[inst_1 : CategoryTheory.IsCofilteredOrEmpty J],
F.IsMittagLeffler → ∀ [inst_2 : ∀ (j : J), Nonempty (F.obj j)] (j : J), Nonempty (F.toEventualRanges.obj j)
The theorem states that if we have a functor `F` from a category `J` to the category of types, and `F` is Mittag-Leffler, then the functor obtained by taking the eventual ranges of `F` at each object of the category is also nonempty at each index. This is true under the condition that `J` is either cofiltered or empty, and `F` is nonempty at each index in `J`.
More concisely: If `F` is a Mittag-Leffler functor from a cofiltered or empty category `J` to the category of types in Lean 4, then the functor of eventual ranges of `F` is nonempty at each object of `J` whenever `F` is nonempty at each index.
|