The category of "structured arrows" #
For T : C ⥤ D
, a T
-structured arrow with source S : D
is just a morphism S ⟶ T.obj Y
, for some Y : C
.
These form a category with morphisms g : Y ⟶ Y'
making the obvious diagram commute.
We prove that 𝟙 (T.obj Y)
is the initial object in T
-structured objects with source T.obj Y
.
The category of T
-structured arrows with domain S : D
(here T : C ⥤ D
),
has as its objects D
-morphisms of the form S ⟶ T Y
, for some Y : C
,
and morphisms C
-morphisms Y ⟶ Y'
making the obvious triangle commute.
Equations
Instances for category_theory.structured_arrow
- category_theory.structured_arrow.category
- category_theory.structured_arrow.has_limits_of_shape
- category_theory.structured_arrow.has_limits
- category_theory.representably_flat.cofiltered
- category_theory.Ran_is_sheaf_of_cover_lifting.category_theory.limits.has_limits_of_shape
- category_theory.functor.final.out
- category_theory.functor.final.category_theory.structured_arrow.nonempty
- category_theory.structured_arrow.well_powered_structured_arrow
- Top.presheaf.sheaf_condition.category_theory.structured_arrow.nonempty
The obvious projection functor from structured arrows.
Equations
Instances for category_theory.structured_arrow.proj
Construct a structured arrow from a morphism.
To construct a morphism of structured arrows, we need a morphism of the objects underlying the target, and to check that the triangle commutes.
Equations
- category_theory.structured_arrow.hom_mk g w = {left := category_theory.eq_to_hom category_theory.structured_arrow.hom_mk._proof_1, right := g, w' := _}
Instances for category_theory.structured_arrow.hom_mk
Given a structured arrow X ⟶ F(U)
, and an arrow U ⟶ Y
, we can construct a morphism of
structured arrow given by (X ⟶ F(U)) ⟶ (X ⟶ F(U) ⟶ F(Y))
.
To construct an isomorphism of structured arrows, we need an isomorphism of the objects underlying the target, and to check that the triangle commutes.
Equations
- category_theory.structured_arrow.iso_mk g w = category_theory.comma.iso_mk (category_theory.eq_to_iso category_theory.structured_arrow.iso_mk._proof_1) g _
The converse of this is true with additional assumptions, see mono_iff_mono_right
.
Eta rule for structured arrows. Prefer structured_arrow.eta
, since equality of objects tends
to cause problems.
Eta rule for structured arrows.
Equations
A morphism between source objects S ⟶ S'
contravariantly induces a functor between structured arrows,
structured_arrow S' T ⥤ structured_arrow S T
.
Ideally this would be described as a 2-functor from D
(promoted to a 2-category with equations as 2-morphisms)
to Cat
.
The identity structured arrow is initial.
Equations
- category_theory.structured_arrow.mk_id_initial = {desc := λ (c : category_theory.limits.cocone (category_theory.functor.empty (category_theory.structured_arrow (T.obj Y) T))), category_theory.structured_arrow.hom_mk (T.preimage c.X.hom) _, fac' := _, uniq' := _}
The functor (S, F ⋙ G) ⥤ (S, G)
.
Equations
The functor (S, F) ⥤ (G(S), F ⋙ G)
.
Equations
- category_theory.structured_arrow.post S F G = {obj := λ (X : category_theory.structured_arrow S F), {left := {as := punit.star}, right := X.right, hom := G.map X.hom}, map := λ (X Y : category_theory.structured_arrow S F) (f : X ⟶ Y), {left := id (λ (S : C) (F : B ⥤ C) (G : C ⥤ D) (X Y : category_theory.structured_arrow S F) (f : X ⟶ Y), {down := id (λ (S : C) (F : B ⥤ C) (G : C ⥤ D) (X Y : category_theory.structured_arrow S F) (f : X ⟶ Y), category_theory.structured_arrow.post._proof_1.mpr {down := _}) S F G X Y f}) S F G X Y f, right := f.right, w' := _}, map_id' := _, map_comp' := _}
The category of S
-costructured arrows with target T : D
(here S : C ⥤ D
),
has as its objects D
-morphisms of the form S Y ⟶ T
, for some Y : C
,
and morphisms C
-morphisms Y ⟶ Y'
making the obvious triangle commute.
Equations
Instances for category_theory.costructured_arrow
The obvious projection functor from costructured arrows.
Equations
Instances for category_theory.costructured_arrow.proj
Construct a costructured arrow from a morphism.
To construct a morphism of costructured arrows, we need a morphism of the objects underlying the source, and to check that the triangle commutes.
Equations
- category_theory.costructured_arrow.hom_mk g w = {left := g, right := category_theory.eq_to_hom category_theory.costructured_arrow.hom_mk._proof_1, w' := _}
Instances for category_theory.costructured_arrow.hom_mk
To construct an isomorphism of costructured arrows, we need an isomorphism of the objects underlying the source, and to check that the triangle commutes.
Equations
- category_theory.costructured_arrow.iso_mk g w = category_theory.comma.iso_mk g (category_theory.eq_to_iso category_theory.costructured_arrow.iso_mk._proof_1) _
The converse of this is true with additional assumptions, see epi_iff_epi_left
.
Eta rule for costructured arrows. Prefer costructured_arrow.eta
, as equality of objects tends
to cause problems.
Eta rule for costructured arrows.
Equations
A morphism between target objects T ⟶ T'
covariantly induces a functor between costructured arrows,
costructured_arrow S T ⥤ costructured_arrow S T'
.
Ideally this would be described as a 2-functor from D
(promoted to a 2-category with equations as 2-morphisms)
to Cat
.
The identity costructured arrow is terminal.
Equations
- category_theory.costructured_arrow.mk_id_terminal = {lift := λ (c : category_theory.limits.cone (category_theory.functor.empty (category_theory.costructured_arrow S (S.obj Y)))), category_theory.costructured_arrow.hom_mk (S.preimage c.X.hom) _, fac' := _, uniq' := _}
The functor (F ⋙ G, S) ⥤ (G, S)
.
Equations
The functor (F, S) ⥤ (F ⋙ G, G(S))
.
Equations
- category_theory.costructured_arrow.post F G S = {obj := λ (X : category_theory.costructured_arrow F S), {left := X.left, right := {as := punit.star}, hom := G.map X.hom}, map := λ (X Y : category_theory.costructured_arrow F S) (f : X ⟶ Y), {left := f.left, right := id (λ (F : B ⥤ C) (G : C ⥤ D) (S : C) (X Y : category_theory.costructured_arrow F S) (f : X ⟶ Y), {down := id (λ (F : B ⥤ C) (G : C ⥤ D) (S : C) (X Y : category_theory.costructured_arrow F S) (f : X ⟶ Y), category_theory.costructured_arrow.post._proof_1.mpr {down := _}) F G S X Y f}) F G S X Y f, w' := _}, map_id' := _, map_comp' := _}
For a functor F : C ⥤ D
and an object d : D
, we obtain a contravariant functor from the
category of structured arrows d ⟶ F.obj c
to the category of costructured arrows
F.op.obj c ⟶ (op d)
.
Equations
- category_theory.structured_arrow.to_costructured_arrow F d = {obj := λ (X : (category_theory.structured_arrow d F)ᵒᵖ), category_theory.costructured_arrow.mk (opposite.unop X).hom.op, map := λ (X Y : (category_theory.structured_arrow d F)ᵒᵖ) (f : X ⟶ Y), category_theory.costructured_arrow.hom_mk (quiver.hom.op f.unop.right) _, map_id' := _, map_comp' := _}
For a functor F : C ⥤ D
and an object d : D
, we obtain a contravariant functor from the
category of structured arrows op d ⟶ F.op.obj c
to the category of costructured arrows
F.obj c ⟶ d
.
Equations
- category_theory.structured_arrow.to_costructured_arrow' F d = {obj := λ (X : (category_theory.structured_arrow (opposite.op d) F.op)ᵒᵖ), category_theory.costructured_arrow.mk (opposite.unop X).hom.unop, map := λ (X Y : (category_theory.structured_arrow (opposite.op d) F.op)ᵒᵖ) (f : X ⟶ Y), category_theory.costructured_arrow.hom_mk (quiver.hom.unop f.unop.right) _, map_id' := _, map_comp' := _}
For a functor F : C ⥤ D
and an object d : D
, we obtain a contravariant functor from the
category of costructured arrows F.obj c ⟶ d
to the category of structured arrows
op d ⟶ F.op.obj c
.
Equations
- category_theory.costructured_arrow.to_structured_arrow F d = {obj := λ (X : (category_theory.costructured_arrow F d)ᵒᵖ), category_theory.structured_arrow.mk (opposite.unop X).hom.op, map := λ (X Y : (category_theory.costructured_arrow F d)ᵒᵖ) (f : X ⟶ Y), category_theory.structured_arrow.hom_mk (quiver.hom.op f.unop.left) _, map_id' := _, map_comp' := _}
For a functor F : C ⥤ D
and an object d : D
, we obtain a contravariant functor from the
category of costructured arrows F.op.obj c ⟶ op d
to the category of structured arrows
d ⟶ F.obj c
.
Equations
- category_theory.costructured_arrow.to_structured_arrow' F d = {obj := λ (X : (category_theory.costructured_arrow F.op (opposite.op d))ᵒᵖ), category_theory.structured_arrow.mk (opposite.unop X).hom.unop, map := λ (X Y : (category_theory.costructured_arrow F.op (opposite.op d))ᵒᵖ) (f : X ⟶ Y), category_theory.structured_arrow.hom_mk (quiver.hom.unop f.unop.left) _, map_id' := _, map_comp' := _}
For a functor F : C ⥤ D
and an object d : D
, the category of structured arrows d ⟶ F.obj c
is contravariantly equivalent to the category of costructured arrows F.op.obj c ⟶ op d
.
Equations
- category_theory.structured_arrow_op_equivalence F d = category_theory.equivalence.mk (category_theory.structured_arrow.to_costructured_arrow F d) (category_theory.costructured_arrow.to_structured_arrow' F d).right_op (category_theory.nat_iso.of_components (λ (X : (category_theory.structured_arrow d F)ᵒᵖ), (category_theory.structured_arrow.iso_mk (category_theory.iso.refl (category_theory.structured_arrow.mk (opposite.unop X).hom).right) _).op) _) (category_theory.nat_iso.of_components (λ (X : category_theory.costructured_arrow F.op (opposite.op d)), category_theory.costructured_arrow.iso_mk (category_theory.iso.refl (category_theory.costructured_arrow.mk X.hom).left) _) _)
For a functor F : C ⥤ D
and an object d : D
, the category of costructured arrows
F.obj c ⟶ d
is contravariantly equivalent to the category of structured arrows
op d ⟶ F.op.obj c
.
Equations
- category_theory.costructured_arrow_op_equivalence F d = category_theory.equivalence.mk (category_theory.costructured_arrow.to_structured_arrow F d) (category_theory.structured_arrow.to_costructured_arrow' F d).right_op (category_theory.nat_iso.of_components (λ (X : (category_theory.costructured_arrow F d)ᵒᵖ), (category_theory.costructured_arrow.iso_mk (category_theory.iso.refl (category_theory.costructured_arrow.mk (opposite.unop X).hom).left) _).op) _) (category_theory.nat_iso.of_components (λ (X : category_theory.structured_arrow (opposite.op d) F.op), category_theory.structured_arrow.iso_mk (category_theory.iso.refl (category_theory.structured_arrow.mk X.hom).right) _) _)