Adjoints of fully faithful functors #
A left adjoint is
- faithful, if and only if the unit is a monomorphism
- full, if and only if the unit is a split epimorphism
- fully faithful, if and only if the unit is an isomorphism
A right adjoint is
- faithful, if and only if the counit is an epimorphism
- full, if and only if the counit is a split monomorphism
- fully faithful, if and only if the counit is an isomorphism
This is Lemma 4.5.13 in Riehl's Category Theory in Context [riehl2017]. See also https://stacks.math.columbia.edu/tag/07RB for the statements about fully faithful functors.
In the file Mathlib.CategoryTheory.Monad.Adjunction, we prove that in fact, if there exists an
isomorphism L ⋙ R ≅ 𝟭 C, then the unit is an isomorphism, and similarly for the counit.
See CategoryTheory.Adjunction.isIso_unit_of_iso and
CategoryTheory.Adjunction.isIso_counit_of_iso.
instance
CategoryTheory.Adjunction.unit_mono_of_L_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.Faithful]
(X : C)
:
CategoryTheory.Mono (h.unit.app X)
If the left adjoint is faithful, then each component of the unit is an monomorphism.
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.Adjunction.unitSplitEpiOfLFull
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.Full]
(X : C)
:
CategoryTheory.SplitEpi (h.unit.app X)
If the left adjoint is full, then each component of the unit is a split epimorphism.
Equations
- h.unitSplitEpiOfLFull X = { section_ := L.preimage (h.counit.app (L.obj X)), id := ⋯ }
Instances For
instance
CategoryTheory.Adjunction.unit_isSplitEpi_of_L_full
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.Full]
(X : C)
:
CategoryTheory.IsSplitEpi (h.unit.app X)
If the right adjoint is full, then each component of the counit is a split monomorphism.
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.Full]
[L.Faithful]
(X : C)
:
CategoryTheory.IsIso (h.unit.app X)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.unit_isIso_of_L_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.Full]
[L.Faithful]
:
CategoryTheory.IsIso h.unit
If the left adjoint is fully faithful, then the unit is an isomorphism.
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.counit_epi_of_R_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.Faithful]
(X : D)
:
CategoryTheory.Epi (h.counit.app X)
If the right adjoint is faithful, then each component of the counit is an epimorphism.
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.Adjunction.counitSplitMonoOfRFull
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.Full]
(X : D)
:
CategoryTheory.SplitMono (h.counit.app X)
If the right adjoint is full, then each component of the counit is a split monomorphism.
Equations
- h.counitSplitMonoOfRFull X = { retraction := R.preimage (h.unit.app (R.obj X)), id := ⋯ }
Instances For
instance
CategoryTheory.Adjunction.counit_isSplitMono_of_R_full
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.Full]
(X : D)
:
CategoryTheory.IsSplitMono (h.counit.app X)
If the right adjoint is full, then each component of the counit is a split monomorphism.
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.instIsIsoAppCounitOfFullOfFaithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.Full]
[R.Faithful]
(X : D)
:
CategoryTheory.IsIso (h.counit.app X)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.Full]
[R.Faithful]
:
CategoryTheory.IsIso h.counit
If the right adjoint is fully faithful, then the counit is an isomorphism.
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Adjunction.inv_map_unit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
{X : C}
[CategoryTheory.IsIso (h.unit.app X)]
:
CategoryTheory.inv (L.map (h.unit.app X)) = h.counit.app (L.obj X)
If the unit of an adjunction is an isomorphism, then its inverse on the image of L is given by L whiskered with the counit.
@[simp]
theorem
CategoryTheory.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnit_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.unit]
(X : C)
:
h.whiskerLeftLCounitIsoOfIsIsoUnit.inv.app X = L.map (h.unit.app X)
@[simp]
theorem
CategoryTheory.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnit_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.unit]
(X : C)
:
h.whiskerLeftLCounitIsoOfIsIsoUnit.hom.app X = h.counit.app (L.obj X)
noncomputable def
CategoryTheory.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.unit]
:
L.comp (R.comp L) ≅ L
If the unit is an isomorphism, bundle one has an isomorphism L ⋙ R ⋙ L ≅ L.
Equations
- h.whiskerLeftLCounitIsoOfIsIsoUnit = (L.associator R L).symm ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.asIso h.unit).symm L ≪≫ L.leftUnitor
Instances For
@[simp]
theorem
CategoryTheory.Adjunction.inv_counit_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
{X : D}
[CategoryTheory.IsIso (h.counit.app X)]
:
CategoryTheory.inv (R.map (h.counit.app X)) = h.unit.app (R.obj X)
If the counit of an adjunction is an isomorphism, then its inverse on the image of R is given by R whiskered with the unit.
@[simp]
theorem
CategoryTheory.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounit_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.counit]
(X : D)
:
h.whiskerLeftRUnitIsoOfIsIsoCounit.hom.app X = R.map (h.counit.app X)
@[simp]
theorem
CategoryTheory.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounit_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.counit]
(X : D)
:
h.whiskerLeftRUnitIsoOfIsIsoCounit.inv.app X = h.unit.app (R.obj X)
noncomputable def
CategoryTheory.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.counit]
:
R.comp (L.comp R) ≅ R
If the counit of an is an isomorphism, one has an isomorphism (R ⋙ L ⋙ R) ≅ R.
Equations
- h.whiskerLeftRUnitIsoOfIsIsoCounit = (R.associator L R).symm ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.asIso h.counit) R ≪≫ R.leftUnitor
Instances For
theorem
CategoryTheory.Adjunction.faithful_L_of_mono_unit_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[∀ (X : C), CategoryTheory.Mono (h.unit.app X)]
:
L.Faithful
If each component of the unit is a monomorphism, then the left adjoint is faithful.
theorem
CategoryTheory.Adjunction.full_L_of_isSplitEpi_unit_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[∀ (X : C), CategoryTheory.IsSplitEpi (h.unit.app X)]
:
L.Full
If each component of the unit is a split epimorphism, then the left adjoint is full.
noncomputable def
CategoryTheory.Adjunction.fullyFaithfulLOfIsIsoUnit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.unit]
:
L.FullyFaithful
If the unit is an isomorphism, then the left adjoint is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Adjunction.faithful_R_of_epi_counit_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[∀ (X : D), CategoryTheory.Epi (h.counit.app X)]
:
R.Faithful
If each component of the counit is an epimorphism, then the right adjoint is faithful.
theorem
CategoryTheory.Adjunction.full_R_of_isSplitMono_counit_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[∀ (X : D), CategoryTheory.IsSplitMono (h.counit.app X)]
:
R.Full
If each component of the counit is a split monomorphism, then the right adjoint is full.
noncomputable def
CategoryTheory.Adjunction.fullyFaithfulROfIsIsoCounit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.counit]
:
R.FullyFaithful
If the counit is an isomorphism, then the right adjoint is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.Adjunction.whiskerLeft_counit_iso_of_L_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.Full]
[L.Faithful]
:
CategoryTheory.IsIso (CategoryTheory.whiskerLeft L h.counit)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.whiskerRight_counit_iso_of_L_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.Full]
[L.Faithful]
:
CategoryTheory.IsIso (CategoryTheory.whiskerRight h.counit R)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.whiskerLeft_unit_iso_of_R_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.Full]
[R.Faithful]
:
CategoryTheory.IsIso (CategoryTheory.whiskerLeft R h.unit)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.whiskerRight_unit_iso_of_R_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.Full]
[R.Faithful]
:
CategoryTheory.IsIso (CategoryTheory.whiskerRight h.unit L)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.instIsIsoAppCounitObjOfFaithfulOfFull
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.Faithful]
[L.Full]
{Y : C}
:
CategoryTheory.IsIso (h.counit.app (L.obj Y))
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.instIsIsoMapAppCounitOfFaithfulOfFull
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.Faithful]
[L.Full]
{Y : D}
:
CategoryTheory.IsIso (R.map (h.counit.app Y))
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.Faithful]
[L.Full]
{X : D}
:
CategoryTheory.IsIso (h.counit.app X) ↔ X ∈ L.essImage
theorem
CategoryTheory.Adjunction.mem_essImage_of_counit_isIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
(A : D)
[CategoryTheory.IsIso (h.counit.app A)]
:
A ∈ L.essImage
theorem
CategoryTheory.Adjunction.isIso_counit_app_of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.Faithful]
[L.Full]
{X : D}
{Y : C}
(e : X ≅ L.obj Y)
:
CategoryTheory.IsIso (h.counit.app X)
instance
CategoryTheory.Adjunction.instIsIsoAppUnitObjOfFaithfulOfFull
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.Faithful]
[R.Full]
{Y : D}
:
CategoryTheory.IsIso (h.unit.app (R.obj Y))
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.instIsIsoMapAppUnitOfFaithfulOfFull
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.Faithful]
[R.Full]
{X : C}
:
CategoryTheory.IsIso (L.map (h.unit.app X))
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Adjunction.isIso_unit_app_iff_mem_essImage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.Faithful]
[R.Full]
{Y : C}
:
CategoryTheory.IsIso (h.unit.app Y) ↔ Y ∈ R.essImage
theorem
CategoryTheory.Adjunction.mem_essImage_of_unit_isIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
(A : C)
[CategoryTheory.IsIso (h.unit.app A)]
:
A ∈ R.essImage
If η_A is an isomorphism, then A is in the essential image of i.
@[deprecated CategoryTheory.Adjunction.mem_essImage_of_unit_isIso]
theorem
CategoryTheory.mem_essImage_of_unit_isIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
(A : C)
[CategoryTheory.IsIso (h.unit.app A)]
:
A ∈ R.essImage
Alias of CategoryTheory.Adjunction.mem_essImage_of_unit_isIso.
If η_A is an isomorphism, then A is in the essential image of i.
theorem
CategoryTheory.Adjunction.isIso_unit_app_of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.Faithful]
[R.Full]
{X : D}
{Y : C}
(e : Y ≅ R.obj X)
:
CategoryTheory.IsIso (h.unit.app Y)
instance
CategoryTheory.Adjunction.instIsIsoFunctorUnitOfIsEquivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.IsEquivalence]
:
CategoryTheory.IsIso h.unit
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.IsEquivalence]
:
CategoryTheory.IsIso h.counit
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Adjunction.isEquivalence_left_of_isEquivalence_right
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.IsEquivalence]
:
L.IsEquivalence
theorem
CategoryTheory.Adjunction.isEquivalence_right_of_isEquivalence_left
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.IsEquivalence]
:
R.IsEquivalence
instance
CategoryTheory.Adjunction.instIsIsoFunctorUnitOfIsEquivalence_1
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[L.IsEquivalence]
:
CategoryTheory.IsIso h.unit
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence_1
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[R.IsEquivalence]
:
CategoryTheory.IsIso h.counit
Equations
- ⋯ = ⋯