Documentation

Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

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-morphisms η : 𝟙 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.Equivalence.mkOfAdjointifyCounit: construct an adjoint equivalence from 2-isomorphisms η : 𝟙 a ≅ f ≫ g and ε : g ≫ f ≅ 𝟙 b, by upgrading ε to a counit.

TODO #

Bicategory.Equivalence.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

Instances For

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

Instances For

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

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.

Instances For

theorem CategoryTheory.Bicategory.Adjunction.ext_iff {B : Type u} {inst✝ : Bicategory B} {a b : B} {f : a ⟶ b} {g : b ⟶ a} {x y : Adjunction f g} :

x = y ↔ x.unit = y.unit ∧ x.counit = y.counit

theorem CategoryTheory.Bicategory.Adjunction.ext {B : Type u} {inst✝ : Bicategory B} {a b : B} {f : a ⟶ b} {g : b ⟶ a} {x y : Adjunction f g} (unit : x.unit = y.unit) (counit : x.counit = y.counit) :

x = y

def CategoryTheory.Bicategory.«term_⊣_» :

Lean.TrailingParserDescr

Adjunction between two 1-morphisms.

Instances For

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

Adjunction (CategoryStruct.id a) (CategoryStruct.id a)

Adjunction between identities.

Instances For

@[implicit_reducible]

instance CategoryTheory.Bicategory.Adjunction.instInhabitedId {B : Type u} [Bicategory B] {a : B} :

Inhabited (Adjunction (CategoryStruct.id a) (CategoryStruct.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.

Instances For

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.

Instances For

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.

Instances For

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

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

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

Instances For

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

Instances For

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

Instances For

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.

Instances For

def CategoryTheory.Bicategory.«term_≌_» :

Lean.TrailingParserDescr

Adjoint equivalences between two objects.

Instances For

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

Equivalence a a

The identity 1-morphism is an equivalence.

Instances For

@[implicit_reducible]

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

Inhabited (Equivalence a 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.

Instances For

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.

Instances For

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

The existence of a right adjoint of f.

mk' :: (

nonempty : Nonempty (RightAdjoint left)

)

Instances

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

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

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

Instances For

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

Instances For

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

Adjunction f (rightAdjoint f)

Evidence that rightAdjoint f is a right adjoint of f.

Instances For

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.

Instances For

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

The existence of a left adjoint of right.

mk' :: (

nonempty : Nonempty (LeftAdjoint right)

)

Instances

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

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

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

Instances For

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

Instances For

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

Adjunction (leftAdjoint f) f

Evidence that leftAdjoint f is a left adjoint of f.

Instances For