Opposites of joins of categories

This file constructs the canonical equivalence of categories (C ⋆ D)ᵒᵖ ≌ Dᵒᵖ ⋆ Cᵒᵖ. The equivalence gets characterized in both directions.

def CategoryTheory.Join.opEquiv (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] : (Join C D)ᵒᵖ ≌ Join Dᵒᵖ Cᵒᵖ

The equivalence (C ⋆ D)ᵒᵖ ≌ Dᵒᵖ ⋆ Cᵒᵖ induced by Join.opEquivFunctor and Join.opEquivInverse.

@[simp]

theorem CategoryTheory.Join.opEquiv_functor_obj_op_left {C : Type u₁} (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (c : C) : (opEquiv C D).functor.obj (Opposite.op (left c)) = right (Opposite.op c)

@[simp]

theorem CategoryTheory.Join.opEquiv_functor_obj_op_right (C : Type u₁) {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (d : D) : (opEquiv C D).functor.obj (Opposite.op (right d)) = left (Opposite.op d)

@[simp]

theorem CategoryTheory.Join.opEquiv_functor_map_op_inclLeft {C : Type u₁} (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {c c' : C} (f : c ⟶ c') : (opEquiv C D).functor.map (Opposite.op ((inclLeft C D).map f)) = (inclRight Dᵒᵖ Cᵒᵖ).map (Opposite.op f)

@[simp]

theorem CategoryTheory.Join.opEquiv_functor_map_op_inclRight (C : Type u₁) {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {d d' : D} (f : d ⟶ d') : (opEquiv C D).functor.map (Opposite.op ((inclRight C D).map f)) = (inclLeft Dᵒᵖ Cᵒᵖ).map (Opposite.op f)

theorem CategoryTheory.Join.opEquiv_functor_map_op_edge {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (c : C) (d : D) : (opEquiv C D).functor.map (Opposite.op (edge c d)) = edge (Opposite.op d) (Opposite.op c)

def CategoryTheory.Join.InclLeftCompRightOpOpEquivFunctor (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] : (inclLeft C D).comp (opEquiv C D).functor.rightOp ≅ (inclRight Dᵒᵖ Cᵒᵖ).rightOp

Characterize (up to a rightOp) the action of the left inclusion on Join.opEquivFunctor.

@[simp]

theorem CategoryTheory.Join.InclLeftCompRightOpOpEquivFunctor_inv_app (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (X : C) : (InclLeftCompRightOpOpEquivFunctor C D).inv.app X = CategoryStruct.id (Opposite.op (right (Opposite.op X)))

@[simp]

theorem CategoryTheory.Join.InclLeftCompRightOpOpEquivFunctor_hom_app (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (X : C) : (InclLeftCompRightOpOpEquivFunctor C D).hom.app X = CategoryStruct.id (Opposite.op (right (Opposite.op X)))

def CategoryTheory.Join.InclRightCompRightOpOpEquivFunctor (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] : (inclRight C D).comp (opEquiv C D).functor.rightOp ≅ (inclLeft Dᵒᵖ Cᵒᵖ).rightOp

Characterize (up to a rightOp) the action of the right inclusion on Join.opEquivFunctor.

@[simp]

theorem CategoryTheory.Join.InclRightCompRightOpOpEquivFunctor_hom_app (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (X : D) : (InclRightCompRightOpOpEquivFunctor C D).hom.app X = CategoryStruct.id (Opposite.op (left (Opposite.op X)))

@[simp]

theorem CategoryTheory.Join.InclRightCompRightOpOpEquivFunctor_inv_app (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (X : D) : (InclRightCompRightOpOpEquivFunctor C D).inv.app X = CategoryStruct.id (Opposite.op (left (Opposite.op X)))

@[simp]

theorem CategoryTheory.Join.opEquiv_inverse_obj_left_op (C : Type u₁) {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (d : D) : (opEquiv C D).inverse.obj (left (Opposite.op d)) = Opposite.op (right d)

@[simp]

theorem CategoryTheory.Join.opEquiv_inverse_obj_right_op {C : Type u₁} (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (c : C) : (opEquiv C D).inverse.obj (right (Opposite.op c)) = Opposite.op (left c)

@[simp]

theorem CategoryTheory.Join.opEquiv_inverse_map_inclLeft_op (C : Type u₁) {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {d d' : D} (f : d ⟶ d') : (opEquiv C D).inverse.map ((inclLeft Dᵒᵖ Cᵒᵖ).map f.op) = Opposite.op ((inclRight C D).map f)

@[simp]

theorem CategoryTheory.Join.opEquiv_inverse_map_inclRight_op (C : Type u₁) {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {c c' : C} (f : c ⟶ c') : (opEquiv C D).inverse.map ((inclRight Dᵒᵖ Cᵒᵖ).map f.op) = Opposite.op ((inclLeft C D).map f)

@[simp]

theorem CategoryTheory.Join.opEquiv_inverse_map_edge_op {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (c : C) (d : D) : (opEquiv C D).inverse.map (edge (Opposite.op d) (Opposite.op c)) = Opposite.op (edge c d)

def CategoryTheory.Join.inclLeftCompOpEquivInverse (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] : (inclLeft Dᵒᵖ Cᵒᵖ).comp (opEquiv C D).inverse ≅ (inclRight C D).op

Characterize Join.opEquivInverse with respect to the left inclusion

def CategoryTheory.Join.inclRightCompOpEquivInverse (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] : (inclRight Dᵒᵖ Cᵒᵖ).comp (opEquiv C D).inverse ≅ (inclLeft C D).op

Characterize Join.opEquivInverse with respect to the right inclusion

@[simp]

theorem CategoryTheory.Join.inclLeftCompOpEquivInverse_hom_app_op (C : Type u₁) {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (d : D) : (inclLeftCompOpEquivInverse C D).hom.app (Opposite.op d) = CategoryStruct.id (Opposite.op (right d))

@[simp]

theorem CategoryTheory.Join.inclRightCompOpEquivInverse_hom_app_op {C : Type u₁} (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (c : C) : (inclRightCompOpEquivInverse C D).hom.app (Opposite.op c) = CategoryStruct.id (Opposite.op (left c))

@[simp]

theorem CategoryTheory.Join.inclLeftCompOpEquivInverse_inv_app_op (C : Type u₁) {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (d : D) : (inclLeftCompOpEquivInverse C D).inv.app (Opposite.op d) = CategoryStruct.id (Opposite.op (right d))

@[simp]

theorem CategoryTheory.Join.inclRightCompOpEquivInverse_inv_app_op {C : Type u₁} (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (c : C) : (inclRightCompOpEquivInverse C D).inv.app (Opposite.op c) = CategoryStruct.id (Opposite.op (left c))