CategoryTheory.mem_essImage_of_unit_isIso
theorem CategoryTheory.mem_essImage_of_unit_isIso :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C}
[inst_2 : CategoryTheory.IsRightAdjoint i] (A : C)
[inst_3 : CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app A)], A ∈ i.essImage
This theorem states that for any categories `C` and `D` and a functor `i` from `D` to `C` that has a right adjoint, if the unit of the adjunction associated with the functor `i` at a particular object `A` in `C` is an isomorphism, then `A` is in the essential image of the functor `i`. In simple terms, if the transformation on `A` induced by the functor `i`'s adjunction creates an isomorphism, `A` is essentially 'reachable' by applying the functor `i` to objects in `D`.
More concisely: If functor `i` from category `D` to category `C` has a right adjoint and the unit of the adjunction at object `A` in `C` is an isomorphism, then `A` is in the image of `i` under the essential embedding.
|
CategoryTheory.mem_essImage_of_unit_isSplitMono
theorem CategoryTheory.mem_essImage_of_unit_isSplitMono :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C}
[inst_2 : CategoryTheory.Reflective i] {A : C}
[inst_3 : CategoryTheory.IsSplitMono ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app A)], A ∈ i.essImage
This theorem states that if `η_A` is a split monomorphism in a category `C`, then the object `A` belongs to the essential image of a functor `i` from category `D` to `C`, provided that the functor `i` is reflective. Here, `η_A` denotes the component at `A` of the unit of the adjunction associated to the functor `i`. The essential image of a functor `i` consists of objects in `C` that are isomorphic to the image of some object under `i`. A split monomorphism is a morphism that has a right-inverse. A functor is said to be reflective if it has a left adjoint. This theorem is thus a condition for membership in the essential image of a reflective functor in terms of split monomorphisms.
More concisely: If a split monomorphism in a category is the component at its domain of the unit of an adjunction from a reflective functor, then the domain of the split monomorphism belongs to the essential image of the reflective functor.
|
CategoryTheory.Functor.essImage.unit_isIso
theorem CategoryTheory.Functor.essImage.unit_isIso :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C}
[inst_2 : CategoryTheory.Reflective i] {A : C},
A ∈ i.essImage → CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app A)
This theorem states that if a category 'A' is essentially in the image of a reflective functor 'i', then the unit of the adjunction associated to the right adjoint of 'i' evaluated at 'A' is an isomorphism. In other words, if 'A' belongs to the essential image of functor 'i', then `η_A` is an isomorphism. This theorem implies that the "witness" for 'A' being in the essential image can be given as the reflection of 'A', with the isomorphism as `η_A`. Note that for any 'B' in the reflective subcategory, we automatically have that `ε_B` is an isomorphism.
More concisely: If a category 'A' is in the essential image of a reflective functor 'i', then the unit of the adjunction between 'i' and its right adjoint is an isomorphism (i.e., `η_A` is an isomorphism).
|
CategoryTheory.unitCompPartialBijectiveAux_symm_apply
theorem CategoryTheory.unitCompPartialBijectiveAux_symm_apply :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C}
[inst_2 : CategoryTheory.Reflective i] {A : C} {B : D}
(f : i.obj ((CategoryTheory.leftAdjoint i).obj A) ⟶ i.obj B),
(CategoryTheory.unitCompPartialBijectiveAux A B).symm f =
CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app A) f
This theorem, `CategoryTheory.unitCompPartialBijectiveAux_symm_apply`, states that for any categories `C` and `D`, a functor `i` from `D` to `C` that is reflective, and objects `A` of `C` and `B` of `D`, given a morphism `f` from the object `i.obj ((CategoryTheory.leftAdjoint i).obj A)` to `i.obj B` in `C`, the inverse of the bijection `unitCompPartialBijectiveAux` applied on `f` is equivalent to the composition of the morphism `(CategoryTheory.Adjunction.ofRightAdjoint i).unit.app A` and `f`. In simpler terms, this theorem establishes a certain relationship between the morphism `f` and the unit of the adjunction associated with `i`, under the action of the inverse of `unitCompPartialBijectiveAux`.
More concisely: For any reflective functor i from category D to category C and objects A in C and B in D, the inverse of `unitCompPartialBijectiveAux` applied to a morphism f from i(X) to B, where X is the left adjoint of i over A, is equivalent to the composition of i.unit.app A and f.
|
CategoryTheory.unit_obj_eq_map_unit
theorem CategoryTheory.unit_obj_eq_map_unit :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C}
[inst_2 : CategoryTheory.Reflective i] (X : C),
(CategoryTheory.Adjunction.ofRightAdjoint i).unit.app (i.obj ((CategoryTheory.leftAdjoint i).obj X)) =
i.map ((CategoryTheory.leftAdjoint i).map ((CategoryTheory.Adjunction.ofRightAdjoint i).unit.app X))
This theorem states that for a given reflective functor `i` (equipped with a left adjoint `L`), and with the unit of the adjunction denoted as `η`, the application of `η` to `iL` at a given object `X` is equal to the mapping of `i` applied to the mapping of `L` applied to the application of `η` at `X`. In other words, we have `η_iL = iL η`, as per the notation used in the theorem. This equality holds for all objects `X` in the category `C`. The functor `i` is assumed to be a functor from category `D` to category `C`, and `C` and `D` are assumed to be categories.
More concisely: For a reflective functor `i : D -> C` with left adjoint `L`, the unit of the adjunction `η` satisfies `η_X = i(η_X.L)` for all objects `X` in category `C`.
|