CategoryTheory.Functor.cofinal_of_colimit_comp_coyoneda_iso_pUnit
theorem CategoryTheory.Functor.cofinal_of_colimit_comp_coyoneda_iso_pUnit :
∀ {C : Type v} [inst : CategoryTheory.Category.{v, v} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v, u₁} D]
(F : CategoryTheory.Functor C D),
((d : D) → CategoryTheory.Limits.colimit (F.comp (CategoryTheory.coyoneda.obj (Opposite.op d))) ≅ PUnit.{v + 1}) →
F.Final
This theorem states that, given any two categories `C` and `D`, and a functor `F` from `C` to `D`, if for every object `d` in `D`, the colimit of the composite functor `F` followed by the object-wise application of the co-Yoneda embedding to the opposite of `d` is isomorphic to the terminal object in the category of types, then the functor `F` is "cofinal".
In this context, "cofinal" is a property of functors which indicates a certain kind of "completeness", intuitively expressing that the functor `F` is abundant enough in terms of how its image in `D` interacts with all objects of `D`.
More concisely: If for every object `d` in category `D`, the colimit of the composite functor `F` and the co-Yoneda embedding of `D`'s opposite at `d` is isomorphic to the terminal object in the category of types, then functor `F` is cofinal.
|
CategoryTheory.Functor.initial_of_equivalence_comp
theorem CategoryTheory.Functor.initial_of_equivalence_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : F.IsEquivalence]
[inst : (F.comp G).Initial], G.Initial
This theorem, `CategoryTheory.Functor.initial_of_equivalence_comp`, states that for any three categories `C`, `D`, and `E` and two functors `F : C -> D` and `G : D -> E`, if `F` is an equivalence (i.e., it has an inverse up to natural isomorphism) and the composition `F.comp G` is initial, then `G` is also initial. In other words, if we have an initial functor from `C` to `E` that factors through `D`, and the first part of the factorization is an equivalence, then the second part of the factorization is also an initial functor.
More concisely: If `F : C -> D` is an equivalence of categories and `G : D -> E` is initial with `F.comp G` being initial, then `G` is initial.
|
CategoryTheory.Functor.final_iff_comp_equivalence
theorem CategoryTheory.Functor.final_iff_comp_equivalence :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : G.IsEquivalence],
F.Final ↔ (F.comp G).Final
This theorem is a statement about category theory. It states that for any categories `C`, `D`, and `E`, and for any functors `F` from `C` to `D` and `G` from `D` to `E`, if `G` is an equivalence of categories, then `F` is a final functor if and only if the composition of `F` and `G` is also a final functor. Here, a final functor is one such that for any object in the codomain category, there is essentially only one morphism from any object in the domain category.
More concisely: If functors `F: C -> D` and `G: D -> E` are such that `G` is an equivalence of categories, then `F` is a final functor if and only if the composite `G ∘ F` is a final functor.
|
CategoryTheory.IsCofilteredOrEmpty.of_initial
theorem CategoryTheory.IsCofilteredOrEmpty.of_initial :
∀ {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 : F.Initial]
[inst : CategoryTheory.IsCofilteredOrEmpty C], CategoryTheory.IsCofilteredOrEmpty D
This theorem states that initial functors preserve the property of being cofiltered or empty. In the context of category theory, given two categories `C` and `D` with a functor `F` from `C` to `D` that is initial (meaning every object in `D` is isomorphic to `F(X)` for some `X` in `C`), if `C` is either cofiltered or empty, then `D` is also either cofiltered or empty. This theorem is a generalization of `IsCofiltered.of_left_adjoint`, which states that left adjoints preserve cofilteredness, as right adjoints are always initial, as stated in `initial_of_adjunction`.
More concisely: If functor `F` from category `C` to category `D` is initial and category `C` is cofiltered or empty, then category `D` is also cofiltered or empty.
|
CategoryTheory.Functor.initial_of_final_op
theorem CategoryTheory.Functor.initial_of_final_op :
∀ {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 : F.op.Final], F.Initial
This theorem states that, given any two categories `C` and `D`, and a functor `F` from `C` to `D`, if the opposite functor `F.op` is final, then the original functor `F` is initial. This is in the context of category theory, and the "opposite" functor reverses the direction of morphisms, while "final" and "initial" relate to certain properties of functors in terms of how they interact with limits and colimits.
More concisely: If the opposite functor of `F` from category `C` to category `D` is final, then `F` is initial.
|
CategoryTheory.Functor.final_comp
theorem CategoryTheory.Functor.final_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [hF : F.Final] [hG : G.Final],
(F.comp G).Final
This theorem is about functors in category theory. It states that for any three categories `C`, `D`, and `E`, and two functors `F` from `C` to `D` and `G` from `D` to `E`, if both `F` and `G` are "final" (a property that relates to how limits are preserved), then the composite functor `F` followed by `G` (notated as `CategoryTheory.Functor.comp F G`) is also final.
More concisely: If functors `F: C -> D` and `G: D -> E` are both final, then their composition `F ∘ G` is also a final functor.
|
CategoryTheory.Functor.final_of_final_comp
theorem CategoryTheory.Functor.final_of_final_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [hF : F.Final] [hFG : (F.comp G).Final],
G.Final
This theorem states that in the context of category theory, given categories `C`, `D`, and `E`, and functors `F` from `C` to `D` and `G` from `D` to `E`, if the functor `F` is final and the composition of functors `F` and `G` is also final, then the functor `G` is final. In other words, if morphisms from any object to the object transformed by `F` and the composition of `F` and `G` determine a unique morphism, then morphisms from any object to the object transformed by `G` also determine a unique morphism.
More concisely: If functors `F: C -> D` and `G: D -> E` have the property that `F` is final and the composite `G ∘ F` is final, then `G` is final.
|
CategoryTheory.Functor.final_iff_equivalence_comp
theorem CategoryTheory.Functor.final_iff_equivalence_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : F.IsEquivalence],
G.Final ↔ (F.comp G).Final
The theorem `CategoryTheory.Functor.final_iff_equivalence_comp` states that for any categories `C`, `D`, and `E`, and any functors `F` from `C` to `D` and `G` from `D` to `E`, if `F` is an equivalence of categories, then `G` is a final functor if and only if the composition of `F` and `G` is a final functor. Here, a functor is "final" if it has certain properties that make it behave like a projection onto a final object in a category.
More concisely: If `F: C -> D` is an equivalence of categories and `G: D -> E` is a final functor, then the composition `F &&& G: C -> E` is a final functor.
|
CategoryTheory.Functor.initial_comp_equivalence
theorem CategoryTheory.Functor.initial_comp_equivalence :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : F.Initial] [inst_4 : G.IsEquivalence],
(F.comp G).Initial
This theorem states that in the context of category theory, given three categories `C`, `D`, and `E`, if we have a functor `F` from `C` to `D` that is initial and another functor `G` from `D` to `E` that is an equivalence, then the composition of `F` and `G` (denoted `F.comp G`) is also initial. This theorem is a more specific version of a more general theorem named `initial_comp`.
More concisely: Given functors `F: C -> D` initial and `G: D -> E` an equivalence, the composition `F.comp G` is also initial in category `E`.
|
CategoryTheory.Functor.final_of_equivalence_comp
theorem CategoryTheory.Functor.final_of_equivalence_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : F.IsEquivalence]
[inst : (F.comp G).Final], G.Final
This theorem states that in the context of category theory, if we have three categories `C`, `D`, and `E`, along with two functors: `F` from `C` to `D` and `G` from `D` to `E`. If `F` is an equivalence functor (meaning that it has a quasi-inverse) and the composition of `F` and `G` (denoted `F.comp G`) is a final functor (meaning that for any object in its domain, all morphisms from it to any other object factor uniquely through it), then `G` is also a final functor.
More concisely: If `F: C -> D` is an equivalence functor with quasi-inverse `F': D -> C` and `G: D -> E` is a functor such that `F.comp G` is a final functor, then `G` is a final functor.
|
CategoryTheory.Functor.final_of_natIso
theorem CategoryTheory.Functor.final_of_natIso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F F' : CategoryTheory.Functor C D} [inst_2 : F.Final],
(F ≅ F') → F'.Final
This theorem states that in the context of category theory, given two categories `C` and `D`, and two functors `F` and `F'` from `C` to `D`, if functor `F` is final and there exists a natural isomorphism between `F` and `F'`, then functor `F'` is also final. In simpler terms, if we can naturally transform a final functor into another functor, that second functor is also final.
More concisely: If functor `F` is final and there exists a natural isomorphism between `F` and `F'`, then `F'` is also a final functor.
|
CategoryTheory.Functor.initial_comp
theorem CategoryTheory.Functor.initial_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : F.Initial] [inst_4 : G.Initial],
(F.comp G).Initial
This theorem states that in category theory, if we have categories C, D and E, with functors F from C to D and G from D to E, and if F and G are initial functors, then the composition of F and G (F followed by G) is also an initial functor. An initial functor is one that maps from an initial category, which is a category with exactly one morphism from each object to any other object.
More concisely: If functors F from C to D and G from D to E are both initial functors with C being an initial category, then the composition F ∘ G is also an initial functor from C to E.
|
CategoryTheory.IsFiltered.of_final
theorem CategoryTheory.IsFiltered.of_final :
∀ {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 : F.Final]
[inst : CategoryTheory.IsFiltered C], CategoryTheory.IsFiltered D
The theorem `CategoryTheory.IsFiltered.of_final` in the Lean 4 programming language states that final functors preserve the property of being filtered in category theory. When applied to a specific category `C` and a functor `F` from `C` to another category `D`, if `C` is a filtered category and `F` is a final functor, then `D` is also a filtered category. This is a generalization of the theorem `IsFiltered.of_right_adjoint`, which states that right adjoints (a kind of functor that is always final) also preserve filteredness.
More concisely: If `F` is a final functor from a filtered category `C` to another category `D`, then `D` is a filtered category.
|
CategoryTheory.Functor.initial_of_comp_full_faithful'
theorem CategoryTheory.Functor.initial_of_comp_full_faithful' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : G.Full] [inst_4 : G.Faithful]
[inst : (F.comp G).Initial], G.Initial
This theorem states that for any categories `C`, `D`, and `E`, and any functors `F` from `C` to `D`, and `G` from `D` to `E`, if the functor `G` is both full and faithful, and the composition of `F` and `G` is initial, then the functor `G` is also initial. In other words, in the context of category theory, if we have a chain of mappings where the second mapping has a "faithful" and "full" relationship and the overall composite mapping is "initial", this implies that the second mapping is also "initial".
More concisely: If functors F from C to D, G from D to E are both full and faithful, and their composition is initial, then G is initial.
|
CategoryTheory.Functor.initial_of_comp_full_faithful
theorem CategoryTheory.Functor.initial_of_comp_full_faithful :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : G.Full] [inst_4 : G.Faithful]
[inst_5 : (F.comp G).Initial], F.Initial
This theorem states that in the context of Category Theory, given categories `C`, `D`, and `E`, and functors `F : C -> D` and `G : D -> E`, if `G` is a full and faithful functor and the composition of `F` and `G` is initial, then `F` is also an initial functor. The concept of being an "initial" functor relates to the idea that there exists a unique morphism from the initial object to any other object. Similarly, a full functor is one where for any two objects, the function mapping the hom-sets is surjective, while a faithful functor is one where that function is injective.
More concisely: If functors `F : C -> D`, `G : D -> E`, and `G` is a full and faithful functor with the composition `F ∘ G` being the initial functor from `E` to `D`, then `F` is the initial functor from `C` to `D`.
|
CategoryTheory.Functor.initial_of_adjunction
theorem CategoryTheory.Functor.initial_of_adjunction :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C},
(L ⊣ R) → L.Initial
This theorem states that in category theory, if a functor `L`, mapping from category `C` to category `D`, is a left adjoint of some functor `R` (denoted by `L ⊣ R`), then `L` is an initial functor. It's important to note that `C` and `D` are categories, while `L` and `R` are functors between these categories.
More concisely: If functor `L` is the left adjoint of `R` in the category theory of functors between categories `C` and `D`, then `L` is the initial object in the category of left adjoints of `R` in `C` to `D`.
|
CategoryTheory.Functor.final_of_comp_full_faithful'
theorem CategoryTheory.Functor.final_of_comp_full_faithful' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : G.Full] [inst_4 : G.Faithful]
[inst : (F.comp G).Final], G.Final
This theorem states that for any categories C, D, and E, and any functors F: C -> D and G: D -> E, if G is a full and faithful functor, and the composition of the functors F and G is final, then G is also a final functor. In the context of category theory, a "final" functor is one where every object in the domain category is isomorphic to a "mapped" object in the codomain category, a "full" functor is one where every morphism in the codomain category "comes from" a morphism in the domain category, and a "faithful" functor is one where different morphisms in the domain category map into different morphisms in the codomain category.
More concisely: If functors F: C -> D and G: D -> E are full and faithful, and composition F \circ G is final, then G is final.
|
CategoryTheory.Functor.final_equivalence_comp
theorem CategoryTheory.Functor.final_equivalence_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : F.IsEquivalence] [inst_4 : G.Final],
(F.comp G).Final
The theorem `CategoryTheory.Functor.final_equivalence_comp` states that for any categories `C`, `D`, and `E`, and for any functors `F` from `C` to `D` and `G` from `D` to `E`, if `F` is an equivalence and `G` is final, then the composite functor `F.comp G` (i.e., the functor obtained by applying `F` and then `G`) is also final. In category theory, a final functor is one which determines a limit for any diagram in the source category, and an equivalence is a functor that has an inverse up to natural isomorphism.
More concisely: If functors `F: C -> D` is an equivalence and `G: D -> E` is final, then the composite functor `F.comp G: C -> E` is also final.
|
CategoryTheory.Functor.final_of_adjunction
theorem CategoryTheory.Functor.final_of_adjunction :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C},
(L ⊣ R) → R.Final
The theorem `CategoryTheory.Functor.final_of_adjunction` states that for any two categories 'C' and 'D', and any pair of functors 'L' from 'C' to 'D' and 'R' from 'D' to 'C', if 'L' is left adjoint to 'R', then the functor 'R' is final. In category theory, a functor is final if for every object in the domain category, the corresponding hom-set to the codomain category is nonempty and every morphism in the domain category to the functor's image can be uniquely extended along the functor.
More concisely: If functor L : C -> D is left adjoint to functor R : D -> C, then R is final on C, i.e., for every object C' in C, the hom-set Hom(C', RC) is nonempty and every morphism f : C' -> L(X) has a unique extension to a morphism g : C' -> X in C for any object X in D with R(g) = f.
|
CategoryTheory.IsCofiltered.of_initial
theorem CategoryTheory.IsCofiltered.of_initial :
∀ {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 : F.Initial]
[inst : CategoryTheory.IsCofiltered C], CategoryTheory.IsCofiltered D
This theorem states that initial functors preserve the property of being cofiltered in category theory. In other words, if we have an initial functor `F` from a category `C` to a category `D` and `C` is cofiltered, then `D` is also cofiltered. This theorem can be seen as a generalization of `IsCofiltered.of_left_adjoint`, which states that left adjoints preserve cofilteredness, as right adjoints are always initial (refer to `intial_of_adjunction`).
More concisely: If `F` is an initial functor from a cofiltered category `C` to a category `D`, then `D` is also cofiltered.
|
CategoryTheory.Functor.final_of_comp_full_faithful
theorem CategoryTheory.Functor.final_of_comp_full_faithful :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : G.Full] [inst_4 : G.Faithful]
[inst_5 : (F.comp G).Final], F.Final
This theorem, `CategoryTheory.Functor.final_of_comp_full_faithful`, states that given categories `C`, `D`, and `E`, if we have functors `F : C -> D` and `G : D -> E`, such that `G` is full and faithful, and the composition `F ∘ G` is final (meaning every morphism in `E` is essentially uniquely determined by its preimage under `F ∘ G`), then `F` is also final. In other words, every morphism in `D` is essentially uniquely determined by its preimage under `F`.
More concisely: If functors `F : C -> D` and `G : D -> E` are such that `F` maps isomorphisms in `C` to isomorphisms in `D`, `G` is full and faithful, and `F ∘ G` is final, then `F` is final.
|
CategoryTheory.Functor.Initial.hasLimit_of_comp
theorem CategoryTheory.Functor.Initial.hasLimit_of_comp :
∀ {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 : F.Initial] {E : Type u₃}
[inst_3 : CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E}
[inst : CategoryTheory.Limits.HasLimit (F.comp G)], CategoryTheory.Limits.HasLimit G
The theorem `CategoryTheory.Functor.Initial.hasLimit_of_comp` states that in category theory, if `F` is an initial functor from some category `C` to another category `D`, and the composition of `F` and another functor `G` (in that order) has a limit, then `G` itself also has a limit. This theorem is not automatically inferred in Lean 4 because the functor `F` is not determined by the goal, and creating an automatic instance would cause a loop with `comp_hasLimit`.
More concisely: If `F: C -> D` is an initial functor from category `C` to `D` and the composition `F ∘ G: C -> D` has a limit for some functor `G: C -> D`, then `G` has a limit.
|
CategoryTheory.IsFilteredOrEmpty.of_final
theorem CategoryTheory.IsFilteredOrEmpty.of_final :
∀ {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 : F.Final]
[inst : CategoryTheory.IsFilteredOrEmpty C], CategoryTheory.IsFilteredOrEmpty D
This theorem states that final functors preserve the property of being filtered or empty in category theory. Given two categories `C` and `D`, and a final functor `F` from `C` to `D`, if `C` is filtered or empty, then `D` is also filtered or empty. This theorem can be seen as a generalization of the theorem `IsFiltered.of_right_adjoint`, which says that right adjoints (a type of functor) preserve filteredness, because right adjoints are always final functors.
More concisely: If `F : C -> D` is a final functor between categories `C` and `D`, then `C` being filtered or empty implies that `D` is also filtered or empty.
|
CategoryTheory.Functor.Final.hasColimit_of_comp
theorem CategoryTheory.Functor.Final.hasColimit_of_comp :
∀ {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 : F.Final] {E : Type u₃}
[inst_3 : CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E}
[inst : CategoryTheory.Limits.HasColimit (F.comp G)], CategoryTheory.Limits.HasColimit G
This theorem states that if we have a functor `F` from category `C` to `D` that is cofinal, and another functor `G` from `D` to `E`, then if the composition of these functors `F ⋙ G` has a colimit, then `G` also has a colimit. In other words, it ensures that the property of having a colimit is preserved under the operation of pre-composition with a cofinal functor. This theorem is not set as an instance because `F` cannot be determined solely by the goal.
More concisely: If `F: C -> D` is a cofinal functor and `G: D -> E` has a right adjoint, then `G` has a colimit if and only if `F ⋙ G` has a colimit.
|
CategoryTheory.Functor.initial_iff_comp_equivalence
theorem CategoryTheory.Functor.initial_iff_comp_equivalence :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : G.IsEquivalence],
F.Initial ↔ (F.comp G).Initial
The theorem `CategoryTheory.Functor.initial_iff_comp_equivalence` states that for any categories `C`, `D`, and `E`, and functors `F` from `C` to `D` and `G` from `D` to `E`, if `G` is an equivalence of categories, then `F` is initial if and only if the composition of `F` and `G` is initial. In the context of category theory, a functor is initial if it maps from an initial object (an object with exactly one morphism going to any other object) in its domain category.
More concisely: A functor is initial in its domain category if and only if its composition with an equivalence of categories is also initial in the target category.
|
CategoryTheory.Functor.initial_iff_equivalence_comp
theorem CategoryTheory.Functor.initial_iff_equivalence_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : F.IsEquivalence],
G.Initial ↔ (F.comp G).Initial
This theorem states that in the context of three categories C, D, and E along with two functors F : C → D and G : D → E, if F is an equivalence of categories, then G is an initial object in its category if and only if the composition of F and G (F.comp G) is an initial object in its category. An initial object is an object for which there exists exactly one morphism from it to any other object in the category.
More concisely: Given categories C, D, and E, functors F : C -> D and G : D -> E, if F is an equivalence of categories then G is the initial object in E if and only if F.comp G is the initial object in C.
|
CategoryTheory.Functor.initial_equivalence_comp
theorem CategoryTheory.Functor.initial_equivalence_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : F.IsEquivalence] [inst_4 : G.Initial],
(F.comp G).Initial
This theorem is in the context of Category Theory, and it states that if we have three categories `C`, `D` and `E`, along with functors `F` from `C` to `D` and `G` from `D` to `E`, if `F` is an equivalence and `G` is initial, then the composition of `F` and `G` (denoted as `F.comp G`) is also initial. An initial functor means a functor where every object in the target category is isomorphic to the image of some object in the source category, and an equivalence of categories is a functor that has both a left and a right adjoint.
More concisely: If functors `F: C -> D` is an equivalence of categories and `G: D -> E` is an initial functor, then the composition `F.comp G` is an initial functor in category `E`.
|
CategoryTheory.Functor.final_comp_equivalence
theorem CategoryTheory.Functor.final_comp_equivalence :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : F.Final] [inst_4 : G.IsEquivalence],
(F.comp G).Final
This theorem, `CategoryTheory.Functor.final_comp_equivalence`, states that for any three categories `C`, `D`, and `E`, given a functor `F` from `C` to `D`, and a functor `G` from `D` to `E`, if the functor `F` is final and the functor `G` is an equivalence, then the composition of `F` and `G` is also final. This is a result in category theory, a branch of mathematics which deals with abstract structures and their relationships.
More concisely: If functors `F: C -> D` is final and `G: D -> E` is an equivalence, then the composition `G ∘ F: C -> E` is a final functor.
|