CategoryTheory.isFiltered_structuredArrow_of_isFiltered_of_exists
theorem CategoryTheory.isFiltered_structuredArrow_of_isFiltered_of_exists :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D)
[inst_2 : CategoryTheory.IsFilteredOrEmpty C],
(∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) →
(∀ {d : D} {c : C} (s s' : d ⟶ F.obj c),
∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)) →
∀ (d : D), CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow d F)
This theorem is about the structure of categories in category theory. Specifically, it states that for any type `C` which forms a category and is either filtered or empty, a given functor `F` from `C` to another category `D`, and under the condition that for any object `d` in `D`, there exists an object `c` in `C` and a morphism from `d` to the image of `c` under the functor `F`, if for any two morphisms `s` and `s'` from object `d` to the image of `c` under `F`, there exists an object `c'` and a morphism `t` such that the composition of `s` and the image of `t` under `F` equals the composition of `s'` and the image of `t` under `F`, then for any object `d` in `D`, the category of structured arrows from `d` to `F` is filtered.
In mathematical terms, this theorem asserts that under these conditions, the category of structured arrows from any object in the target category to the functor is a filtered category. It essentially highlights a particular structure preservation property of functors in category theory.
More concisely: If `C` is a filtered or empty category, `F` is a functor from `C` to another category `D`, and for every object `d` in `D`, there exists an object `c` in `C` and a morphism `t` such that for any morphisms `s` and `s'` from `d` to the image of `c` under `F`, the existence of `c'` implies the equality `s ∘ F(t) = s' ∘ F(t)`, then the category of structured arrows from `d` to `F` is filtered.
|
CategoryTheory.Functor.final_iff_of_isFiltered
theorem CategoryTheory.Functor.final_iff_of_isFiltered :
∀ {C : Type v₁} [inst : CategoryTheory.Category.{v₁, v₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D)
[inst_2 : CategoryTheory.IsFilteredOrEmpty C],
F.Final ↔
(∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧
∀ {d : D} {c : C} (s s' : d ⟶ F.obj c),
∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)
The theorem `CategoryTheory.Functor.final_iff_of_isFiltered` states that given a category `C` that is filtered or empty, and another category `D`, along with a functor `F` from `C` to `D`, the functor `F` is final if and only if the following conditions hold:
1. For every object `d` in `D`, there exists an object `c` in `C` such that there is at least one morphism from `d` to `F.obj c`, and
2. For any two morphisms `s` and `s'` from an object `d` in `D` to `F.obj c` for some object `c` in `C`, there exists an object `c'` in `C` and a morphism `t` from `c` to `c'` such that composing `s` with `F.map t` is equal to composing `s'` with `F.map t`.
Here, `F.obj c` denotes the object obtained by applying the functor `F` to the object `c`, and `F.map t` denotes the morphism obtained by applying the functor `F` to the morphism `t`. The term `CategoryTheory.CategoryStruct.comp` denotes the composition of morphisms in a category.
More concisely: A functor from a filtered or empty category to another category is final if and only if for every object in the target category, there exists an object in the source category with at least one morphism to it and any two such morphisms can be connected by a morphism in the source category whose image under the functor equals their composition.
|