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} [CategoryTheory.Bicategory B] {a 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

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Bicategory.rightZigzag {B : Type u} [CategoryTheory.Bicategory B] {a 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

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} [CategoryTheory.Bicategory B] {a 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) (h : CategoryTheory.Bicategory.leftZigzag η ε = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom (CategoryTheory.Bicategory.rightUnitor f).inv) : CategoryTheory.bicategoricalComp (CategoryTheory.Bicategory.rightZigzag η ε) (CategoryTheory.Bicategory.rightZigzag η ε) = CategoryTheory.Bicategory.rightZigzag η ε

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

Adjunction between two 1-morphisms.

• 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 self.unit self.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 self.unit self.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.

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} [CategoryTheory.Bicategory B] (a : B) : CategoryTheory.Bicategory.Adjunction (CategoryTheory.CategoryStruct.id a) (CategoryTheory.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} [CategoryTheory.Bicategory B] {a : B} : Inhabited (CategoryTheory.Bicategory.Adjunction (CategoryTheory.CategoryStruct.id a) (CategoryTheory.CategoryStruct.id a))

Equations

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

def CategoryTheory.Bicategory.Adjunction.compUnit {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b} (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂) : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f₁ f₂) (CategoryTheory.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} [CategoryTheory.Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b} (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g₂ g₁) (CategoryTheory.CategoryStruct.comp f₁ f₂) ⟶ CategoryTheory.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} [CategoryTheory.Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b} (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂) : CategoryTheory.Bicategory.leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f₁ f₂)).hom (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f₁ f₂)).inv

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

def CategoryTheory.Bicategory.Adjunction.comp {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b} (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂) : CategoryTheory.Bicategory.Adjunction (CategoryTheory.CategoryStruct.comp f₁ f₂) (CategoryTheory.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} [CategoryTheory.Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b} (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂) : (adj₁.comp adj₂).unit = adj₁.compUnit adj₂

@[simp]

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

@[reducible, inline]

abbrev CategoryTheory.Bicategory.leftZigzagIso {B : Type u} [CategoryTheory.Bicategory B] {a 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.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Bicategory.rightZigzagIso {B : Type u} [CategoryTheory.Bicategory B] {a 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.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.leftZigzagIso_hom {B : Type u} [CategoryTheory.Bicategory B] {a 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} {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} {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} {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} {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} {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

instance CategoryTheory.Bicategory.instIsIsoHomLeftZigzagHom {B : Type u} [CategoryTheory.Bicategory B] {a 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.IsIso (CategoryTheory.Bicategory.leftZigzag η.hom ε.hom)

instance CategoryTheory.Bicategory.instIsIsoHomRightZigzagHom {B : Type u} [CategoryTheory.Bicategory B] {a 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.IsIso (CategoryTheory.Bicategory.rightZigzag η.hom ε.hom)

theorem CategoryTheory.Bicategory.right_triangle_of_left_triangle {B : Type u} [CategoryTheory.Bicategory B] {a 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) (h : CategoryTheory.Bicategory.leftZigzag η.hom ε.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom (CategoryTheory.Bicategory.rightUnitor f).inv) : CategoryTheory.Bicategory.rightZigzag η.hom ε.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom (CategoryTheory.Bicategory.leftUnitor g).inv

def CategoryTheory.Bicategory.adjointifyCounit {B : Type u} [CategoryTheory.Bicategory B] {a 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.

Equations

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

theorem CategoryTheory.Bicategory.adjointifyCounit_left_triangle {B : Type u} [CategoryTheory.Bicategory B] {a 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) : 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 : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp self.hom self.inv

  The composition hom ≫ inv is isomorphic to the identity.

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

  The composition inv ≫ hom is isomorphic to the identity.

• left_triangle : CategoryTheory.Bicategory.leftZigzagIso self.unit self.counit = CategoryTheory.Bicategory.leftUnitor self.hom ≪≫ (CategoryTheory.Bicategory.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} [CategoryTheory.Bicategory B] (a : B) : CategoryTheory.Bicategory.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} [CategoryTheory.Bicategory B] {a : B} : Inhabited (CategoryTheory.Bicategory.Equivalence a a)

Equations

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

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

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

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

def CategoryTheory.Bicategory.Equivalence.mkOfAdjointifyCounit {B : Type u} [CategoryTheory.Bicategory B] {a 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.

Equations

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

structure CategoryTheory.Bicategory.RightAdjoint {B : Type u} [CategoryTheory.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 : CategoryTheory.Bicategory.Adjunction left self.right

  The adjunction between left and right.

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

The existence of a right adjoint of f.

• mk' :: (
• nonempty : Nonempty (CategoryTheory.Bicategory.RightAdjoint left)
• )

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

def CategoryTheory.Bicategory.getRightAdjoint {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) [CategoryTheory.Bicategory.IsLeftAdjoint f] : CategoryTheory.Bicategory.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} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) [CategoryTheory.Bicategory.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} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) [CategoryTheory.Bicategory.IsLeftAdjoint f] : CategoryTheory.Bicategory.Adjunction f (CategoryTheory.Bicategory.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} [CategoryTheory.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 : CategoryTheory.Bicategory.Adjunction self.left right

  The adjunction between left and right.

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

The existence of a left adjoint of f.

• mk' :: (
• nonempty : Nonempty (CategoryTheory.Bicategory.LeftAdjoint right)
• )

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

def CategoryTheory.Bicategory.getLeftAdjoint {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : b ⟶ a) [CategoryTheory.Bicategory.IsRightAdjoint f] : CategoryTheory.Bicategory.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} [CategoryTheory.Bicategory B] {a b : B} (f : b ⟶ a) [CategoryTheory.Bicategory.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} [CategoryTheory.Bicategory B] {a b : B} (f : b ⟶ a) [CategoryTheory.Bicategory.IsRightAdjoint f] : CategoryTheory.Bicategory.Adjunction (CategoryTheory.Bicategory.leftAdjoint f) f

Evidence that f⁺ is a left adjoint of f.

Equations

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