# Documentation

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} {a : B} {b : B} {f : a b} {g : b a} :

The 2-morphism defined by the following pasting diagram:

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

Equations
Instances For
def CategoryTheory.Bicategory.rightZigzag {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :

The 2-morphism defined by the following pasting diagram:

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

Equations
Instances For
theorem CategoryTheory.Bicategory.rightZigzag_idempotent_of_left_triangle {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :
structure CategoryTheory.Bicategory.Adjunction {B : Type u} {a : B} {b : B} (f : a b) (g : b a) :

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

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} {a : B} {b : B} {f : a b} {g : b a} (self : ) :

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• CategoryTheory.Bicategory.Adjunction.instInhabitedId = { default := }
def CategoryTheory.Bicategory.Adjunction.compUnit {B : Type u} {a : B} {b : B} {c : B} {f₁ : a b} {g₁ : b a} {f₂ : b c} {g₂ : c b} (adj₁ : ) (adj₂ : ) :

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} {a : B} {b : B} {c : B} {f₁ : a b} {g₁ : b a} {f₂ : b c} {g₂ : c b} (adj₁ : ) (adj₂ : ) :

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} {a : B} {b : B} {c : B} {f₁ : a b} {g₁ : b a} {f₂ : b c} {g₂ : c b} (adj₁ : ) (adj₂ : ) :
theorem CategoryTheory.Bicategory.Adjunction.comp_right_triangle_aux {B : Type u} {a : B} {b : B} {c : B} {f₁ : a b} {g₁ : b a} {f₂ : b c} {g₂ : c b} (adj₁ : ) (adj₂ : ) :
@[simp]
theorem CategoryTheory.Bicategory.Adjunction.comp_counit {B : Type u} {a : B} {b : B} {c : B} {f₁ : a b} {g₁ : b a} {f₂ : b c} {g₂ : c b} (adj₁ : ) (adj₂ : ) :
@[simp]
theorem CategoryTheory.Bicategory.Adjunction.comp_unit {B : Type u} {a : B} {b : B} {c : B} {f₁ : a b} {g₁ : b a} {f₂ : b c} {g₂ : c b} (adj₁ : ) (adj₂ : ) :
def CategoryTheory.Bicategory.Adjunction.comp {B : Type u} {a : B} {b : B} {c : B} {f₁ : a b} {g₁ : b a} {f₂ : b c} {g₂ : c b} (adj₁ : ) (adj₂ : ) :

Equations
Instances For
def CategoryTheory.Bicategory.leftZigzagIso {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :

The isomorphism version of leftZigzag.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Bicategory.rightZigzagIso {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :

The isomorphism version of rightZigzag.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Bicategory.leftZigzagIso_hom {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :
@[simp]
theorem CategoryTheory.Bicategory.rightZigzagIso_hom {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :
@[simp]
theorem CategoryTheory.Bicategory.leftZigzagIso_inv {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :
@[simp]
theorem CategoryTheory.Bicategory.rightZigzagIso_inv {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :
@[simp]
theorem CategoryTheory.Bicategory.leftZigzagIso_symm {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :
@[simp]
theorem CategoryTheory.Bicategory.rightZigzagIso_symm {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :
Equations
• =
instance CategoryTheory.Bicategory.instIsIsoHomRightZigzagHom {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :
Equations
• =
theorem CategoryTheory.Bicategory.right_triangle_of_left_triangle {B : Type u} {a : B} {b : B} {f : a b} {g : b a} (h : ) :
def CategoryTheory.Bicategory.adjointifyCounit {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :

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} {a : B} {b : B} {f : a b} {g : b a} :
structure CategoryTheory.Bicategory.Equivalence {B : Type u} (a : B) (b : B) :
Type (max v w)

Instances For
theorem CategoryTheory.Bicategory.Equivalence.left_triangle {B : Type u} {a : B} {b : B} (self : ) :
CategoryTheory.Bicategory.leftZigzagIso self.unit self.counit = ≪≫ ().symm

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

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

The identity 1-morphism is an equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• CategoryTheory.Bicategory.Equivalence.instInhabited = { default := }
def CategoryTheory.Bicategory.Equivalence.mkOfAdjointifyCounit {B : Type u} {a : B} {b : B} {f : a b} {g : b a} :

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

Equations
• = { hom := f, inv := g, unit := η, counit := , left_triangle := }
Instances For
structure CategoryTheory.Bicategory.RightAdjoint {B : Type u} {a : B} {b : B} (left : a b) :
Type (max v w)

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

Instances For
class CategoryTheory.Bicategory.IsLeftAdjoint {B : Type u} {a : B} {b : B} (left : a b) :

The existence of a right adjoint of f.

• mk' :: (
• nonempty :
• )
Instances
theorem CategoryTheory.Bicategory.IsLeftAdjoint.nonempty {B : Type u} {a : B} {b : B} {left : a b} [self : ] :
theorem CategoryTheory.Bicategory.IsLeftAdjoint.mk {B : Type u} {a : B} {b : B} {f : a b} {g : b a} (adj : ) :
def CategoryTheory.Bicategory.getRightAdjoint {B : Type u} {a : B} {b : B} (f : a b) :

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

Equations
Instances For
def CategoryTheory.Bicategory.rightAdjoint {B : Type u} {a : B} {b : B} (f : a b) :
b a

The right adjoint of a 1-morphism.

Equations
Instances For
def CategoryTheory.Bicategory.Adjunction.ofIsLeftAdjoint {B : Type u} {a : B} {b : B} (f : a b) :

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

Equations
Instances For
structure CategoryTheory.Bicategory.LeftAdjoint {B : Type u} {a : B} {b : B} (right : b a) :
Type (max v w)

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

Instances For
class CategoryTheory.Bicategory.IsRightAdjoint {B : Type u} {a : B} {b : B} (right : b a) :

The existence of a left adjoint of f.

• mk' :: (
• nonempty :
• )
Instances
theorem CategoryTheory.Bicategory.IsRightAdjoint.nonempty {B : Type u} {a : B} {b : B} {right : b a} [self : ] :
theorem CategoryTheory.Bicategory.IsRightAdjoint.mk {B : Type u} {a : B} {b : B} {f : a b} {g : b a} (adj : ) :
def CategoryTheory.Bicategory.getLeftAdjoint {B : Type u} {a : B} {b : B} (f : b a) :

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

Equations
Instances For
def CategoryTheory.Bicategory.leftAdjoint {B : Type u} {a : B} {b : B} (f : b a) :
a b

The left adjoint of a 1-morphism.

Equations
Instances For
def CategoryTheory.Bicategory.Adjunction.ofIsRightAdjoint {B : Type u} {a : B} {b : B} (f : b a) :

Evidence that f⁺ is a left adjoint of f.

Equations
Instances For