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_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
        @[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
        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_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
          @[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_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
          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_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
            @[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