Adjunctions in bicategories

For 1-morphisms f : a ⟶ b and g : b ⟶ a in a bicategory, an adjunction between f and g consists of a pair of 2-morphism η : 𝟙 a ⟶ f ≫ g and ε : g ≫ f ⟶ 𝟙 b satisfying the triangle identities. The 2-morphism η is called the unit and ε is called the counit.

Main definitions

• Bicategory.Adjunction: adjunctions between two 1-morphisms.
• Bicategory.Equivalence: adjoint equivalences between two objects.
• Bicategory.mkOfAdjointifyCounit: construct an adjoint equivalence from 2-isomorphisms η : 𝟙 a ≅ f ≫ g and ε : g ≫ f ≅ 𝟙 b, by upgrading ε to a counit.

Implementation notes

The computation of 2-morphisms in the proof is done using calc blocks. Typically, the LHS and the RHS in each step of calc are related by simple rewriting up to associators and unitors. So the proof for each step should be of the form rw [...]; coherence. In practice, our proofs look like rw [...]; simp [bicategoricalComp]; coherence. The simp is not strictly necessary, but it speeds up the proof and allow us to avoid increasing the maxHeartbeats. The speedup is probably due to reducing the length of the expression e.g. by absorbing identity maps or applying the pentagon relation. Such a hack may not be necessary if the coherence tactic is improved. One possible way would be to perform such a simplification in the preprocessing of the coherence tactic.

Todo

• Bicategory.mkOfAdjointifyUnit: construct an adjoint equivalence from 2-isomorphisms η : 𝟙 a ≅ f ≫ g and ε : g ≫ f ≅ 𝟙 b, by upgrading η to a unit.

def CategoryTheory.Bicategory.leftZigzag {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ⟶ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)

The 2-morphism defined by the following pasting diagram:

a －－－－－－ ▸ a
  ＼    η      ◥   ＼
  f ＼   g  ／       ＼ f
       ◢  ／     ε      ◢
        b －－－－－－ ▸ b

def CategoryTheory.Bicategory.rightZigzag {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b) : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id a) ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id b) g

The 2-morphism defined by the following pasting diagram:

        a －－－－－－ ▸ a
       ◥  ＼     η      ◥
  g ／      ＼ f     ／ g
  ／    ε      ◢   ／
b －－－－－－ ▸ b

structure CategoryTheory.Bicategory.Adjunction {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : b ⟶ a) : Type w

• unit : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g

  The unit of an adjunction.

• counit : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b

  The counit of an adjunction.

• left_triangle : CategoryTheory.Bicategory.leftZigzag s.unit s.counit = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom (CategoryTheory.Bicategory.rightUnitor f).inv

  The composition of the unit and the counit is equal to the identity up to unitors.

• right_triangle : CategoryTheory.Bicategory.rightZigzag s.unit s.counit = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom (CategoryTheory.Bicategory.leftUnitor g).inv

  The composition of the unit and the counit is equal to the identity up to unitors.

Adjunction between two 1-morphisms.

def CategoryTheory.Bicategory.«term_⊣_» : Lean.TrailingParserDescr

Adjunction between two 1-morphisms.

def CategoryTheory.Bicategory.Adjunction.id {B : Type u} [CategoryTheory.Bicategory B] (a : B) : CategoryTheory.Bicategory.Adjunction (CategoryTheory.CategoryStruct.id a) (CategoryTheory.CategoryStruct.id a)

Adjunction between identities.

instance CategoryTheory.Bicategory.Adjunction.instInhabitedAdjunctionIdToCategoryStruct {B : Type u} [CategoryTheory.Bicategory B] {a : B} : Inhabited (CategoryTheory.Bicategory.Adjunction (CategoryTheory.CategoryStruct.id a) (CategoryTheory.CategoryStruct.id a))

def CategoryTheory.Bicategory.leftZigzagIso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ≅ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)

The isomorphism version of leftZigzag.

def CategoryTheory.Bicategory.rightZigzagIso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id b) g

The isomorphism version of rightZigzag.

@[simp]

theorem CategoryTheory.Bicategory.leftZigzagIso_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) : (CategoryTheory.Bicategory.leftZigzagIso η ε).hom = CategoryTheory.Bicategory.leftZigzag η.hom ε.hom

@[simp]

theorem CategoryTheory.Bicategory.rightZigzagIso_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) : (CategoryTheory.Bicategory.rightZigzagIso η ε).hom = CategoryTheory.Bicategory.rightZigzag η.hom ε.hom

@[simp]

theorem CategoryTheory.Bicategory.leftZigzagIso_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) : (CategoryTheory.Bicategory.leftZigzagIso η ε).inv = CategoryTheory.Bicategory.rightZigzag ε.inv η.inv

@[simp]

theorem CategoryTheory.Bicategory.rightZigzagIso_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) : (CategoryTheory.Bicategory.rightZigzagIso η ε).inv = CategoryTheory.Bicategory.leftZigzag ε.inv η.inv

@[simp]

theorem CategoryTheory.Bicategory.leftZigzagIso_symm {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) : (CategoryTheory.Bicategory.leftZigzagIso η ε).symm = CategoryTheory.Bicategory.rightZigzagIso ε.symm η.symm

@[simp]

theorem CategoryTheory.Bicategory.rightZigzagIso_symm {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) : (CategoryTheory.Bicategory.rightZigzagIso η ε).symm = CategoryTheory.Bicategory.leftZigzagIso ε.symm η.symm

def CategoryTheory.Bicategory.adjointifyCounit {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b

An auxiliary definition for mkOfAdjointifyCounit.

theorem CategoryTheory.Bicategory.adjointifyCounit_left_triangle {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) : CategoryTheory.Bicategory.leftZigzagIso η (CategoryTheory.Bicategory.adjointifyCounit η ε) = CategoryTheory.Bicategory.leftUnitor f ≪≫ (CategoryTheory.Bicategory.rightUnitor f).symm

structure CategoryTheory.Bicategory.Equivalence {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) : Type (max v w)

• hom : a ⟶ b

  A 1-morphism in one direction.

• inv : b ⟶ a

  A 1-morphism in the other direction.

• unit : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp s.hom s.inv

  The composition hom ≫ inv is isomorphic to the identity.

• counit : CategoryTheory.CategoryStruct.comp s.inv s.hom ≅ CategoryTheory.CategoryStruct.id b

  The composition inv ≫ hom is isomorphic to the identity.

• left_triangle : CategoryTheory.Bicategory.leftZigzagIso s.unit s.counit = CategoryTheory.Bicategory.leftUnitor s.hom ≪≫ (CategoryTheory.Bicategory.rightUnitor s.hom).symm

  The composition of the unit and the counit is equal to the identity up to unitors.

Adjoint equivalences between two objects.

def CategoryTheory.Bicategory.«term_≌_» : Lean.TrailingParserDescr

Adjoint equivalences between two objects.

def CategoryTheory.Bicategory.Equivalence.id {B : Type u} [CategoryTheory.Bicategory B] (a : B) : CategoryTheory.Bicategory.Equivalence a a

The identity 1-morphism is an equivalence.

instance CategoryTheory.Bicategory.Equivalence.instInhabitedEquivalence {B : Type u} [CategoryTheory.Bicategory B] {a : B} : Inhabited (CategoryTheory.Bicategory.Equivalence a a)

def CategoryTheory.Bicategory.Equivalence.mkOfAdjointifyCounit {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) : CategoryTheory.Bicategory.Equivalence a b

Construct an adjoint equivalence from 2-isomorphisms by upgrading ε to a counit.