Theorems · Definition · category theory

CategoryTheory.Equivalence.toAdjunction

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (e : C ≌ D) → e.functor ⊣ e.inverse

The adjunction given by an equivalence of categories. (To obtain the opposite adjunction, simply use e.symm.toAdjunction.)

Defined in

Mathlib.CategoryTheory.Adjunction.Basic

Cited by

60 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category