CategoryTheory.Functor.map_injective
theorem CategoryTheory.Functor.map_injective :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {X Y : C} (F : CategoryTheory.Functor C D) [inst_2 : F.Faithful],
Function.Injective F.map
The theorem `CategoryTheory.Functor.map_injective` states that for any types `C` and `D` with `C` being of the category instance and `D` being of another category instance, and any two objects `X` and `Y` from `C` and a functor `F` from `C` to `D` that is faithful, the `map` function of the functor `F` is injective. In other words, if two objects of `C` are mapped to the same object in `D` by the functor `F`, then these two objects must be the same in `C`. This is a property of faithful functors in category theory.
More concisely: Given faithful functors F from category C to category D, if F(X) = F(Y) for objects X and Y in C, then X = Y in C.
|
CategoryTheory.Faithful.of_comp_iso
theorem CategoryTheory.Faithful.of_comp_iso :
∀ {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} {H : CategoryTheory.Functor C E}
[inst_3 : H.Faithful], (F.comp G ≅ H) → F.Faithful
This theorem, `CategoryTheory.Faithful.of_comp_iso`, states that given categories `C`, `D` and `E`, with `C` and `D` being functors `F` and `G` respectively, and another functor `H` from `C` to `E`, if `H` is a faithful functor (i.e., a functor that is injective on hom-sets) and the composition of `F` and `G` is isomorphic to `H`, then `F` is also a faithful functor. This theorem explores the property of faithfulness in the context of functor composition and isomorphism in Category Theory.
More concisely: If functors `F: C -> E` and `G: D -> E` are such that `F` is faithful, `G` is a functor, `H: C -> E` is isomorphic to the composition `F ∘ G`, and `H` is faithful, then `F` is faithful.
|
CategoryTheory.Faithful.of_comp_eq
theorem CategoryTheory.Faithful.of_comp_eq :
∀ {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} {H : CategoryTheory.Functor C E}
[ℋ : H.Faithful], F.comp G = H → F.Faithful
This theorem states that in the context of category theory, given categories C, D, and E, and functors F: C → D, G: D → E, and H: C → E, if H is a faithful functor (meaning it injects morphisms) and the composition of F and G equals H, then F is also a faithful functor.
More concisely: If functors F: C → D, G: D → E, and H: C → E are such that H is faithful, and F = G ∘ H, then F is faithful.
|
CategoryTheory.isIso_of_fully_faithful
theorem CategoryTheory.isIso_of_fully_faithful :
∀ {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.Full]
[inst_3 : F.Faithful] {X Y : C} (f : X ⟶ Y) [inst_4 : CategoryTheory.IsIso (F.map f)], CategoryTheory.IsIso f
This theorem states that if a morphism's image under a fully faithful functor is an isomorphism in category theory, then the original morphism is also an isomorphism. In category theory, a functor is fully faithful if its function on morphisms is bijective. So, this theorem essentially says that under these conditions, the property of being an isomorphism is preserved through the functor.
More concisely: If a functor that preserves isomorphisms and has bijective morphism maps maps a morphism to an isomorphism, then the original morphism is an isomorphism.
|
CategoryTheory.Functor.map_surjective
theorem CategoryTheory.Functor.map_surjective :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {X Y : C} (F : CategoryTheory.Functor C D) [inst_2 : F.Full],
Function.Surjective F.map
The theorem `CategoryTheory.Functor.map_surjective` states that for any two objects `X` and `Y` of category `C`, and for any functor `F` from `C` to another category `D`, if the functor `F` is full (i.e., for any morphism in `D` between the images of `X` and `Y`, there exists a morphism in `C` between `X` and `Y` that maps to it), then the `map` function of the functor `F` is surjective. In other words, for every morphism in `D` between images of objects in `C`, there exists a morphism in `C` that maps to it under the functor `F`.
More concisely: If a functor between categories is full, then its map function is surjective on morphisms.
|
CategoryTheory.Faithful.of_comp
theorem CategoryTheory.Faithful.of_comp :
∀ {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).Faithful], F.Faithful
The theorem `CategoryTheory.Faithful.of_comp` states that in the context of category theory, given any three categories `C`, `D`, and `E`, and two functors `F` from `C` to `D` and `G` from `D` to `E`, if the composition of the functors `F` and `G` is faithful (which means that it reflects monomorphisms), then the functor `F` is also faithful.
More concisely: If functors `F: C -> D` and `G: D -> E` have faithful composition `F ∘ G`, then `F` is faithful.
|
CategoryTheory.Iso.faithful_of_comp
theorem CategoryTheory.Iso.faithful_of_comp :
∀ {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} {H : CategoryTheory.Functor C E}
[inst_3 : H.Faithful], (F.comp G ≅ H) → F.Faithful
This theorem, named `CategoryTheory.Iso.faithful_of_comp`, states that in the context of category theory, if we have three categories `C`, `D`, and `E`, along with three functors `F: C -> D`, `G: D -> E`, and `H: C -> E`, where `H` is faithful (i.e., injective on Hom-sets), then if the composition of `F` and `G` is naturally isomorphic to `H`, it follows that `F` is also faithful.
More concisely: If `F: C -> D`, `G: D -> E`, and `H: C -> E` are functors with `H` faithful, and `F ≅ G∘H` as natural transformations, then `F` is faithful.
|
CategoryTheory.preimage_map
theorem CategoryTheory.preimage_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.Full]
[inst_3 : F.Faithful] {X Y : C} (f : X ⟶ Y), F.preimage (F.map f) = f
This theorem states that for any two objects `X` and `Y` in a category `C`, and a functor `F` from `C` to another category `D` that is both full and faithful, the preimage under `F` of the morphism in `D` obtained by applying `F` to a morphism `f` from `X` to `Y` in `C`, is equal to `f` itself. Specifically, this theorem is asserting the property of functors that are both full (every morphism in `D` can be traced back to a morphism in `C`) and faithful (distinct morphisms in `C` are mapped to distinct morphisms in `D`). In simpler terms, if you have a morphism in `C`, map it to `D` using `F`, and then take the preimage under `F`, you'll end up back where you started.
More concisely: For any functor F from category C to D that is both full and faithful, the preimage under F of a morphism in D obtained from a morphism f in C is equal to f itself.
|
Eq.faithful_of_comp
theorem Eq.faithful_of_comp :
∀ {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} {H : CategoryTheory.Functor C E}
[ℋ : H.Faithful], F.comp G = H → F.Faithful
This theorem, `faithful_of_comp`, states that for three categories `C`, `D`, and `E`, and functors `F : C → D`, `G : D → E`, and `H : C → E`, if `H` is a faithful functor (i.e., it fully reflects the morphism structure of the category it maps from) and the composition of `F` and `G` equals `H`, then `F` is also a faithful functor. Basically, if a composition of two functors results in a faithful functor, then the first functor in the composition sequence is also faithful.
More concisely: If `F : C -> D`, `G : D -> E`, and `H : C -> E` are functors with `H` faithful and `F = G . H`, then `F` is faithful.
|
CategoryTheory.Functor.image_preimage
theorem CategoryTheory.Functor.image_preimage :
∀ {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.Full] {X Y : C}
(f : F.obj X ⟶ F.obj Y), F.map (F.preimage f) = f
This theorem states that for any two objects `X` and `Y` in a category `C`, and a functor `F` from `C` to another category `D`, if there exists a morphism `f` from `F.obj X` to `F.obj Y` in `D`, then the mapping of the preimage of `f` under `F` is equal to `f` itself. Here, `F` is a fully faithful functor, meaning it fully and faithfully preserves the morphisms of the category. The theorem verifies this property by showing the preservation of morphism `f` through its preimage and mapping.
More concisely: For any fully faithful functor F from category C to D and any morphism f in D from F(X) to F(Y) in D, the preimage of f under F equals f itself.
|