CategoryTheory.AbelianOfAdjunction.hasKernels
theorem CategoryTheory.AbelianOfAdjunction.hasKernels :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
[inst_2 : CategoryTheory.Category.{v, u₂} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D C) [inst_4 : G.PreservesZeroMorphisms],
(F.comp G ≅ CategoryTheory.Functor.id C) →
∀ [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits G], CategoryTheory.Limits.HasKernels C
This theorem, named `CategoryTheory.AbelianOfAdjunction.hasKernels`, states that for any given types `C` and `D` that are categories, with `C` being preadditive and `D` being abelian, and for any functors `F` and `G` from `C` to `D` and `D` to `C` respectively, if `G` preserves zero morphisms and the composition of `F` and `G` is isomorphic to the identity functor on `C`, then if `G` preserves finite limits, `C` has kernels.
In simpler terms, this theorem pertains to the properties of categories and their functors in category theory. It says, if we have two categories and two functors that meet certain conditions related to additive and abelian properties, and their composition behaves in a specific way (isomorphic to the identity), then under the provision that one of the functors preserves finite limits, the first category is guaranteed to have kernels, which are important concepts in category theory related to limits.
More concisely: Given preadditive category `C` and abelian category `D`, if functors `F: C -> D`, `G: D -> C`, and their composition is an isomorphism, with `G` preserving zero morphisms and finite limits, then `C` has kernels.
|
CategoryTheory.AbelianOfAdjunction.hasCokernels
theorem CategoryTheory.AbelianOfAdjunction.hasCokernels :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
[inst_2 : CategoryTheory.Category.{v, u₂} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D C) [inst_4 : G.PreservesZeroMorphisms],
(F.comp G ≅ CategoryTheory.Functor.id C) → (G ⊣ F) → CategoryTheory.Limits.HasCokernels C
This theorem states that, given a category `C` with structure `inst` and preadditive structure `inst_1`, a category `D` with structure `inst_2` and abelian structure `inst_3`, functors `F` and `G` between `C` and `D` with `G` preserving zero morphisms (`inst_4`), if the composition `F.comp G` of the functors is naturally isomorphic (`≅`) to the identity functor `CategoryTheory.Functor.id C` on `C`, and `G` is left adjoint (`⊣`) to `F`, then `C` has cokernels (denoted by `CategoryTheory.Limits.HasCokernels C`).
In simpler terms, this theorem is about a special property of categories in category theory (a branch of mathematics). It says that if we have a certain structure on two categories and two functors with specific properties (being adjoint with one preserving zero morphisms), and if the composition of these functors is essentially the same as doing nothing (the identity), then the original category has a certain desirable property: it has cokernels.
More concisely: Given categories `C` and `D` with specific structures, functors `F: C -> D` and `G: D -> C` that are left adjoint and preserve zero morphisms, if `F.comp G` is naturally isomorphic to the identity functor on `C`, then `C` has cokernels.
|