Documentation

Mathlib.CategoryTheory.Bicategory.Adjunction

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 : 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 ε)

Instances For

@[reducible, inline]

abbrev 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

Equations

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

Instances For

theorem CategoryTheory.Bicategory.rightZigzag_idempotent_of_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) (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 : B} (f : a ⟶ b) (g : b ⟶ a) :

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.

Instances For

@[simp]

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

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.

@[simp]

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

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.

Instances For

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.

Instances For

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} {b : 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.

Instances For

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

Instances For

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

@[simp]

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

@[simp]

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

def CategoryTheory.Bicategory.Adjunction.comp {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : 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 := ⋯ }

Instances For

@[reducible, inline]

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

Equations

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

Instances For

@[reducible, inline]

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

Equations

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

Instances For

@[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

instance CategoryTheory.Bicategory.instIsIsoHomLeftZigzagHom {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.IsIso (CategoryTheory.Bicategory.leftZigzag η.hom ε.hom)

Equations

⋯ = ⋯

instance CategoryTheory.Bicategory.instIsIsoHomRightZigzagHom {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.IsIso (CategoryTheory.Bicategory.rightZigzag η.hom ε.hom)

Equations

⋯ = ⋯

theorem CategoryTheory.Bicategory.right_triangle_of_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) (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 : 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.

Instances For

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)

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.

Instances For

theorem CategoryTheory.Bicategory.Equivalence.left_triangle {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (self : CategoryTheory.Bicategory.Equivalence a b) :

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.

Instances For

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.

Instances For

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 : 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 : 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 : 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 : 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 := ⋯ }

Instances For

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

Instances For

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

The existence of a right adjoint of f.

mk' :: (

nonempty : Nonempty (CategoryTheory.Bicategory.RightAdjoint left)

)

Instances

theorem CategoryTheory.Bicategory.IsLeftAdjoint.nonempty {B : Type u} :

∀ {inst : CategoryTheory.Bicategory B} {a b : B} {left : a ⟶ b} [self : CategoryTheory.Bicategory.IsLeftAdjoint left], Nonempty (CategoryTheory.Bicategory.RightAdjoint left)

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

The existence of a left adjoint of f.

mk' :: (

nonempty : Nonempty (CategoryTheory.Bicategory.LeftAdjoint right)

)

Instances

theorem CategoryTheory.Bicategory.IsRightAdjoint.nonempty {B : Type u} :

∀ {inst : CategoryTheory.Bicategory B} {a b : B} {right : b ⟶ a} [self : CategoryTheory.Bicategory.IsRightAdjoint right], Nonempty (CategoryTheory.Bicategory.LeftAdjoint right)

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

Instances For

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

Instances For

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

Instances For