CategoryTheory.Functor.essImage_eq_of_natIso
theorem CategoryTheory.Functor.essImage_eq_of_natIso :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F F' : CategoryTheory.Functor C D},
(F ≅ F') → F.essImage = F'.essImage
This theorem in category theory states that if two functors (F and F') from a category C to a category D are isomorphic (F ≅ F'), then they have the same essential images. Here, the essential image of a functor is the subcategory of the target category consisting of objects isomorphic to the image of some object in the source category. In other words, we can say that the essential images of two isomorphic functors are equal.
More concisely: If functors F and F' from category C to category D are isomorphic, then their essential images are equal.
|
CategoryTheory.Functor.essImage.ofIso
theorem CategoryTheory.Functor.essImage.ofIso :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y Y' : D},
(Y ≅ Y') → Y ∈ F.essImage → Y' ∈ F.essImage
This theorem, `CategoryTheory.Functor.essImage.ofIso`, states that being in the essential image of a functor is a property preserved under isomorphisms in category theory. Specifically, if we have any two types `C` and `D` that form categories, and a functor `F` from `C` to `D`, then for any two objects `Y` and `Y'` in `D`, if `Y` is isomorphic to `Y'` and `Y` is in the essential image of `F`, then `Y'` is also in the essential image of `F`. This is why the property of being in the essential image is described as "hygienic".
More concisely: If `F` is a functor from category `C` to category `D`, `Y` is an object in `D` that is isomorphic to an object `X` in the essential image of `F` from `C`, then `Y` is in the essential image of `F`.
|
CategoryTheory.Functor.essImage.ofNatIso
theorem CategoryTheory.Functor.essImage.ofNatIso :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F F' : CategoryTheory.Functor C D},
(F ≅ F') → ∀ {Y : D}, Y ∈ F.essImage → Y ∈ F'.essImage
This theorem states that if `Y` is in the essential image of a functor `F`, then `Y` is also in the essential image of another functor `F'` provided that `F` is naturally isomorphic to `F'`. Here, `F` and `F'` are functors from category `C` to category `D`, and the essential image of a functor is a subcategory of the codomain containing all objects isomorphic to an object in the image of the functor. The theorem is applicable in the context of category theory, a branch of mathematics that deals with abstract algebraic structures and their relationships.
More concisely: If functors F and F' are naturally isomorphic from category C to category D, then the essential image of F is equal to the essential image of F'.
|
CategoryTheory.Functor.obj_mem_essImage
theorem CategoryTheory.Functor.obj_mem_essImage :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) (Y : D), F.obj Y ∈ F.essImage
This theorem states that for any two categories `C` and `D` and a functor `F` from `D` to `C`, any object `Y` in category `D` is also in the essential image of the functor `F`. In the context of category theory, the "essential image" of a functor refers to the collection of objects in the target category that are isomorphic to the image of some object in the source category under the functor.
More concisely: For any functor F from category D to category C and any object Y in D, Y is in the essential image of F.
|