Theorems · Inductive type · category theory

CategoryTheory.Adjunction

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor D C → Type (max (max (max u₁ u₂) v₁) v₂)

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).

Defined in

Mathlib.CategoryTheory.Adjunction.Basic

Cited by

524 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 3 definitions · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category