CategoryTheory.SplitMono.id
theorem CategoryTheory.SplitMono.id :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y}
(self : CategoryTheory.SplitMono f),
CategoryTheory.CategoryStruct.comp f self.retraction = CategoryTheory.CategoryStruct.id X
This theorem states that for any category `C` with objects `X` and `Y` and a morphism `f` from `X` to `Y` that is a split monomorphism (i.e., has a retraction), the composition of `f` with its retraction is the identity morphism on `X`. In terms of category theory, this theorem is saying that if there exists a morphism that "undoes" the action of `f`, then applying `f` and then its retraction is equivalent to doing nothing at all (the identity operation).
More concisely: In any category, if a morphism has a retraction, then the composition of the morphism with its retraction is the identity morphism on the domain of the morphism.
|
CategoryTheory.isSplitEpi_of_epi
theorem CategoryTheory.isSplitEpi_of_epi :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.SplitEpiCategory C] {X Y : C}
(f : X ⟶ Y) [inst_2 : CategoryTheory.Epi f], CategoryTheory.IsSplitEpi f
This theorem states that in a category where every epimorphism is split, any specific epimorphism also splits. Here, the category has objects of type C and morphisms (also known as arrows) from object X to object Y. The morphism f from X to Y is an epimorphism, which in categorical terms, means it has certain "surjectivity" properties. The theorem asserts that in such a category, if every epimorphism can be split (meaning there exists a morphism in the opposite direction that undoes the effect of the original morphism), then any given epimorphism can also be split. This is not set as an instance because it would lead to an instance loop, or circular reasoning in the instance inference mechanism of Lean.
More concisely: In a category where every epimorphism is split, any given epimorphism splits.
|
CategoryTheory.IsSplitEpi.id
theorem CategoryTheory.IsSplitEpi.id :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
[hf : CategoryTheory.IsSplitEpi f],
CategoryTheory.CategoryStruct.comp (CategoryTheory.section_ f) f = CategoryTheory.CategoryStruct.id Y
This theorem states that, for any category `C`, and any objects `X` and `Y` in `C`, given a morphism `f` from `X` to `Y` that is a split epimorphism, the composition of the section of `f` (denoted by `CategoryTheory.section_ f`) with `f` itself is the identity morphism on `Y`. In the language of category theory, this means that if `f` is a split epimorphism, then there exists a morphism from `Y` to `X` that "undoes" the effect of `f` when composed with it, leaving the identity on `Y`. This is a fundamental property in category theory relating to the concept of splitting idempotents.
More concisely: For any object `X`, `Y` in a category `C` and a split epimorphism `f` from `X` to `Y`, `CategoryTheory.section_ f ∘ f = id_Y`.
|
CategoryTheory.IsSplitEpi.mk'
theorem CategoryTheory.IsSplitEpi.mk' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y},
CategoryTheory.SplitEpi f → CategoryTheory.IsSplitEpi f
This theorem is a constructor for the `IsSplitEpi` property of a morphism `f` in category theory, given that `f` is a `SplitEpi` (split epimorphism). Specifically, for any category `C`, and objects `X` and `Y` in `C`, if there is a morphism `f` from `X` to `Y` that is a split epimorphism, then `f` is an `IsSplitEpi`, i.e., has the "is split epimorphism" property.
More concisely: In any category, a split epimorphism is an object with the "is split epimorphism" property.
|
CategoryTheory.isIso_of_mono_of_isSplitEpi
theorem CategoryTheory.isIso_of_mono_of_isSplitEpi :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f]
[inst_2 : CategoryTheory.IsSplitEpi f], CategoryTheory.IsIso f
The theorem `CategoryTheory.isIso_of_mono_of_isSplitEpi` states that, for any category `C` and objects `X` and `Y` in this category, if `f` is a morphism from `X` to `Y` that is both a monomorphism (`CategoryTheory.Mono f`) and a split epimorphism (`CategoryTheory.IsSplitEpi f`), then `f` is an isomorphism (`CategoryTheory.IsIso f`). Essentially, it's saying that a morphism in a category is invertible if it is both a monomorphism and a split epimorphism.
More concisely: In any category, a morphism that is both a monomorphism and a split epimorphism is an isomorphism.
|
CategoryTheory.IsIso.of_mono_retraction
theorem CategoryTheory.IsIso.of_mono_retraction :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
[hf : CategoryTheory.IsSplitMono f] [hf' : CategoryTheory.Mono (CategoryTheory.retraction f)],
CategoryTheory.IsIso f
The theorem `CategoryTheory.IsIso.of_mono_retraction` states that in any category `C`, for all objects `X` and `Y` and morphism `f` from `X` to `Y`, if `f` is a split monomorphism and the retraction of `f` is also a monomorphism, then `f` is an isomorphism. In other words, a split monomorphism with a monomorphic retraction is necessarily an isomorphism in the category `C`.
More concisely: If in a category `C`, a morphism `f` from object `X` to object `Y` is both a split monomorphism and has a monomorphic retraction, then `f` is an isomorphism.
|
CategoryTheory.IsIso.of_epi_section
theorem CategoryTheory.IsIso.of_epi_section :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsSplitEpi f]
[hf' : CategoryTheory.Epi (CategoryTheory.section_ f)], CategoryTheory.IsIso f
This theorem states that in any category 'C', for any two objects 'X' and 'Y' in 'C', if a morphism 'f' from 'X' to 'Y' is split epimorphism and the section of this split epimorphism is an epimorphism, then 'f' is an isomorphism. In category theory, a split epimorphism or split epi is a type of morphism with a specified right inverse, and an isomorphism is a morphism that has an inverse morphism. Hence, this theorem connects the concepts of split epimorphisms, epimorphisms, and isomorphisms.
More concisely: In any category, if a morphism is both a split epimorphism and its section is an epimorphism, then it is an isomorphism.
|
CategoryTheory.IsSplitMono.id
theorem CategoryTheory.IsSplitMono.id :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
[hf : CategoryTheory.IsSplitMono f],
CategoryTheory.CategoryStruct.comp f (CategoryTheory.retraction f) = CategoryTheory.CategoryStruct.id X
This theorem states that in any category `C`, for any two objects `X` and `Y` and any morphism `f` from `X` to `Y` that is a split monomorphism, the composition of `f` and its retraction (a morphism from `Y` back to `X`) is equal to the identity morphism on `X`. This result is a key property of split monomorphisms in category theory, reflecting the idea that a split monomorphism can be "undone" by its retraction.
More concisely: In any category, for any split monomorphism `f`: `f ∘ r = id_X`, where `r` is `f`'s retraction and `id_X` is the identity morphism on `X`.
|
CategoryTheory.IsSplitMono.mk'
theorem CategoryTheory.IsSplitMono.mk' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y},
CategoryTheory.SplitMono f → CategoryTheory.IsSplitMono f
This theorem provides a constructor for `IsSplitMono f` in the context of Category Theory. It takes as an argument `SplitMono f`. Specifically, for any category `C` with objects of type `X` and `Y` and a morphism `f : X ⟶ Y`, if `f` is a split monomorphism (indicated by `SplitMono f`), then `f` is also an isomorphism in the category `C` where the morphism splits or, in other words, `f` is a split monomorphism (`IsSplitMono f`).
More concisely: If `f : X ⟶ Y` is a split monomorphism in a category `C`, then `f` is an isomorphism in `C`.
|
CategoryTheory.SplitEpiCategory.isSplitEpi_of_epi
theorem CategoryTheory.SplitEpiCategory.isSplitEpi_of_epi :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [self : CategoryTheory.SplitEpiCategory C] {X Y : C}
(f : X ⟶ Y) [inst_1 : CategoryTheory.Epi f], CategoryTheory.IsSplitEpi f
This theorem states that in any split epi-category `C`, for any objects `X` and `Y` in `C`, and any morphism `f` from `X` to `Y` that is epi (i.e., an epimorphism, which is a morphism where the post-composition of `f` with any other morphism is injective), then `f` is a split epi. In other words, there exists a morphism `g` such that the composition of `f` and `g` is the identity morphism on `Y`. This is a concept in category theory, a branch of mathematics that deals with abstract algebraic structures.
More concisely: In a split epi-category, every epimorphism is split.
|
CategoryTheory.IsIso.of_mono_retraction'
theorem CategoryTheory.IsIso.of_mono_retraction' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (hf : CategoryTheory.SplitMono f)
[inst_1 : CategoryTheory.Mono hf.retraction], CategoryTheory.IsIso f
The theorem states that in any category `C`, for every morphism `f` from an object `X` to another object `Y` that is a split monomorphism, if its retraction is also a monomorphism, then `f` is an isomorphism. In the language of category theory, a split monomorphism is a morphism that has a retraction, meaning there is another morphism going in the opposite direction such that their composition is the identity. This theorem asserts that if such a morphism also has the property that its retraction is monic (i.e., left-cancellable), then it's actually an isomorphism, having a two-sided inverse.
More concisely: In any category, if a split monomorphism with monic retraction is morphism, then it is an isomorphism.
|
CategoryTheory.isSplitMono_of_mono
theorem CategoryTheory.isSplitMono_of_mono :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.SplitMonoCategory C] {X Y : C}
(f : X ⟶ Y) [inst_2 : CategoryTheory.Mono f], CategoryTheory.IsSplitMono f
This theorem states that in a category theory context, for any category `C` which has the property that every monomorphism is split (indicated by `CategoryTheory.SplitMonoCategory C`), any monomorphism `f` from object `X` to object `Y` in `C` is also a split monomorphism (indicated by `CategoryTheory.IsSplitMono f`). The theorem also notes that it's not an instance because creating it as such would result in an instance loop.
More concisely: In a split mono category `C`, every monomorphism `f : X → Y` is a split monomorphism.
|
CategoryTheory.isIso_of_epi_of_isSplitMono
theorem CategoryTheory.isIso_of_epi_of_isSplitMono :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.IsSplitMono f] [inst_2 : CategoryTheory.Epi f], CategoryTheory.IsIso f
This theorem states that in any category 'C', for any two objects 'X' and 'Y' in 'C', if there exists a morphism 'f' from 'X' to 'Y' which is both a split monomorphism (i.e., there exists a retraction) and an epimorphism (i.e., it is surjective), then 'f' is an isomorphism (i.e., it has an inverse).
More concisely: In any category, if a morphism between two objects is both a split monomorphism and an epimorphism, then it is an isomorphism.
|
CategoryTheory.SplitMonoCategory.isSplitMono_of_mono
theorem CategoryTheory.SplitMonoCategory.isSplitMono_of_mono :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [self : CategoryTheory.SplitMonoCategory C] {X Y : C}
(f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f], CategoryTheory.IsSplitMono f
This theorem states that in any split mono category `C`, given two objects `X` and `Y` and a morphism `f` from `X` to `Y` which is mono (i.e., has the property that for any two morphisms `g, h` from any other object `Z` to `X`, if `f ∘ g = f ∘ h` then `g = h`), then `f` is a split mono. In category theory, a morphism is a split mono if it has a right inverse, meaning there exists another morphism going the other way which composes with `f` to give the identity morphism.
More concisely: In a split mono category, a monomorphism is a split monomorphism. (A monomorphism is a morphism with the property that if two morphisms have the same composite with it, then they are equal, and a split monomorphism is a monomorphism with a right inverse.)
|
CategoryTheory.SplitEpi.id
theorem CategoryTheory.SplitEpi.id :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y}
(self : CategoryTheory.SplitEpi f),
CategoryTheory.CategoryStruct.comp self.section_ f = CategoryTheory.CategoryStruct.id Y
This theorem states that, for any category `C` and objects `X` and `Y` in `C`, if a morphism `f` from `X` to `Y` is a split epimorphism, then the composition of the section of `f` (denoted as `self.section_`) with `f` is the identity morphism on `Y`. In other words, for a split epimorphism `f`, we have `self.section_ ≫ f = id_Y`. This articulates one of the defining properties of split epimorphisms in category theory, that there exists a morphism which when composed with `f` results in the identity.
More concisely: For any category `C` and morphism `f: X → Y` that is a split epimorphism, the section of `f` and `f` compose to yield the identity morphism on `Y`, that is, `self.section_ ∘ f = id_Y`.
|
CategoryTheory.IsIso.of_epi_section'
theorem CategoryTheory.IsIso.of_epi_section' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (hf : CategoryTheory.SplitEpi f)
[inst_1 : CategoryTheory.Epi hf.section_], CategoryTheory.IsIso f
This theorem states that in any category `C`, for any two objects `X` and `Y` and any morphism `f` from `X` to `Y`, if `f` is a split epimorphism (a morphism with a right inverse) and its section (the right inverse) is an epimorphism, then `f` is an isomorphism. In simple terms, if a morphism has a right inverse that is surjective (epi), then the original morphism is a bijective map (iso).
More concisely: In any category, if a morphism with a right inverse that is an epimorphism is a split epimorphism, then it is an isomorphism.
|
CategoryTheory.IsSplitEpi.id_assoc
theorem CategoryTheory.IsSplitEpi.id_assoc :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsSplitEpi f]
{Z : C} (h : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.section_ f) (CategoryTheory.CategoryStruct.comp f h) = h
The theorem `CategoryTheory.IsSplitEpi.id_assoc` asserts that for any category `C`, any objects `X`, `Y`, and `Z` in `C`, any morphism `f` from `X` to `Y` that is a split epimorphism, and any morphism `h` from `Y` to `Z`, the composition of the section of `f` (a morphism from `Y` to `X`) with the composition of `f` and `h` (a morphism from `X` to `Z`) is equal to `h`. In other words, if `f` is a split epimorphism, then pre-composing `h` with `f` and its section is an identity operation on `h`.
More concisely: For any category C, given objects X, Y, and Z, a split epimorphism f : X -> Y in C, and a morphism h : Y -> Z, the section of f and the composition of f and h are equal: section(f) . (f . h) = h.
|
CategoryTheory.IsSplitMono.exists_splitMono
theorem CategoryTheory.IsSplitMono.exists_splitMono :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y}
[self : CategoryTheory.IsSplitMono f], Nonempty (CategoryTheory.SplitMono f)
This theorem states that for any category `C` and any two objects `X` and `Y` in `C`, if `f` is a morphism from `X` to `Y` and `f` is a split monomorphism, then there exists a split monomorphism for `f`. In other words, if `f` is a morphism from `X` to `Y` that has a right inverse, then we can find a specific morphism that splits `f`, i.e., a morphism that when composed with `f`, gives the identity morphism.
More concisely: If `f : X ➝ Y` is a split monomorphism in a category `C`, then there exists a morphism `s : Y ➝ X` making the composition `s ∘ f` equal to the identity morphism on `X`.
|
CategoryTheory.IsSplitMono.id_assoc
theorem CategoryTheory.IsSplitMono.id_assoc :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
[hf : CategoryTheory.IsSplitMono f] {Z : C} (h : X ⟶ Z),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) h) = h
This theorem states that for any category `C`, any objects `X`, `Y`, `Z` in `C`, and any morphism `f` from `X` to `Y` that is a split monomorphism, the composition of `f` with the composition of the retraction of `f` and any morphism `h` from `X` to `Z` is equal to `h`. In simple terms, it means that if you first apply a morphism and then its retraction, you can "cancel" them out in the composition, akin to the inverse function principle in mathematics. This property is a fundamental aspect of the category theory, a branch of mathematics which studies abstract structure within a mathematical context.
More concisely: For any category C, if f : X -> Y is a split monomorphism in C, then for any h : X -> Z, we have f o (h o rf) = h, where rf is the retraction of f.
|
CategoryTheory.IsSplitEpi.exists_splitEpi
theorem CategoryTheory.IsSplitEpi.exists_splitEpi :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y}
[self : CategoryTheory.IsSplitEpi f], Nonempty (CategoryTheory.SplitEpi f)
This theorem states that for any category `C` with objects `X` and `Y`, and morphism `f` from `X` to `Y`, if `f` is a split epimorphism (a morphism where there exists a morphism g from Y to X such that the composition of f and g is the identity morphism on Y), then there exists a split epimorphism for `f`. In terms of category theory, this means that if `f` is a morphism that "splits" or separates the objects in a certain way, then there's another morphism that can "split" the objects in the same way.
More concisely: Given any morphism `f` in a category `C` that is a split epimorphism, there exists a morphism `g` making `f` and `g` a pair of mutually inverse split epimorphisms.
|