# mathlibdocumentation

category_theory.structured_arrow

# 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.

@[nolint]
def category_theory.structured_arrow {C : Type u₁} {D : Type u₂} (S : D) (T : C D) :
Type (max u₁ v₂)

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
@[protected, instance]
def category_theory.structured_arrow.category {C : Type u₁} {D : Type u₂} (S : D) (T : C D) :
@[simp]
theorem category_theory.structured_arrow.proj_map {C : Type u₁} {D : Type u₂} (S : D) (T : C D) (_x _x_1 : T) (f : _x _x_1) :
def category_theory.structured_arrow.proj {C : Type u₁} {D : Type u₂} (S : D) (T : C D) :

The obvious projection functor from structured arrows.

Equations
Instances for category_theory.structured_arrow.proj
@[simp]
theorem category_theory.structured_arrow.proj_obj {C : Type u₁} {D : Type u₂} (S : D) (T : C D)  :
def category_theory.structured_arrow.mk {C : Type u₁} {D : Type u₂} {S : D} {Y : C} {T : C D} (f : S T.obj Y) :

Construct a structured arrow from a morphism.

Equations
@[simp]
theorem category_theory.structured_arrow.mk_left {C : Type u₁} {D : Type u₂} {S : D} {Y : C} {T : C D} (f : S T.obj Y) :
= {as := punit.star}
@[simp]
theorem category_theory.structured_arrow.mk_right {C : Type u₁} {D : Type u₂} {S : D} {Y : C} {T : C D} (f : S T.obj Y) :
@[simp]
theorem category_theory.structured_arrow.mk_hom_eq_self {C : Type u₁} {D : Type u₂} {S : D} {Y : C} {T : C D} (f : S T.obj Y) :
@[simp]
theorem category_theory.structured_arrow.w_assoc {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {A B : T} (f : A B) {X' : D} (f' : T.obj B.right X') :
A.hom T.map f.right f' = B.hom f'
@[simp]
theorem category_theory.structured_arrow.w {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {A B : T} (f : A B) :
A.hom T.map f.right = B.hom
def category_theory.structured_arrow.hom_mk {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {f f' : T} (g : f.right f'.right) (w : f.hom T.map g = f'.hom) :
f f'

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
Instances for category_theory.structured_arrow.hom_mk
@[simp]
theorem category_theory.structured_arrow.hom_mk_left {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {f f' : T} (g : f.right f'.right) (w : f.hom T.map g = f'.hom) :
= category_theory.eq_to_hom category_theory.structured_arrow.hom_mk._proof_1
@[simp]
theorem category_theory.structured_arrow.hom_mk_right {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {f f' : T} (g : f.right f'.right) (w : f.hom T.map g = f'.hom) :
def category_theory.structured_arrow.hom_mk' {C : Type u₁} {D : Type u₂} {F : C D} {X : D} {Y : C} (U : F) (f : U.right Y) :
U

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)).

Equations
@[simp]
theorem category_theory.structured_arrow.iso_mk_inv_right {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {f f' : T} (g : f.right f'.right) (w : f.hom T.map g.hom = f'.hom) :
def category_theory.structured_arrow.iso_mk {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {f f' : T} (g : f.right f'.right) (w : f.hom T.map g.hom = f'.hom) :
f f'

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
@[simp]
theorem category_theory.structured_arrow.iso_mk_inv_left {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {f f' : T} (g : f.right f'.right) (w : f.hom T.map g.hom = f'.hom) :
@[simp]
theorem category_theory.structured_arrow.iso_mk_hom_left {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {f f' : T} (g : f.right f'.right) (w : f.hom T.map g.hom = f'.hom) :
= category_theory.eq_to_hom category_theory.structured_arrow.iso_mk._proof_1
@[simp]
theorem category_theory.structured_arrow.iso_mk_hom_right {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {f f' : T} (g : f.right f'.right) (w : f.hom T.map g.hom = f'.hom) :
theorem category_theory.structured_arrow.ext {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {A B : T} (f g : A B) :
f.right = g.rightf = g
theorem category_theory.structured_arrow.ext_iff {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {A B : T} (f g : A B) :
f = g f.right = g.right
@[protected, instance]
def category_theory.structured_arrow.proj_faithful {C : Type u₁} {D : Type u₂} {S : D} {T : C D} :
theorem category_theory.structured_arrow.mono_of_mono_right {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {A B : T} (f : A B) [h : category_theory.mono f.right] :

The converse of this is true with additional assumptions, see mono_iff_mono_right.

theorem category_theory.structured_arrow.epi_of_epi_right {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {A B : T} (f : A B) [h : category_theory.epi f.right] :
@[protected, instance]
def category_theory.structured_arrow.mono_hom_mk {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {A B : T} (f : A.right B.right) (w : A.hom T.map f = B.hom) [h : category_theory.mono f] :
@[protected, instance]
def category_theory.structured_arrow.epi_hom_mk {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {A B : T} (f : A.right B.right) (w : A.hom T.map f = B.hom) [h : category_theory.epi f] :
theorem category_theory.structured_arrow.eq_mk {C : Type u₁} {D : Type u₂} {S : D} {T : C D} (f : T) :

Eta rule for structured arrows. Prefer structured_arrow.eta, since equality of objects tends to cause problems.

@[simp]
theorem category_theory.structured_arrow.eta_inv_right {C : Type u₁} {D : Type u₂} {S : D} {T : C D} (f : T) :
@[simp]
theorem category_theory.structured_arrow.eta_hom_left {C : Type u₁} {D : Type u₂} {S : D} {T : C D} (f : T) :
f.eta.hom.left = category_theory.eq_to_hom category_theory.structured_arrow.iso_mk._proof_1
def category_theory.structured_arrow.eta {C : Type u₁} {D : Type u₂} {S : D} {T : C D} (f : T) :

Eta rule for structured arrows.

Equations
@[simp]
theorem category_theory.structured_arrow.eta_inv_left {C : Type u₁} {D : Type u₂} {S : D} {T : C D} (f : T) :
@[simp]
theorem category_theory.structured_arrow.eta_hom_right {C : Type u₁} {D : Type u₂} {S : D} {T : C D} (f : T) :
def category_theory.structured_arrow.map {C : Type u₁} {D : Type u₂} {S S' : D} {T : C D} (f : S S') :

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.

Equations
@[simp]
theorem category_theory.structured_arrow.map_map_left {C : Type u₁} {D : Type u₂} {S S' : D} {T : C D} (f : S S') (X Y : T) (f_1 : X Y) :
f_1).left = f_1.left
@[simp]
theorem category_theory.structured_arrow.map_obj_right {C : Type u₁} {D : Type u₂} {S S' : D} {T : C D} (f : S S')  :
@[simp]
theorem category_theory.structured_arrow.map_map_right {C : Type u₁} {D : Type u₂} {S S' : D} {T : C D} (f : S S') (X Y : T) (f_1 : X Y) :
f_1).right = f_1.right
@[simp]
theorem category_theory.structured_arrow.map_obj_hom {C : Type u₁} {D : Type u₂} {S S' : D} {T : C D} (f : S S')  :
= f X.hom
@[simp]
theorem category_theory.structured_arrow.map_obj_left {C : Type u₁} {D : Type u₂} {S S' : D} {T : C D} (f : S S')  :
= X.left
@[simp]
theorem category_theory.structured_arrow.map_mk {C : Type u₁} {D : Type u₂} {S S' : D} {Y : C} {T : C D} {f : S' T.obj Y} (g : S S') :
@[simp]
theorem category_theory.structured_arrow.map_id {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {f : T} :
= f
@[simp]
theorem category_theory.structured_arrow.map_comp {C : Type u₁} {D : Type u₂} {S S' S'' : D} {T : C D} {f : S S'} {f' : S' S''} {h : T} :
@[protected, instance]
def category_theory.structured_arrow.proj_reflects_iso {C : Type u₁} {D : Type u₂} {S : D} {T : C D} :
def category_theory.structured_arrow.mk_id_initial {C : Type u₁} {D : Type u₂} {Y : C} {T : C D}  :

The identity structured arrow is initial.

Equations
@[simp]
theorem category_theory.structured_arrow.pre_obj_hom {C : Type u₁} {D : Type u₂} {B : Type u₄} (S : D) (F : B C) (G : C D) (X : (F G)) :
.obj X).hom = X.hom
@[simp]
theorem category_theory.structured_arrow.pre_obj_left {C : Type u₁} {D : Type u₂} {B : Type u₄} (S : D) (F : B C) (G : C D) (X : (F G)) :
.obj X).left = X.left
@[simp]
theorem category_theory.structured_arrow.pre_obj_right {C : Type u₁} {D : Type u₂} {B : Type u₄} (S : D) (F : B C) (G : C D) (X : (F G)) :
.obj X).right = F.obj X.right
@[simp]
theorem category_theory.structured_arrow.pre_map_left {C : Type u₁} {D : Type u₂} {B : Type u₄} (S : D) (F : B C) (G : C D) (X Y : (F G)) (f : X Y) :
.map f).left = f.left
def category_theory.structured_arrow.pre {C : Type u₁} {D : Type u₂} {B : Type u₄} (S : D) (F : B C) (G : C D) :

The functor (S, F ⋙ G) ⥤ (S, G).

Equations
@[simp]
theorem category_theory.structured_arrow.pre_map_right {C : Type u₁} {D : Type u₂} {B : Type u₄} (S : D) (F : B C) (G : C D) (X Y : (F G)) (f : X Y) :
.map f).right = F.map f.right
@[simp]
theorem category_theory.structured_arrow.post_map_left {C : Type u₁} {D : Type u₂} {B : Type u₄} (S : C) (F : B C) (G : C D) (X Y : F) (f : X Y) :
.map f).left = id (λ (S : C) (F : B C) (G : C D) (X Y : (f : X Y), {down := id (λ (S : C) (F : B C) (G : C D) (X Y : (f : X Y), category_theory.structured_arrow.post._proof_1.mpr {down := _}) S F G X Y f}) S F G X Y f
@[simp]
theorem category_theory.structured_arrow.post_obj_hom {C : Type u₁} {D : Type u₂} {B : Type u₄} (S : C) (F : B C) (G : C D) (X : F) :
.obj X).hom = G.map X.hom
@[simp]
theorem category_theory.structured_arrow.post_map_right {C : Type u₁} {D : Type u₂} {B : Type u₄} (S : C) (F : B C) (G : C D) (X Y : F) (f : X Y) :
@[simp]
theorem category_theory.structured_arrow.post_obj_right {C : Type u₁} {D : Type u₂} {B : Type u₄} (S : C) (F : B C) (G : C D) (X : F) :
def category_theory.structured_arrow.post {C : Type u₁} {D : Type u₂} {B : Type u₄} (S : C) (F : B C) (G : C D) :
(F G)

The functor (S, F) ⥤ (G(S), F ⋙ G).

Equations
@[protected, instance]
def category_theory.structured_arrow.small_proj_preimage_of_locally_small {C : Type u₁} {D : Type u₂} {S : D} {T : C D} {𝒢 : set C} [small 𝒢]  :
@[nolint]
def category_theory.costructured_arrow {C : Type u₁} {D : Type u₂} (S : C D) (T : D) :
Type (max u₁ v₂)

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
@[protected, instance]
def category_theory.costructured_arrow.category {C : Type u₁} {D : Type u₂} (S : C D) (T : D) :
@[simp]
theorem category_theory.costructured_arrow.proj_obj {C : Type u₁} {D : Type u₂} (S : C D) (T : D)  :
def category_theory.costructured_arrow.proj {C : Type u₁} {D : Type u₂} (S : C D) (T : D) :

The obvious projection functor from costructured arrows.

Equations
Instances for category_theory.costructured_arrow.proj
@[simp]
theorem category_theory.costructured_arrow.proj_map {C : Type u₁} {D : Type u₂} (S : C D) (T : D) (_x _x_1 : ) (f : _x _x_1) :
def category_theory.costructured_arrow.mk {C : Type u₁} {D : Type u₂} {T : D} {Y : C} {S : C D} (f : S.obj Y T) :

Construct a costructured arrow from a morphism.

Equations
@[simp]
theorem category_theory.costructured_arrow.mk_left {C : Type u₁} {D : Type u₂} {T : D} {Y : C} {S : C D} (f : S.obj Y T) :
@[simp]
theorem category_theory.costructured_arrow.mk_right {C : Type u₁} {D : Type u₂} {T : D} {Y : C} {S : C D} (f : S.obj Y T) :
= {as := punit.star}
@[simp]
theorem category_theory.costructured_arrow.mk_hom_eq_self {C : Type u₁} {D : Type u₂} {T : D} {Y : C} {S : C D} (f : S.obj Y T) :
@[simp]
theorem category_theory.costructured_arrow.w {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {A B : T} (f : A B) :
S.map f.left B.hom = A.hom
@[simp]
theorem category_theory.costructured_arrow.w_assoc {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {A B : T} (f : A B) {X' : D} (f' : X') :
S.map f.left B.hom f' = A.hom f'
@[simp]
theorem category_theory.costructured_arrow.hom_mk_right {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {f f' : T} (g : f.left f'.left) (w : S.map g f'.hom = f.hom) :
= category_theory.eq_to_hom category_theory.costructured_arrow.hom_mk._proof_1
def category_theory.costructured_arrow.hom_mk {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {f f' : T} (g : f.left f'.left) (w : S.map g f'.hom = f.hom) :
f f'

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
Instances for category_theory.costructured_arrow.hom_mk
@[simp]
theorem category_theory.costructured_arrow.hom_mk_left {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {f f' : T} (g : f.left f'.left) (w : S.map g f'.hom = f.hom) :
@[simp]
theorem category_theory.costructured_arrow.iso_mk_inv_right {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {f f' : T} (g : f.left f'.left) (w : S.map g.hom f'.hom = f.hom) :
@[simp]
theorem category_theory.costructured_arrow.iso_mk_hom_right {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {f f' : T} (g : f.left f'.left) (w : S.map g.hom f'.hom = f.hom) :
= category_theory.eq_to_hom category_theory.costructured_arrow.iso_mk._proof_1
@[simp]
theorem category_theory.costructured_arrow.iso_mk_inv_left {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {f f' : T} (g : f.left f'.left) (w : S.map g.hom f'.hom = f.hom) :
def category_theory.costructured_arrow.iso_mk {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {f f' : T} (g : f.left f'.left) (w : S.map g.hom f'.hom = f.hom) :
f f'

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
@[simp]
theorem category_theory.costructured_arrow.iso_mk_hom_left {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {f f' : T} (g : f.left f'.left) (w : S.map g.hom f'.hom = f.hom) :
theorem category_theory.costructured_arrow.ext {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {A B : T} (f g : A B) (h : f.left = g.left) :
f = g
theorem category_theory.costructured_arrow.ext_iff {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {A B : T} (f g : A B) :
f = g f.left = g.left
@[protected, instance]
def category_theory.costructured_arrow.proj_faithful {C : Type u₁} {D : Type u₂} {T : D} {S : C D} :
theorem category_theory.costructured_arrow.mono_of_mono_left {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {A B : T} (f : A B) [h : category_theory.mono f.left] :
theorem category_theory.costructured_arrow.epi_of_epi_left {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {A B : T} (f : A B) [h : category_theory.epi f.left] :

The converse of this is true with additional assumptions, see epi_iff_epi_left.

@[protected, instance]
def category_theory.costructured_arrow.mono_hom_mk {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {A B : T} (f : A.left B.left) (w : S.map f B.hom = A.hom) [h : category_theory.mono f] :
@[protected, instance]
def category_theory.costructured_arrow.epi_hom_mk {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {A B : T} (f : A.left B.left) (w : S.map f B.hom = A.hom) [h : category_theory.epi f] :
theorem category_theory.costructured_arrow.eq_mk {C : Type u₁} {D : Type u₂} {T : D} {S : C D}  :

Eta rule for costructured arrows. Prefer costructured_arrow.eta, as equality of objects tends to cause problems.

@[simp]
theorem category_theory.costructured_arrow.eta_hom_right {C : Type u₁} {D : Type u₂} {T : D} {S : C D}  :
f.eta.hom.right = category_theory.eq_to_hom category_theory.costructured_arrow.iso_mk._proof_1
@[simp]
theorem category_theory.costructured_arrow.eta_inv_left {C : Type u₁} {D : Type u₂} {T : D} {S : C D}  :
@[simp]
theorem category_theory.costructured_arrow.eta_hom_left {C : Type u₁} {D : Type u₂} {T : D} {S : C D}  :
@[simp]
theorem category_theory.costructured_arrow.eta_inv_right {C : Type u₁} {D : Type u₂} {T : D} {S : C D}  :
def category_theory.costructured_arrow.eta {C : Type u₁} {D : Type u₂} {T : D} {S : C D}  :

Eta rule for costructured arrows.

Equations
@[simp]
theorem category_theory.costructured_arrow.map_map_right {C : Type u₁} {D : Type u₂} {T T' : D} {S : C D} (f : T T') (f_1 : X Y) :
@[simp]
theorem category_theory.costructured_arrow.map_obj_hom {C : Type u₁} {D : Type u₂} {T T' : D} {S : C D} (f : T T')  :
= X.hom f
def category_theory.costructured_arrow.map {C : Type u₁} {D : Type u₂} {T T' : D} {S : C D} (f : T T') :

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.

Equations
@[simp]
theorem category_theory.costructured_arrow.map_obj_right {C : Type u₁} {D : Type u₂} {T T' : D} {S : C D} (f : T T')  :
@[simp]
theorem category_theory.costructured_arrow.map_map_left {C : Type u₁} {D : Type u₂} {T T' : D} {S : C D} (f : T T') (f_1 : X Y) :
.left = f_1.left
@[simp]
theorem category_theory.costructured_arrow.map_obj_left {C : Type u₁} {D : Type u₂} {T T' : D} {S : C D} (f : T T')  :
@[simp]
theorem category_theory.costructured_arrow.map_mk {C : Type u₁} {D : Type u₂} {T T' : D} {Y : C} {S : C D} {f : S.obj Y T} (g : T T') :
@[simp]
theorem category_theory.costructured_arrow.map_id {C : Type u₁} {D : Type u₂} {T : D} {S : C D}  :
= f
@[simp]
theorem category_theory.costructured_arrow.map_comp {C : Type u₁} {D : Type u₂} {T T' T'' : D} {S : C D} {f : T T'} {f' : T' T''}  :
@[protected, instance]
def category_theory.costructured_arrow.proj_reflects_iso {C : Type u₁} {D : Type u₂} {T : D} {S : C D} :
def category_theory.costructured_arrow.mk_id_terminal {C : Type u₁} {D : Type u₂} {Y : C} {S : C D}  :

The identity costructured arrow is terminal.

Equations
@[simp]
theorem category_theory.costructured_arrow.pre_obj_hom {C : Type u₁} {D : Type u₂} {B : Type u₄} (F : B C) (G : C D) (S : D) (X : category_theory.comma (F G) ) :
X).hom = X.hom
@[simp]
theorem category_theory.costructured_arrow.pre_obj_right {C : Type u₁} {D : Type u₂} {B : Type u₄} (F : B C) (G : C D) (S : D) (X : category_theory.comma (F G) ) :
X).right = X.right
def category_theory.costructured_arrow.pre {C : Type u₁} {D : Type u₂} {B : Type u₄} (F : B C) (G : C D) (S : D) :

The functor (F ⋙ G, S) ⥤ (G, S).

Equations
@[simp]
theorem category_theory.costructured_arrow.pre_map_left {C : Type u₁} {D : Type u₂} {B : Type u₄} (F : B C) (G : C D) (S : D) (X Y : category_theory.comma (F G) ) (f : X Y) :
f).left = F.map f.left
@[simp]
theorem category_theory.costructured_arrow.pre_map_right {C : Type u₁} {D : Type u₂} {B : Type u₄} (F : B C) (G : C D) (S : D) (X Y : category_theory.comma (F G) ) (f : X Y) :
f).right = f.right
@[simp]
theorem category_theory.costructured_arrow.pre_obj_left {C : Type u₁} {D : Type u₂} {B : Type u₄} (F : B C) (G : C D) (S : D) (X : category_theory.comma (F G) ) :
X).left = F.obj X.left
@[simp]
theorem category_theory.costructured_arrow.post_map_right {C : Type u₁} {D : Type u₂} {B : Type u₄} (F : B C) (G : C D) (S : C) (X Y : S) (f : X Y) :
f).right = id (λ (F : B C) (G : C D) (S : C) (X Y : (f : X Y), {down := id (λ (F : B C) (G : C D) (S : C) (X Y : (f : X Y), category_theory.costructured_arrow.post._proof_1.mpr {down := _}) F G S X Y f}) F G S X Y f
def category_theory.costructured_arrow.post {C : Type u₁} {D : Type u₂} {B : Type u₄} (F : B C) (G : C D) (S : C) :

The functor (F, S) ⥤ (F ⋙ G, G(S)).

Equations
@[simp]
theorem category_theory.costructured_arrow.post_obj_hom {C : Type u₁} {D : Type u₂} {B : Type u₄} (F : B C) (G : C D) (S : C)  :
X).hom = G.map X.hom
@[simp]
theorem category_theory.costructured_arrow.post_map_left {C : Type u₁} {D : Type u₂} {B : Type u₄} (F : B C) (G : C D) (S : C) (X Y : S) (f : X Y) :
f).left = f.left
@[simp]
theorem category_theory.costructured_arrow.post_obj_left {C : Type u₁} {D : Type u₂} {B : Type u₄} (F : B C) (G : C D) (S : C)  :
X).left = X.left
@[protected, instance]
def category_theory.costructured_arrow.small_proj_preimage_of_locally_small {C : Type u₁} {D : Type u₂} {T : D} {S : C D} {𝒢 : set C} [small 𝒢]  :
@[simp]
theorem category_theory.structured_arrow.to_costructured_arrow_obj {C : Type u₁} {D : Type u₂} (F : C D) (d : D) (X : ᵒᵖ) :
@[simp]
theorem category_theory.structured_arrow.to_costructured_arrow_map {C : Type u₁} {D : Type u₂} (F : C D) (d : D) (X Y : ᵒᵖ) (f : X Y) :
def category_theory.structured_arrow.to_costructured_arrow {C : Type u₁} {D : Type u₂} (F : C D) (d : D) :

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
@[simp]
theorem category_theory.structured_arrow.to_costructured_arrow'_map {C : Type u₁} {D : Type u₂} (F : C D) (d : D) (X Y : ᵒᵖ) (f : X Y) :
@[simp]
theorem category_theory.structured_arrow.to_costructured_arrow'_obj {C : Type u₁} {D : Type u₂} (F : C D) (d : D) (X : ᵒᵖ) :
def category_theory.structured_arrow.to_costructured_arrow' {C : Type u₁} {D : Type u₂} (F : C D) (d : D) :

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
@[simp]
theorem category_theory.costructured_arrow.to_structured_arrow_map {C : Type u₁} {D : Type u₂} (F : C D) (d : D) (X Y : ᵒᵖ) (f : X Y) :
def category_theory.costructured_arrow.to_structured_arrow {C : Type u₁} {D : Type u₂} (F : C D) (d : D) :

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
@[simp]
theorem category_theory.costructured_arrow.to_structured_arrow_obj {C : Type u₁} {D : Type u₂} (F : C D) (d : D) (X : ᵒᵖ) :
def category_theory.costructured_arrow.to_structured_arrow' {C : Type u₁} {D : Type u₂} (F : C D) (d : D) :

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
@[simp]
theorem category_theory.costructured_arrow.to_structured_arrow'_obj {C : Type u₁} {D : Type u₂} (F : C D) (d : D) (X : ᵒᵖ) :
@[simp]
theorem category_theory.costructured_arrow.to_structured_arrow'_map {C : Type u₁} {D : Type u₂} (F : C D) (d : D) (X Y : ᵒᵖ) (f : X Y) :
def category_theory.structured_arrow_op_equivalence {C : Type u₁} {D : Type u₂} (F : C D) (d : D) :

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
def category_theory.costructured_arrow_op_equivalence {C : Type u₁} {D : Type u₂} (F : C D) (d : D) :

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