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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (T : CategoryTheory.Functor C D) :
CategoryTheory.Functor Dᵒᵖ CategoryTheory.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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.StructuredArrow.functor_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (T : CategoryTheory.Functor C D) (d : Dᵒᵖ) :
    (CategoryTheory.StructuredArrow.functor T).obj d = CategoryTheory.Cat.of (CategoryTheory.StructuredArrow (Opposite.unop d) T)
    source
    @[simp]
    theorem CategoryTheory.StructuredArrow.functor_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (T : CategoryTheory.Functor C D) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) :
    (CategoryTheory.StructuredArrow.functor T).map f = CategoryTheory.StructuredArrow.map f.unop
    source
    def CategoryTheory.CostructuredArrow.functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (T : CategoryTheory.Functor C D) :
    CategoryTheory.Functor D CategoryTheory.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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.CostructuredArrow.functor_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (T : CategoryTheory.Functor C D) (d : D) :
      (CategoryTheory.CostructuredArrow.functor T).obj d = CategoryTheory.Cat.of (CategoryTheory.CostructuredArrow T d)
      source
      @[simp]
      theorem CategoryTheory.CostructuredArrow.functor_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (T : CategoryTheory.Functor C D) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) :
      (CategoryTheory.CostructuredArrow.functor T).map f = CategoryTheory.CostructuredArrow.map f
      source
      def CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) :
      CategoryTheory.Functor (CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))) (CategoryTheory.Comma L R)

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) {X✝ Y✝ : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))} (f : X✝ ⟶ Y✝) :
        ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).map f).right = f.base
        source
        @[simp]
        theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (P : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))) :
        ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).obj P).right = P.base
        source
        @[simp]
        theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) {X✝ Y✝ : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))} (f : X✝ ⟶ Y✝) :
        ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).map f).left = f.fiber.left
        source
        @[simp]
        theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (P : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))) :
        ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).obj P).hom = P.fiber.hom
        source
        @[simp]
        theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (P : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))) :
        ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).obj P).left = P.fiber.left
        source
        def CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : E) :
        (CategoryTheory.Grothendieck.ι (R.comp (CategoryTheory.CostructuredArrow.functor L)) X).comp ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).comp (CategoryTheory.Comma.fst L R)) ≅ CategoryTheory.CostructuredArrow.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
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : E) (X✝ : ↑((R.comp (CategoryTheory.CostructuredArrow.functor L)).obj X)) :
          (CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst L R X).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
          source
          @[simp]
          theorem CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : E) (X✝ : ↑((R.comp (CategoryTheory.CostructuredArrow.functor L)).obj X)) :
          (CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst L R X).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
          source
          def CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) :
          CategoryTheory.Functor (CategoryTheory.Comma L R) (CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L)))

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) {X✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) :
            ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).map f).fiber = CategoryTheory.CostructuredArrow.homMk f.left ⋯
            source
            @[simp]
            theorem CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_base {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : CategoryTheory.Comma L R) :
            ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).obj X).base = X.right
            source
            @[simp]
            theorem CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_base {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) {X✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) :
            ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).map f).base = f.right
            source
            @[simp]
            theorem CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_fiber {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : CategoryTheory.Comma L R) :
            ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).obj X).fiber = CategoryTheory.CostructuredArrow.mk X.hom
            source
            def CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) :
            CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L)) ≌ CategoryTheory.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
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) :
              (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence L R).functor = CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R
              source
              @[simp]
              theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) :
              (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence L R).inverse = CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R
              source
              @[simp]
              theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) :
              (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence L R).counitIso = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.Comma L R) => CategoryTheory.Iso.refl (((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).comp (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R)).obj x)) ⋯
              source
              @[simp]
              theorem CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) :
              (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence L R).unitIso = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))) => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L)))).obj x)) ⋯
              source
              def CategoryTheory.CostructuredArrow.grothendieckProj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) :
              CategoryTheory.Functor (CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)) C

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.CostructuredArrow.grothendieckProj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)} (f : X✝ ⟶ Y✝) :
                (CategoryTheory.CostructuredArrow.grothendieckProj L).map f = f.fiber.left
                source
                @[simp]
                theorem CategoryTheory.CostructuredArrow.grothendieckProj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (X : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)) :
                (CategoryTheory.CostructuredArrow.grothendieckProj L).obj X = X.fiber.left
                source
                def CategoryTheory.CostructuredArrow.ιCompGrothendieckProj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (X : D) :
                (CategoryTheory.Grothendieck.ι (CategoryTheory.CostructuredArrow.functor L) X).comp (CategoryTheory.CostructuredArrow.grothendieckProj L) ≅ CategoryTheory.CostructuredArrow.proj L X

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

                Equations
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (X : D) (X✝ : ↑(((CategoryTheory.Functor.id D).comp (CategoryTheory.CostructuredArrow.functor L)).obj X)) :
                  (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
                  source
                  @[simp]
                  theorem CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (X : D) (X✝ : ↑(((CategoryTheory.Functor.id D).comp (CategoryTheory.CostructuredArrow.functor L)).obj X)) :
                  (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
                  source
                  def CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) :
                  (CategoryTheory.CostructuredArrow.map f).comp ((CategoryTheory.Grothendieck.ι (CategoryTheory.CostructuredArrow.functor L) Y).comp (CategoryTheory.CostructuredArrow.grothendieckProj L)) ≅ CategoryTheory.CostructuredArrow.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
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) (X✝ : CategoryTheory.CostructuredArrow L X) :
                    (CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj L f).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
                    source
                    @[simp]
                    theorem CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) (X✝ : CategoryTheory.CostructuredArrow L X) :
                    (CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj L f).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝.left