CategoryTheory.RegularMono.w
theorem CategoryTheory.RegularMono.w :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y}
[self : CategoryTheory.RegularMono f],
CategoryTheory.CategoryStruct.comp f CategoryTheory.RegularMono.left =
CategoryTheory.CategoryStruct.comp f CategoryTheory.RegularMono.right
The theorem `CategoryTheory.RegularMono.w` states that, for any category `C`, and any morphism `f` from `X` to `Y` in `C` that is a regular monomorphism, the compositions of `f` with two other morphisms from `Y` to another object `Z` (denoted `CategoryTheory.RegularMono.left` and `CategoryTheory.RegularMono.right`) are equal. In other words, `f` equalizes these two morphisms, which means that, when followed by `f`, the two morphisms have the same effect. This is a property specific to regular monomorphisms in category theory.
More concisely: For any category `C` and regular monomorphism `f` in `C`, the morphisms `CategoryTheory.RegularMono.left` and `CategoryTheory.RegularMono.right` from `Y` to another object `Z` satisfy `f ∘ CategoryTheory.RegularMono.left = f ∘ CategoryTheory.RegularMono.right`.
|
CategoryTheory.isIso_of_regularEpi_of_mono
theorem CategoryTheory.isIso_of_regularEpi_of_mono :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.RegularEpi f] [inst_2 : CategoryTheory.Mono f], CategoryTheory.IsIso f
This theorem states that in any category `C`, for any morphism `f` from object `X` to object `Y`, if `f` is both a regular epimorphism and a monomorphism, then `f` is an isomorphism. A regular epimorphism is a morphism that is the coequalizer of some parallel pair, a monomorphism is a morphism that is left-cancellative, and an isomorphism is a morphism that has an inverse.
More concisely: In any category, if a morphism is both a regular epimorphism and a monomorphism, then it is an isomorphism.
|
CategoryTheory.isIso_of_regularMono_of_epi
theorem CategoryTheory.isIso_of_regularMono_of_epi :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.RegularMono f] [inst_2 : CategoryTheory.Epi f], CategoryTheory.IsIso f
This theorem states that in a category `C`, for any two objects `X` and `Y` and a morphism `f` from `X` to `Y`, if `f` is a regular monomorphism and also an epimorphism, then `f` is an isomorphism. In other words, a morphism that is both a regular monomorphism (a morphism that is the equalizer of some parallel pair of morphisms) and an epimorphism (a morphism that is right-cancellable) is necessarily an isomorphism (a morphism that has an inverse) in the category theory framework.
More concisely: In a category, if a morphism is both a regular monomorphism and an epimorphism, then it is an isomorphism.
|
CategoryTheory.RegularEpi.w
theorem CategoryTheory.RegularEpi.w :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y}
[self : CategoryTheory.RegularEpi f],
CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.left f =
CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.right f
This theorem states that for any category `C`, and any morphism `f` from object `X` to `Y` in `C` which is a regular epimorphism, the composition of the left morphism from the source of `f` to `X` with `f` is equal to the composition of the right morphism from the source of `f` to `X` with `f`. In other words, morphism `f` coequalizes the left and right morphisms. This theorem is a property of regular epimorphisms in category theory, where a regular epimorphism is a morphism that is the coequalizer of some parallel pair of morphisms.
More concisely: For any regular epimorphism `f` in a category `C` from object `X` to `Y`, the left and right compositions with `f` of morphisms to `X` from the source of `f` are equal.
|