Mates in bicategories #
This file establishes the bijection between the 2-cells
l₁ r₁
c --→ d c ←-- d
g ↓ ↗ ↓ h g ↓ ↘ ↓ h
e --→ f e ←-- f
l₂ r₂
where l₁ ⊣ r₁ and l₂ ⊣ r₂. The corresponding natural transformations are called mates.
For the bicategory Cat, the definitions in this file are provided in
Mathlib/CategoryTheory/Adjunction/Mates.lean, where you can find more detailed documentation
about mates.
Implementation #
The correspondence between mates is obtained by combining
bijections of the form (g ⟶ l ≫ h) ≃ (r ≫ g ⟶ h)
and (g ≫ l ⟶ h) ≃ (g ⟶ h ≫ r) when l ⊣ r is an adjunction.
Indeed, g ≫ l₂ ⟶ l₁ ≫ h identifies to g ⟶ (l₁ ≫ h) ≫ r₂ by using the
second bijection applied to l₂ ⊣ r₂, and this identifies to r₁ ≫ g ⟶ h ≫ r₂
by using the first bijection applied to l₁ ⊣ r₁.
Remarks #
To be precise, the definitions in Mathlib/CategoryTheory/Adjunction/Mates.lean are universe
polymorphic, so they are not simple specializations of the definitions in this file.
def
CategoryTheory.Bicategory.Adjunction.homEquiv₁
{B : Type u}
[Bicategory B]
{b c d : B}
{l : b ⟶ c}
{r : c ⟶ b}
(adj : Adjunction l r)
{g : b ⟶ d}
{h : c ⟶ d}
:
The bijection (g ⟶ l ≫ h) ≃ (r ≫ g ⟶ h) induced by an adjunction
l ⊣ r in a bicategory.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Bicategory.Adjunction.homEquiv₁_apply
{B : Type u}
[Bicategory B]
{b c d : B}
{l : b ⟶ c}
{r : c ⟶ b}
(adj : Adjunction l r)
{g : b ⟶ d}
{h : c ⟶ d}
(γ : g ⟶ CategoryStruct.comp l h)
:
adj.homEquiv₁ γ = CategoryStruct.comp (whiskerLeft r γ)
(CategoryStruct.comp (associator r l h).inv (CategoryStruct.comp (whiskerRight adj.counit h) (leftUnitor h).hom))
theorem
CategoryTheory.Bicategory.Adjunction.homEquiv₁_symm_apply
{B : Type u}
[Bicategory B]
{b c d : B}
{l : b ⟶ c}
{r : c ⟶ b}
(adj : Adjunction l r)
{g : b ⟶ d}
{h : c ⟶ d}
(β : CategoryStruct.comp r g ⟶ h)
:
adj.homEquiv₁.symm β = CategoryStruct.comp (leftUnitor g).inv
(CategoryStruct.comp (whiskerRight adj.unit g) (CategoryStruct.comp (associator l r g).hom (whiskerLeft l β)))
def
CategoryTheory.Bicategory.Adjunction.homEquiv₂
{B : Type u}
[Bicategory B]
{a b c : B}
{l : b ⟶ c}
{r : c ⟶ b}
(adj : Adjunction l r)
{g : a ⟶ b}
{h : a ⟶ c}
:
The bijection (g ≫ l ⟶ h) ≃ (g ⟶ h ≫ r) induced by an adjunction
l ⊣ r in a bicategory.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Bicategory.Adjunction.homEquiv₂_apply
{B : Type u}
[Bicategory B]
{a b c : B}
{l : b ⟶ c}
{r : c ⟶ b}
(adj : Adjunction l r)
{g : a ⟶ b}
{h : a ⟶ c}
(α : CategoryStruct.comp g l ⟶ h)
:
adj.homEquiv₂ α = CategoryStruct.comp (rightUnitor g).inv
(CategoryStruct.comp (whiskerLeft g adj.unit) (CategoryStruct.comp (associator g l r).inv (whiskerRight α r)))
theorem
CategoryTheory.Bicategory.Adjunction.homEquiv₂_symm_apply
{B : Type u}
[Bicategory B]
{a b c : B}
{l : b ⟶ c}
{r : c ⟶ b}
(adj : Adjunction l r)
{g : a ⟶ b}
{h : a ⟶ c}
(γ : g ⟶ CategoryStruct.comp h r)
:
adj.homEquiv₂.symm γ = CategoryStruct.comp (whiskerRight γ l)
(CategoryStruct.comp (associator h r l).hom (CategoryStruct.comp (whiskerLeft h adj.counit) (rightUnitor h).hom))
def
CategoryTheory.Bicategory.mateEquiv
{B : Type u}
[Bicategory B]
{c d e f : B}
{g : c ⟶ e}
{h : d ⟶ f}
{l₁ : c ⟶ d}
{r₁ : d ⟶ c}
{l₂ : e ⟶ f}
{r₂ : f ⟶ e}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
:
(CategoryStruct.comp g l₂ ⟶ CategoryStruct.comp l₁ h) ≃ (CategoryStruct.comp r₁ g ⟶ CategoryStruct.comp h r₂)
Suppose we have a square of 1-morphisms (where the top and bottom are adjunctions l₁ ⊣ r₁
and l₂ ⊣ r₂ respectively).
c ↔ d
g ↓ ↓ h
e ↔ f
Then we have a bijection between natural transformations g ≫ l₂ ⟶ l₁ ≫ h and
r₁ ≫ g ⟶ h ≫ r₂. This can be seen as a bijection of the 2-cells:
l₁ r₁
c --→ d c ←-- d
g ↓ ↗ ↓ h g ↓ ↘ ↓ h
e --→ f e ←-- f
L₂ R₂
Note that if one of the transformations is an iso, it does not imply the other is an iso.
Equations
- CategoryTheory.Bicategory.mateEquiv adj₁ adj₂ = adj₂.homEquiv₂.trans (((CategoryTheory.Iso.refl g).homCongr (CategoryTheory.Bicategory.associator l₁ h r₂)).trans adj₁.homEquiv₁)
Instances For
theorem
CategoryTheory.Bicategory.mateEquiv_apply
{B : Type u}
[Bicategory B]
{c d e f : B}
{g : c ⟶ e}
{h : d ⟶ f}
{l₁ : c ⟶ d}
{r₁ : d ⟶ c}
{l₂ : e ⟶ f}
{r₂ : f ⟶ e}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(a✝ : CategoryStruct.comp g l₂ ⟶ CategoryStruct.comp l₁ h)
:
(mateEquiv adj₁ adj₂) a✝ = adj₁.homEquiv₁ (CategoryStruct.comp (adj₂.homEquiv₂ a✝) (associator l₁ h r₂).hom)
theorem
CategoryTheory.Bicategory.mateEquiv_symm_apply
{B : Type u}
[Bicategory B]
{c d e f : B}
{g : c ⟶ e}
{h : d ⟶ f}
{l₁ : c ⟶ d}
{r₁ : d ⟶ c}
{l₂ : e ⟶ f}
{r₂ : f ⟶ e}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(a✝ : CategoryStruct.comp r₁ g ⟶ CategoryStruct.comp h r₂)
:
(mateEquiv adj₁ adj₂).symm a✝ = adj₂.homEquiv₂.symm (CategoryStruct.comp (adj₁.homEquiv₁.symm a✝) (associator l₁ h r₂).inv)
theorem
CategoryTheory.Bicategory.mateEquiv_eq_iff
{B : Type u}
[Bicategory B]
{c d e f : B}
{g : c ⟶ e}
{h : d ⟶ f}
{l₁ : c ⟶ d}
{r₁ : d ⟶ c}
{l₂ : e ⟶ f}
{r₂ : f ⟶ e}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(α : CategoryStruct.comp g l₂ ⟶ CategoryStruct.comp l₁ h)
(β : CategoryStruct.comp r₁ g ⟶ CategoryStruct.comp h r₂)
:
(mateEquiv adj₁ adj₂) α = β ↔ adj₁.homEquiv₁.symm β = CategoryStruct.comp (adj₂.homEquiv₂ α) (associator l₁ h r₂).hom
theorem
CategoryTheory.Bicategory.mateEquiv_apply'
{B : Type u}
[Bicategory B]
{c d e f : B}
{g : c ⟶ e}
{h : d ⟶ f}
{l₁ : c ⟶ d}
{r₁ : d ⟶ c}
{l₂ : e ⟶ f}
{r₂ : f ⟶ e}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(α : CategoryStruct.comp g l₂ ⟶ CategoryStruct.comp l₁ h)
:
(mateEquiv adj₁ adj₂) α = bicategoricalComp (CategoryStruct.id (CategoryStruct.comp r₁ g))
(bicategoricalComp (whiskerLeft r₁ (whiskerLeft g adj₂.unit))
(bicategoricalComp (whiskerLeft r₁ (whiskerRight α r₂))
(bicategoricalComp (whiskerRight (whiskerRight adj₁.counit h) r₂)
(CategoryStruct.id (CategoryStruct.comp h r₂)))))
theorem
CategoryTheory.Bicategory.mateEquiv_symm_apply'
{B : Type u}
[Bicategory B]
{c d e f : B}
{g : c ⟶ e}
{h : d ⟶ f}
{l₁ : c ⟶ d}
{r₁ : d ⟶ c}
{l₂ : e ⟶ f}
{r₂ : f ⟶ e}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(β : CategoryStruct.comp r₁ g ⟶ CategoryStruct.comp h r₂)
:
(mateEquiv adj₁ adj₂).symm β = bicategoricalComp (CategoryStruct.id (CategoryStruct.comp g l₂))
(bicategoricalComp (whiskerRight (whiskerRight adj₁.unit g) l₂)
(bicategoricalComp (whiskerLeft l₁ (whiskerRight β l₂))
(bicategoricalComp (whiskerLeft l₁ (whiskerLeft h adj₂.counit))
(CategoryStruct.id (CategoryStruct.comp l₁ h)))))
def
CategoryTheory.Bicategory.leftAdjointSquare.vcomp
{B : Type u}
[Bicategory B]
{a b c d e f : B}
{g₁ : a ⟶ c}
{g₂ : c ⟶ e}
{h₁ : b ⟶ d}
{h₂ : d ⟶ f}
{l₁ : a ⟶ b}
{l₂ : c ⟶ d}
{l₃ : e ⟶ f}
(α : CategoryStruct.comp g₁ l₂ ⟶ CategoryStruct.comp l₁ h₁)
(β : CategoryStruct.comp g₂ l₃ ⟶ CategoryStruct.comp l₂ h₂)
:
CategoryStruct.comp (CategoryStruct.comp g₁ g₂) l₃ ⟶ CategoryStruct.comp l₁ (CategoryStruct.comp h₁ h₂)
Squares between left adjoints can be composed "vertically" by pasting.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Bicategory.rightAdjointSquare.vcomp
{B : Type u}
[Bicategory B]
{a b c d e f : B}
{g₁ : a ⟶ c}
{g₂ : c ⟶ e}
{h₁ : b ⟶ d}
{h₂ : d ⟶ f}
{r₁ : b ⟶ a}
{r₂ : d ⟶ c}
{r₃ : f ⟶ e}
(α : CategoryStruct.comp r₁ g₁ ⟶ CategoryStruct.comp h₁ r₂)
(β : CategoryStruct.comp r₂ g₂ ⟶ CategoryStruct.comp h₂ r₃)
:
CategoryStruct.comp r₁ (CategoryStruct.comp g₁ g₂) ⟶ CategoryStruct.comp (CategoryStruct.comp h₁ h₂) r₃
Squares between right adjoints can be composed "vertically" by pasting.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Bicategory.mateEquiv_vcomp
{B : Type u}
[Bicategory B]
{a b c d e f : B}
{g₁ : a ⟶ c}
{g₂ : c ⟶ e}
{h₁ : b ⟶ d}
{h₂ : d ⟶ f}
{l₁ : a ⟶ b}
{r₁ : b ⟶ a}
{l₂ : c ⟶ d}
{r₂ : d ⟶ c}
{l₃ : e ⟶ f}
{r₃ : f ⟶ e}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(adj₃ : Adjunction l₃ r₃)
(α : CategoryStruct.comp g₁ l₂ ⟶ CategoryStruct.comp l₁ h₁)
(β : CategoryStruct.comp g₂ l₃ ⟶ CategoryStruct.comp l₂ h₂)
:
(mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp α β) = rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) α) ((mateEquiv adj₂ adj₃) β)
The mates equivalence commutes with vertical composition.
def
CategoryTheory.Bicategory.leftAdjointSquare.hcomp
{B : Type u}
[Bicategory B]
{a b c d e f : B}
{g : a ⟶ d}
{h : b ⟶ e}
{k : c ⟶ f}
{l₁ : a ⟶ b}
{l₂ : d ⟶ e}
{l₃ : b ⟶ c}
{l₄ : e ⟶ f}
(α : CategoryStruct.comp g l₂ ⟶ CategoryStruct.comp l₁ h)
(β : CategoryStruct.comp h l₄ ⟶ CategoryStruct.comp l₃ k)
:
CategoryStruct.comp g (CategoryStruct.comp l₂ l₄) ⟶ CategoryStruct.comp (CategoryStruct.comp l₁ l₃) k
Squares between left adjoints can be composed "horizontally" by pasting.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Bicategory.rightAdjointSquare.hcomp
{B : Type u}
[Bicategory B]
{a b c d e f : B}
{g : a ⟶ d}
{h : b ⟶ e}
{k : c ⟶ f}
{r₁ : b ⟶ a}
{r₂ : e ⟶ d}
{r₃ : c ⟶ b}
{r₄ : f ⟶ e}
(α : CategoryStruct.comp r₁ g ⟶ CategoryStruct.comp h r₂)
(β : CategoryStruct.comp r₃ h ⟶ CategoryStruct.comp k r₄)
:
CategoryStruct.comp (CategoryStruct.comp r₃ r₁) g ⟶ CategoryStruct.comp k (CategoryStruct.comp r₄ r₂)
Squares between right adjoints can be composed "horizontally" by pasting.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Bicategory.mateEquiv_hcomp
{B : Type u}
[Bicategory B]
{a b c d e f : B}
{g : a ⟶ d}
{h : b ⟶ e}
{k : c ⟶ f}
{l₁ : a ⟶ b}
{r₁ : b ⟶ a}
{l₂ : d ⟶ e}
{r₂ : e ⟶ d}
{l₃ : b ⟶ c}
{r₃ : c ⟶ b}
{l₄ : e ⟶ f}
{r₄ : f ⟶ e}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(adj₃ : Adjunction l₃ r₃)
(adj₄ : Adjunction l₄ r₄)
(α : CategoryStruct.comp g l₂ ⟶ CategoryStruct.comp l₁ h)
(β : CategoryStruct.comp h l₄ ⟶ CategoryStruct.comp l₃ k)
:
(mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (leftAdjointSquare.hcomp α β) = rightAdjointSquare.hcomp ((mateEquiv adj₁ adj₂) α) ((mateEquiv adj₃ adj₄) β)
The mates equivalence commutes with horizontal composition of squares.
def
CategoryTheory.Bicategory.leftAdjointSquare.comp
{B : Type u}
[Bicategory B]
{a b c d e f x y z : B}
{g₁ : a ⟶ d}
{h₁ : b ⟶ e}
{k₁ : c ⟶ f}
{g₂ : d ⟶ x}
{h₂ : e ⟶ y}
{k₂ : f ⟶ z}
{l₁ : a ⟶ b}
{l₂ : b ⟶ c}
{l₃ : d ⟶ e}
{l₄ : e ⟶ f}
{l₅ : x ⟶ y}
{l₆ : y ⟶ z}
(α : CategoryStruct.comp g₁ l₃ ⟶ CategoryStruct.comp l₁ h₁)
(β : CategoryStruct.comp h₁ l₄ ⟶ CategoryStruct.comp l₂ k₁)
(γ : CategoryStruct.comp g₂ l₅ ⟶ CategoryStruct.comp l₃ h₂)
(δ : CategoryStruct.comp h₂ l₆ ⟶ CategoryStruct.comp l₄ k₂)
:
CategoryStruct.comp (CategoryStruct.comp g₁ g₂) (CategoryStruct.comp l₅ l₆) ⟶ CategoryStruct.comp (CategoryStruct.comp l₁ l₂) (CategoryStruct.comp k₁ k₂)
Squares of squares between left adjoints can be composed by iterating vertical and horizontal composition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Bicategory.leftAdjointSquare.comp_vhcomp
{B : Type u}
[Bicategory B]
{a b c d e f x y z : B}
{g₁ : a ⟶ d}
{h₁ : b ⟶ e}
{k₁ : c ⟶ f}
{g₂ : d ⟶ x}
{h₂ : e ⟶ y}
{k₂ : f ⟶ z}
{l₁ : a ⟶ b}
{l₂ : b ⟶ c}
{l₃ : d ⟶ e}
{l₄ : e ⟶ f}
{l₅ : x ⟶ y}
{l₆ : y ⟶ z}
(α : CategoryStruct.comp g₁ l₃ ⟶ CategoryStruct.comp l₁ h₁)
(β : CategoryStruct.comp h₁ l₄ ⟶ CategoryStruct.comp l₂ k₁)
(γ : CategoryStruct.comp g₂ l₅ ⟶ CategoryStruct.comp l₃ h₂)
(δ : CategoryStruct.comp h₂ l₆ ⟶ CategoryStruct.comp l₄ k₂)
:
theorem
CategoryTheory.Bicategory.leftAdjointSquare.comp_hvcomp
{B : Type u}
[Bicategory B]
{a b c d e f x y z : B}
{g₁ : a ⟶ d}
{h₁ : b ⟶ e}
{k₁ : c ⟶ f}
{g₂ : d ⟶ x}
{h₂ : e ⟶ y}
{k₂ : f ⟶ z}
{l₁ : a ⟶ b}
{l₂ : b ⟶ c}
{l₃ : d ⟶ e}
{l₄ : e ⟶ f}
{l₅ : x ⟶ y}
{l₆ : y ⟶ z}
(α : CategoryStruct.comp g₁ l₃ ⟶ CategoryStruct.comp l₁ h₁)
(β : CategoryStruct.comp h₁ l₄ ⟶ CategoryStruct.comp l₂ k₁)
(γ : CategoryStruct.comp g₂ l₅ ⟶ CategoryStruct.comp l₃ h₂)
(δ : CategoryStruct.comp h₂ l₆ ⟶ CategoryStruct.comp l₄ k₂)
:
Horizontal and vertical composition of squares commutes.
def
CategoryTheory.Bicategory.rightAdjointSquare.comp
{B : Type u}
[Bicategory B]
{a b c d e f x y z : B}
{g₁ : a ⟶ d}
{h₁ : b ⟶ e}
{k₁ : c ⟶ f}
{g₂ : d ⟶ x}
{h₂ : e ⟶ y}
{k₂ : f ⟶ z}
{r₁ : b ⟶ a}
{r₂ : c ⟶ b}
{r₃ : e ⟶ d}
{r₄ : f ⟶ e}
{r₅ : y ⟶ x}
{r₆ : z ⟶ y}
(α : CategoryStruct.comp r₁ g₁ ⟶ CategoryStruct.comp h₁ r₃)
(β : CategoryStruct.comp r₂ h₁ ⟶ CategoryStruct.comp k₁ r₄)
(γ : CategoryStruct.comp r₃ g₂ ⟶ CategoryStruct.comp h₂ r₅)
(δ : CategoryStruct.comp r₄ h₂ ⟶ CategoryStruct.comp k₂ r₆)
:
CategoryStruct.comp (CategoryStruct.comp r₂ r₁) (CategoryStruct.comp g₁ g₂) ⟶ CategoryStruct.comp (CategoryStruct.comp k₁ k₂) (CategoryStruct.comp r₆ r₅)
Squares of squares between right adjoints can be composed by iterating vertical and horizontal composition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Bicategory.rightAdjointSquare.comp_vhcomp
{B : Type u}
[Bicategory B]
{a b c d e f x y z : B}
{g₁ : a ⟶ d}
{h₁ : b ⟶ e}
{k₁ : c ⟶ f}
{g₂ : d ⟶ x}
{h₂ : e ⟶ y}
{k₂ : f ⟶ z}
{r₁ : b ⟶ a}
{r₂ : c ⟶ b}
{r₃ : e ⟶ d}
{r₄ : f ⟶ e}
{r₅ : y ⟶ x}
{r₆ : z ⟶ y}
(α : CategoryStruct.comp r₁ g₁ ⟶ CategoryStruct.comp h₁ r₃)
(β : CategoryStruct.comp r₂ h₁ ⟶ CategoryStruct.comp k₁ r₄)
(γ : CategoryStruct.comp r₃ g₂ ⟶ CategoryStruct.comp h₂ r₅)
(δ : CategoryStruct.comp r₄ h₂ ⟶ CategoryStruct.comp k₂ r₆)
:
theorem
CategoryTheory.Bicategory.rightAdjointSquare.comp_hvcomp
{B : Type u}
[Bicategory B]
{a b c d e f x y z : B}
{g₁ : a ⟶ d}
{h₁ : b ⟶ e}
{k₁ : c ⟶ f}
{g₂ : d ⟶ x}
{h₂ : e ⟶ y}
{k₂ : f ⟶ z}
{r₁ : b ⟶ a}
{r₂ : c ⟶ b}
{r₃ : e ⟶ d}
{r₄ : f ⟶ e}
{r₅ : y ⟶ x}
{r₆ : z ⟶ y}
(α : CategoryStruct.comp r₁ g₁ ⟶ CategoryStruct.comp h₁ r₃)
(β : CategoryStruct.comp r₂ h₁ ⟶ CategoryStruct.comp k₁ r₄)
(γ : CategoryStruct.comp r₃ g₂ ⟶ CategoryStruct.comp h₂ r₅)
(δ : CategoryStruct.comp r₄ h₂ ⟶ CategoryStruct.comp k₂ r₆)
:
Horizontal and vertical composition of squares commutes.
theorem
CategoryTheory.Bicategory.mateEquiv_square
{B : Type u}
[Bicategory B]
{a b c d e f x y z : B}
{g₁ : a ⟶ d}
{h₁ : b ⟶ e}
{k₁ : c ⟶ f}
{g₂ : d ⟶ x}
{h₂ : e ⟶ y}
{k₂ : f ⟶ z}
{l₁ : a ⟶ b}
{r₁ : b ⟶ a}
{l₂ : b ⟶ c}
{r₂ : c ⟶ b}
{l₃ : d ⟶ e}
{r₃ : e ⟶ d}
{l₄ : e ⟶ f}
{r₄ : f ⟶ e}
{l₅ : x ⟶ y}
{r₅ : y ⟶ x}
{l₆ : y ⟶ z}
{r₆ : z ⟶ y}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(adj₃ : Adjunction l₃ r₃)
(adj₄ : Adjunction l₄ r₄)
(adj₅ : Adjunction l₅ r₅)
(adj₆ : Adjunction l₆ r₆)
(α : CategoryStruct.comp g₁ l₃ ⟶ CategoryStruct.comp l₁ h₁)
(β : CategoryStruct.comp h₁ l₄ ⟶ CategoryStruct.comp l₂ k₁)
(γ : CategoryStruct.comp g₂ l₅ ⟶ CategoryStruct.comp l₃ h₂)
(δ : CategoryStruct.comp h₂ l₆ ⟶ CategoryStruct.comp l₄ k₂)
:
(mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.comp α β γ δ) = rightAdjointSquare.comp ((mateEquiv adj₁ adj₃) α) ((mateEquiv adj₂ adj₄) β) ((mateEquiv adj₃ adj₅) γ)
((mateEquiv adj₄ adj₆) δ)
The mates equivalence commutes with composition of squares of squares. These results form the basis for an isomorphism of double categories to be proven later.
def
CategoryTheory.Bicategory.conjugateEquiv
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
:
Given two adjunctions l₁ ⊣ r₁ and l₂ ⊣ r₂ both between objects c, d, there is a
bijection between 2-morphisms l₂ ⟶ l₁ and 2-morphisms r₁ ⟶ r₂. This is
defined as a special case of mateEquiv, where the two "vertical" 1-morphisms are identities.
Corresponding 2-morphisms are called conjugateEquiv.
Furthermore, this bijection preserves (and reflects) isomorphisms, i.e. a 2-morphism is an iso iff its image under the bijection is an iso.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Bicategory.conjugateEquiv_apply
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(α : l₂ ⟶ l₁)
:
(conjugateEquiv adj₁ adj₂) α = CategoryStruct.comp (rightUnitor r₁).inv
(CategoryStruct.comp
((mateEquiv adj₁ adj₂) (CategoryStruct.comp (leftUnitor l₂).hom (CategoryStruct.comp α (rightUnitor l₁).inv)))
(leftUnitor r₂).hom)
theorem
CategoryTheory.Bicategory.conjugateEquiv_apply'
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(α : l₂ ⟶ l₁)
:
(conjugateEquiv adj₁ adj₂) α = CategoryStruct.comp (rightUnitor r₁).inv
(CategoryStruct.comp (whiskerLeft r₁ adj₂.unit)
(CategoryStruct.comp (whiskerLeft r₁ (whiskerRight α r₂))
(CategoryStruct.comp (associator r₁ l₁ r₂).inv
(CategoryStruct.comp (whiskerRight adj₁.counit r₂) (leftUnitor r₂).hom))))
theorem
CategoryTheory.Bicategory.conjugateEquiv_symm_apply
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(α : r₁ ⟶ r₂)
:
(conjugateEquiv adj₁ adj₂).symm α = CategoryStruct.comp (leftUnitor l₂).inv
(CategoryStruct.comp
((mateEquiv adj₁ adj₂).symm
(CategoryStruct.comp (rightUnitor r₁).hom (CategoryStruct.comp α (leftUnitor r₂).inv)))
(rightUnitor l₁).hom)
theorem
CategoryTheory.Bicategory.conjugateEquiv_symm_apply'
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(α : r₁ ⟶ r₂)
:
(conjugateEquiv adj₁ adj₂).symm α = CategoryStruct.comp (leftUnitor l₂).inv
(CategoryStruct.comp (whiskerRight adj₁.unit l₂)
(CategoryStruct.comp (associator l₁ r₁ l₂).hom
(CategoryStruct.comp (whiskerLeft l₁ (whiskerRight α l₂))
(CategoryStruct.comp (whiskerLeft l₁ adj₂.counit) (rightUnitor l₁).hom))))
@[simp]
theorem
CategoryTheory.Bicategory.conjugateEquiv_id
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ : c ⟶ d}
{r₁ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
:
@[simp]
theorem
CategoryTheory.Bicategory.conjugateEquiv_symm_id
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ : c ⟶ d}
{r₁ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
:
theorem
CategoryTheory.Bicategory.conjugateEquiv_adjunction_id
{B : Type u}
[Bicategory B]
{c : B}
{l r : c ⟶ c}
(adj : Adjunction l r)
(α : CategoryStruct.id c ⟶ l)
:
(conjugateEquiv adj (Adjunction.id c)) α = CategoryStruct.comp (rightUnitor r).inv (CategoryStruct.comp (whiskerLeft r α) adj.counit)
theorem
CategoryTheory.Bicategory.conjugateEquiv_adjunction_id_symm
{B : Type u}
[Bicategory B]
{c : B}
{l r : c ⟶ c}
(adj : Adjunction l r)
(α : r ⟶ CategoryStruct.id c)
:
(conjugateEquiv adj (Adjunction.id c)).symm α = CategoryStruct.comp adj.unit (CategoryStruct.comp (whiskerLeft l α) (rightUnitor l).hom)
@[simp]
theorem
CategoryTheory.Bicategory.conjugateEquiv_comp
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ l₃ : c ⟶ d}
{r₁ r₂ r₃ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(adj₃ : Adjunction l₃ r₃)
(α : l₂ ⟶ l₁)
(β : l₃ ⟶ l₂)
:
CategoryStruct.comp ((conjugateEquiv adj₁ adj₂) α) ((conjugateEquiv adj₂ adj₃) β) = (conjugateEquiv adj₁ adj₃) (CategoryStruct.comp β α)
@[simp]
theorem
CategoryTheory.Bicategory.conjugateEquiv_symm_comp
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ l₃ : c ⟶ d}
{r₁ r₂ r₃ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(adj₃ : Adjunction l₃ r₃)
(α : r₁ ⟶ r₂)
(β : r₂ ⟶ r₃)
:
CategoryStruct.comp ((conjugateEquiv adj₂ adj₃).symm β) ((conjugateEquiv adj₁ adj₂).symm α) = (conjugateEquiv adj₁ adj₃).symm (CategoryStruct.comp α β)
theorem
CategoryTheory.Bicategory.conjugateEquiv_comm
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
{α : l₂ ⟶ l₁}
{β : l₁ ⟶ l₂}
(βα : CategoryStruct.comp β α = CategoryStruct.id l₁)
:
CategoryStruct.comp ((conjugateEquiv adj₁ adj₂) α) ((conjugateEquiv adj₂ adj₁) β) = CategoryStruct.id r₁
theorem
CategoryTheory.Bicategory.conjugateEquiv_symm_comm
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
{α : r₁ ⟶ r₂}
{β : r₂ ⟶ r₁}
(αβ : CategoryStruct.comp α β = CategoryStruct.id r₁)
:
CategoryStruct.comp ((conjugateEquiv adj₂ adj₁).symm β) ((conjugateEquiv adj₁ adj₂).symm α) = CategoryStruct.id l₁
instance
CategoryTheory.Bicategory.conjugateEquiv_iso
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(α : l₂ ⟶ l₁)
[IsIso α]
:
IsIso ((conjugateEquiv adj₁ adj₂) α)
If α is an isomorphism between left adjoints, then its conjugate transformation is an
isomorphism. The converse is given in conjugateEquiv_of_iso.
instance
CategoryTheory.Bicategory.conjugateEquiv_symm_iso
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(α : r₁ ⟶ r₂)
[IsIso α]
:
IsIso ((conjugateEquiv adj₁ adj₂).symm α)
If α is an isomorphism between right adjoints, then its conjugate transformation is an
isomorphism. The converse is given in conjugateEquiv_symm_of_iso.
theorem
CategoryTheory.Bicategory.conjugateEquiv_of_iso
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(α : l₂ ⟶ l₁)
[IsIso ((conjugateEquiv adj₁ adj₂) α)]
:
IsIso α
If α is a natural transformation between left adjoints whose conjugate natural transformation
is an isomorphism, then α is an isomorphism. The converse is given in Conjugate_iso.
theorem
CategoryTheory.Bicategory.conjugateEquiv_symm_of_iso
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(α : r₁ ⟶ r₂)
[IsIso ((conjugateEquiv adj₁ adj₂).symm α)]
:
IsIso α
If α is a natural transformation between right adjoints whose conjugate natural transformation is
an isomorphism, then α is an isomorphism. The converse is given in conjugateEquiv_symm_iso.
def
CategoryTheory.Bicategory.conjugateIsoEquiv
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
:
Thus conjugation defines an equivalence between natural isomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Bicategory.conjugateIsoEquiv_symm_apply_inv
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(β : r₁ ≅ r₂)
:
@[simp]
theorem
CategoryTheory.Bicategory.conjugateIsoEquiv_apply_inv
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(α : l₂ ≅ l₁)
:
@[simp]
theorem
CategoryTheory.Bicategory.conjugateIsoEquiv_symm_apply_hom
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(β : r₁ ≅ r₂)
:
@[simp]
theorem
CategoryTheory.Bicategory.conjugateIsoEquiv_apply_hom
{B : Type u}
[Bicategory B]
{c d : B}
{l₁ l₂ : c ⟶ d}
{r₁ r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(α : l₂ ≅ l₁)
:
theorem
CategoryTheory.Bicategory.iterated_mateEquiv_conjugateEquiv
{B : Type u}
[Bicategory B]
{a b c d : B}
{f₁ : a ⟶ c}
{u₁ : c ⟶ a}
{f₂ : b ⟶ d}
{u₂ : d ⟶ b}
{l₁ : a ⟶ b}
{r₁ : b ⟶ a}
{l₂ : c ⟶ d}
{r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(adj₃ : Adjunction f₁ u₁)
(adj₄ : Adjunction f₂ u₂)
(α : CategoryStruct.comp f₁ l₂ ⟶ CategoryStruct.comp l₁ f₂)
:
When all four morphisms in a square are left adjoints, the mates operation can be iterated: l₁ r₁ r₁ c --→ d c ←-- d c ←-- d f₁ ↓ ↗ ↓ f₂ f₁ ↓ ↘ ↓ f₂ u₁ ↑ ↙ ↑ u₂ a --→ b a ←-- b a ←-- b l₂ r₂ r₂ In this case the iterated mate equals the conjugate of the original 2-morphism and is thus an isomorphism if and only if the original 2-morphism is. This explains why some Beck-Chevalley 2-morphisms are isomorphisms.
theorem
CategoryTheory.Bicategory.iterated_mateEquiv_conjugateEquiv_symm
{B : Type u}
[Bicategory B]
{a b c d : B}
{f₁ : a ⟶ c}
{u₁ : c ⟶ a}
{f₂ : b ⟶ d}
{u₂ : d ⟶ b}
{l₁ : a ⟶ b}
{r₁ : b ⟶ a}
{l₂ : c ⟶ d}
{r₂ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(adj₃ : Adjunction f₁ u₁)
(adj₄ : Adjunction f₂ u₂)
(α : CategoryStruct.comp u₂ r₁ ⟶ CategoryStruct.comp r₂ u₁)
:
def
CategoryTheory.Bicategory.leftAdjointSquareConjugate.vcomp
{B : Type u}
[Bicategory B]
{a b c d : B}
{g : a ⟶ c}
{h : b ⟶ d}
{l₁ : a ⟶ b}
{l₂ l₃ : c ⟶ d}
(α : CategoryStruct.comp g l₂ ⟶ CategoryStruct.comp l₁ h)
(β : l₃ ⟶ l₂)
:
Composition of a squares between left adjoints with a conjugate square.
Equations
Instances For
def
CategoryTheory.Bicategory.rightAdjointSquareConjugate.vcomp
{B : Type u}
[Bicategory B]
{a b c d : B}
{g : a ⟶ c}
{h : b ⟶ d}
{r₁ : b ⟶ a}
{r₂ r₃ : d ⟶ c}
(α : CategoryStruct.comp r₁ g ⟶ CategoryStruct.comp h r₂)
(β : r₂ ⟶ r₃)
:
Composition of a squares between right adjoints with a conjugate square.
Equations
Instances For
theorem
CategoryTheory.Bicategory.mateEquiv_conjugateEquiv_vcomp
{B : Type u}
[Bicategory B]
{a b c d : B}
{g : a ⟶ c}
{h : b ⟶ d}
{l₁ : a ⟶ b}
{r₁ : b ⟶ a}
{l₂ : c ⟶ d}
{r₂ : d ⟶ c}
{l₃ : c ⟶ d}
{r₃ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(adj₃ : Adjunction l₃ r₃)
(α : CategoryStruct.comp g l₂ ⟶ CategoryStruct.comp l₁ h)
(β : l₃ ⟶ l₂)
:
(mateEquiv adj₁ adj₃) (leftAdjointSquareConjugate.vcomp α β) = rightAdjointSquareConjugate.vcomp ((mateEquiv adj₁ adj₂) α) ((conjugateEquiv adj₂ adj₃) β)
The mates equivalence commutes with this composition, essentially by mateEquiv_vcomp.
def
CategoryTheory.Bicategory.leftAdjointConjugateSquare.vcomp
{B : Type u}
[Bicategory B]
{a b c d : B}
{g : a ⟶ c}
{h : b ⟶ d}
{l₁ l₂ : a ⟶ b}
{l₃ : c ⟶ d}
(α : l₂ ⟶ l₁)
(β : CategoryStruct.comp g l₃ ⟶ CategoryStruct.comp l₂ h)
:
Composition of a conjugate square with a squares between left adjoints.
Equations
Instances For
def
CategoryTheory.Bicategory.rightAdjointConjugateSquare.vcomp
{B : Type u}
[Bicategory B]
{a b c d : B}
{g : a ⟶ c}
{h : b ⟶ d}
{r₁ r₂ : b ⟶ a}
{r₃ : d ⟶ c}
(α : r₁ ⟶ r₂)
(β : CategoryStruct.comp r₂ g ⟶ CategoryStruct.comp h r₃)
:
Composition of a conjugate square with a squares between right adjoints.
Equations
Instances For
theorem
CategoryTheory.Bicategory.conjugateEquiv_mateEquiv_vcomp
{B : Type u}
[Bicategory B]
{a b c d : B}
{g : a ⟶ c}
{h : b ⟶ d}
{l₁ : a ⟶ b}
{r₁ : b ⟶ a}
{l₂ : a ⟶ b}
{r₂ : b ⟶ a}
{l₃ : c ⟶ d}
{r₃ : d ⟶ c}
(adj₁ : Adjunction l₁ r₁)
(adj₂ : Adjunction l₂ r₂)
(adj₃ : Adjunction l₃ r₃)
(α : l₂ ⟶ l₁)
(β : CategoryStruct.comp g l₃ ⟶ CategoryStruct.comp l₂ h)
:
(mateEquiv adj₁ adj₃) (leftAdjointConjugateSquare.vcomp α β) = rightAdjointConjugateSquare.vcomp ((conjugateEquiv adj₁ adj₂) α) ((mateEquiv adj₂ adj₃) β)
The mates equivalence commutes with this composition, essentially by mateEquiv_vcomp.