Opposite bicategories

We construct the 1-cell opposite of a bicategory B, called Bᵒᵖ. It is defined as follows

• The objects of Bᵒᵖ correspond to objects of B.
• The morphisms X ⟶ Y in Bᵒᵖ are the morphisms Y ⟶ X in B.
• The 2-morphisms f ⟶ g in Bᵒᵖ are the 2-morphisms f ⟶ g in B. In other words, the directions of the 2-morphisms are preserved.

Remarks

There are multiple notions of opposite categories for bicategories.

• There is 1-cell dual Bᵒᵖ as defined above.
• There is the 2-cell dual, Cᶜᵒ where only the 2-morphisms are reversed
• There is the bi-dual Cᶜᵒᵒᵖ where the directions of both the 1-morphisms and the 2-morphisms are reversed.

TODO

• Define the 2-cell dual Cᶜᵒ.
• Provide various lemmas for going between LocallyDiscrete Cᵒᵖ and (LocallyDiscrete C)ᵒᵖ.

Note: Cᶜᵒᵒᵖ is WIP by Christian Merten.

structure Bicategory.Opposite.Hom2 {B : Type u} [CategoryTheory.Bicategory B] {a b : Bᵒᵖ} (f g : a ⟶ b) : Type w

Type synonym for 2-morphisms in the opposite bicategory.

• op2' :: (
• unop2 : f.unop ⟶ g.unop

  Bᵒᵖ preserves the direction of all 2-morphisms in B

• )

@[implicit_reducible]

instance Bicategory.Opposite.homCategory {B : Type u} [CategoryTheory.Bicategory B] (a b : Bᵒᵖ) : CategoryTheory.Category.{w, v} (a ⟶ b)

Equations

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

@[simp]

theorem Bicategory.Opposite.homCategory_comp_unop2 {B : Type u} [CategoryTheory.Bicategory B] (a b : Bᵒᵖ) {X✝ Y✝ Z✝ : a ⟶ b} (η : Hom2 X✝ Y✝) (θ : Hom2 Y✝ Z✝) : (CategoryTheory.CategoryStruct.comp η θ).unop2 = CategoryTheory.CategoryStruct.comp η.unop2 θ.unop2

@[simp]

theorem Bicategory.Opposite.homCategory_id_unop2 {B : Type u} [CategoryTheory.Bicategory B] (a b : Bᵒᵖ) (f : a ⟶ b) : (CategoryTheory.CategoryStruct.id f).unop2 = CategoryTheory.CategoryStruct.id f.unop

def Bicategory.Opposite.op2 {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g) : f.op ⟶ g.op

Synonym for constructor of Hom2 where the 1-morphisms f and g lie in B and not Bᵒᵖ.

Equations

• Bicategory.Opposite.op2 η = { unop2 := η }

@[simp]

theorem Bicategory.Opposite.unop2_op2 {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g) : (op2 η).unop2 = η

@[simp]

theorem Bicategory.Opposite.op2_unop2 {B : Type u} [CategoryTheory.Bicategory B] {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f ⟶ g) : op2 η.unop2 = η

@[simp]

theorem Bicategory.Opposite.op2_comp {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) : op2 (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (op2 η) (op2 θ)

@[simp]

theorem Bicategory.Opposite.op2_id {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} : op2 (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id f.op

@[simp]

theorem Bicategory.Opposite.unop2_comp {B : Type u} [CategoryTheory.Bicategory B] {a b : Bᵒᵖ} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) : (CategoryTheory.CategoryStruct.comp η θ).unop2 = CategoryTheory.CategoryStruct.comp η.unop2 θ.unop2

@[simp]

theorem Bicategory.Opposite.unop2_id {B : Type u} [CategoryTheory.Bicategory B] {a b : Bᵒᵖ} {f : a ⟶ b} : (CategoryTheory.CategoryStruct.id f).unop2 = CategoryTheory.CategoryStruct.id f.unop

@[simp]

theorem Bicategory.Opposite.unop2_id_bop {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} : (CategoryTheory.CategoryStruct.id f.op).unop2 = CategoryTheory.CategoryStruct.id f

@[simp]

theorem Bicategory.Opposite.op2_id_unbop {B : Type u} [CategoryTheory.Bicategory B] {a b : Bᵒᵖ} {f : a ⟶ b} : op2 (CategoryTheory.CategoryStruct.id f.unop) = CategoryTheory.CategoryStruct.id f

def Bicategory.Opposite.opFunctor {B : Type u} [CategoryTheory.Bicategory B] (a b : B) : CategoryTheory.Functor (a ⟶ b) (Opposite.op b ⟶ Opposite.op a)

The natural functor from the hom-category a ⟶ b in B to its bicategorical opposite bop b ⟶ bop a.

Equations

• Bicategory.Opposite.opFunctor a b = { obj := fun (f : a ⟶ b) => f.op, map := fun {X Y : a ⟶ b} (η : X ⟶ Y) => Bicategory.Opposite.op2 η, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Bicategory.Opposite.opFunctor_map {B : Type u} [CategoryTheory.Bicategory B] (a b : B) {X✝ Y✝ : a ⟶ b} (η : X✝ ⟶ Y✝) : (opFunctor a b).map η = op2 η

@[simp]

theorem Bicategory.Opposite.opFunctor_obj {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (f : a ⟶ b) : (opFunctor a b).obj f = f.op

def Bicategory.Opposite.unopFunctor {B : Type u} [CategoryTheory.Bicategory B] (a b : Bᵒᵖ) : CategoryTheory.Functor (a ⟶ b) (Opposite.unop b ⟶ Opposite.unop a)

The functor from the hom-category a ⟶ b in Bᵒᵖ to its bicategorical opposite unop b ⟶ unop a.

Equations

• Bicategory.Opposite.unopFunctor a b = { obj := fun (f : a ⟶ b) => f.unop, map := fun {X Y : a ⟶ b} (η : X ⟶ Y) => η.unop2, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Bicategory.Opposite.unopFunctor_map {B : Type u} [CategoryTheory.Bicategory B] (a b : Bᵒᵖ) {X✝ Y✝ : a ⟶ b} (η : X✝ ⟶ Y✝) : (unopFunctor a b).map η = η.unop2

@[simp]

theorem Bicategory.Opposite.unopFunctor_obj {B : Type u} [CategoryTheory.Bicategory B] (a b : Bᵒᵖ) (f : a ⟶ b) : (unopFunctor a b).obj f = f.unop

@[reducible, inline]

abbrev CategoryTheory.Iso.op2 {B : Type u} [Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ≅ g) : f.op ≅ g.op

A 2-isomorphism in B gives a 2-isomorphism in Bᵒᵖ

Equations

• η.op2 = (Bicategory.Opposite.opFunctor a b).mapIso η

@[simp]

theorem CategoryTheory.Iso.op2_inv_unop2 {B : Type u} [Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ≅ g) : η.op2.inv.unop2 = η.inv

@[simp]

theorem CategoryTheory.Iso.op2_hom_unop2 {B : Type u} [Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ≅ g) : η.op2.hom.unop2 = η.hom

@[reducible, inline]

abbrev CategoryTheory.Iso.op2_unop {B : Type u} [Bicategory B] {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f.unop ≅ g.unop) : f ≅ g

A 2-isomorphism in B gives a 2-isomorphism in Bᵒᵖ

Equations

• η.op2_unop = (Bicategory.Opposite.opFunctor (Opposite.unop b) (Opposite.unop a)).mapIso η

@[simp]

theorem CategoryTheory.Iso.op2_unop_hom_unop2 {B : Type u} [Bicategory B] {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f.unop ≅ g.unop) : η.op2_unop.hom.unop2 = η.hom

@[simp]

theorem CategoryTheory.Iso.op2_unop_inv_unop2 {B : Type u} [Bicategory B] {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f.unop ≅ g.unop) : η.op2_unop.inv.unop2 = η.inv

@[reducible, inline]

abbrev CategoryTheory.Iso.unop2 {B : Type u} [Bicategory B] {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f ≅ g) : f.unop ≅ g.unop

A 2-isomorphism in Bᵒᵖ gives a 2-isomorphism in B

Equations

• η.unop2 = (Bicategory.Opposite.unopFunctor a b).mapIso η

@[simp]

theorem CategoryTheory.Iso.unop2_hom {B : Type u} [Bicategory B] {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f ≅ g) : η.unop2.hom = η.hom.unop2

@[simp]

theorem CategoryTheory.Iso.unop2_inv {B : Type u} [Bicategory B] {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f ≅ g) : η.unop2.inv = η.inv.unop2

@[reducible, inline]

abbrev CategoryTheory.Iso.unop2_op {B : Type u} [Bicategory B] {a b : B} {f g : a ⟶ b} (η : f.op ≅ g.op) : f ≅ g

A 2-isomorphism in Bᵒᵖ gives a 2-isomorphism in B

Equations

• η.unop2_op = (Bicategory.Opposite.unopFunctor (Opposite.op b) (Opposite.op a)).mapIso η

@[simp]

theorem CategoryTheory.Iso.unop2_op_inv {B : Type u} [Bicategory B] {a b : B} {f g : a ⟶ b} (η : f.op ≅ g.op) : η.unop2_op.inv = η.inv.unop2

@[simp]

theorem CategoryTheory.Iso.unop2_op_hom {B : Type u} [Bicategory B] {a b : B} {f g : a ⟶ b} (η : f.op ≅ g.op) : η.unop2_op.hom = η.hom.unop2

@[simp]

theorem CategoryTheory.Iso.unop2_op2 {B : Type u} [Bicategory B] {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f ≅ g) : η.unop2.op2 = η

@[implicit_reducible]

instance Bicategory.Opposite.bicategory {B : Type u} [CategoryTheory.Bicategory B] : CategoryTheory.Bicategory Bᵒᵖ

The 1-cell dual bicategory Bᵒᵖ.

It is defined as follows.

• The objects of Bᵒᵖ correspond to objects of B.
• The morphisms X ⟶ Y in Bᵒᵖ are the morphisms Y ⟶ X in B.
• The 2-morphisms f ⟶ g in Bᵒᵖ are the 2-morphisms f ⟶ g in B. In other words, the directions of the 2-morphisms are preserved.

Equations

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

@[simp]

theorem Bicategory.Opposite.bicategory_homCategory_comp_unop2 {B : Type u} [CategoryTheory.Bicategory B] (a b : Bᵒᵖ) {X✝ Y✝ Z✝ : a ⟶ b} (η : Hom2 X✝ Y✝) (θ : Hom2 Y✝ Z✝) : (CategoryTheory.CategoryStruct.comp η θ).unop2 = CategoryTheory.CategoryStruct.comp η.unop2 θ.unop2

@[simp]

theorem Bicategory.Opposite.bicategory_associator_hom_unop2 {B : Type u} [CategoryTheory.Bicategory B] {a✝ b✝ c✝ d✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (h : c✝ ⟶ d✝) : (CategoryTheory.Bicategory.associator f g h).hom.unop2 = (CategoryTheory.Bicategory.associator h.unop g.unop f.unop).inv

@[simp]

theorem Bicategory.Opposite.bicategory_whiskerLeft_unop2 {B : Type u} [CategoryTheory.Bicategory B] {a✝ b✝ c✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) (g h : b✝ ⟶ c✝) (η : g ⟶ h) : (CategoryTheory.Bicategory.whiskerLeft f η).unop2 = CategoryTheory.Bicategory.whiskerRight η.unop2 f.unop

@[simp]

theorem Bicategory.Opposite.bicategory_leftUnitor_inv_unop2 {B : Type u} [CategoryTheory.Bicategory B] {a✝ b✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) : (CategoryTheory.Bicategory.leftUnitor f).inv.unop2 = (CategoryTheory.Bicategory.rightUnitor f.unop).inv

@[simp]

theorem Bicategory.Opposite.bicategory_leftUnitor_hom_unop2 {B : Type u} [CategoryTheory.Bicategory B] {a✝ b✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) : (CategoryTheory.Bicategory.leftUnitor f).hom.unop2 = (CategoryTheory.Bicategory.rightUnitor f.unop).hom

@[simp]

theorem Bicategory.Opposite.bicategory_rightUnitor_inv_unop2 {B : Type u} [CategoryTheory.Bicategory B] {a✝ b✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) : (CategoryTheory.Bicategory.rightUnitor f).inv.unop2 = (CategoryTheory.Bicategory.leftUnitor f.unop).inv

@[simp]

theorem Bicategory.Opposite.bicategory_associator_inv_unop2 {B : Type u} [CategoryTheory.Bicategory B] {a✝ b✝ c✝ d✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (h : c✝ ⟶ d✝) : (CategoryTheory.Bicategory.associator f g h).inv.unop2 = (CategoryTheory.Bicategory.associator h.unop g.unop f.unop).hom

@[simp]

theorem Bicategory.Opposite.bicategory_homCategory_id_unop2 {B : Type u} [CategoryTheory.Bicategory B] (a b : Bᵒᵖ) (f : a ⟶ b) : (CategoryTheory.CategoryStruct.id f).unop2 = CategoryTheory.CategoryStruct.id f.unop

@[simp]

theorem Bicategory.Opposite.bicategory_whiskerRight_unop2 {B : Type u} [CategoryTheory.Bicategory B] {a✝ b✝ c✝ : Bᵒᵖ} {f✝ g✝ : a✝ ⟶ b✝} (η : f✝ ⟶ g✝) (h : b✝ ⟶ c✝) : (CategoryTheory.Bicategory.whiskerRight η h).unop2 = CategoryTheory.Bicategory.whiskerLeft h.unop η.unop2

@[simp]

theorem Bicategory.Opposite.bicategory_rightUnitor_hom_unop2 {B : Type u} [CategoryTheory.Bicategory B] {a✝ b✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) : (CategoryTheory.Bicategory.rightUnitor f).hom.unop2 = (CategoryTheory.Bicategory.leftUnitor f.unop).hom

@[simp]

theorem Bicategory.Opposite.op2_whiskerLeft {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g g' : b ⟶ c} (η : g ⟶ g') : op2 (CategoryTheory.Bicategory.whiskerLeft f η) = CategoryTheory.Bicategory.whiskerRight (op2 η) f.op

@[simp]

theorem Bicategory.Opposite.op2_whiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f f' : a ⟶ b} {g : b ⟶ c} (η : f ⟶ f') : op2 (CategoryTheory.Bicategory.whiskerRight η g) = CategoryTheory.Bicategory.whiskerLeft g.op (op2 η)

@[simp]

theorem Bicategory.Opposite.op2_associator {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : (CategoryTheory.Bicategory.associator f g h).op2 = (CategoryTheory.Bicategory.associator h.op g.op f.op).symm

@[simp]

theorem Bicategory.Opposite.op2_associator_hom {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : op2 (CategoryTheory.Bicategory.associator f g h).hom = (CategoryTheory.Bicategory.associator h.op g.op f.op).symm.hom

@[simp]

theorem Bicategory.Opposite.op2_associator_inv {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : op2 (CategoryTheory.Bicategory.associator f g h).inv = (CategoryTheory.Bicategory.associator h.op g.op f.op).symm.inv

@[simp]

theorem Bicategory.Opposite.op2_leftUnitor {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) : (CategoryTheory.Bicategory.leftUnitor f).op2 = CategoryTheory.Bicategory.rightUnitor f.op

@[simp]

theorem Bicategory.Opposite.op2_leftUnitor_hom {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) : op2 (CategoryTheory.Bicategory.leftUnitor f).hom = (CategoryTheory.Bicategory.rightUnitor f.op).hom

@[simp]

theorem Bicategory.Opposite.op2_leftUnitor_inv {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) : op2 (CategoryTheory.Bicategory.leftUnitor f).inv = (CategoryTheory.Bicategory.rightUnitor f.op).inv

@[simp]

theorem Bicategory.Opposite.op2_rightUnitor {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) : (CategoryTheory.Bicategory.rightUnitor f).op2 = CategoryTheory.Bicategory.leftUnitor f.op

@[simp]

theorem Bicategory.Opposite.op2_rightUnitor_hom {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) : op2 (CategoryTheory.Bicategory.rightUnitor f).hom = (CategoryTheory.Bicategory.leftUnitor f.op).hom

@[simp]

theorem Bicategory.Opposite.op2_rightUnitor_inv {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) : op2 (CategoryTheory.Bicategory.rightUnitor f).inv = (CategoryTheory.Bicategory.leftUnitor f.op).inv