Documentation

Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Structured Arrow Categories as strict functor to Cat #

Forming a structured arrow category StructuredArrow d T with d : D and T : C ⥤ D is strictly functorial in S, inducing a functor Dᵒᵖ ⥤ Cat. This file constructs said functor and proves that, in the dual case, we can precompose it with another functor L : E ⥤ D to obtain a category equivalent to Comma L T.

source
def CategoryTheory.StructuredArrow.functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (T : Functor C D) :
Functor Dᵒᵖ Cat

The structured arrow category StructuredArrow d T depends on the chosen domain d : D in a functorial way, inducing a functor Dᵒᵖ ⥤ Cat.

Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.StructuredArrow.functor_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (T : Functor C D) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) :
      (functor T).map f = map f.unop
      source
      @[simp]
      theorem CategoryTheory.StructuredArrow.functor_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (T : Functor C D) (d : Dᵒᵖ) :
      (functor T).obj d = Cat.of (StructuredArrow (Opposite.unop d) T)
      source
      def CategoryTheory.CostructuredArrow.functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (T : Functor C D) :
      Functor D Cat

      The costructured arrow category CostructuredArrow T d depends on the chosen codomain d : D in a functorial way, inducing a functor D ⥤ Cat.

      Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.CostructuredArrow.functor_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (T : Functor C D) (d : D) :
          (functor T).obj d = Cat.of (CostructuredArrow T d)
          source
          @[simp]
          theorem CategoryTheory.CostructuredArrow.functor_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (T : Functor C D) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) :
          (functor T).map f = map f
          source
          def CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) :
          Functor (Grothendieck (R.comp (functor L))) (Comma L R)

          The functor used to establish the equivalence grothendieckPrecompFunctorEquivalence between the Grothendieck construction on CostructuredArrow.functor and the comma category.

          Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) {X✝ Y✝ : Grothendieck (R.comp (functor L))} (f : X✝ ⟶ Y✝) :
              ((grothendieckPrecompFunctorToComma L R).map f).right = f.base
              source
              @[simp]
              theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) {X✝ Y✝ : Grothendieck (R.comp (functor L))} (f : X✝ ⟶ Y✝) :
              ((grothendieckPrecompFunctorToComma L R).map f).left = f.fiber.left
              source
              @[simp]
              theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) (P : Grothendieck (R.comp (functor L))) :
              ((grothendieckPrecompFunctorToComma L R).obj P).right = P.base
              source
              @[simp]
              theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) (P : Grothendieck (R.comp (functor L))) :
              ((grothendieckPrecompFunctorToComma L R).obj P).left = P.fiber.left
              source
              @[simp]
              theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) (P : Grothendieck (R.comp (functor L))) :
              ((grothendieckPrecompFunctorToComma L R).obj P).hom = P.fiber.hom
              source
              def CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) (X : E) :
              (Grothendieck.ι (R.comp (functor L)) X).comp ((grothendieckPrecompFunctorToComma L R).comp (Comma.fst L R)) ≅ proj L (R.obj X)

              Fibers of grothendieckPrecompFunctorToComma L R, composed with Comma.fst L R, are isomorphic to the projection proj L (R.obj X).

              Equations
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) (X : E) (X✝ : ↑((R.comp (functor L)).obj X)) :
                  (ιCompGrothendieckPrecompFunctorToCommaCompFst L R X).hom.app X✝ = CategoryStruct.id X✝.left
                  source
                  @[simp]
                  theorem CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) (X : E) (X✝ : ↑((R.comp (functor L)).obj X)) :
                  (ιCompGrothendieckPrecompFunctorToCommaCompFst L R X).inv.app X✝ = CategoryStruct.id X✝.left
                  source
                  def CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) :
                  Functor (Comma L R) (Grothendieck (R.comp (functor L)))

                  The inverse functor used to establish the equivalence grothendieckPrecompFunctorEquivalence between the Grothendieck construction on CostructuredArrow.functor and the comma category.

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_fiber {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) (X : Comma L R) :
                      ((commaToGrothendieckPrecompFunctor L R).obj X).fiber = mk X.hom
                      source
                      @[simp]
                      theorem CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_base {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) (X : Comma L R) :
                      ((commaToGrothendieckPrecompFunctor L R).obj X).base = X.right
                      source
                      @[simp]
                      theorem CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) {X✝ Y✝ : Comma L R} (f : X✝ ⟶ Y✝) :
                      ((commaToGrothendieckPrecompFunctor L R).map f).fiber = homMk f.left ⋯
                      source
                      @[simp]
                      theorem CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_base {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) {X✝ Y✝ : Comma L R} (f : X✝ ⟶ Y✝) :
                      ((commaToGrothendieckPrecompFunctor L R).map f).base = f.right
                      source
                      def CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) :
                      Grothendieck (R.comp (functor L)) ≌ Comma L R

                      For L : C ⥤ D, taking the Grothendieck construction of CostructuredArrow.functor L precomposed with another functor R : E ⥤ D results in a category which is equivalent to the comma category Comma L R.

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) :
                          (grothendieckPrecompFunctorEquivalence L R).inverse = commaToGrothendieckPrecompFunctor L R
                          source
                          @[simp]
                          theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) :
                          (grothendieckPrecompFunctorEquivalence L R).unitIso = NatIso.ofComponents (fun (x : Grothendieck (R.comp (functor L))) => Iso.refl ((Functor.id (Grothendieck (R.comp (functor L)))).obj x)) ⋯
                          source
                          @[simp]
                          theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) :
                          (grothendieckPrecompFunctorEquivalence L R).counitIso = NatIso.ofComponents (fun (x : Comma L R) => Iso.refl (((commaToGrothendieckPrecompFunctor L R).comp (grothendieckPrecompFunctorToComma L R)).obj x)) ⋯
                          source
                          @[simp]
                          theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (L : Functor C D) (R : Functor E D) :
                          (grothendieckPrecompFunctorEquivalence L R).functor = grothendieckPrecompFunctorToComma L R
                          source
                          def CategoryTheory.CostructuredArrow.grothendieckProj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) :
                          Functor (Grothendieck (functor L)) C

                          The functor projecting out the domain of arrows from the Grothendieck construction on costructured arrows.

                          Equations
                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.CostructuredArrow.grothendieckProj_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (X : Grothendieck (functor L)) :
                              (grothendieckProj L).obj X = X.fiber.left
                              source
                              @[simp]
                              theorem CategoryTheory.CostructuredArrow.grothendieckProj_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) {X✝ Y✝ : Grothendieck (functor L)} (f : X✝ ⟶ Y✝) :
                              (grothendieckProj L).map f = f.fiber.left
                              source
                              def CategoryTheory.CostructuredArrow.ιCompGrothendieckProj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (X : D) :
                              (Grothendieck.ι (functor L) X).comp (grothendieckProj L) ≅ proj L X

                              Fibers of grothendieckProj L are isomorphic to the projection proj L X.

                              Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (X : D) (X✝ : ↑(((Functor.id D).comp (functor L)).obj X)) :
                                  (ιCompGrothendieckProj L X).inv.app X✝ = CategoryStruct.id X✝.left
                                  source
                                  @[simp]
                                  theorem CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (X : D) (X✝ : ↑(((Functor.id D).comp (functor L)).obj X)) :
                                  (ιCompGrothendieckProj L X).hom.app X✝ = CategoryStruct.id X✝.left
                                  source
                                  def CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) {X Y : D} (f : X ⟶ Y) :
                                  (map f).comp ((Grothendieck.ι (functor L) Y).comp (grothendieckProj L)) ≅ proj L X

                                  Functors between costructured arrow categories induced by morphisms in the base category composed with fibers of grothendieckProj L are isomorphic to the projection proj L X.

                                  Equations
                                    Instances For
                                      source
                                      @[simp]
                                      theorem CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) {X Y : D} (f : X ⟶ Y) (X✝ : CostructuredArrow L X) :
                                      (mapCompιCompGrothendieckProj L f).hom.app X✝ = CategoryStruct.id X✝.left
                                      source
                                      @[simp]
                                      theorem CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) {X Y : D} (f : X ⟶ Y) (X✝ : CostructuredArrow L X) :
                                      (mapCompιCompGrothendieckProj L f).inv.app X✝ = CategoryStruct.id X✝.left
                                      source
                                      def CategoryTheory.CostructuredArrow.preFunctor {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] {D : Type u₁} [Category.{v₁, u₁} D] (S : Functor C D) (T : Functor D E) :
                                      functor (S.comp T) ⟶ functor T

                                      The functor CostructuredArrow.pre induces a natural transformation CostructuredArrow.functor (S ⋙ T) ⟶ CostructuredArrow.functor T for S : C ⥤ D and T : D ⥤ E.

                                      Equations
                                        Instances For
                                          source
                                          @[simp]
                                          theorem CategoryTheory.CostructuredArrow.preFunctor_app {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] {D : Type u₁} [Category.{v₁, u₁} D] (S : Functor C D) (T : Functor D E) (e : E) :
                                          (preFunctor S T).app e = pre S T e