doc-next-gen

Mathlib.CategoryTheory.Adjunction.Basic

Module docstring

{"# Adjunctions between functors

F ⊣ G represents the data of an adjunction between two functors F : C ⥤ D and G : D ⥤ C. F is the left adjoint and G is the right adjoint.

We provide various useful constructors: * mkOfHomEquiv * mk': construct an adjunction from the data of a hom set equivalence, unit and counit natural transformations together with proofs of the equalities homEquiv_unit and homEquiv_counit relating them to each other. * leftAdjointOfEquiv / rightAdjointOfEquiv construct a left/right adjoint of a given functor given the action on objects and the relevant equivalence of morphism spaces. * adjunctionOfEquivLeft / adjunctionOfEquivRight witness that these constructions give adjunctions.

There are also typeclasses IsLeftAdjoint / IsRightAdjoint, which asserts the existence of a adjoint functor. Given [F.IsLeftAdjoint], a chosen right adjoint can be obtained as F.rightAdjoint.

Adjunction.comp composes adjunctions.

toEquivalence upgrades an adjunction to an equivalence, given witnesses that the unit and counit are pointwise isomorphisms. Conversely Equivalence.toAdjunction recovers the underlying adjunction from an equivalence.

Overview of the directory CategoryTheory.Adjunction

  • Adjoint lifting theorems are in the directory Lifting.
  • The file AdjointFunctorTheorems proves the adjoint functor theorems.
  • The file Comma shows that for a functor G : D ⥤ C the data of an initial object in each StructuredArrow category on G is equivalent to a left adjoint to G, as well as the dual.
  • The file Evaluation shows that products and coproducts are adjoint to evaluation of functors.
  • The file FullyFaithful characterizes when adjoints are full or faithful in terms of the unit and counit.
  • The file Limits proves that left adjoints preserve colimits and right adjoints preserve limits.
  • The file Mates establishes the bijection between the 2-cells L₁ R₁ C --→ D C ←-- D G ↓ ↗ ↓ H G ↓ ↘ ↓ H E --→ F E ←-- F L₂ R₂ where L₁ ⊣ R₁ and L₂ ⊣ R₂. Specializing to a pair of adjoints L₁ L₂ : C ⥤ D, R₁ R₂ : D ⥤ C, it provides equivalences (L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂) and (L₂ ≅ L₁) ≃ (R₁ ≅ R₂).
  • The file Opposites contains constructions to relate adjunctions of functors to adjunctions of their opposites.
  • The file Reflective defines reflective functors, i.e. fully faithful right adjoints. Note that many facts about reflective functors are proved in the earlier file FullyFaithful.
  • The file Restrict defines the restriction of an adjunction along fully faithful functors.
  • The file Triple proves that in an adjoint triple, the left adjoint is fully faithful if and only if the right adjoint is.
  • The file Unique proves uniqueness of adjoints.
  • The file Whiskering proves that functors F : D ⥤ E and G : E ⥤ D with an adjunction F ⊣ G, induce adjunctions between the functor categories C ⥤ D and C ⥤ E, and the functor categories E ⥤ C and D ⥤ C.

Other files related to adjunctions

  • The file CategoryTheory.Monad.Adjunction develops the basic relationship between adjunctions and (co)monads. There it is also shown that given an adjunction L ⊣ R and an isomorphism L ⋙ R ≅ 𝟭 C, the unit is an isomorphism, and similarly for the counit. "}
CategoryTheory.Adjunction structure
(F : C ⥤ D) (G : D ⥤ C)
Full source 
/-- `F ⊣ G` represents the data of an adjunction between two functors
`F : C ⥤ D` and `G : D ⥤ C`. `F` is the left adjoint and `G` is the right adjoint.

We use the unit-counit definition of an adjunction. There is a constructor `Adjunction.mk'`
which constructs an adjunction from the data of a hom set equivalence, a unit, and a counit,
together with proofs of the equalities `homEquiv_unit` and `homEquiv_counit` relating them to each
other.

There is also a constructor `Adjunction.mkOfHomEquiv` which constructs an adjunction from a natural
hom set equivalence.

To construct adjoints to a given functor, there are constructors `leftAdjointOfEquiv` and
`adjunctionOfEquivLeft` (as well as their duals). -/
@[stacks 0037]
structure Adjunction (F : C ⥤ D) (G : D ⥤ C) where
  /-- The unit of an adjunction -/
  unit : 𝟭𝟭 C ⟶ F.comp G
  /-- The counit of an adjunction -/
  counit : G.comp F ⟶ 𝟭 D
  /-- Equality of the composition of the unit and counit with the identity `F ⟶ FGF ⟶ F = 𝟙` -/
  left_triangle_components (X : C) :
      F.map (unit.app X) ≫ counit.app (F.obj X) = 𝟙 (F.obj X) := by aesop_cat
  /-- Equality of the composition of the unit and counit with the identity `G ⟶ GFG ⟶ G = 𝟙` -/
  right_triangle_components (Y : D) :
      unit.app (G.obj Y) ≫ G.map (counit.app Y) = 𝟙 (G.obj Y) := by aesop_cat
Adjunction between functors
Informal description
An adjunction between two functors $F \colon C \to D$ (the left adjoint) and $G \colon D \to C$ (the right adjoint), denoted $F \dashv G$, consists of natural transformations $\eta \colon \text{id}_C \Rightarrow G \circ F$ (the unit) and $\epsilon \colon F \circ G \Rightarrow \text{id}_D$ (the counit) satisfying the triangle identities. Alternatively, it can be characterized by a natural bijection between hom-sets $\text{Hom}_D(FX, Y) \cong \text{Hom}_C(X, GY)$ for all objects $X$ in $C$ and $Y$ in $D$.
CategoryTheory.Functor.IsLeftAdjoint structure
(left : C ⥤ D)
Full source 
/-- A class asserting the existence of a right adjoint. -/
class IsLeftAdjoint (left : C ⥤ D) : Prop where
  exists_rightAdjoint : ∃ (right : D ⥤ C), Nonempty (left ⊣ right)
Existence of a right adjoint functor
Informal description
The structure asserting that a functor $F \colon C \to D$ has a right adjoint functor $G \colon D \to C$, meaning there exists a natural bijection between morphisms $F(X) \to Y$ in $D$ and morphisms $X \to G(Y)$ in $C$ for all objects $X \in C$ and $Y \in D$.
CategoryTheory.Functor.IsRightAdjoint structure
(right : D ⥤ C)
Full source 
/-- A class asserting the existence of a left adjoint. -/
class IsRightAdjoint (right : D ⥤ C) : Prop where
  exists_leftAdjoint : ∃ (left : C ⥤ D), Nonempty (left ⊣ right)
Existence of a left adjoint functor
Informal description
The structure asserting that a functor $G \colon D \to C$ has a left adjoint functor $F \colon C \to D$, meaning there exists a natural bijection between morphisms $F(X) \to Y$ in $D$ and morphisms $X \to G(Y)$ in $C$ for all objects $X \in C$ and $Y \in D$.
CategoryTheory.Functor.leftAdjoint definition
(R : D ⥤ C) [IsRightAdjoint R] : C ⥤ D
Full source 
/-- A chosen left adjoint to a functor that is a right adjoint. -/
noncomputable def leftAdjoint (R : D ⥤ C) [IsRightAdjoint R] : C ⥤ D :=
  (IsRightAdjoint.exists_leftAdjoint (right := R)).choose
Left adjoint functor of a right adjoint
Informal description
Given a functor $R \colon D \to C$ that is a right adjoint (i.e., there exists a left adjoint functor $L \colon C \to D$ such that $L \dashv R$), this definition selects a specific left adjoint functor $L$ for $R$. The existence of such a left adjoint is guaranteed by the `IsRightAdjoint` instance for $R$.
CategoryTheory.Functor.rightAdjoint definition
(L : C ⥤ D) [IsLeftAdjoint L] : D ⥤ C
Full source 
/-- A chosen right adjoint to a functor that is a left adjoint. -/
noncomputable def rightAdjoint (L : C ⥤ D) [IsLeftAdjoint L] : D ⥤ C :=
  (IsLeftAdjoint.exists_rightAdjoint (left := L)).choose
Right adjoint functor of a left adjoint
Informal description
Given a functor $L \colon C \to D$ that is a left adjoint (i.e., there exists a right adjoint functor $R \colon D \to C$ such that $L \dashv R$), this definition selects a specific right adjoint functor $R$ for $L$. The existence of such a right adjoint is guaranteed by the `IsLeftAdjoint` instance for $L$.
CategoryTheory.Adjunction.ofIsLeftAdjoint definition
(left : C ⥤ D) [left.IsLeftAdjoint] : left ⊣ left.rightAdjoint
Full source 
/-- The adjunction associated to a functor known to be a left adjoint. -/
noncomputable def Adjunction.ofIsLeftAdjoint (left : C ⥤ D) [left.IsLeftAdjoint] :
    left ⊣ left.rightAdjoint :=
  Functor.IsLeftAdjoint.exists_rightAdjoint.choose_spec.some
Adjunction from a left adjoint functor
Informal description
Given a functor $F \colon C \to D$ that is known to be a left adjoint (i.e., there exists a right adjoint functor $G \colon D \to C$), this definition constructs the adjunction $F \dashv G$ by providing the unit and counit natural transformations satisfying the triangle identities.
CategoryTheory.Adjunction.ofIsRightAdjoint definition
(right : C ⥤ D) [right.IsRightAdjoint] : right.leftAdjoint ⊣ right
Full source 
/-- The adjunction associated to a functor known to be a right adjoint. -/
noncomputable def Adjunction.ofIsRightAdjoint (right : C ⥤ D) [right.IsRightAdjoint] :
    right.leftAdjoint ⊣ right :=
  Functor.IsRightAdjoint.exists_leftAdjoint.choose_spec.some
Adjunction from a right adjoint functor
Informal description
Given a functor $G \colon C \to D$ that is known to be a right adjoint (i.e., there exists a left adjoint functor $F \colon D \to C$), this definition constructs the adjunction $F \dashv G$ by providing the unit and counit natural transformations satisfying the triangle identities.
CategoryTheory.Adjunction.homEquiv definition
{F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) (X : C) (Y : D) : (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
Full source 
/-- The hom set equivalence associated to an adjunction. -/
@[simps -isSimp]
def homEquiv {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) (X : C) (Y : D) :
    (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y) where
  toFun := fun f => adj.unit.app X ≫ G.map f
  invFun := fun g => F.map g ≫ adj.counit.app Y
  left_inv := fun f => by
    dsimp
    rw [F.map_comp, assoc, ← Functor.comp_map, adj.counit.naturality, ← assoc]
    simp
  right_inv := fun g => by
    simp only [Functor.comp_obj, Functor.map_comp]
    rw [← assoc, ← Functor.comp_map, ← adj.unit.naturality]
    simp
Hom-set equivalence in an adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, for any objects $X$ in $C$ and $Y$ in $D$, there is a natural bijection between the hom-sets $\text{Hom}_D(F(X), Y)$ and $\text{Hom}_C(X, G(Y))$. The bijection is given by mapping a morphism $f \colon F(X) \to Y$ to $\eta_X \circ G(f)$, where $\eta$ is the unit of the adjunction, and its inverse maps $g \colon X \to G(Y)$ to $F(g) \circ \epsilon_Y$, where $\epsilon$ is the counit of the adjunction.
CategoryTheory.Adjunction.ext theorem
{F : C ⥤ D} {G : D ⥤ C} {adj adj' : F ⊣ G} (h : adj.unit = adj'.unit) : adj = adj'
Full source 
@[ext]
lemma ext {F : C ⥤ D} {G : D ⥤ C} {adj adj' : F ⊣ G}
    (h : adj.unit = adj'.unit) : adj = adj' := by
  suffices h' : adj.counit = adj'.counit by cases adj; cases adj'; aesop
  ext X
  apply (adj.homEquiv _ _).injective
  rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit,
    Adjunction.right_triangle_components, h, Adjunction.right_triangle_components]
Uniqueness of Adjunction via Unit Equality
Informal description
Given two adjunctions $F \dashv G$ and $F \dashv G$ between the same functors $F \colon C \to D$ and $G \colon D \to C$, if their unit natural transformations are equal, then the adjunctions themselves are equal.
CategoryTheory.Adjunction.isLeftAdjoint theorem
(adj : F ⊣ G) : F.IsLeftAdjoint
Full source 
lemma isLeftAdjoint (adj : F ⊣ G) : F.IsLeftAdjoint := ⟨_, ⟨adj⟩⟩
Left adjoint property in an adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, the left adjoint $F$ satisfies the property of having a right adjoint (namely $G$), i.e., $F$ is a left adjoint functor.
CategoryTheory.Adjunction.isRightAdjoint theorem
(adj : F ⊣ G) : G.IsRightAdjoint
Full source 
lemma isRightAdjoint (adj : F ⊣ G) : G.IsRightAdjoint := ⟨_, ⟨adj⟩⟩
Right adjoint property in an adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, the right adjoint $G$ satisfies the property of having a left adjoint (namely $F$), i.e., $G$ is a right adjoint functor.
CategoryTheory.Adjunction.instIsLeftAdjointLeftAdjoint instance
(R : D ⥤ C) [R.IsRightAdjoint] : R.leftAdjoint.IsLeftAdjoint
Full source 
instance (R : D ⥤ C) [R.IsRightAdjoint] : R.leftAdjoint.IsLeftAdjoint :=
  (ofIsRightAdjoint R).isLeftAdjoint
Left Adjoint of a Right Adjoint is a Left Adjoint
Informal description
For any functor $R \colon D \to C$ that is a right adjoint, its chosen left adjoint functor $L \colon C \to D$ is a left adjoint (i.e., has a right adjoint, which is $R$).
CategoryTheory.Adjunction.instIsRightAdjointRightAdjoint instance
(L : C ⥤ D) [L.IsLeftAdjoint] : L.rightAdjoint.IsRightAdjoint
Full source 
instance (L : C ⥤ D) [L.IsLeftAdjoint] : L.rightAdjoint.IsRightAdjoint :=
  (ofIsLeftAdjoint L).isRightAdjoint
Right Adjoint of a Left Adjoint is a Right Adjoint
Informal description
For any functor $L \colon C \to D$ that is a left adjoint, its right adjoint functor $R \colon D \to C$ is a right adjoint (i.e., has a left adjoint, which is $L$).
CategoryTheory.Adjunction.homEquiv_id theorem
(X : C) : adj.homEquiv X _ (𝟙 _) = adj.unit.app X
Full source 
theorem homEquiv_id (X : C) : adj.homEquiv X _ (𝟙 _) = adj.unit.app X := by simp
Unit as Image of Identity under Hom-set Bijection in Adjunction
Informal description
For any object $X$ in category $C$ and an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, the bijection $\text{Hom}_D(F(X), Y) \cong \text{Hom}_C(X, G(Y))$ maps the identity morphism $1_{F(X)}$ to the unit morphism $\eta_X$ of the adjunction at $X$. In other words, $\text{adj.homEquiv}_X(1_{F(X)}) = \eta_X$.
CategoryTheory.Adjunction.homEquiv_symm_id theorem
(X : D) : (adj.homEquiv _ X).symm (𝟙 _) = adj.counit.app X
Full source 
theorem homEquiv_symm_id (X : D) : (adj.homEquiv _ X).symm (𝟙 _) = adj.counit.app X := by simp
Counit as Inverse Hom-Set Equivalence of Identity
Informal description
For any object $X$ in the category $D$, the inverse of the hom-set equivalence $\text{Hom}_D(F(G(X)), X) \cong \text{Hom}_C(G(X), G(X))$ applied to the identity morphism $\text{id}_{G(X)}$ yields the counit morphism $\epsilon_X \colon F(G(X)) \to X$ of the adjunction $F \dashv G$.
CategoryTheory.Adjunction.homEquiv_naturality_left_symm theorem
(f : X' ⟶ X) (g : X ⟶ G.obj Y) : (adj.homEquiv X' Y).symm (f ≫ g) = F.map f ≫ (adj.homEquiv X Y).symm g
Full source 
theorem homEquiv_naturality_left_symm (f : X' ⟶ X) (g : X ⟶ G.obj Y) :
    (adj.homEquiv X' Y).symm (f ≫ g) = F.map f ≫ (adj.homEquiv X Y).symm g := by
  simp
Naturality of the inverse hom-set equivalence under precomposition in the left argument
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, for any morphisms $f \colon X' \to X$ in $C$ and $g \colon X \to G(Y)$ in $C$, the following equality holds: $$(adj.homEquiv_{X',Y})^{-1}(f \circ g) = F(f) \circ (adj.homEquiv_{X,Y})^{-1}(g)$$ where $adj.homEquiv_{X,Y} \colon \text{Hom}_D(F(X), Y) \simeq \text{Hom}_C(X, G(Y))$ is the natural bijection of hom-sets given by the adjunction, and $(-)^{-1}$ denotes its inverse.
CategoryTheory.Adjunction.homEquiv_naturality_left theorem
(f : X' ⟶ X) (g : F.obj X ⟶ Y) : (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g
Full source 
theorem homEquiv_naturality_left (f : X' ⟶ X) (g : F.obj X ⟶ Y) :
    (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g := by
  rw [← Equiv.eq_symm_apply]
  simp only [Equiv.symm_apply_apply, eq_self_iff_true, homEquiv_naturality_left_symm]
Naturality of Hom-Set Equivalence under Precomposition in an Adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, for any morphisms $f \colon X' \to X$ in $C$ and $g \colon F(X) \to Y$ in $D$, the following equality holds: \[ \text{adj.homEquiv}_{X',Y}(F(f) \circ g) = f \circ \text{adj.homEquiv}_{X,Y}(g) \] where $\text{adj.homEquiv}_{X,Y} \colon \text{Hom}_D(F(X), Y) \simeq \text{Hom}_C(X, G(Y))$ is the natural bijection of hom-sets given by the adjunction.
CategoryTheory.Adjunction.homEquiv_naturality_right theorem
(f : F.obj X ⟶ Y) (g : Y ⟶ Y') : (adj.homEquiv X Y') (f ≫ g) = (adj.homEquiv X Y) f ≫ G.map g
Full source 
theorem homEquiv_naturality_right (f : F.obj X ⟶ Y) (g : Y ⟶ Y') :
    (adj.homEquiv X Y') (f ≫ g) = (adj.homEquiv X Y) f ≫ G.map g := by
  simp
Naturality of Hom-set Equivalence under Post-composition in an Adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, for any objects $X$ in $C$ and $Y, Y'$ in $D$, and morphisms $f \colon F(X) \to Y$ and $g \colon Y \to Y'$, the following diagram commutes: \[ \text{Hom}_D(F(X), Y') \xrightarrow{\text{adj.homEquiv}_{X,Y'}} \text{Hom}_C(X, G(Y')) \] \[ \text{Hom}_D(F(X), Y) \xrightarrow{\text{adj.homEquiv}_{X,Y}} \text{Hom}_C(X, G(Y)) \] where the vertical maps are given by post-composition with $g$ on the left and $G(g)$ on the right. Specifically, we have: \[ \text{adj.homEquiv}_{X,Y'}(f \circ g) = \text{adj.homEquiv}_{X,Y}(f) \circ G(g). \]
CategoryTheory.Adjunction.homEquiv_naturality_right_symm theorem
(f : X ⟶ G.obj Y) (g : Y ⟶ Y') : (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g
Full source 
theorem homEquiv_naturality_right_symm (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
    (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g := by
  rw [Equiv.symm_apply_eq]
  simp only [homEquiv_naturality_right, eq_self_iff_true, Equiv.apply_symm_apply]
Naturality of Inverse Hom-set Equivalence under Post-composition in an Adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, for any objects $X$ in $C$ and $Y, Y'$ in $D$, and morphisms $f \colon X \to G(Y)$ and $g \colon Y \to Y'$, the following equality holds: \[ \text{adj.homEquiv}_{X,Y'}^{-1}(f \circ G(g)) = \text{adj.homEquiv}_{X,Y}^{-1}(f) \circ g. \] Here, $\text{adj.homEquiv}^{-1}$ denotes the inverse of the hom-set bijection given by the adjunction.
CategoryTheory.Adjunction.homEquiv_naturality_left_square theorem
(f : X' ⟶ X) (g : F.obj X ⟶ Y') (h : F.obj X' ⟶ Y) (k : Y ⟶ Y') (w : F.map f ≫ g = h ≫ k) : f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k
Full source 
@[reassoc]
theorem homEquiv_naturality_left_square (f : X' ⟶ X) (g : F.obj X ⟶ Y')
    (h : F.obj X' ⟶ Y) (k : Y ⟶ Y') (w : F.map f ≫ g = h ≫ k) :
    f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k := by
  rw [← homEquiv_naturality_left, ← homEquiv_naturality_right, w]
Naturality Square for Left Hom-Set Equivalence in an Adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, for any morphisms $f \colon X' \to X$ in $C$, $g \colon F(X) \to Y'$ in $D$, $h \colon F(X') \to Y$ in $D$, and $k \colon Y \to Y'$ in $D$ such that $F(f) \circ g = h \circ k$, the following diagram commutes: \[ \begin{tikzcd} X' \arrow[r, "f"] & X \arrow[d, "\text{adj.homEquiv}_{X,Y'}(g)"] \\ F(X') \arrow[u, "\text{adj.homEquiv}_{X',Y}(h)"] & G(Y') \\ Y \arrow[r, "k"] & Y' \arrow[u, "G(k)"] \end{tikzcd} \] Specifically, we have: \[ f \circ \text{adj.homEquiv}_{X,Y'}(g) = \text{adj.homEquiv}_{X',Y}(h) \circ G(k). \]
CategoryTheory.Adjunction.homEquiv_naturality_right_square theorem
(f : X' ⟶ X) (g : X ⟶ G.obj Y') (h : X' ⟶ G.obj Y) (k : Y ⟶ Y') (w : f ≫ g = h ≫ G.map k) : F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k
Full source 
@[reassoc]
theorem homEquiv_naturality_right_square (f : X' ⟶ X) (g : X ⟶ G.obj Y')
    (h : X' ⟶ G.obj Y) (k : Y ⟶ Y') (w : f ≫ g = h ≫ G.map k) :
    F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k := by
  rw [← homEquiv_naturality_left_symm, ← homEquiv_naturality_right_symm, w]
Naturality of Inverse Hom-set Equivalence in a Commutative Square under an Adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, for any morphisms $f \colon X' \to X$ in $C$, $g \colon X \to G(Y')$ in $C$, $h \colon X' \to G(Y)$ in $C$, and $k \colon Y \to Y'$ in $D$ such that $f \circ g = h \circ G(k)$, the following equality holds: \[ F(f) \circ \text{adj.homEquiv}_{X,Y'}^{-1}(g) = \text{adj.homEquiv}_{X',Y}^{-1}(h) \circ k. \] Here, $\text{adj.homEquiv}^{-1}$ denotes the inverse of the hom-set bijection given by the adjunction.
CategoryTheory.Adjunction.homEquiv_naturality_left_square_iff theorem
(f : X' ⟶ X) (g : F.obj X ⟶ Y') (h : F.obj X' ⟶ Y) (k : Y ⟶ Y') : (f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k) ↔ (F.map f ≫ g = h ≫ k)
Full source 
theorem homEquiv_naturality_left_square_iff (f : X' ⟶ X) (g : F.obj X ⟶ Y')
    (h : F.obj X' ⟶ Y) (k : Y ⟶ Y') :
    (f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k) ↔
      (F.map f ≫ g = h ≫ k) :=
  ⟨fun w ↦ by simpa only [Equiv.symm_apply_apply]
      using homEquiv_naturality_right_square adj _ _ _ _ w,
    homEquiv_naturality_left_square adj f g h k⟩
Equivalence of Naturality Conditions for Left Hom-Set Bijection in an Adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, for any morphisms $f \colon X' \to X$ in $C$, $g \colon F(X) \to Y'$ in $D$, $h \colon F(X') \to Y$ in $D$, and $k \colon Y \to Y'$ in $D$, the following are equivalent: 1. The composition $f \circ \text{adj.homEquiv}_{X,Y'}(g)$ equals $\text{adj.homEquiv}_{X',Y}(h) \circ G(k)$. 2. The composition $F(f) \circ g$ equals $h \circ k$. Here, $\text{adj.homEquiv}$ denotes the natural bijection $\text{Hom}_D(F(X), Y) \cong \text{Hom}_C(X, G(Y))$ provided by the adjunction.
CategoryTheory.Adjunction.homEquiv_naturality_right_square_iff theorem
(f : X' ⟶ X) (g : X ⟶ G.obj Y') (h : X' ⟶ G.obj Y) (k : Y ⟶ Y') : (F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k) ↔ (f ≫ g = h ≫ G.map k)
Full source 
theorem homEquiv_naturality_right_square_iff (f : X' ⟶ X) (g : X ⟶ G.obj Y')
    (h : X' ⟶ G.obj Y) (k : Y ⟶ Y') :
    (F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k) ↔
      (f ≫ g = h ≫ G.map k) :=
  ⟨fun w ↦ by simpa only [Equiv.apply_symm_apply]
      using homEquiv_naturality_left_square adj _ _ _ _ w,
    homEquiv_naturality_right_square adj f g h k⟩
Naturality of Inverse Hom-Set Equivalence in an Adjunction (Equivalence Form)
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, for any morphisms $f \colon X' \to X$ in $C$, $g \colon X \to G(Y')$ in $C$, $h \colon X' \to G(Y)$ in $C$, and $k \colon Y \to Y'$ in $D$, the following are equivalent: 1. The composition $F(f) \circ \text{adj.homEquiv}_{X,Y'}^{-1}(g)$ equals $\text{adj.homEquiv}_{X',Y}^{-1}(h) \circ k$. 2. The composition $f \circ g$ equals $h \circ G(k)$. Here, $\text{adj.homEquiv}^{-1}$ denotes the inverse of the hom-set bijection given by the adjunction.
CategoryTheory.Adjunction.left_triangle theorem
: whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = 𝟙 _
Full source 
@[simp]
theorem left_triangle : whiskerRightwhiskerRight adj.unit F ≫ whiskerLeft F adj.counit = 𝟙 _ := by
  ext; simp
Left Triangle Identity for Adjunctions
Informal description
For an adjunction $F \dashv G$ with unit $\eta \colon \text{id}_C \Rightarrow G \circ F$ and counit $\epsilon \colon F \circ G \Rightarrow \text{id}_D$, the left triangle identity holds: \[ (\eta \circ F) \cdot (F \circ \epsilon) = \text{id}_F \] where $\cdot$ denotes vertical composition of natural transformations and $\circ$ denotes horizontal composition (whiskering).
CategoryTheory.Adjunction.right_triangle theorem
: whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = 𝟙 _
Full source 
@[simp]
theorem right_triangle : whiskerLeftwhiskerLeft G adj.unit ≫ whiskerRight adj.counit G = 𝟙 _ := by
  ext; simp
Right Triangle Identity for Adjunctions
Informal description
For an adjunction $F \dashv G$ with unit $\eta \colon \text{id}_C \Rightarrow G \circ F$ and counit $\epsilon \colon F \circ G \Rightarrow \text{id}_D$, the right triangle identity holds: \[ (G \circ \eta) \cdot (\epsilon \circ G) = \text{id}_G \] where $\cdot$ denotes vertical composition of natural transformations and $\circ$ denotes horizontal composition (whiskering).
CategoryTheory.Adjunction.counit_naturality theorem
{X Y : D} (f : X ⟶ Y) : F.map (G.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f
Full source 
@[reassoc (attr := simp)]
theorem counit_naturality {X Y : D} (f : X ⟶ Y) :
    F.map (G.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f :=
  adj.counit.naturality f
Naturality of the Counit in an Adjunction
Informal description
For any morphism $f \colon X \to Y$ in category $D$, the following diagram commutes: \[ F(G(f)) \circ \epsilon_Y = \epsilon_X \circ f \] where $\epsilon$ is the counit of the adjunction $F \dashv G$, and $F \colon C \to D$ and $G \colon D \to C$ are the left and right adjoint functors respectively.
CategoryTheory.Adjunction.unit_naturality theorem
{X Y : C} (f : X ⟶ Y) : adj.unit.app X ≫ G.map (F.map f) = f ≫ adj.unit.app Y
Full source 
@[reassoc (attr := simp)]
theorem unit_naturality {X Y : C} (f : X ⟶ Y) :
    adj.unit.app X ≫ G.map (F.map f) = f ≫ adj.unit.app Y :=
  (adj.unit.naturality f).symm
Naturality of the Unit in an Adjunction
Informal description
For any morphism $f \colon X \to Y$ in category $C$, the following diagram commutes: \[ \eta_X \circ G(F(f)) = f \circ \eta_Y \] where $\eta$ is the unit of the adjunction $F \dashv G$, and $F \colon C \to D$ and $G \colon D \to C$ are the left and right adjoint functors respectively.
CategoryTheory.Adjunction.unit_comp_map_eq_iff theorem
{A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) : adj.unit.app A ≫ G.map f = g ↔ f = F.map g ≫ adj.counit.app B
Full source 
lemma unit_comp_map_eq_iff {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) :
    adj.unit.app A ≫ G.map fadj.unit.app A ≫ G.map f = g ↔ f = F.map g ≫ adj.counit.app B :=
  ⟨fun h => by simp [← h], fun h => by simp [h]⟩
Equivalence between Unit-Composition and Counit-Composition in Adjunction
Informal description
For any objects $A$ in category $C$ and $B$ in category $D$, and morphisms $f \colon F(A) \to B$ and $g \colon A \to G(B)$, the following equivalence holds: \[ \eta_A \circ G(f) = g \quad \text{if and only if} \quad f = F(g) \circ \epsilon_B \] where $\eta$ is the unit and $\epsilon$ is the counit of the adjunction $F \dashv G$.
CategoryTheory.Adjunction.homEquiv_apply_eq theorem
{A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) : adj.homEquiv A B f = g ↔ f = (adj.homEquiv A B).symm g
Full source 
theorem homEquiv_apply_eq {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) :
    adj.homEquiv A B f = g ↔ f = (adj.homEquiv A B).symm g :=
  unit_comp_map_eq_iff adj f g
Bijection Condition for Adjunction Hom-Set Equivalence
Informal description
For any objects $A$ in category $C$ and $B$ in category $D$, and morphisms $f \colon F(A) \to B$ and $g \colon A \to G(B)$, the hom-set equivalence $\text{Hom}_D(F(A), B) \simeq \text{Hom}_C(A, G(B))$ satisfies: \[ \varphi(f) = g \quad \text{if and only if} \quad f = \varphi^{-1}(g) \] where $\varphi$ is the bijection given by the adjunction $F \dashv G$ and $\varphi^{-1}$ is its inverse.
CategoryTheory.Adjunction.corepresentableBy definition
(X : C) : (G ⋙ coyoneda.obj (Opposite.op X)).CorepresentableBy (F.obj X)
Full source 
/-- If `adj : F ⊣ G`, and `X : C`, then `F.obj X` corepresents `Y ↦ (X ⟶ G.obj Y)`. -/
@[simps]
def corepresentableBy (X : C) :
    (G ⋙ coyoneda.obj (Opposite.op X)).CorepresentableBy (F.obj X) where
  homEquiv := adj.homEquiv _ _
  homEquiv_comp := by simp
Corepresentability of the composition of right adjoint with co-Yoneda embedding
Informal description
For an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, and for any object $X$ in $C$, the functor $G$ composed with the co-Yoneda embedding evaluated at $X^{\mathrm{op}}$ is corepresentable by $F(X)$. This means there is a natural isomorphism between the functor $Y \mapsto \mathrm{Hom}_C(X, G(Y))$ and the functor $Y \mapsto \mathrm{Hom}_D(F(X), Y)$.
CategoryTheory.Adjunction.representableBy definition
(Y : D) : (F.op ⋙ yoneda.obj Y).RepresentableBy (G.obj Y)
Full source 
/-- If `adj : F ⊣ G`, and `Y : D`, then `G.obj Y` represents `X ↦ (F.obj X ⟶ Y)`. -/
@[simps]
def representableBy (Y : D) :
    (F.op ⋙ yoneda.obj Y).RepresentableBy (G.obj Y) where
  homEquiv := (adj.homEquiv _ _).symm
  homEquiv_comp := by simp
Representability of the composition of opposite left adjoint with Yoneda embedding
Informal description
For an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, and for any object $Y$ in $D$, the functor obtained by composing the opposite functor $F^{\mathrm{op}}$ with the Yoneda embedding evaluated at $Y$ is representable by $G(Y)$. This means there is a natural isomorphism between the functor $X \mapsto \mathrm{Hom}_D(F(X), Y)$ and the functor $X \mapsto \mathrm{Hom}_C(X, G(Y))$.
CategoryTheory.Adjunction.CoreHomEquivUnitCounit structure
(F : C ⥤ D) (G : D ⥤ C)
Full source 
/--
This is an auxiliary data structure useful for constructing adjunctions.
See `Adjunction.mk'`. This structure won't typically be used anywhere else.
-/
structure CoreHomEquivUnitCounit (F : C ⥤ D) (G : D ⥤ C) where
  /-- The equivalence between `Hom (F X) Y` and `Hom X (G Y)` coming from an adjunction -/
  homEquiv : ∀ X Y, (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
  /-- The unit of an adjunction -/
  unit : 𝟭𝟭 C ⟶ F ⋙ G
  /-- The counit of an adjunction -/
  counit : G ⋙ FG ⋙ F ⟶ 𝟭 D
  /-- The relationship between the unit and hom set equivalence of an adjunction -/
  homEquiv_unit : ∀ {X Y f}, (homEquiv X Y) f = unit.app X ≫ G.map f := by aesop_cat
  /-- The relationship between the counit and hom set equivalence of an adjunction -/
  homEquiv_counit : ∀ {X Y g}, (homEquiv X Y).symm g = F.map g ≫ counit.app Y := by aesop_cat
Core Data for Adjunction Construction
Informal description
The structure `CoreHomEquivUnitCounit` provides auxiliary data for constructing adjunctions between functors `F : C ⥤ D` and `G : D ⥤ C`. It consists of a natural bijection between hom-sets `homEquiv` (for each `X : C` and `Y : D`, a bijection `(F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)`), along with natural transformations `unit : 𝟭 C ⟶ F ⋙ G` and `counit : G ⋙ F ⟶ 𝟭 D`, satisfying certain coherence conditions.
CategoryTheory.Adjunction.CoreHomEquiv structure
(F : C ⥤ D) (G : D ⥤ C)
Full source 
/-- This is an auxiliary data structure useful for constructing adjunctions.
See `Adjunction.mkOfHomEquiv`.
This structure won't typically be used anywhere else.
-/
structure CoreHomEquiv (F : C ⥤ D) (G : D ⥤ C) where
  /-- The equivalence between `Hom (F X) Y` and `Hom X (G Y)` -/
  homEquiv : ∀ X Y, (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
  /-- The property that describes how `homEquiv.symm` transforms compositions `X' ⟶ X ⟶ G Y` -/
  homEquiv_naturality_left_symm :
    ∀ {X' X Y} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
      (homEquiv X' Y).symm (f ≫ g) = F.map f ≫ (homEquiv X Y).symm g := by
    aesop_cat
  /-- The property that describes how `homEquiv` transforms compositions `F X ⟶ Y ⟶ Y'` -/
  homEquiv_naturality_right :
    ∀ {X Y Y'} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
      (homEquiv X Y') (f ≫ g) = (homEquiv X Y) f ≫ G.map g := by
    aesop_cat
Core Hom-Set Equivalence for Adjunctions
Informal description
The structure `CoreHomEquiv` provides the data of a hom-set equivalence between the functors `F : C ⥤ D` and `G : D ⥤ C`, which is an auxiliary construction used to build adjunctions. Specifically, it consists of a natural bijection between the hom-sets `Hom(F(X), Y)` and `Hom(X, G(Y))` for all objects `X` in `C` and `Y` in `D`.
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left theorem
(f : X' ⟶ X) (g : F.obj X ⟶ Y) : (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g
Full source 
theorem homEquiv_naturality_left (f : X' ⟶ X) (g : F.obj X ⟶ Y) :
    (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g := by
  rw [← Equiv.eq_symm_apply]; simp
Naturality of Hom-Set Equivalence in Left Argument for Adjunctions
Informal description
For an adjunction between functors $F \colon C \to D$ and $G \colon D \to C$ with hom-set equivalence $\text{homEquiv}$, given a morphism $f \colon X' \to X$ in $C$ and a morphism $g \colon F(X) \to Y$ in $D$, the following naturality condition holds: \[ \text{homEquiv}_{X', Y}(F(f) \circ g) = f \circ \text{homEquiv}_{X, Y}(g). \]
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm theorem
(f : X ⟶ G.obj Y) (g : Y ⟶ Y') : (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g
Full source 
theorem homEquiv_naturality_right_symm (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
    (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g := by
  rw [Equiv.symm_apply_eq]; simp
Naturality of Inverse Hom-Set Equivalence in Right Argument for Adjunctions
Informal description
For an adjunction between functors $F \colon C \to D$ and $G \colon D \to C$ with hom-set equivalence $\text{homEquiv}$, given a morphism $f \colon X \to G(Y)$ in $C$ and a morphism $g \colon Y \to Y'$ in $D$, the following naturality condition holds for the inverse of the hom-set equivalence: \[ \text{homEquiv}^{-1}_{X, Y'}(f \circ G(g)) = \text{homEquiv}^{-1}_{X, Y}(f) \circ g. \]
CategoryTheory.Adjunction.CoreUnitCounit structure
(F : C ⥤ D) (G : D ⥤ C)
Full source 
/-- This is an auxiliary data structure useful for constructing adjunctions.
See `Adjunction.mkOfUnitCounit`.
This structure won't typically be used anywhere else.
-/
structure CoreUnitCounit (F : C ⥤ D) (G : D ⥤ C) where
  /-- The unit of an adjunction between `F` and `G` -/
  unit : 𝟭𝟭 C ⟶ F.comp G
  /-- The counit of an adjunction between `F` and `G`s -/
  counit : G.comp F ⟶ 𝟭 D
  /-- Equality of the composition of the unit, associator, and counit with the identity
  `F ⟶ (F G) F ⟶ F (G F) ⟶ F = NatTrans.id F` -/
  left_triangle :
    whiskerRightwhiskerRight unit F ≫ (Functor.associator F G F).hom ≫ whiskerLeft F counit =
      NatTrans.id (𝟭𝟭 C ⋙ F) := by
    aesop_cat
  /-- Equality of the composition of the unit, associator, and counit with the identity
  `G ⟶ G (F G) ⟶ (F G) F ⟶ G = NatTrans.id G` -/
  right_triangle :
    whiskerLeftwhiskerLeft G unit ≫ (Functor.associator G F G).inv ≫ whiskerRight counit G =
      NatTrans.id (G ⋙ 𝟭 C) := by
    aesop_cat
Adjunction Core Data (Unit and Counit)
Informal description
The structure `CoreUnitCounit` provides auxiliary data for constructing adjunctions between functors `F : C ⥤ D` and `G : D ⥤ C`, consisting of a unit natural transformation and a counit natural transformation. This structure is typically used internally in the construction of adjunctions and is not meant for general use.
CategoryTheory.Adjunction.mk' definition
(adj : CoreHomEquivUnitCounit F G) : F ⊣ G
Full source 
/--
Construct an adjunction from the data of a `CoreHomEquivUnitCounit`, i.e. a hom set
equivalence, unit and counit natural transformations together with proofs of the equalities
`homEquiv_unit` and `homEquiv_counit` relating them to each other.
-/
@[simps]
def mk' (adj : CoreHomEquivUnitCounit F G) : F ⊣ G where
  unit := adj.unit
  counit := adj.counit
  left_triangle_components X := by
    rw [← adj.homEquiv_counit, (adj.homEquiv _ _).symm_apply_eq, adj.homEquiv_unit]
    simp
  right_triangle_components Y := by
    rw [← adj.homEquiv_unit, ← (adj.homEquiv _ _).eq_symm_apply, adj.homEquiv_counit]
    simp
Construction of adjunction from hom-set equivalence, unit, and counit
Informal description
Given a `CoreHomEquivUnitCounit` structure for functors \( F \colon C \to D \) and \( G \colon D \to C \), consisting of: - A natural bijection \(\text{homEquiv} \colon \text{Hom}_D(FX, Y) \cong \text{Hom}_C(X, GY)\) for all \(X \in C\) and \(Y \in D\), - A unit natural transformation \(\eta \colon \text{id}_C \Rightarrow G \circ F\), - A counit natural transformation \(\epsilon \colon F \circ G \Rightarrow \text{id}_D\), - Proofs that \(\text{homEquiv}\) relates \(\eta\) and \(\epsilon\) via the conditions \(\text{homEquiv}(\epsilon_{FX} \circ F(\eta_X)) = \text{id}_{G(FX)}\) and \(\text{homEquiv}^{-1}(G(\epsilon_Y) \circ \eta_{GY}) = \text{id}_{F(GY)}\), the function constructs an adjunction \( F \dashv G \).
CategoryTheory.Adjunction.mk'_homEquiv theorem
(adj : CoreHomEquivUnitCounit F G) : (mk' adj).homEquiv = adj.homEquiv
Full source 
lemma mk'_homEquiv (adj : CoreHomEquivUnitCounit F G) : (mk' adj).homEquiv = adj.homEquiv := by
  ext
  rw [homEquiv_unit, adj.homEquiv_unit, mk'_unit]
Hom-set Equivalence Preservation in Adjunction Construction via `mk'`
Informal description
Given an adjunction constructed via `mk'` from a `CoreHomEquivUnitCounit` structure for functors $F \colon C \to D$ and $G \colon D \to C$, the hom-set equivalence of the resulting adjunction is equal to the hom-set equivalence provided in the original structure. That is, if $\text{adj}$ is a `CoreHomEquivUnitCounit` structure, then $(\text{mk' adj}).\text{homEquiv} = \text{adj}.\text{homEquiv}$.
CategoryTheory.Adjunction.mkOfHomEquiv definition
(adj : CoreHomEquiv F G) : F ⊣ G
Full source 
/-- Construct an adjunction between `F` and `G` out of a natural bijection between each
`F.obj X ⟶ Y` and `X ⟶ G.obj Y`. -/
@[simps!]
def mkOfHomEquiv (adj : CoreHomEquiv F G) : F ⊣ G :=
  mk' {
    unit :=
      { app := fun X => (adj.homEquiv X (F.obj X)) (𝟙 (F.obj X))
        naturality := by
          intros
          simp [← adj.homEquiv_naturality_left, ← adj.homEquiv_naturality_right] }
    counit :=
      { app := fun Y => (adj.homEquiv _ _).invFun (𝟙 (G.obj Y))
        naturality := by
          intros
          simp [← adj.homEquiv_naturality_left_symm, ← adj.homEquiv_naturality_right_symm] }
    homEquiv := adj.homEquiv
    homEquiv_unit := fun {X Y f} => by simp [← adj.homEquiv_naturality_right]
    homEquiv_counit := fun {X Y f} => by simp [← adj.homEquiv_naturality_left_symm] }
Adjunction from hom-set equivalence
Informal description
Given a natural bijection $\text{Hom}_D(F(X), Y) \cong \text{Hom}_C(X, G(Y))$ for all objects $X$ in category $C$ and $Y$ in category $D$, this constructs an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$. The unit and counit natural transformations are derived from this bijection by applying it to identity morphisms.
CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv theorem
(adj : CoreHomEquiv F G) : (mkOfHomEquiv adj).homEquiv = adj.homEquiv
Full source 
@[simp]
lemma mkOfHomEquiv_homEquiv (adj : CoreHomEquiv F G) :
    (mkOfHomEquiv adj).homEquiv = adj.homEquiv := by
  ext X Y g
  simp [mkOfHomEquiv, ← adj.homEquiv_naturality_right (𝟙 _) g]
Hom-set equivalence preservation in adjunction construction
Informal description
Given a natural bijection $\text{Hom}_D(F(X), Y) \cong \text{Hom}_C(X, G(Y))$ for all objects $X$ in category $C$ and $Y$ in category $D$, the hom-set equivalence constructed by `mkOfHomEquiv adj` is equal to the original hom-set equivalence $\text{adj.homEquiv}$.
CategoryTheory.Adjunction.mkOfUnitCounit definition
(adj : CoreUnitCounit F G) : F ⊣ G
Full source 
/-- Construct an adjunction between functors `F` and `G` given a unit and counit for the adjunction
satisfying the triangle identities. -/
@[simps!]
def mkOfUnitCounit (adj : CoreUnitCounit F G) : F ⊣ G where
  unit := adj.unit
  counit := adj.counit
  left_triangle_components X := by
    have := adj.left_triangle
    rw [NatTrans.ext_iff, funext_iff] at this
    simpa [-CoreUnitCounit.left_triangle] using this X
  right_triangle_components Y := by
    have := adj.right_triangle
    rw [NatTrans.ext_iff, funext_iff] at this
    simpa [-CoreUnitCounit.right_triangle] using this Y
Adjunction from unit and counit natural transformations
Informal description
Given a structure `CoreUnitCounit` containing natural transformations $\eta \colon \text{id}_C \Rightarrow G \circ F$ (the unit) and $\epsilon \colon F \circ G \Rightarrow \text{id}_D$ (the counit) satisfying the triangle identities, this constructs an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$.
CategoryTheory.Adjunction.id definition
: 𝟭 C ⊣ 𝟭 C
Full source 
/-- The adjunction between the identity functor on a category and itself. -/
def id : 𝟭𝟭 C ⊣ 𝟭 C where
  unit := 𝟙 _
  counit := 𝟙 _

-- Satisfy the inhabited linter.
Adjunction of the identity functor with itself
Informal description
The adjunction between the identity functor $\text{id}_C$ on a category $C$ and itself, where both the unit $\eta \colon \text{id}_C \Rightarrow \text{id}_C$ and the counit $\epsilon \colon \text{id}_C \Rightarrow \text{id}_C$ are given by the identity natural transformation.
CategoryTheory.Adjunction.instInhabitedId instance
: Inhabited (Adjunction (𝟭 C) (𝟭 C))
Full source 
instance : Inhabited (Adjunction (𝟭 C) (𝟭 C)) :=
  ⟨id⟩
Trivial Adjunction of the Identity Functor
Informal description
The identity functor $\text{id}_C$ on a category $C$ is trivially adjoint to itself, with both the unit and counit being the identity natural transformations.
CategoryTheory.Adjunction.equivHomsetLeftOfNatIso definition
{F F' : C ⥤ D} (iso : F ≅ F') {X : C} {Y : D} : (F.obj X ⟶ Y) ≃ (F'.obj X ⟶ Y)
Full source 
/-- If F and G are naturally isomorphic functors, establish an equivalence of hom-sets. -/
@[simps]
def equivHomsetLeftOfNatIso {F F' : C ⥤ D} (iso : F ≅ F') {X : C} {Y : D} :
    (F.obj X ⟶ Y) ≃ (F'.obj X ⟶ Y) where
  toFun f := iso.inv.app _ ≫ f
  invFun g := iso.hom.app _ ≫ g
  left_inv f := by simp
  right_inv g := by simp
Hom-set equivalence for naturally isomorphic left adjoints
Informal description
Given two naturally isomorphic functors \( F, F' : \mathcal{C} \to \mathcal{D} \) with a natural isomorphism \( \text{iso} : F \cong F' \), and objects \( X \in \mathcal{C} \), \( Y \in \mathcal{D} \), there is a bijection between the hom-sets \( \text{Hom}(F(X), Y) \) and \( \text{Hom}(F'(X), Y) \). The bijection is given by composing with the natural isomorphism components: a morphism \( f : F(X) \to Y \) is mapped to \( \text{iso}^{-1}_X \cdot f \), and its inverse maps \( g : F'(X) \to Y \) to \( \text{iso}_X \cdot g \).
CategoryTheory.Adjunction.equivHomsetRightOfNatIso definition
{G G' : D ⥤ C} (iso : G ≅ G') {X : C} {Y : D} : (X ⟶ G.obj Y) ≃ (X ⟶ G'.obj Y)
Full source 
/-- If G and H are naturally isomorphic functors, establish an equivalence of hom-sets. -/
@[simps]
def equivHomsetRightOfNatIso {G G' : D ⥤ C} (iso : G ≅ G') {X : C} {Y : D} :
    (X ⟶ G.obj Y) ≃ (X ⟶ G'.obj Y) where
  toFun f := f ≫ iso.hom.app _
  invFun g := g ≫ iso.inv.app _
  left_inv f := by simp
  right_inv g := by simp
Hom-set equivalence for naturally isomorphic right adjoints
Informal description
Given two naturally isomorphic functors $G, G' : D \to C$ with a natural isomorphism $\text{iso} : G \cong G'$, and objects $X \in C$, $Y \in D$, there is a bijection between the hom-sets $\text{Hom}(X, G(Y))$ and $\text{Hom}(X, G'(Y))$. The bijection is given by composing with the natural isomorphism components: a morphism $f : X \to G(Y)$ is mapped to $f \cdot \text{iso}_Y$, and its inverse maps $g : X \to G'(Y)$ to $g \cdot \text{iso}^{-1}_Y$.
CategoryTheory.Adjunction.ofNatIsoLeft definition
{F G : C ⥤ D} {H : D ⥤ C} (adj : F ⊣ H) (iso : F ≅ G) : G ⊣ H
Full source 
/-- Transport an adjunction along a natural isomorphism on the left. -/
def ofNatIsoLeft {F G : C ⥤ D} {H : D ⥤ C} (adj : F ⊣ H) (iso : F ≅ G) : G ⊣ H :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun X Y => (equivHomsetLeftOfNatIso iso.symm).trans (adj.homEquiv X Y) }
Adjunction transport along left natural isomorphism
Informal description
Given an adjunction $F \dashv H$ between functors $F \colon C \to D$ and $H \colon D \to C$, and a natural isomorphism $\text{iso} \colon F \cong G$ between $F$ and another functor $G \colon C \to D$, this constructs a new adjunction $G \dashv H$. The hom-set equivalence for this adjunction is obtained by composing the inverse of the hom-set equivalence induced by $\text{iso}$ with the original adjunction's hom-set equivalence.
CategoryTheory.Adjunction.ofNatIsoRight definition
{F : C ⥤ D} {G H : D ⥤ C} (adj : F ⊣ G) (iso : G ≅ H) : F ⊣ H
Full source 
/-- Transport an adjunction along a natural isomorphism on the right. -/
def ofNatIsoRight {F : C ⥤ D} {G H : D ⥤ C} (adj : F ⊣ G) (iso : G ≅ H) : F ⊣ H :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun X Y => (adj.homEquiv X Y).trans (equivHomsetRightOfNatIso iso) }
Transport of adjunction along natural isomorphism of right adjoints
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, and a natural isomorphism $\text{iso} \colon G \cong H$ between functors $G, H \colon D \to C$, this constructs a new adjunction $F \dashv H$. The hom-set equivalence for the new adjunction is obtained by composing the original adjunction's hom-set equivalence with the bijection induced by the natural isomorphism $\text{iso}$ on the right adjoint side.
CategoryTheory.Adjunction.compYonedaIso definition
{C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₁} D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : G ⋙ yoneda ≅ yoneda ⋙ (whiskeringLeft _ _ _).obj F.op
Full source 
/-- The isomorpism which an adjunction `F ⊣ G` induces on `G ⋙ yoneda`. This states that
`Adjunction.homEquiv` is natural in both arguments. -/
@[simps!]
def compYonedaIso {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₁} D]
    {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
    G ⋙ yonedaG ⋙ yoneda ≅ yoneda ⋙ (whiskeringLeft _ _ _).obj F.op :=
  NatIso.ofComponents fun X => NatIso.ofComponents fun Y => (adj.homEquiv Y.unop X).toIso.symm
Natural isomorphism of Yoneda embeddings under adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, there is a natural isomorphism between the functors $G \circ \mathrm{yoneda}$ and $\mathrm{yoneda} \circ \mathrm{whiskeringLeft}\, F^{\mathrm{op}}$, where: - $\mathrm{yoneda}$ is the Yoneda embedding functor, - $\mathrm{whiskeringLeft}\, F^{\mathrm{op}}$ is the left whiskering functor applied to the opposite functor of $F$. This isomorphism is constructed componentwise using the hom-set equivalence induced by the adjunction, demonstrating the naturality of the adjunction's hom-set bijection in both arguments.
CategoryTheory.Adjunction.compCoyonedaIso definition
{C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₁} D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : F.op ⋙ coyoneda ≅ coyoneda ⋙ (whiskeringLeft _ _ _).obj G
Full source 
/-- The isomorpism which an adjunction `F ⊣ G` induces on `F.op ⋙ coyoneda`. This states that
`Adjunction.homEquiv` is natural in both arguments. -/
@[simps!]
def compCoyonedaIso {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₁} D]
    {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
    F.op ⋙ coyonedaF.op ⋙ coyoneda ≅ coyoneda ⋙ (whiskeringLeft _ _ _).obj G :=
  NatIso.ofComponents fun X => NatIso.ofComponents fun Y => (adj.homEquiv X.unop Y).toIso
Natural isomorphism of co-Yoneda embeddings under adjunction
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, there is a natural isomorphism between the functors $F^{\mathrm{op}} \circ \mathrm{coyoneda}$ and $\mathrm{coyoneda} \circ \mathrm{whiskeringLeft}\, G$, where: - $F^{\mathrm{op}}$ is the opposite functor of $F$, - $\mathrm{coyoneda}$ is the co-Yoneda embedding functor, - $\mathrm{whiskeringLeft}\, G$ is the left whiskering functor applied to $G$. This isomorphism is constructed componentwise using the hom-set equivalence induced by the adjunction, and it demonstrates the naturality of the adjunction's hom-set bijection in both arguments.
CategoryTheory.Adjunction.comp definition
: F ⋙ H ⊣ I ⋙ G
Full source 
/-- Composition of adjunctions. -/
@[simps! -isSimp unit counit, stacks 0DV0]
def comp : F ⋙ HF ⋙ H ⊣ I ⋙ G :=
  mk' {
    homEquiv := fun _ _ ↦ Equiv.trans (adj₂.homEquiv _ _) (adj₁.homEquiv _ _)
    unit := adj₁.unit ≫ whiskerRight (F.rightUnitor.inv ≫ whiskerLeft F adj₂.unit ≫
      (Functor.associator _ _ _ ).inv) G ≫ (Functor.associator _ _ _).hom
    counit := (Functor.associator _ _ _ ).inv ≫ whiskerRight ((Functor.associator _ _ _ ).hom ≫
      whiskerLeft _ adj₁.counit ≫ I.rightUnitor.hom) _ ≫ adj₂.counit }
Composition of adjunctions
Informal description
Given adjunctions $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, and $H \dashv I$ between functors $H \colon D \to E$ and $I \colon E \to D$, their composition forms an adjunction $F \circ H \dashv I \circ G$ between the composed functors. The adjunction is constructed with: 1. A hom-set equivalence given by composing the equivalences from both adjunctions: $\text{Hom}_E(H(F(X)), Y) \cong \text{Hom}_D(F(X), I(Y)) \cong \text{Hom}_C(X, G(I(Y)))$ 2. A unit natural transformation obtained by composing the units of both adjunctions with appropriate whiskerings and associators 3. A counit natural transformation obtained by composing the counits of both adjunctions with appropriate whiskerings and associators
CategoryTheory.Adjunction.comp_unit_app theorem
(X : C) : (adj₁.comp adj₂).unit.app X = adj₁.unit.app X ≫ G.map (adj₂.unit.app (F.obj X))
Full source 
@[simp, reassoc]
lemma comp_unit_app (X : C) :
    (adj₁.comp adj₂).unit.app X = adj₁.unit.app X ≫ G.map (adj₂.unit.app (F.obj X)) := by
  simp [Adjunction.comp]
Component formula for unit of composed adjunction
Informal description
For any object $X$ in category $C$, the component of the unit natural transformation for the composed adjunction $(F \circ H) \dashv (I \circ G)$ at $X$ is given by the composition of: 1. The component of the unit of the first adjunction $F \dashv G$ at $X$, and 2. The image under $G$ of the component of the unit of the second adjunction $H \dashv I$ at $F(X)$. That is, $(\text{adj}_1 \circ \text{adj}_2).\text{unit}_X = \text{adj}_1.\text{unit}_X \circ G(\text{adj}_2.\text{unit}_{F(X)})$.
CategoryTheory.Adjunction.comp_counit_app theorem
(X : E) : (adj₁.comp adj₂).counit.app X = H.map (adj₁.counit.app (I.obj X)) ≫ adj₂.counit.app X
Full source 
@[simp, reassoc]
lemma comp_counit_app (X : E) :
    (adj₁.comp adj₂).counit.app X = H.map (adj₁.counit.app (I.obj X)) ≫ adj₂.counit.app X := by
  simp [Adjunction.comp]
Composition of Adjunctions: Formula for Counit Component
Informal description
For any object $X$ in category $E$, the counit of the composed adjunction $(F \circ H) \dashv (I \circ G)$ at $X$ is given by the composition: \[ (\text{adj}_1 \circ \text{adj}_2).\text{counit}_X = H(\text{adj}_1.\text{counit}_{I(X)}) \circ \text{adj}_2.\text{counit}_X \] where $\text{adj}_1 \colon F \dashv G$ and $\text{adj}_2 \colon H \dashv I$ are the component adjunctions.
CategoryTheory.Adjunction.comp_homEquiv theorem
: (adj₁.comp adj₂).homEquiv = fun _ _ ↦ Equiv.trans (adj₂.homEquiv _ _) (adj₁.homEquiv _ _)
Full source 
lemma comp_homEquiv :  (adj₁.comp adj₂).homEquiv =
    fun _ _ ↦ Equiv.trans (adj₂.homEquiv _ _) (adj₁.homEquiv _ _) :=
  mk'_homEquiv _
Composition of adjunctions preserves hom-set equivalence
Informal description
Given adjunctions $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, and $H \dashv I$ between functors $H \colon D \to E$ and $I \colon E \to D$, the hom-set equivalence of their composition $(F \circ H) \dashv (I \circ G)$ is given by the composition of hom-set equivalences: \[ \text{Hom}_E(H(F(X)), Y) \simeq \text{Hom}_D(F(X), I(Y)) \simeq \text{Hom}_C(X, G(I(Y))) \] for all objects $X$ in $C$ and $Y$ in $E$.
CategoryTheory.Adjunction.leftAdjointOfEquiv definition
(he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g) : C ⥤ D
Full source 
/-- Construct a left adjoint functor to `G`, given the functor's value on objects `F_obj` and
a bijection `e` between `F_obj X ⟶ Y` and `X ⟶ G.obj Y` satisfying a naturality law
`he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g`.
Dual to `rightAdjointOfEquiv`. -/
@[simps!]
def leftAdjointOfEquiv (he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g) : C ⥤ D where
  obj := F_obj
  map {X} {X'} f := (e X (F_obj X')).symm (f ≫ e X' (F_obj X') (𝟙 _))
  map_comp := fun f f' => by
    rw [Equiv.symm_apply_eq, he, Equiv.apply_symm_apply]
    conv =>
      rhs
      rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
    simp
Construction of Left Adjoint from Object Mapping and Natural Bijection
Informal description
Given a functor \( G : D \to C \), a function \( F_{\text{obj}} \) mapping objects of \( C \) to objects of \( D \), and a family of bijections \( e(X, Y) : \text{Hom}_D(F_{\text{obj}} X, Y) \simeq \text{Hom}_C(X, G Y) \) that is natural in \( Y \) (i.e., for all \( X, Y, Y' \), \( g : Y \to Y' \), and \( h : F_{\text{obj}} X \to Y \), the equation \( e(X, Y') (h \circ g) = e(X, Y) h \circ G g \) holds), this constructs a left adjoint functor \( F : C \to D \) to \( G \). The functor \( F \) is defined on objects by \( F_{\text{obj}} \) and on morphisms by \( F f = e(X, F_{\text{obj}} X')^{-1}(f \circ e(X', F_{\text{obj}} X') \text{id}) \).
CategoryTheory.Adjunction.adjunctionOfEquivLeft definition
: leftAdjointOfEquiv e he ⊣ G
Full source 
/-- Show that the functor given by `leftAdjointOfEquiv` is indeed left adjoint to `G`. Dual
to `adjunctionOfRightEquiv`. -/
@[simps!]
def adjunctionOfEquivLeft : leftAdjointOfEquivleftAdjointOfEquiv e he ⊣ G :=
  mkOfHomEquiv
    { homEquiv := e
      homEquiv_naturality_left_symm := fun {X'} {X} {Y} f g => by
        have {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
            (e X Y').symm (f ≫ G.map g) = (e X Y).symm f ≫ g := by
          rw [Equiv.symm_apply_eq, he]; simp
        simp [← this, ← Equiv.apply_eq_iff_eq (e X' Y), ← he] }
Adjunction from left adjoint construction via natural bijection
Informal description
Given a functor \( G : D \to C \), an object function \( F_{\text{obj}} : C \to D \), and a family of bijections \( e(X, Y) : \text{Hom}_D(F_{\text{obj}} X, Y) \simeq \text{Hom}_C(X, G Y) \) that is natural in \( Y \) (i.e., for all \( X, Y, Y' \), \( g : Y \to Y' \), and \( h : F_{\text{obj}} X \to Y \), the equation \( e(X, Y') (h \circ g) = e(X, Y) h \circ G g \) holds), the functor \( F \) constructed by `leftAdjointOfEquiv` is indeed left adjoint to \( G \). This adjunction is witnessed by the natural bijection \( e \).
CategoryTheory.Adjunction.rightAdjointOfEquiv definition
(he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g) : D ⥤ C
Full source 
/-- Construct a right adjoint functor to `F`, given the functor's value on objects `G_obj` and
a bijection `e` between `F.obj X ⟶ Y` and `X ⟶ G_obj Y` satisfying a naturality law
`he : ∀ X Y Y' g h, e X' Y (F.map f ≫ g) = f ≫ e X Y g`.
Dual to `leftAdjointOfEquiv`. -/
@[simps!]
def rightAdjointOfEquiv (he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g) : D ⥤ C where
  obj := G_obj
  map {Y} {Y'} g := (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 _) ≫ g)
  map_comp := fun {Y} {Y'} {Y''} g g' => by
    rw [← Equiv.eq_symm_apply, ← he'' e he, Equiv.symm_apply_apply]
    conv =>
      rhs
      rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
    simp
Construction of a right adjoint functor via natural bijection
Informal description
Given a functor \( F : C \to D \), an object function \( G_{\text{obj}} : D \to C \), and a natural bijection \( e \) between morphisms \( F(X) \to Y \) in \( D \) and morphisms \( X \to G_{\text{obj}}(Y) \) in \( C \) satisfying the naturality condition \( e_{X'Y}(F(f) \circ g) = f \circ e_{XY}(g) \) for all \( f : X \to X' \) and \( g : F(X') \to Y \), this constructs a right adjoint functor \( G : D \to C \) to \( F \). The functor \( G \) is defined on objects by \( G_{\text{obj}} \) and on morphisms by \( G(g) = e_{G_{\text{obj}}(Y)Y'}(\text{id}_{G_{\text{obj}}(Y)} \circ g) \).
CategoryTheory.Adjunction.adjunctionOfEquivRight definition
(he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g) : F ⊣ (rightAdjointOfEquiv e he)
Full source 
/-- Show that the functor given by `rightAdjointOfEquiv` is indeed right adjoint to `F`. Dual
to `adjunctionOfEquivRight`. -/
@[simps!]
def adjunctionOfEquivRight (he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g) :
    F ⊣ (rightAdjointOfEquiv e he) :=
  mkOfHomEquiv
    { homEquiv := e
      homEquiv_naturality_left_symm := by
        intro X X' Y f g; rw [Equiv.symm_apply_eq]; simp [he]
      homEquiv_naturality_right := by
        intro X Y Y' g h
        simp [← he, reassoc_of% (he'' e)] }
Adjunction from natural bijection with right adjoint construction
Informal description
Given a functor $F \colon C \to D$, an object function $G_{\text{obj}} \colon D \to C$, and a natural bijection $e$ between morphisms $F(X) \to Y$ in $D$ and morphisms $X \to G_{\text{obj}}(Y)$ in $C$ satisfying the naturality condition $e_{X'Y}(F(f) \circ g) = f \circ e_{XY}(g)$ for all $f \colon X \to X'$ and $g \colon F(X') \to Y$, this constructs an adjunction $F \dashv G$ where $G$ is the right adjoint functor obtained from $G_{\text{obj}}$ via `rightAdjointOfEquiv`. The adjunction is built using the hom-set equivalence $e$ and its naturality properties.
CategoryTheory.Adjunction.toEquivalence definition
(adj : F ⊣ G) [∀ X, IsIso (adj.unit.app X)] [∀ Y, IsIso (adj.counit.app Y)] : C ≌ D
Full source 
/--
If the unit and counit of a given adjunction are (pointwise) isomorphisms, then we can upgrade the
adjunction to an equivalence.
-/
@[simps!]
noncomputable def toEquivalence (adj : F ⊣ G) [∀ X, IsIso (adj.unit.app X)]
    [∀ Y, IsIso (adj.counit.app Y)] : C ≌ D where
  functor := F
  inverse := G
  unitIso := NatIso.ofComponents fun X => asIso (adj.unit.app X)
  counitIso := NatIso.ofComponents fun Y => asIso (adj.counit.app Y)
Equivalence from adjunction with invertible unit and counit
Informal description
Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, if the unit $\eta_X \colon X \to GFX$ and counit $\epsilon_Y \colon FGY \to Y$ are isomorphisms for all objects $X$ in $C$ and $Y$ in $D$, then the adjunction can be upgraded to an equivalence of categories $C \simeq D$. Here, $F$ serves as the equivalence functor, $G$ as its inverse, and the unit and counit become natural isomorphisms.
CategoryTheory.Functor.isEquivalence_of_isRightAdjoint theorem
(G : C ⥤ D) [IsRightAdjoint G] [∀ X, IsIso ((Adjunction.ofIsRightAdjoint G).unit.app X)] [∀ Y, IsIso ((Adjunction.ofIsRightAdjoint G).counit.app Y)] : G.IsEquivalence
Full source 
/--
If the unit and counit for the adjunction corresponding to a right adjoint functor are (pointwise)
isomorphisms, then the functor is an equivalence of categories.
-/
lemma Functor.isEquivalence_of_isRightAdjoint (G : C ⥤ D) [IsRightAdjoint G]
    [∀ X, IsIso ((Adjunction.ofIsRightAdjoint G).unit.app X)]
    [∀ Y, IsIso ((Adjunction.ofIsRightAdjoint G).counit.app Y)] : G.IsEquivalence :=
  (Adjunction.ofIsRightAdjoint G).toEquivalence.isEquivalence_inverse
Right adjoint functor with invertible unit and counit is an equivalence
Informal description
Let $G \colon C \to D$ be a functor that is a right adjoint (i.e., there exists a left adjoint functor $F \colon D \to C$ such that $F \dashv G$). If for every object $X$ in $C$ the unit morphism $\eta_X \colon X \to GFX$ is an isomorphism, and for every object $Y$ in $D$ the counit morphism $\epsilon_Y \colon FGY \to Y$ is an isomorphism, then $G$ is an equivalence of categories.
CategoryTheory.Equivalence.toAdjunction definition
: e.functor ⊣ e.inverse
Full source 
/-- The adjunction given by an equivalence of categories. (To obtain the opposite adjunction,
simply use `e.symm.toAdjunction`. -/
@[simps]
def toAdjunction : e.functor ⊣ e.inverse where
  unit := e.unit
  counit := e.counit
Adjunction from equivalence of categories
Informal description
Given an equivalence of categories $e \colon C \simeq D$, the adjunction $e.\text{functor} \dashv e.\text{inverse}$ is constructed using the unit $\eta \colon \text{id}_C \Rightarrow e.\text{functor} \circ e.\text{inverse}$ and counit $\epsilon \colon e.\text{inverse} \circ e.\text{functor} \Rightarrow \text{id}_D$ natural transformations from the equivalence data.
CategoryTheory.Equivalence.isLeftAdjoint_functor theorem
: e.functor.IsLeftAdjoint
Full source 
lemma isLeftAdjoint_functor : e.functor.IsLeftAdjoint where
  exists_rightAdjoint := ⟨_, ⟨e.toAdjunction⟩⟩
Functor in an equivalence is a left adjoint
Informal description
For any equivalence of categories $e \colon C \simeq D$, the functor $e.\text{functor} \colon C \to D$ is a left adjoint.
CategoryTheory.Equivalence.isRightAdjoint_inverse theorem
: e.inverse.IsRightAdjoint
Full source 
lemma isRightAdjoint_inverse : e.inverse.IsRightAdjoint where
  exists_leftAdjoint := ⟨_, ⟨e.toAdjunction⟩⟩
Inverse of an equivalence is right adjoint
Informal description
For any equivalence of categories $e \colon C \simeq D$, the inverse functor $e^{-1} \colon D \to C$ is a right adjoint functor.
CategoryTheory.Equivalence.isLeftAdjoint_inverse theorem
: e.inverse.IsLeftAdjoint
Full source 
lemma isLeftAdjoint_inverse : e.inverse.IsLeftAdjoint :=
  e.symm.isLeftAdjoint_functor
Inverse Functor in Equivalence is Left Adjoint
Informal description
For any equivalence of categories $e \colon C \simeq D$, the inverse functor $e^{-1} \colon D \to C$ is a left adjoint functor.
CategoryTheory.Equivalence.isRightAdjoint_functor theorem
: e.functor.IsRightAdjoint
Full source 
lemma isRightAdjoint_functor : e.functor.IsRightAdjoint :=
  e.symm.isRightAdjoint_inverse
Functor of an equivalence is right adjoint
Informal description
For any equivalence of categories $e \colon C \simeq D$, the functor $e.\text{functor} \colon C \to D$ is a right adjoint functor.
CategoryTheory.Equivalence.refl_toAdjunction theorem
: (refl (C := C)).toAdjunction = Adjunction.id
Full source 
lemma refl_toAdjunction : (refl (C := C)).toAdjunction = Adjunction.id := rfl
Adjunction from Reflexive Equivalence Equals Identity Adjunction
Informal description
The adjunction derived from the reflexive equivalence of a category $C$ is equal to the adjunction of the identity functor with itself, i.e., $(\text{refl} \colon C \simeq C).\text{toAdjunction} = \text{Adjunction.id}$.
CategoryTheory.Equivalence.trans_toAdjunction theorem
{E : Type*} [Category E] (e' : D ≌ E) : (e.trans e').toAdjunction = e.toAdjunction.comp e'.toAdjunction
Full source 
lemma trans_toAdjunction {E : Type*} [Category E] (e' : D ≌ E) :
    (e.trans e').toAdjunction = e.toAdjunction.comp e'.toAdjunction := rfl
Composition of Equivalences Preserves Adjunction Composition
Informal description
Given an equivalence of categories $e \colon C \simeq D$ and another equivalence $e' \colon D \simeq E$, the adjunction obtained from the composition $e \circ e'$ is equal to the composition of the adjunctions obtained from $e$ and $e'$ individually. That is, $(e \circ e').\text{toAdjunction} = e.\text{toAdjunction} \circ e'.\text{toAdjunction}$.
CategoryTheory.Functor.isLeftAdjoint_comp instance
{E : Type u₃} [Category.{v₃} E] (F : C ⥤ D) (G : D ⥤ E) [F.IsLeftAdjoint] [G.IsLeftAdjoint] : (F ⋙ G).IsLeftAdjoint
Full source 
/-- If `F` and `G` are left adjoints then `F ⋙ G` is a left adjoint too. -/
instance isLeftAdjoint_comp {E : Type u₃} [Category.{v₃} E] (F : C ⥤ D) (G : D ⥤ E)
    [F.IsLeftAdjoint] [G.IsLeftAdjoint] : (F ⋙ G).IsLeftAdjoint where
  exists_rightAdjoint :=
    ⟨_, ⟨(Adjunction.ofIsLeftAdjoint F).comp (Adjunction.ofIsLeftAdjoint G)⟩⟩
Composition of Left Adjoint Functors is Left Adjoint
Informal description
The composition of two left adjoint functors $F \colon C \to D$ and $G \colon D \to E$ is again a left adjoint functor. That is, if $F$ has a right adjoint $F' \colon D \to C$ and $G$ has a right adjoint $G' \colon E \to D$, then $F \circ G$ has a right adjoint $G' \circ F'$.
CategoryTheory.Functor.isRightAdjoint_comp instance
{E : Type u₃} [Category.{v₃} E] {F : C ⥤ D} {G : D ⥤ E} [IsRightAdjoint F] [IsRightAdjoint G] : IsRightAdjoint (F ⋙ G)
Full source 
/-- If `F` and `G` are right adjoints then `F ⋙ G` is a right adjoint too. -/
instance isRightAdjoint_comp {E : Type u₃} [Category.{v₃} E] {F : C ⥤ D} {G : D ⥤ E}
    [IsRightAdjoint F] [IsRightAdjoint G] : IsRightAdjoint (F ⋙ G) where
  exists_leftAdjoint :=
    ⟨_, ⟨(Adjunction.ofIsRightAdjoint G).comp (Adjunction.ofIsRightAdjoint F)⟩⟩
Composition of Right Adjoint Functors is Right Adjoint
Informal description
If $F \colon C \to D$ and $G \colon D \to E$ are right adjoint functors, then their composition $F \circ G \colon C \to E$ is also a right adjoint functor.
CategoryTheory.Functor.isRightAdjoint_of_iso theorem
{F G : C ⥤ D} (h : F ≅ G) [F.IsRightAdjoint] : IsRightAdjoint G
Full source 
/-- Transport being a right adjoint along a natural isomorphism. -/
lemma isRightAdjoint_of_iso {F G : C ⥤ D} (h : F ≅ G) [F.IsRightAdjoint] :
    IsRightAdjoint G where
  exists_leftAdjoint := ⟨_, ⟨(Adjunction.ofIsRightAdjoint F).ofNatIsoRight h⟩⟩
Right Adjoint Property Preserved under Natural Isomorphism
Informal description
Given two functors $F, G \colon C \to D$ and a natural isomorphism $h \colon F \cong G$, if $F$ is a right adjoint functor, then $G$ is also a right adjoint functor.
CategoryTheory.Functor.isLeftAdjoint_of_iso theorem
{F G : C ⥤ D} (h : F ≅ G) [IsLeftAdjoint F] : IsLeftAdjoint G
Full source 
/-- Transport being a left adjoint along a natural isomorphism. -/
lemma isLeftAdjoint_of_iso {F G : C ⥤ D} (h : F ≅ G) [IsLeftAdjoint F] :
    IsLeftAdjoint G where
  exists_rightAdjoint := ⟨_, ⟨(Adjunction.ofIsLeftAdjoint F).ofNatIsoLeft h⟩⟩
Left adjoint property preserved under natural isomorphism
Informal description
Given two functors $F, G \colon C \to D$ and a natural isomorphism $h \colon F \cong G$, if $F$ is a left adjoint, then $G$ is also a left adjoint.
CategoryTheory.Functor.adjunction definition
(E : C ⥤ D) [IsEquivalence E] : E ⊣ E.inv
Full source 
/-- An equivalence `E` is left adjoint to its inverse. -/
noncomputable def adjunction (E : C ⥤ D) [IsEquivalence E] : E ⊣ E.inv :=
  E.asEquivalence.toAdjunction
Adjunction from an equivalence of categories
Informal description
Given an equivalence of categories $E \colon C \simeq D$, the adjunction $E \dashv E^{-1}$ is constructed, where $E^{-1}$ is the quasi-inverse functor of $E$. This adjunction consists of natural transformations $\eta \colon \text{id}_C \Rightarrow E^{-1} \circ E$ (the unit) and $\epsilon \colon E \circ E^{-1} \Rightarrow \text{id}_D$ (the counit) satisfying the triangle identities.