CategoryTheory.Functor.PreservesMonomorphisms.preserves
theorem CategoryTheory.Functor.PreservesMonomorphisms.preserves :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [self : F.PreservesMonomorphisms]
{X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Mono f], CategoryTheory.Mono (F.map f)
This theorem states that for any categories `C` and `D`, if a functor `F` exists from `C` to `D` that preserves monomorphisms (injective morphisms), then for any objects `X` and `Y` in `C` and any monomorphism `f` from `X` to `Y`, the image of `f` under `F` is also a monomorphism in `D`. In other words, if a functor preserves monomorphisms, then it maps monomorphisms to monomorphisms.
More concisely: If functor F : C -> D preserves monomorphisms, then for all objects X, Y in C and monomorphism f : X -> Y in C, the image F(f) is a monomorphism in D.
|
CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects
theorem CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_3 : (F.comp G).PreservesEpimorphisms]
[inst_4 : G.ReflectsEpimorphisms], F.PreservesEpimorphisms
This theorem states that for any three categories `C`, `D`, and `E`, and two functors `F : C -> D` and `G : D -> E`, if the composite functor `G ∘ F` preserves epimorphisms and `G` reflects epimorphisms, then the functor `F` also preserves epimorphisms. Here, "preserves epimorphisms" means that if a morphism in the source category is an epimorphism, its image in the target category is also an epimorphism, and "reflects epimorphisms" means that if a morphism's image in the target category is an epimorphism, then the original morphism in the source category is also an epimorphism.
More concisely: If functors `F : C -> D` and `G : D -> E` preserve and reflect epimorphisms with `G ∘ F` preserving epimorphisms, then `F` preserves epimorphisms.
|
CategoryTheory.Functor.ReflectsEpimorphisms.reflects
theorem CategoryTheory.Functor.ReflectsEpimorphisms.reflects :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [self : F.ReflectsEpimorphisms]
{X Y : C} (f : X ⟶ Y), CategoryTheory.Epi (F.map f) → CategoryTheory.Epi f
This theorem states that for any categories `C` and `D`, and any functor `F` from `C` to `D` that reflects epimorphisms, if a morphism `f` from `X` to `Y` in category `C` is mapped to an epimorphism (a morphism that's right-cancellable) in category `D` by the functor `F`, then `f` itself is an epimorphism in category `C`. In mathematical terms, if `F.map f` is an epimorphism in category `D`, then `f` is an epimorphism in category `C`.
More concisely: If functor `F` from category `C` to category `D` reflects epimorphisms, then any epimorphism `f` in `C` mapped to an epimorphism in `D` implies `f` is an epimorphism in `C`.
|
CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence
theorem CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [inst_2 : F.IsEquivalence]
[inst : CategoryTheory.SplitEpiCategory C], CategoryTheory.SplitEpiCategory D
This theorem states that if there is an equivalence of categories `F : C ⥤ D` and `C` is a split epimorphism category (a category in which every epimorphism has a section or right inverse), then `D` is also a split epimorphism category. In other words, the property of being a split epimorphism category is preserved under an equivalence of categories.
More concisely: If `F : C ⥤ D` is an equivalence of categories and `C` is a split epimorphism category, then `D` is also a split epimorphism category.
|
CategoryTheory.Functor.ReflectsMonomorphisms.reflects
theorem CategoryTheory.Functor.ReflectsMonomorphisms.reflects :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [self : F.ReflectsMonomorphisms]
{X Y : C} (f : X ⟶ Y), CategoryTheory.Mono (F.map f) → CategoryTheory.Mono f
This theorem states that a functor reflects monomorphisms. In the context of category theory, this means that if we have a functor `F` from category `C` to category `D` that reflects monomorphisms, then for any two objects `X` and `Y` in `C` and a morphism `f` from `X` to `Y`, if the functor `F` maps `f` to a monomorphism in `D`, then `f` is a monomorphism in `C`. Essentially, the functor `F` is able to 'detect' or 'reflect' the property of being a monomorphism.
More concisely: If `F` is a functor from category `C` to category `D` that reflects monomorphisms, then for any pair of objects `X` and `Y` in `C` and a morphism `f` from `X` to `Y` in `C`, `f` is a monomorphism in `C` if and only if `F(f)` is a monomorphism in `D`.
|
CategoryTheory.Functor.mono_of_mono_map
theorem CategoryTheory.Functor.mono_of_mono_map :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [inst_2 : F.ReflectsMonomorphisms]
{X Y : C} {f : X ⟶ Y}, CategoryTheory.Mono (F.map f) → CategoryTheory.Mono f
This theorem states that in the context of category theory, given two categories `C` and `D`, and a functor `F` from `C` to `D` that reflects monomorphisms, if the map of a morphism `f` from `X` to `Y` in `C` under the functor `F` is a monomorphism in `D`, then `f` itself is a monomorphism in `C`. In other words, if the functor `F` "sees" a morphism as a monomorphism after mapping, then the original morphism is indeed a monomorphism.
More concisely: Given functors F from category C to D and reflecting monomorphisms, if for any morphism f in C, F(f) is a monomorphism in D, then f is a monomorphism in C.
|
CategoryTheory.Functor.PreservesEpimorphisms.preserves
theorem CategoryTheory.Functor.PreservesEpimorphisms.preserves :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [self : F.PreservesEpimorphisms]
{X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Epi f], CategoryTheory.Epi (F.map f)
The theorem states that a functor in category theory preserves epimorphisms. Given a category `C`, a category `D`, a functor `F` from `C` to `D` that preserves epimorphisms, and an epimorphism `f` from an object `X` to an object `Y` in `C`, the functor `F` will map `f` to an epimorphism from `F(X)` to `F(Y)` in `D`. In other words, if `f` is an epimorphism in `C`, then `F.map f` is an epimorphism in `D`.
More concisely: Given a functor F from category C to category D, if every epimorphism in C is mapped to an epimorphism in D by F, then F preserves epimorphisms.
|
CategoryTheory.Functor.epi_of_epi_map
theorem CategoryTheory.Functor.epi_of_epi_map :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [inst_2 : F.ReflectsEpimorphisms]
{X Y : C} {f : X ⟶ Y}, CategoryTheory.Epi (F.map f) → CategoryTheory.Epi f
This theorem from category theory states that for any two objects `X` and `Y` in a category `C`, and a functor `F` from `C` to another category `D` that reflects epimorphisms, if the image of a morphism `f : X ⟶ Y` under `F` is an epimorphism in `D`, then `f` is an epimorphism in `C`. An epimorphism is a morphism whose cancellation property holds for all pairs of morphisms. This theorem, in essence, asserts that the property of being an epimorphism is preserved under the functor `F`.
More concisely: If `F` is a functor from category `C` to category `D` that reflects epimorphisms, then for any objects `X` and `Y` in `C` and morphism `f : X ⟶ Y` in `C`, if `F(f)` is an epimorphism in `D`, then `f` is an epimorphism in `C`.
|