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.

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

Equations

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

Instances For

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

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

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.

Equations

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

Instances For

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.

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