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.

TODO

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

@[reducible, inline]

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

The 2-morphism defined by the following pasting diagram:

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

Equations

• CategoryTheory.Bicategory.leftZigzag η ε = CategoryTheory.bicategoricalComp (CategoryTheory.Bicategory.whiskerRight η f) (CategoryTheory.Bicategory.whiskerLeft f ε)

@[reducible, inline]

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

The 2-morphism defined by the following pasting diagram:

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

Equations

• CategoryTheory.Bicategory.rightZigzag η ε = CategoryTheory.bicategoricalComp (CategoryTheory.Bicategory.whiskerLeft g η) (CategoryTheory.Bicategory.whiskerRight ε g)

theorem CategoryTheory.Bicategory.rightZigzag_idempotent_of_left_triangle {B : Type u} [Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryStruct.id a ⟶ CategoryStruct.comp f g) (ε : CategoryStruct.comp g f ⟶ CategoryStruct.id b) (h : leftZigzag η ε = CategoryStruct.comp (leftUnitor f).hom (rightUnitor f).inv) : bicategoricalComp (rightZigzag η ε) (rightZigzag η ε) = rightZigzag η ε

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

Adjunction between two 1-morphisms.

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

  The unit of an adjunction.

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

  The counit of an adjunction.

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

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

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

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

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

Adjunction between two 1-morphisms.

Equations

• One or more equations did not get rendered due to their size.

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

Adjunction between identities.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.Bicategory.Adjunction.instInhabitedId = { default := CategoryTheory.Bicategory.Adjunction.id a }

def CategoryTheory.Bicategory.Adjunction.compUnit {B : Type u} [Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b} (adj₁ : Adjunction f₁ g₁) (adj₂ : Adjunction f₂ g₂) : CategoryStruct.id a ⟶ CategoryStruct.comp (CategoryStruct.comp f₁ f₂) (CategoryStruct.comp g₂ g₁)

Auxiliary definition for adjunction.comp.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Bicategory.Adjunction.compCounit {B : Type u} [Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b} (adj₁ : Adjunction f₁ g₁) (adj₂ : Adjunction f₂ g₂) : CategoryStruct.comp (CategoryStruct.comp g₂ g₁) (CategoryStruct.comp f₁ f₂) ⟶ CategoryStruct.id c

Auxiliary definition for adjunction.comp.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Bicategory.Adjunction.comp_left_triangle_aux {B : Type u} [Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b} (adj₁ : Adjunction f₁ g₁) (adj₂ : Adjunction f₂ g₂) : leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = CategoryStruct.comp (leftUnitor (CategoryStruct.comp f₁ f₂)).hom (rightUnitor (CategoryStruct.comp f₁ f₂)).inv

theorem CategoryTheory.Bicategory.Adjunction.comp_right_triangle_aux {B : Type u} [Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b} (adj₁ : Adjunction f₁ g₁) (adj₂ : Adjunction f₂ g₂) : rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = CategoryStruct.comp (rightUnitor (CategoryStruct.comp g₂ g₁)).hom (leftUnitor (CategoryStruct.comp g₂ g₁)).inv

def CategoryTheory.Bicategory.Adjunction.comp {B : Type u} [Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b} (adj₁ : Adjunction f₁ g₁) (adj₂ : Adjunction f₂ g₂) : Adjunction (CategoryStruct.comp f₁ f₂) (CategoryStruct.comp g₂ g₁)

Composition of adjunctions.

Equations

• adj₁.comp adj₂ = { unit := adj₁.compUnit adj₂, counit := adj₁.compCounit adj₂, left_triangle := ⋯, right_triangle := ⋯ }

@[simp]

theorem CategoryTheory.Bicategory.Adjunction.comp_unit {B : Type u} [Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b} (adj₁ : Adjunction f₁ g₁) (adj₂ : Adjunction f₂ g₂) : (adj₁.comp adj₂).unit = adj₁.compUnit adj₂

@[simp]

theorem CategoryTheory.Bicategory.Adjunction.comp_counit {B : Type u} [Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b} (adj₁ : Adjunction f₁ g₁) (adj₂ : Adjunction f₂ g₂) : (adj₁.comp adj₂).counit = adj₁.compCounit adj₂

@[reducible, inline]

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

The isomorphism version of leftZigzag.

Equations

• CategoryTheory.Bicategory.leftZigzagIso η ε = CategoryTheory.bicategoricalIsoComp (CategoryTheory.Bicategory.whiskerRightIso η f) (CategoryTheory.Bicategory.whiskerLeftIso f ε)

@[reducible, inline]

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

The isomorphism version of rightZigzag.

Equations

• CategoryTheory.Bicategory.rightZigzagIso η ε = CategoryTheory.bicategoricalIsoComp (CategoryTheory.Bicategory.whiskerLeftIso g η) (CategoryTheory.Bicategory.whiskerRightIso ε g)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem CategoryTheory.Bicategory.right_triangle_of_left_triangle {B : Type u} [Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a} (η : CategoryStruct.id a ≅ CategoryStruct.comp f g) (ε : CategoryStruct.comp g f ≅ CategoryStruct.id b) (h : leftZigzag η.hom ε.hom = CategoryStruct.comp (leftUnitor f).hom (rightUnitor f).inv) : rightZigzag η.hom ε.hom = CategoryStruct.comp (rightUnitor g).hom (leftUnitor g).inv

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

An auxiliary definition for mkOfAdjointifyCounit.

Equations

• One or more equations did not get rendered due to their size.

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

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

Adjoint equivalences between two objects.

• hom : a ⟶ b

  A 1-morphism in one direction.

• inv : b ⟶ a

  A 1-morphism in the other direction.

• unit : CategoryStruct.id a ≅ CategoryStruct.comp self.hom self.inv

  The composition hom ≫ inv is isomorphic to the identity.

• counit : CategoryStruct.comp self.inv self.hom ≅ CategoryStruct.id b

  The composition inv ≫ hom is isomorphic to the identity.

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

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

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

Adjoint equivalences between two objects.

Equations

• One or more equations did not get rendered due to their size.

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

The identity 1-morphism is an equivalence.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.Bicategory.Equivalence.instInhabited = { default := CategoryTheory.Bicategory.Equivalence.id a }

theorem CategoryTheory.Bicategory.Equivalence.left_triangle_hom {B : Type u} [Bicategory B] {a b : B} (e : Equivalence a b) : leftZigzag e.unit.hom e.counit.hom = CategoryStruct.comp (leftUnitor e.hom).hom (rightUnitor e.hom).inv

theorem CategoryTheory.Bicategory.Equivalence.right_triangle {B : Type u} [Bicategory B] {a b : B} (e : Equivalence a b) : rightZigzagIso e.unit e.counit = rightUnitor e.inv ≪≫ (leftUnitor e.inv).symm

theorem CategoryTheory.Bicategory.Equivalence.right_triangle_hom {B : Type u} [Bicategory B] {a b : B} (e : Equivalence a b) : rightZigzag e.unit.hom e.counit.hom = CategoryStruct.comp (rightUnitor e.inv).hom (leftUnitor e.inv).inv

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

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

Equations

• CategoryTheory.Bicategory.Equivalence.mkOfAdjointifyCounit η ε = { hom := f, inv := g, unit := η, counit := CategoryTheory.Bicategory.adjointifyCounit η ε, left_triangle := ⋯ }

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

A structure giving a chosen right adjoint of a 1-morphism left.

• right : b ⟶ a

  The right adjoint to left.

• adj : Adjunction left self.right

  The adjunction between left and right.

class CategoryTheory.Bicategory.IsLeftAdjoint {B : Type u} [Bicategory B] {a b : B} (left : a ⟶ b) : Prop

The existence of a right adjoint of f.

• mk' :: (
• nonempty : Nonempty (RightAdjoint left)
• )

theorem CategoryTheory.Bicategory.IsLeftAdjoint.mk {B : Type u} [Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a} (adj : Adjunction f g) : IsLeftAdjoint f

def CategoryTheory.Bicategory.getRightAdjoint {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) [IsLeftAdjoint f] : RightAdjoint f

Use the axiom of choice to extract a right adjoint from an IsLeftAdjoint instance.

Equations

• CategoryTheory.Bicategory.getRightAdjoint f = Classical.choice ⋯

def CategoryTheory.Bicategory.rightAdjoint {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) [IsLeftAdjoint f] : b ⟶ a

The right adjoint of a 1-morphism.

Equations

• CategoryTheory.Bicategory.rightAdjoint f = (CategoryTheory.Bicategory.getRightAdjoint f).right

def CategoryTheory.Bicategory.Adjunction.ofIsLeftAdjoint {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) [IsLeftAdjoint f] : Adjunction f (rightAdjoint f)

Evidence that f⁺⁺ is a right adjoint of f.

Equations

• CategoryTheory.Bicategory.Adjunction.ofIsLeftAdjoint f = (CategoryTheory.Bicategory.getRightAdjoint f).adj

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

A structure giving a chosen left adjoint of a 1-morphism right.

• left : a ⟶ b

  The left adjoint to right.

• adj : Adjunction self.left right

  The adjunction between left and right.

class CategoryTheory.Bicategory.IsRightAdjoint {B : Type u} [Bicategory B] {a b : B} (right : b ⟶ a) : Prop

The existence of a left adjoint of f.

• mk' :: (
• nonempty : Nonempty (LeftAdjoint right)
• )

theorem CategoryTheory.Bicategory.IsRightAdjoint.mk {B : Type u} [Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a} (adj : Adjunction f g) : IsRightAdjoint g

def CategoryTheory.Bicategory.getLeftAdjoint {B : Type u} [Bicategory B] {a b : B} (f : b ⟶ a) [IsRightAdjoint f] : LeftAdjoint f

Use the axiom of choice to extract a left adjoint from an IsRightAdjoint instance.

Equations

• CategoryTheory.Bicategory.getLeftAdjoint f = Classical.choice ⋯

def CategoryTheory.Bicategory.leftAdjoint {B : Type u} [Bicategory B] {a b : B} (f : b ⟶ a) [IsRightAdjoint f] : a ⟶ b

The left adjoint of a 1-morphism.

Equations

• CategoryTheory.Bicategory.leftAdjoint f = (CategoryTheory.Bicategory.getLeftAdjoint f).left

def CategoryTheory.Bicategory.Adjunction.ofIsRightAdjoint {B : Type u} [Bicategory B] {a b : B} (f : b ⟶ a) [IsRightAdjoint f] : Adjunction (leftAdjoint f) f

Evidence that f⁺ is a left adjoint of f.

Equations

• CategoryTheory.Bicategory.Adjunction.ofIsRightAdjoint f = (CategoryTheory.Bicategory.getLeftAdjoint f).adj