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

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
Instances for category_theory.structured_arrow.hom_mk
@[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) :

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
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
theorem category_theory.structured_arrow.ext {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 g : A B) :
f.right = g.rightf = g
theorem category_theory.structured_arrow.ext_iff {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 g : A B) :
f = g f.right = g.right

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.

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

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]
@[simp]
theorem category_theory.structured_arrow.pre_map_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {B : Type u₄} [category_theory.category B] (S : D) (F : B C) (G : C D) (X Y : category_theory.comma (category_theory.functor.from_punit S) (F G)) (f : X Y) :
@[simp]
theorem category_theory.structured_arrow.pre_map_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {B : Type u₄} [category_theory.category B] (S : D) (F : B C) (G : C D) (X Y : category_theory.comma (category_theory.functor.from_punit S) (F G)) (f : X Y) :
@[simp]
theorem category_theory.structured_arrow.post_map_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {B : Type u₄} [category_theory.category B] (S : C) (F : B C) (G : C D) (X Y : category_theory.structured_arrow S F) (f : X Y) :
((category_theory.structured_arrow.post S F G).map f).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
@[simp]
theorem category_theory.structured_arrow.post_obj_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {B : Type u₄} [category_theory.category B] (S : C) (F : B C) (G : C D) (X : category_theory.structured_arrow S F) :
@[simp]
theorem category_theory.structured_arrow.post_map_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {B : Type u₄} [category_theory.category B] (S : C) (F : B C) (G : C D) (X Y : category_theory.structured_arrow S F) (f : X Y) :
@[simp]

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

Equations
@[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
Instances for category_theory.costructured_arrow
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
Instances for category_theory.costructured_arrow.hom_mk
@[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
theorem category_theory.costructured_arrow.ext {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 g : A B) (h : f.left = g.left) :
f = g
theorem category_theory.costructured_arrow.ext_iff {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 g : A B) :
f = g f.left = g.left

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.

@[simp]
theorem category_theory.costructured_arrow.eta_hom_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T : D} {S : C D} (f : category_theory.costructured_arrow S T) :
f.eta.hom.right = category_theory.eq_to_hom category_theory.costructured_arrow.iso_mk._proof_1
@[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]
@[simp]
theorem category_theory.costructured_arrow.pre_map_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {B : Type u₄} [category_theory.category B] (F : B C) (G : C D) (S : D) (X Y : category_theory.comma (F G) (category_theory.functor.from_punit S)) (f : X Y) :
@[simp]
@[simp]
theorem category_theory.costructured_arrow.post_map_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {B : Type u₄} [category_theory.category B] (F : B C) (G : C D) (S : C) (X Y : category_theory.costructured_arrow F S) (f : X Y) :
((category_theory.costructured_arrow.post F G S).map f).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

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

Equations
@[simp]
@[simp]
theorem category_theory.costructured_arrow.post_map_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {B : Type u₄} [category_theory.category B] (F : B C) (G : C D) (S : C) (X Y : category_theory.costructured_arrow F S) (f : X Y) :
@[simp]

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

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

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

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