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.

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.

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

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

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.

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

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

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.

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

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

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

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

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

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.

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

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

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.

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

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

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

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

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.

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

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

@[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)) ⋯

@[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)) ⋯

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.

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

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

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

• CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X = CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst L (CategoryTheory.Functor.id D) X

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

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

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.

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

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