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

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
@[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
@[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) :
@[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
theorem category_theory.structured_arrow.eq_mk {C : Type u₁} {D : Type u₂} {S : D} {T : C D} (f : T) :
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
@[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) :
@[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) :
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} :
@[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
@[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
@[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
@[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) :
@[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'
theorem category_theory.costructured_arrow.eq_mk {C : Type u₁} {D : Type u₂} {T : D} {S : C D}  :
@[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
@[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) :
@[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''}  :
@[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