Documentation

Mathlib.CategoryTheory.Join.Opposites

Opposites of joins of categories #

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

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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)
    source
    @[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)
    source
    @[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)
    source
    @[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)
    source
    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)
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[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.comp (CategoryStruct.id (Opposite.op (right (Opposite.op X)))) (((inclLeft C D).isoWhiskerLeft (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp { app := fun (x : C × D) => (edge (Opposite.op x.2) (Opposite.op x.1)).op, naturality := ⋯ }).leftOpRightOpIso).inv.app X)
      source
      @[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.comp (((inclLeft C D).isoWhiskerLeft (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp { app := fun (x : C × D) => (edge (Opposite.op x.2) (Opposite.op x.1)).op, naturality := ⋯ }).leftOpRightOpIso).hom.app X) (CategoryStruct.id (Opposite.op (right (Opposite.op X))))
      source
      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[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.comp (((inclRight C D).isoWhiskerLeft (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp { app := fun (x : C × D) => (edge (Opposite.op x.2) (Opposite.op x.1)).op, naturality := ⋯ }).leftOpRightOpIso).hom.app X) (CategoryStruct.id (Opposite.op (left (Opposite.op X))))
        source
        @[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.comp (CategoryStruct.id (Opposite.op (left (Opposite.op X)))) (((inclRight C D).isoWhiskerLeft (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp { app := fun (x : C × D) => (edge (Opposite.op x.2) (Opposite.op x.1)).op, naturality := ⋯ }).leftOpRightOpIso).inv.app X)
        source
        @[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)
        source
        @[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)
        source
        @[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)
        source
        @[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)
        source
        @[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)
        source
        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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[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))
            source
            @[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))
            source
            @[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))
            source
            @[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))