CategoryTheory.L_faithful_of_unit_isIso
theorem CategoryTheory.L_faithful_of_unit_isIso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
(h : L ⊣ R) [inst_2 : CategoryTheory.IsIso h.unit], L.Faithful
This theorem states that if the unit of an adjunction between two categories is an isomorphism, then the left adjoint functor is faithful. Here, we have two categories `C` and `D`, and two functors `L` and `R` such that `L` is left adjoint to `R`. The unit of the adjunction is a natural transformation, and the theorem asserts that if this natural transformation is an isomorphism, then the functor `L` is faithful, meaning it injectively maps morphisms from `C` to `D`.
More concisely: If the unit of an adjunction between categories is an isomorphism, then the left adjoint functor preserves identity morphisms, i.e., it is faithful.
|
CategoryTheory.R_faithful_of_counit_isIso
theorem CategoryTheory.R_faithful_of_counit_isIso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
(h : L ⊣ R) [inst_2 : CategoryTheory.IsIso h.counit], R.Faithful
This theorem states that in category theory, if the counit of an adjunction is an isomorphism, then the right adjoint functor is faithful. Here, `C` and `D` are categories, `L` is a functor from `C` to `D`, `R` is a functor from `D` to `C`, and `h` represents an adjunction between `L` and `R`. The adjunction `h` has a counit, which is assumed to be an isomorphism. Under these conditions, the theorem assures that the right adjoint functor `R` is faithful, meaning it maps distinct morphisms to distinct morphisms.
More concisely: If in the adjunction between functors L : C -> D and R : D -> C, the counit is an isomorphism, then the right adjoint functor R is faithful.
|
CategoryTheory.inv_map_unit
theorem CategoryTheory.inv_map_unit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
(h : L ⊣ R) {X : C} [inst_2 : CategoryTheory.IsIso (h.unit.app X)],
CategoryTheory.inv (L.map (h.unit.app X)) = h.counit.app (L.obj X)
The theorem `CategoryTheory.inv_map_unit` states that in the context of two categories `C` and `D`, and two functors `L : C -> D` and `R : D -> C` forming an adjunction `h : L ⊣ R`, if the unit of the adjunction at an object `X` in `C` is an isomorphism, then the inverse of the image of the unit under the functor `L` is equal to the application of the counit of the adjunction at the image of `X` under `L`. This means that if the unit of an adjunction is invertible, its inverse in the image of the left adjoint functor is obtained by applying the right adjoint functor to the counit.
More concisely: If functors `L : C -> D` and `R : D -> C` form an adjunction `h : L ⊣ R`, and the unit of the adjunction at an object `X` in `C` is an isomorphism, then `L(ηx)^-1 = ε(L(X))`.
|
CategoryTheory.inv_counit_map
theorem CategoryTheory.inv_counit_map :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
(h : L ⊣ R) {X : D} [inst_2 : CategoryTheory.IsIso (h.counit.app X)],
CategoryTheory.inv (R.map (h.counit.app X)) = h.unit.app (R.obj X)
This theorem states that for any categories `C` and `D`, and for any adjunction `h` between the functors `L` (from `C` to `D`) and `R` (from `D` to `C`), if the counit of the adjunction `h` at a specific object `X` in `D` is an isomorphism, then the inverse of the morphism obtained by applying the functor `R` to the counit of `h` at `X`, is equal to the unit of the adjunction `h` applied to the object obtained by applying the functor `R` to `X`. In simpler terms, it asserts a particular relationship between the unit and the counit of an adjunction in category theory when the counit is an isomorphism.
More concisely: For any adjunction between functors h : C -> D and R : D -> C, if the counit ε : L(X) -> R(X) is an isomorphism for some object X in D, then ε^-1 ∘ R(ι(X)) = ι(R(X)), where ι is the unit of the adjunction.
|