CategoryTheory.IsCoreflexivePair.swap
theorem CategoryTheory.IsCoreflexivePair.swap :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B}
[inst_1 : CategoryTheory.IsCoreflexivePair f g], CategoryTheory.IsCoreflexivePair g f
This theorem states that for any category `C` and objects `A` and `B` in this category, if the pair of morphisms `(f, g)` from `A` to `B` is coreflexive (meaning that there exists an arrow `e` such that `e ∘ f = e ∘ g` and `f ∘ e = g ∘ e = 𝟙`), then the pair `(g, f)` is also coreflexive. The order of the pair of morphisms doesn't matter for it to be considered as coreflexive.
More concisely: If morphisms `f` and `g` from object `A` to object `B` in a category `C` form a coreflexive pair, then so does the pair `(g, f)`.
|
CategoryTheory.IsCoreflexivePair.common_retraction
theorem CategoryTheory.IsCoreflexivePair.common_retraction :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B)
[inst_1 : CategoryTheory.IsCoreflexivePair f g],
∃ s,
CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.id A ∧
CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.id A
This theorem, `CategoryTheory.IsCoreflexivePair.common_retraction`, states that for any category `C` of a certain type `u` and for any two objects `A` and `B` in `C`, given two morphisms `f` and `g` from `A` to `B` such that `f` and `g` form a coreflexive pair, there exists a morphism `s` such that the composition of `f` with `s` equals the identity on `A` and, similarly, the composition of `g` with `s` equals the identity on `A`. In other words, `s` is a common retraction of `f` and `g` in the category `C`.
More concisely: For any category `C` and objects `A`, `B` in `C`, if morphisms `f` and `g` from `A` to `B` form a coreflexive pair, then there exists a morphism `s` making both `fs = id_A` and `gs = id_A` in `C`.
|
CategoryTheory.IsReflexivePair.common_section
theorem CategoryTheory.IsReflexivePair.common_section :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B)
[inst_1 : CategoryTheory.IsReflexivePair f g],
∃ s,
CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B ∧
CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B
The theorem `CategoryTheory.IsReflexivePair.common_section` states that for any Category `C` and objects `A` and `B` in `C`, given two morphisms `f` and `g` from `A` to `B` that form a reflexive pair (`CategoryTheory.IsReflexivePair f g`), there exists a common section `s` such that composing `s` with `f` or `g` yields the identity morphism on `B`. In other words, both `f` and `g` can be "undone" by `s`, leading back to the original object `B`. This theorem is part of the category theory in mathematics and serves to assert the existence of such a section `s` under the given conditions.
More concisely: For any category C and objects A, B with reflexive pair morphisms f and g from A to B, there exists a common section s such that fs = g andgs = f.
|
CategoryTheory.IsReflexivePair.mk'
theorem CategoryTheory.IsReflexivePair.mk' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B} (s : B ⟶ A),
CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B →
CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B →
CategoryTheory.IsReflexivePair f g
This theorem states that for any Category 'C', and any objects 'A' and 'B' in 'C', if there exist morphisms 'f' and 'g' from 'A' to 'B' and a morphism 's' from 'B' to 'A', such that the composition of 's' and 'f' equals the identity of 'B', and the composition of 's' and 'g' also equals the identity of 'B', then 'f' and 'g' form a reflexive pair in category theory. Here, the reflexivity refers to the existence of a morphism from 'B' to 'A' that, when composed with 'f' or 'g', yields the identity on 'B'.
More concisely: In any category 'C', if there exist morphisms 'f' and 'g' from object 'A' to 'B' and morphism 's' from 'B' to 'A' such that the compositions 's * f' and 's * g' equal the identity of 'B', then 'f' and 'g' form a reflexive pair.
|
CategoryTheory.IsReflexivePair.swap
theorem CategoryTheory.IsReflexivePair.swap :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B}
[inst_1 : CategoryTheory.IsReflexivePair f g], CategoryTheory.IsReflexivePair g f
This theorem states that in the context of category theory, if we have a pair of morphisms `f` and `g` from object `A` to object `B` in a category `C` that forms a reflexive pair (meaning each morphism has a right inverse), then swapping the order of the morphisms also results in a reflexive pair, i.e., `g` and `f` together form a reflexive pair as well.
More concisely: If morphisms `f` and `g` from object `A` to object `B` in a category `C` have right inverses `r_f` and `r_g` respectively, then the pair `(g, f)` forms a reflexive pair in `C`, i.e., `g ∘ r_f = r_g ∘ f`.
|
CategoryTheory.IsKernelPair.isReflexivePair
theorem CategoryTheory.IsKernelPair.isReflexivePair :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B R : C} {f g : R ⟶ A} {q : A ⟶ B},
CategoryTheory.IsKernelPair q f g → CategoryTheory.IsReflexivePair f g
This theorem states that if `(f, g)` forms a kernel pair for some morphism `q` in a category `C`, then `(f, g)` is a reflexive pair. The kernel pair condition means that `f` composed with `q` equals `g` composed with `q`, and the square from `R` to `A` to `B` (with both `f` and `g` from `R` to `A` and `q` from `A` to `B`) is a pullback square. A reflexive pair condition means that there exist some morphism `i` such that both `f` composed with `i` and `g` composed with `i` are identity morphisms.
More concisely: If `(f, g)` forms a kernel pair in a category `C` for some morphism `q`, then there exists an identity morphism `i` such that both `f` and `g` factor through `i`, i.e., `fi = id_R` and `gi = id_R`.
|