mathlib documentation

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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

The obvious projection functor from structured arrows.

Equations
def category_theory.structured_arrow.mk {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {Y : C} {T : C D} (f : S T.obj Y) :
@[simp]
theorem category_theory.structured_arrow.mk_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {Y : C} {T : C D} (f : S T.obj Y) :
@[simp]
theorem category_theory.structured_arrow.w_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C D} {A B : category_theory.structured_arrow S 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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C D} {A B : category_theory.structured_arrow S T} (f : A B) :
A.hom T.map f.right = B.hom
def category_theory.structured_arrow.hom_mk {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C D} {f f' : category_theory.structured_arrow S 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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C D} {f f' : category_theory.structured_arrow S T} (g : f.right f'.right) (w : f.hom T.map g = f'.hom) :
(category_theory.structured_arrow.hom_mk g w).left = 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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C D} {f f' : category_theory.structured_arrow S T} (g : f.right f'.right) (w : f.hom T.map g = f'.hom) :
def category_theory.structured_arrow.iso_mk {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C D} {f f' : category_theory.structured_arrow S 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_hom_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C D} {f f' : category_theory.structured_arrow S T} (g : f.right f'.right) (w : f.hom T.map g.hom = f'.hom) :
(category_theory.structured_arrow.iso_mk g w).hom.left = category_theory.eq_to_hom category_theory.structured_arrow.iso_mk._proof_1

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S S' : D} {T : C D} (f : S S') (X Y : category_theory.comma (category_theory.functor.from_punit S') T) (f_1 : X Y) :
@[simp]
@[nolint]
def category_theory.costructured_arrow {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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

The obvious projection functor from costructured arrows.

Equations
def category_theory.costructured_arrow.mk {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T : D} {Y : C} {S : C D} (f : S.obj Y T) :
@[simp]
theorem category_theory.costructured_arrow.mk_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T : D} {Y : C} {S : C D} (f : S.obj Y T) :
@[simp]
theorem category_theory.costructured_arrow.w {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T : D} {S : C D} {A B : category_theory.costructured_arrow S T} (f : A B) :
S.map f.left B.hom = A.hom
@[simp]
theorem category_theory.costructured_arrow.w_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T : D} {S : C D} {A B : category_theory.costructured_arrow S T} (f : A B) {X' : D} (f' : (category_theory.functor.from_punit T).obj B.right X') :
S.map f.left B.hom f' = A.hom f'
@[simp]
theorem category_theory.costructured_arrow.hom_mk_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T : D} {S : C D} {f f' : category_theory.costructured_arrow S T} (g : f.left f'.left) (w : S.map g f'.hom = f.hom) :
(category_theory.costructured_arrow.hom_mk g w).right = category_theory.eq_to_hom category_theory.costructured_arrow.hom_mk._proof_1
def category_theory.costructured_arrow.hom_mk {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T : D} {S : C D} {f f' : category_theory.costructured_arrow S 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]
@[simp]
theorem category_theory.costructured_arrow.iso_mk_hom_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T : D} {S : C D} {f f' : category_theory.costructured_arrow S T} (g : f.left f'.left) (w : S.map g.hom f'.hom = f.hom) :
(category_theory.costructured_arrow.iso_mk g w).hom.right = category_theory.eq_to_hom category_theory.costructured_arrow.iso_mk._proof_1
def category_theory.costructured_arrow.iso_mk {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T : D} {S : C D} {f f' : category_theory.costructured_arrow S 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]

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]