CategoryTheory.Idempotents.Karoubi.comp_p
theorem CategoryTheory.Idempotents.Karoubi.comp_p :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
(f : P.Hom Q), CategoryTheory.CategoryStruct.comp f.f Q.p = f.f
The theorem `CategoryTheory.Idempotents.Karoubi.comp_p` states that for any category `C`, and for any two objects `P` and `Q` in the Karoubi envelope of `C` (i.e., the category obtained by 'adding' idempotents to `C`), if there exists a morphism `f` from `P` to `Q`, then the composition of `f.f` and `Q.p` (where `f.f` is the morphism underlying `f`, and `Q.p` is the idempotent associated with `Q`) is just `f.f`. In other words, the idempotent `Q.p` acts like an identity with respect to the composition operation on the morphism `f.f`.
More concisely: In the Karoubi envelope of a category `C`, for any objects `P` and `Q` and morphism `f` from `P` to `Q`, the composition of `f.f` and `Q.p` equals `f.f`.
|
CategoryTheory.Idempotents.Karoubi.Hom.comm
theorem CategoryTheory.Idempotents.Karoubi.Hom.comm :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
(self : P.Hom Q),
self.f = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp self.f Q.p)
This theorem, named `CategoryTheory.Idempotents.Karoubi.Hom.comm`, states that for any category `C` and for any two objects `P` and `Q` in the idempotent completion (Karoubi envelope) of `C`, given a morphism `self` from `P` to `Q`, the morphism `self.f` is equal to the composition of the idempotent `P.p`, the morphism `self.f`, and the idempotent `Q.p`. This ensures that the given morphism is compatible with the given idempotents, i.e., it respects the idempotent structure of objects in the category.
More concisely: In the idempotent completion of a category, for any morphism from an idempotent object to another, it is equal to the composition of the two idempotents and the morphism itself.
|
CategoryTheory.Idempotents.Karoubi.p_comm
theorem CategoryTheory.Idempotents.Karoubi.p_comm :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
(f : P.Hom Q), CategoryTheory.CategoryStruct.comp P.p f.f = CategoryTheory.CategoryStruct.comp f.f Q.p
The theorem `CategoryTheory.Idempotents.Karoubi.p_comm` states that for any category `C` and any two objects `P` and `Q` in the Karoubi envelope (which is a category formed from `C` by adding new morphisms) of `C`, and for any morphism `f` from `P` to `Q` in this Karoubi envelope, the composition of the projection morphism of `P` and `f` is equal to the composition of `f` and the projection morphism of `Q`. In other words, the projection morphisms commute with any morphism in the Karoubi envelope of the category.
More concisely: For any category C and objects P, Q in its Karoubi envelope, and any morphism f from P to Q in the Karoubi envelope, the composition of the projection of P with f equals the composition of f with the projection of Q.
|
CategoryTheory.Idempotents.Karoubi.idem
theorem CategoryTheory.Idempotents.Karoubi.idem :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (self : CategoryTheory.Idempotents.Karoubi C),
CategoryTheory.CategoryStruct.comp self.p self.p = self.p
The theorem `CategoryTheory.Idempotents.Karoubi.idem` asserts the property of an endomorphism in a category theoretic context. Specifically, for any category `C` and any `Karoubi` idempotent object `self` in `C`, the composition of the morphism `self.p` with itself (notated as `CategoryTheory.CategoryStruct.comp self.p self.p`) is equivalent to `self.p`. In simpler words, this theorem states that the morphism `self.p` is idempotent, meaning applying it twice has the same effect as applying it once.
More concisely: For any category `C` and `Karoubi` idempotent object `self` in `C`, the endomorphism `self.p` is idempotent, i.e., `self.p ∘ self.p = self.p`.
|
CategoryTheory.Idempotents.Karoubi.coe.proof_1
theorem CategoryTheory.Idempotents.Karoubi.coe.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (X : C),
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X) =
CategoryTheory.CategoryStruct.id X
This theorem, part of the category theory library in Lean 4, states that for any object `X` in a category `C`, the composition of the identity morphism on `X` with itself is equal to the identity morphism on `X`. In mathematical terms, this can be represented as `id_X ∘ id_X = id_X`, where `∘` denotes the composition of morphisms and `id_X` is the identity morphism on the object `X`.
More concisely: The composition of the identity morphism with itself is equal to the identity morphism for any object in a category.
|
CategoryTheory.Idempotents.Karoubi.hom_ext_iff
theorem CategoryTheory.Idempotents.Karoubi.hom_ext_iff :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
{f g : P ⟶ Q}, f = g ↔ f.f = g.f
This theorem states that for any two morphisms `f` and `g` from `P` to `Q` in the Karoubi enlargement of a category `C`, `f` is equal to `g` if and only if the underlying functions of `f` and `g` (represented as `f.f` and `g.f`) are equal. The Karoubi enlargement of a category is a construction in category theory that includes all idempotents of the category.
More concisely: In the Karoubi enlargement of a category `C`, two morphisms `f` and `g` from `P` to `Q` are equal if and only if their underlying functions `f.f` and `g.f` are equal.
|
Mathlib.CategoryTheory.Idempotents.Karoubi._auxLemma.1
theorem Mathlib.CategoryTheory.Idempotents.Karoubi._auxLemma.1 :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
{f g : P ⟶ Q}, (f = g) = (f.f = g.f)
This theorem states that in the context of category theory, for any category `C` and any two idempotent Karoubi envelopes `P` and `Q` of `C`, two morphisms `f` and `g` from `P` to `Q` are equal if and only if their underlying morphisms (`f.f` and `g.f`) are equal. In formal terms, it establishes an equivalence between the equality of morphisms and the equality of their underlying structures in the category of idempotent Karoubi envelopes.
More concisely: In category theory, two morphisms between idempotent Karoubi envelopes of a category are equal if and only if their underlying morphisms have the same underlying structure.
|
CategoryTheory.Idempotents.Karoubi.p_comp
theorem CategoryTheory.Idempotents.Karoubi.p_comp :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
(f : P.Hom Q), CategoryTheory.CategoryStruct.comp P.p f.f = f.f
This theorem, `CategoryTheory.Idempotents.Karoubi.p_comp`, states that for any category `C`, and for any two objects `P` and `Q` in the Karoubi envelope of `C` (a construction that adds new objects to the category such that every idempotent morphism becomes an isomorphism), given a morphism `f` from `P` to `Q`, the composition of the projection of `P` and the morphism `f` is equal to `f` itself. This is a property in the context of idempotent completion, highlighting the nature of the Karoubi envelope in dealing with idempotent morphisms.
More concisely: In the Karoubi envelope of a category `C`, for any object `P`, any object `Q`, and any morphism `f` from `P` to `Q` of idempotent source and target, the projection of `P` followed by `f` equals `f`.
|
CategoryTheory.Idempotents.Karoubi.hom_ext
theorem CategoryTheory.Idempotents.Karoubi.hom_ext :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
(f g : P ⟶ Q), f.f = g.f → f = g
This theorem, `CategoryTheory.Idempotents.Karoubi.hom_ext`, states that for any category `C` and any two objects `P` and `Q` in the Karoubi envelope of `C`, if two morphisms `f` and `g` from `P` to `Q` satisfy `f.f = g.f`, then `f` is equal to `g`. In other words, this theorem asserts that, in the Karoubi envelope of a category, two morphisms are equal if and only if their underlying morphisms in the original category are equal. This theorem aids in proving the equivalence between the Karoubi envelope and the category of idempotents.
More concisely: In the Karoubi envelope of a category, two morphisms between objects have the same underlying morphism in the original category if and only if they are equal.
|
CategoryTheory.Idempotents.Karoubi.decompId
theorem CategoryTheory.Idempotents.Karoubi.decompId :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Idempotents.Karoubi C),
CategoryTheory.CategoryStruct.id P = CategoryTheory.CategoryStruct.comp P.decompId_i P.decompId_p
This theorem states that for any given category `C` and any idempotent `P` in the Karoubi envelope of `C`, the identity morphism on `P` is equal to the composition of the morphisms given by `P.decompId_i` and `P.decompId_p`. In other words, this theorem is stating a property of idempotents in the Karoubi envelope of a category where the identity morphism on an idempotent is decomposable into a composition of two other morphisms.
More concisely: In the Karoubi envelope of a category `C`, the identity morphism on an idempotent `P` is equal to the composition of `P.decompId_i` and `P.decompId_p`.
|