CategoryTheory.preserves_epi_of_preservesColimit
theorem CategoryTheory.preserves_epi_of_preservesColimit :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y)
[inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f f) F]
[inst_3 : CategoryTheory.Epi f], CategoryTheory.Epi (F.map f)
The theorem `CategoryTheory.preserves_epi_of_preservesColimit` states that, given a functor `F` from a category `C` to a category `D`, if `F` preserves the colimit of the diagram formed by a morphism `f` from object `X` to object `Y` in `C` (in other words, `F` preserves the pushouts), then `F` also preserves epimorphisms. This means that if `f` is an epimorphism (surjective morphism) in `C`, then its image under `F`, namely `F.map f`, is also an epimorphism in `D`.
More concisely: If a functor F from category C to category D preserves colimits, then it preserves epimorphisms, that is, for any epimorphism f in C, the image F.map f is an epimorphism in D.
|
CategoryTheory.preserves_mono_of_preservesLimit
theorem CategoryTheory.preserves_mono_of_preservesLimit :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y)
[inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f f) F]
[inst_3 : CategoryTheory.Mono f], CategoryTheory.Mono (F.map f)
The theorem `CategoryTheory.preserves_mono_of_preservesLimit` states that for any categories `C` and `D`, given a functor `F` from `C` to `D`, if `F` preserves the limit of the cospan of a morphism `f` from `X` to `Y` in `C` (i.e., `F` preserves pullbacks), and if `f` is a monomorphism in `C`, then the image of `f` under `F` is a monomorphism in `D`. In other words, if a functor preserves pullbacks, it also preserves monomorphisms.
More concisely: If functor $F : C \to D$ preserves limits and $f : X \to Y$ is a monomorphism in $C$, then $F(f) : F(X) \to F(Y)$ is a monomorphism in $D$.
|
CategoryTheory.reflects_mono_of_reflectsLimit
theorem CategoryTheory.reflects_mono_of_reflectsLimit :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y)
[inst_2 : CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan f f) F]
[inst_3 : CategoryTheory.Mono (F.map f)], CategoryTheory.Mono f
This theorem states that if a functor `F` from category `C` to category `D` reflects pullbacks, then it also reflects monomorphisms. More formally, given categories `C` and `D`, a functor `F` from `C` to `D`, and a morphism `f` from `X` to `Y` in `C`, if `F` reflects the limit of the cospan of `f` and `f` and the image of `f` under `F` is a monomorphism, then `f` is a monomorphism. A morphism is a monomorphism if it is left-cancellable, that is, for any two morphisms `g` and `h`, if `f` composed with `g` is equal to `f` composed with `h`, then `g` is equal to `h`. A functor reflects limits (in this case, pullbacks) if whenever the image of a diagram under the functor has a limit in `D`, then the diagram has a limit in `C` which is preserved by the functor.
More concisely: If a functor reflecting pullbacks maps monomorphisms in the domain category to monomorphisms in the target category.
|
CategoryTheory.reflects_epi_of_reflectsColimit
theorem CategoryTheory.reflects_epi_of_reflectsColimit :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y)
[inst_2 : CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f f) F]
[inst_3 : CategoryTheory.Epi (F.map f)], CategoryTheory.Epi f
The theorem `CategoryTheory.reflects_epi_of_reflectsColimit` states that if a functor `F` reflects pushouts in category theory, then it also reflects epimorphisms. More specifically, given any categories `C` and `D`, and a functor `F` from `C` to `D`, if `F` has the property that it reflects colimits for the span of a morphism `f` from objects `X` to `Y` in `C`, and if the image of `f` under `F` is an epimorphism in `D`, then `f` is an epimorphism in `C`. In simpler terms, this theorem connects the reflection of pushouts and the reflection of epimorphisms in the context of category theory, saying that if a functor reflects one, it must reflect the other.
More concisely: If a functor reflects colimits for a morphism and preserves its image as an epimorphism, then the morphism is an epimorphism in the source category.
|