Documentation

Mathlib.CategoryTheory.Join.Pseudofunctor

Pseudofunctoriality of categorical joins #

In this file, we promote the join construction to two pseudofunctors Join.pseudofunctorLeft and Join.pseudoFunctorRight, expressing its pseudofunctoriality in each variable.

The structural isomorphism for composition of pseudoFunctorRight.

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

    The structural isomorphism for composition of pseudoFunctorLeft.

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

      The pseudofunctor sending D to C ⋆ D.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.Join.pseudofunctorRight_mapId_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Cat) (x : Join C D) :
        ((pseudofunctorRight C).mapId D).hom.app x = match x with | left x => comp (left x).id (comp (left x).id (left x).id) | right x => comp (right x).id (comp (right x).id (right x).id)
        @[simp]
        theorem CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_obj (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Cat} (F : X✝ Y✝) (X : Join C X✝) :
        ((pseudofunctorRight C).map F).obj X = match X with | left x => left x | right x => right (F.obj x)
        @[simp]
        theorem CategoryTheory.Join.pseudofunctorRight_mapComp_inv_app (C : Type u₁) [Category.{v₁, u₁} C] {a✝ b✝ c✝ : Cat} (F : Functor a✝ b✝) (G : Functor b✝ c✝) (X : Join C a✝) :
        ((pseudofunctorRight C).mapComp F G).inv.app X = comp ((mapPairComp (Functor.id C) F (Functor.id C) G).inv.app X) (match X with | left x => (left x).id | right x => (right (G.obj (F.obj x))).id)
        @[simp]
        theorem CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Cat} (F : X✝ Y✝) {X✝¹ Y✝¹ : Join C X✝} (f : X✝¹ Y✝¹) :
        ((pseudofunctorRight C).map F).map f = homInduction (fun (x x_1 : C) (f : x x_1) => (inclLeft C Y✝).map f) (fun (x x_1 : X✝) (g : x x_1) => (inclRight C Y✝).map (F.map g)) (fun (c : C) (d : X✝) => edge c (F.obj d)) f
        @[simp]
        theorem CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp (C : Type u₁) [Category.{v₁, u₁} C] (D : Cat) {X✝ Y✝ Z✝ : Join C D} (a✝ : X✝.Hom Y✝) (a✝¹ : Y✝.Hom Z✝) :
        CategoryStruct.comp a✝ a✝¹ = comp a✝ a✝¹
        @[simp]
        theorem CategoryTheory.Join.pseudofunctorRight_mapId_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Cat) (x : Join C D) :
        ((pseudofunctorRight C).mapId D).inv.app x = match x with | left x => comp (comp (left x).id (left x).id) (left x).id | right x => comp (comp (right x).id (right x).id) (right x).id
        @[simp]
        theorem CategoryTheory.Join.pseudofunctorRight_mapComp_hom_app (C : Type u₁) [Category.{v₁, u₁} C] {a✝ b✝ c✝ : Cat} (F : Functor a✝ b✝) (G : Functor b✝ c✝) (X : Join C a✝) :
        ((pseudofunctorRight C).mapComp F G).hom.app X = comp (match X with | left x => (left x).id | right x => (right (G.obj (F.obj x))).id) ((mapPairComp (Functor.id C) F (Functor.id C) G).hom.app X)
        @[simp]
        theorem CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_app (C : Type u₁) [Category.{v₁, u₁} C] {a✝ b✝ : Cat} {f✝ g✝ : a✝ b✝} (α : f✝ g✝) (x : Join C a✝) :
        ((pseudofunctorRight C).map₂ α).app x = match x with | left x => comp (left x).id (comp (left x).id (left x).id) | right x => comp (right (f✝.obj x)).id (comp ((inclRight C b✝).map (α.app x)) (right (g✝.obj x)).id)

        The pseudofunctor sending C to C ⋆ D.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_map (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : Cat} (F : X✝ Y✝) {X✝¹ Y✝¹ : Join (↑X✝) D} (f : X✝¹ Y✝¹) :
          ((pseudofunctorLeft D).map F).map f = homInduction (fun (x x_1 : X✝) (f : x x_1) => (inclLeft (↑Y✝) D).map (F.map f)) (fun (x x_1 : D) (g : x x_1) => (inclRight (↑Y✝) D).map g) (fun (c : X✝) (d : D) => edge (F.obj c) d) f
          @[simp]
          theorem CategoryTheory.Join.pseudofunctorLeft_mapId_hom_app (D : Type u₂) [Category.{v₂, u₂} D] (D✝ : Cat) (x : Join (↑D✝) D) :
          ((pseudofunctorLeft D).mapId D✝).hom.app x = match x with | left x => comp (left x).id (comp (left x).id (left x).id) | right x => comp (right x).id (comp (right x).id (right x).id)
          @[simp]
          theorem CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp (D : Type u₂) [Category.{v₂, u₂} D] (C : Cat) {X✝ Y✝ Z✝ : Join (↑C) D} (a✝ : X✝.Hom Y✝) (a✝¹ : Y✝.Hom Z✝) :
          CategoryStruct.comp a✝ a✝¹ = comp a✝ a✝¹
          @[simp]
          theorem CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_obj (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : Cat} (F : X✝ Y✝) (X : Join (↑X✝) D) :
          ((pseudofunctorLeft D).map F).obj X = match X with | left x => left (F.obj x) | right x => right x
          @[simp]
          theorem CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_app (D : Type u₂) [Category.{v₂, u₂} D] {a✝ b✝ c✝ : Cat} (F : Functor a✝ b✝) (G : Functor b✝ c✝) (X : Join (↑a✝) D) :
          ((pseudofunctorLeft D).mapComp F G).inv.app X = comp ((mapPairComp F (Functor.id D) G (Functor.id D)).inv.app X) (match X with | left x => (left (G.obj (F.obj x))).id | right x => (right x).id)
          @[simp]
          theorem CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_app (D : Type u₂) [Category.{v₂, u₂} D] {a✝ b✝ c✝ : Cat} (F : Functor a✝ b✝) (G : Functor b✝ c✝) (X : Join (↑a✝) D) :
          ((pseudofunctorLeft D).mapComp F G).hom.app X = comp (match X with | left x => (left (G.obj (F.obj x))).id | right x => (right x).id) ((mapPairComp F (Functor.id D) G (Functor.id D)).hom.app X)
          @[simp]
          theorem CategoryTheory.Join.pseudofunctorLeft_mapId_inv_app (D : Type u₂) [Category.{v₂, u₂} D] (D✝ : Cat) (x : Join (↑D✝) D) :
          ((pseudofunctorLeft D).mapId D✝).inv.app x = match x with | left x => comp (comp (left x).id (left x).id) (left x).id | right x => comp (comp (right x).id (right x).id) (right x).id
          @[simp]
          theorem CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_app (D : Type u₂) [Category.{v₂, u₂} D] {a✝ b✝ : Cat} {f✝ g✝ : a✝ b✝} (x✝ : f✝ g✝) (x : Join (↑a✝) D) :
          ((pseudofunctorLeft D).map₂ x✝).app x = match x with | left x => comp (left (f✝.obj x)).id (comp ((inclLeft (↑b✝) D).map (x✝.app x)) (left (g✝.obj x)).id) | right x => comp (right x).id (comp (right x).id (right x).id)