CategoryTheory.Idempotents.isIdempotentComplete_iff_of_equivalence
theorem CategoryTheory.Idempotents.isIdempotentComplete_iff_of_equivalence :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_3, u_2} D],
(C ≌ D) → (CategoryTheory.IsIdempotentComplete C ↔ CategoryTheory.IsIdempotentComplete D)
The theorem `CategoryTheory.Idempotents.isIdempotentComplete_iff_of_equivalence` states that for any two types `C` and `D` that are regarded as categories (i.e., they have the structure of a category specified), if `C` and `D` are equivalent categories, then `C` is idempotent complete if and only if `D` is idempotent complete. In categorical terms, being "idempotent complete" means that every idempotent (an endomorphism that is its own square) has a splitting, which is an object that behaves like the decomposition of the idempotent.
More concisely: If two categories `C` and `D` are equivalent, then `C` is idempotent complete if and only if `D` is idempotent complete.
|
CategoryTheory.Idempotents.idem_of_id_sub_idem
theorem CategoryTheory.Idempotents.idem_of_id_sub_idem :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X : C}
(p : X ⟶ X),
CategoryTheory.CategoryStruct.comp p p = p →
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X - p)
(CategoryTheory.CategoryStruct.id X - p) =
CategoryTheory.CategoryStruct.id X - p
This theorem states that in a preadditive category, if a morphism `p : X → X` is idempotent (meaning that composing `p` with itself results in `p`), then the morphism `𝟙 X - p` (where `𝟙 X` is the identity morphism on `X`) is also idempotent. That is, composing `𝟙 X - p` with itself results in `𝟙 X - p`. The category is defined by the type `C`, `X` is an object of this category, and `p` is a morphism from `X` to `X`.
More concisely: In a preadditive category, an idempotent morphism's identity morphism subtraction is also idempotent. (Or, the identity morphism minus an idempotent morphism is idempotent in a preadditive category.)
|
CategoryTheory.IsIdempotentComplete.idempotents_split
theorem CategoryTheory.IsIdempotentComplete.idempotents_split :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [self : CategoryTheory.IsIdempotentComplete C]
(X : C) (p : X ⟶ X),
CategoryTheory.CategoryStruct.comp p p = p →
∃ Y i e,
CategoryTheory.CategoryStruct.comp i e = CategoryTheory.CategoryStruct.id Y ∧
CategoryTheory.CategoryStruct.comp e i = p
This theorem states that a category is idempotent complete if and only if all idempotent endomorphisms `p` on an object `X` can be represented as a composition `p = e ≫ i` of two other morphisms `e` and `i`, such that the composition `i ≫ e` equals the identity morphism on some object `Y`. Here, `≫` represents the composition of morphisms, and `𝟙 _` represents the identity morphism. In other words, in an idempotent complete category, every idempotent morphism `p` can be "split" into two morphisms `e` and `i` in this manner.
More concisely: In an idempotent complete category, every idempotent endomorphism can be written as a composition of two other morphisms whose composition is the identity on some object.
|
CategoryTheory.Idempotents.isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent
theorem CategoryTheory.Idempotents.isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent :
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C],
CategoryTheory.IsIdempotentComplete C ↔
∀ (X : C) (p : X ⟶ X),
CategoryTheory.CategoryStruct.comp p p = p →
CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.id X) p
The theorem states that a category is idempotent complete if and only if for every object in the category and for every idempotent endomorphism on this object (an endomorphism is idempotent if the composition of the endomorphism with itself equals the endomorphism), there exists an equalizer of the identity morphism on the object and the idempotent endomorphism. In other words, a category is idempotent complete if for any object and any idempotent endomorphism, there is a way to limit the parallel pair of the identity morphism and the idempotent endomorphism.
More concisely: A category is idempotent complete if and only if for every object and every idempotent endomorphism, there exists an equalizer of the identity and idempotent endomorphism.
|
CategoryTheory.Idempotents.isIdempotentComplete_iff_idempotents_have_kernels
theorem CategoryTheory.Idempotents.isIdempotentComplete_iff_idempotents_have_kernels :
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
CategoryTheory.IsIdempotentComplete C ↔
∀ (X : C) (p : X ⟶ X), CategoryTheory.CategoryStruct.comp p p = p → CategoryTheory.Limits.HasKernel p
This theorem states that a preadditive category is pseudoabelian if and only if all idempotent endomorphisms in the category have a kernel. In more detail, for any category 'C', where 'C' is a preadditive category (meaning that it has the ability to perform addition operations on morphisms), the property of 'C' being idempotent complete (meaning that every idempotent morphism in 'C' can be completed to an idempotent split) is equivalent to the property that for every object 'X' in 'C' and for every endomorphism 'p' from 'X' to 'X', if 'p' is idempotent (meaning that the composition of 'p' with itself equals 'p'), then 'p' has a kernel (meaning that there exists a morphism from some object to 'X' that maps to the zero morphism under 'p').
More concisely: A preadditive category is pseudoabelian if and only if every idempotent endomorphism has a kernel.
|