mathlib3 documentation

category_theory.structured_arrow

The category of "structured arrows" #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
@[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
Instances for category_theory.structured_arrow
source
@[protected, instance]
def category_theory.structured_arrow.category {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (S : D) (T : C ⥤ D) :
category_theory.category (category_theory.structured_arrow S T)
source
@[simp]
theorem category_theory.structured_arrow.proj_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (S : D) (T : C ⥤ D) (_x _x_1 : category_theory.comma (category_theory.functor.from_punit S) T) (f : _x ⟶ _x_1) :
(category_theory.structured_arrow.proj S T).map f = f.right
source
def category_theory.structured_arrow.proj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (S : D) (T : C ⥤ D) :
category_theory.structured_arrow S T ⥤ C

The obvious projection functor from structured arrows.

Equations
Instances for category_theory.structured_arrow.proj
source
@[simp]
theorem category_theory.structured_arrow.proj_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (S : D) (T : C ⥤ D) (X : category_theory.comma (category_theory.functor.from_punit S) T) :
(category_theory.structured_arrow.proj S T).obj X = X.right
source
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) :
category_theory.structured_arrow S T

Construct a structured arrow from a morphism.

Equations
source
@[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) :
(category_theory.structured_arrow.mk f).left = {as := punit.star}
source
@[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) :
(category_theory.structured_arrow.mk f).right = Y
source
@[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) :
(category_theory.structured_arrow.mk f).hom = f
source
@[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'
source
@[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
source
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
source
@[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
source
@[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) :
(category_theory.structured_arrow.hom_mk g w).right = g
source
def category_theory.structured_arrow.hom_mk' {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} {X : D} {Y : C} (U : category_theory.structured_arrow X F) (f : U.right ⟶ Y) :
U ⟶ category_theory.structured_arrow.mk (U.hom ≫ F.map f)

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
source
@[simp]
theorem category_theory.structured_arrow.iso_mk_inv_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.hom = f'.hom) :
(category_theory.structured_arrow.iso_mk g w).inv.right = g.inv
source
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
source
@[simp]
theorem category_theory.structured_arrow.iso_mk_inv_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).inv.left = category_theory.eq_to_hom _
source
@[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
source
@[simp]
theorem category_theory.structured_arrow.iso_mk_hom_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.hom = f'.hom) :
(category_theory.structured_arrow.iso_mk g w).hom.right = g.hom
source
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.right → f = g
source
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
source
@[protected, instance]
def category_theory.structured_arrow.proj_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C ⥤ D} :
category_theory.faithful (category_theory.structured_arrow.proj S T)
source
theorem category_theory.structured_arrow.mono_of_mono_right {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) [h : category_theory.mono f.right] :
category_theory.mono f

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

source
theorem category_theory.structured_arrow.epi_of_epi_right {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) [h : category_theory.epi f.right] :
category_theory.epi f
source
@[protected, instance]
def category_theory.structured_arrow.mono_hom_mk {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.right ⟶ B.right) (w : A.hom ≫ T.map f = B.hom) [h : category_theory.mono f] :
category_theory.mono (category_theory.structured_arrow.hom_mk f w)
source
@[protected, instance]
def category_theory.structured_arrow.epi_hom_mk {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.right ⟶ B.right) (w : A.hom ≫ T.map f = B.hom) [h : category_theory.epi f] :
category_theory.epi (category_theory.structured_arrow.hom_mk f w)
source
theorem category_theory.structured_arrow.eq_mk {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 = category_theory.structured_arrow.mk f.hom

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

source
@[simp]
theorem category_theory.structured_arrow.eta_inv_right {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.inv.right = 𝟙 f.right
source
@[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
source
def category_theory.structured_arrow.eta {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 ≅ category_theory.structured_arrow.mk f.hom

Eta rule for structured arrows.

Equations
source
@[simp]
theorem category_theory.structured_arrow.eta_inv_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.inv.left = category_theory.eq_to_hom _
source
@[simp]
theorem category_theory.structured_arrow.eta_hom_right {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.right = 𝟙 f.right
source
def category_theory.structured_arrow.map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S S' : D} {T : C ⥤ D} (f : S ⟶ S') :
category_theory.structured_arrow S' T ⥤ category_theory.structured_arrow S T

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
source
@[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) :
((category_theory.structured_arrow.map f).map f_1).left = f_1.left
source
@[simp]
theorem category_theory.structured_arrow.map_obj_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S S' : D} {T : C ⥤ D} (f : S ⟶ S') (X : category_theory.comma (category_theory.functor.from_punit S') T) :
((category_theory.structured_arrow.map f).obj X).right = X.right
source
@[simp]
theorem category_theory.structured_arrow.map_map_right {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) :
((category_theory.structured_arrow.map f).map f_1).right = f_1.right
source
@[simp]
theorem category_theory.structured_arrow.map_obj_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S S' : D} {T : C ⥤ D} (f : S ⟶ S') (X : category_theory.comma (category_theory.functor.from_punit S') T) :
((category_theory.structured_arrow.map f).obj X).hom = f ≫ X.hom
source
@[simp]
theorem category_theory.structured_arrow.map_obj_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 : category_theory.comma (category_theory.functor.from_punit S') T) :
((category_theory.structured_arrow.map f).obj X).left = X.left
source
@[simp]
theorem category_theory.structured_arrow.map_mk {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S S' : D} {Y : C} {T : C ⥤ D} {f : S' ⟶ T.obj Y} (g : S ⟶ S') :
(category_theory.structured_arrow.map g).obj (category_theory.structured_arrow.mk f) = category_theory.structured_arrow.mk (g ≫ f)
source
@[simp]
theorem category_theory.structured_arrow.map_id {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} :
(category_theory.structured_arrow.map (𝟙 S)).obj f = f
source
@[simp]
theorem category_theory.structured_arrow.map_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S S' S'' : D} {T : C ⥤ D} {f : S ⟶ S'} {f' : S' ⟶ S''} {h : category_theory.structured_arrow S'' T} :
(category_theory.structured_arrow.map (f ≫ f')).obj h = (category_theory.structured_arrow.map f).obj ((category_theory.structured_arrow.map f').obj h)
source
@[protected, instance]
def category_theory.structured_arrow.proj_reflects_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C ⥤ D} :
category_theory.reflects_isomorphisms (category_theory.structured_arrow.proj S T)
source
def category_theory.structured_arrow.mk_id_initial {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {Y : C} {T : C ⥤ D} [category_theory.full T] [category_theory.faithful T] :
category_theory.limits.is_initial (category_theory.structured_arrow.mk (𝟙 (T.obj Y)))

The identity structured arrow is initial.

Equations
source
@[simp]
theorem category_theory.structured_arrow.pre_obj_hom {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 : category_theory.comma (category_theory.functor.from_punit S) (F ⋙ G)) :
((category_theory.structured_arrow.pre S F G).obj X).hom = X.hom
source
@[simp]
theorem category_theory.structured_arrow.pre_obj_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 : category_theory.comma (category_theory.functor.from_punit S) (F ⋙ G)) :
((category_theory.structured_arrow.pre S F G).obj X).left = X.left
source
@[simp]
theorem category_theory.structured_arrow.pre_obj_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 : category_theory.comma (category_theory.functor.from_punit S) (F ⋙ G)) :
((category_theory.structured_arrow.pre S F G).obj X).right = F.obj X.right
source
@[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) :
((category_theory.structured_arrow.pre S F G).map f).left = f.left
source
def category_theory.structured_arrow.pre {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) :
category_theory.structured_arrow S (F ⋙ G) ⥤ category_theory.structured_arrow S G

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

Equations
source
@[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) :
((category_theory.structured_arrow.pre S F G).map f).right = F.map f.right
source
@[simp]
theorem category_theory.structured_arrow.post_obj {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) :
(category_theory.structured_arrow.post S F G).obj X = category_theory.structured_arrow.mk (G.map X.hom)
source
@[simp]
theorem category_theory.structured_arrow.post_map {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 = category_theory.structured_arrow.hom_mk f.right _
source
def category_theory.structured_arrow.post {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) :
category_theory.structured_arrow S F ⥤ category_theory.structured_arrow (G.obj S) (F ⋙ G)

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

Equations
source
@[protected, instance]
def category_theory.structured_arrow.small_proj_preimage_of_locally_small {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C ⥤ D} {𝒢 : set C} [small ↥𝒢] [category_theory.locally_small D] :
small ↥((category_theory.structured_arrow.proj S T).obj ⁻¹' 𝒢)
source
@[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
source
@[protected, instance]
def category_theory.costructured_arrow.category {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (S : C ⥤ D) (T : D) :
category_theory.category (category_theory.costructured_arrow S T)
source
@[simp]
theorem category_theory.costructured_arrow.proj_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (S : C ⥤ D) (T : D) (X : category_theory.comma S (category_theory.functor.from_punit T)) :
(category_theory.costructured_arrow.proj S T).obj X = X.left
source
def category_theory.costructured_arrow.proj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (S : C ⥤ D) (T : D) :
category_theory.costructured_arrow S T ⥤ C

The obvious projection functor from costructured arrows.

Equations
Instances for category_theory.costructured_arrow.proj
source
@[simp]
theorem category_theory.costructured_arrow.proj_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (S : C ⥤ D) (T : D) (_x _x_1 : category_theory.comma S (category_theory.functor.from_punit T)) (f : _x ⟶ _x_1) :
(category_theory.costructured_arrow.proj S T).map f = f.left
source
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) :
category_theory.costructured_arrow S T

Construct a costructured arrow from a morphism.

Equations
source
@[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) :
(category_theory.costructured_arrow.mk f).left = Y
source
@[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) :
(category_theory.costructured_arrow.mk f).right = {as := punit.star}
source
@[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) :
(category_theory.costructured_arrow.mk f).hom = f
source
@[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
source
@[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'
source
@[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
source
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
source
@[simp]
theorem category_theory.costructured_arrow.hom_mk_left {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).left = g
source
@[simp]
theorem category_theory.costructured_arrow.iso_mk_inv_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).inv.right = category_theory.eq_to_hom _
source
@[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
source
@[simp]
theorem category_theory.costructured_arrow.iso_mk_inv_left {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).inv.left = g.inv
source
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
source
@[simp]
theorem category_theory.costructured_arrow.iso_mk_hom_left {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.left = g.hom
source
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
source
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
source
@[protected, instance]
def category_theory.costructured_arrow.proj_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T : D} {S : C ⥤ D} :
category_theory.faithful (category_theory.costructured_arrow.proj S T)
source
theorem category_theory.costructured_arrow.mono_of_mono_left {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) [h : category_theory.mono f.left] :
category_theory.mono f
source
theorem category_theory.costructured_arrow.epi_of_epi_left {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) [h : category_theory.epi f.left] :
category_theory.epi f

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

source
@[protected, instance]
def category_theory.costructured_arrow.mono_hom_mk {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.left ⟶ B.left) (w : S.map f ≫ B.hom = A.hom) [h : category_theory.mono f] :
category_theory.mono (category_theory.costructured_arrow.hom_mk f w)
source
@[protected, instance]
def category_theory.costructured_arrow.epi_hom_mk {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.left ⟶ B.left) (w : S.map f ≫ B.hom = A.hom) [h : category_theory.epi f] :
category_theory.epi (category_theory.costructured_arrow.hom_mk f w)
source
theorem category_theory.costructured_arrow.eq_mk {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 = category_theory.costructured_arrow.mk f.hom

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

source
@[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
source
@[simp]
theorem category_theory.costructured_arrow.eta_inv_left {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.inv.left = 𝟙 f.left
source
@[simp]
theorem category_theory.costructured_arrow.eta_hom_left {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.left = 𝟙 f.left
source
@[simp]
theorem category_theory.costructured_arrow.eta_inv_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.inv.right = category_theory.eq_to_hom _
source
def category_theory.costructured_arrow.eta {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 ≅ category_theory.costructured_arrow.mk f.hom

Eta rule for costructured arrows.

Equations
source
@[simp]
theorem category_theory.costructured_arrow.map_map_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T T' : D} {S : C ⥤ D} (f : T ⟶ T') (X Y : category_theory.comma S (category_theory.functor.from_punit T)) (f_1 : X ⟶ Y) :
((category_theory.costructured_arrow.map f).map f_1).right = f_1.right
source
@[simp]
theorem category_theory.costructured_arrow.map_obj_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T T' : D} {S : C ⥤ D} (f : T ⟶ T') (X : category_theory.comma S (category_theory.functor.from_punit T)) :
((category_theory.costructured_arrow.map f).obj X).hom = X.hom ≫ f
source
def category_theory.costructured_arrow.map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T T' : D} {S : C ⥤ D} (f : T ⟶ T') :
category_theory.costructured_arrow S T ⥤ category_theory.costructured_arrow S 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
source
@[simp]
theorem category_theory.costructured_arrow.map_obj_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T T' : D} {S : C ⥤ D} (f : T ⟶ T') (X : category_theory.comma S (category_theory.functor.from_punit T)) :
((category_theory.costructured_arrow.map f).obj X).right = X.right
source
@[simp]
theorem category_theory.costructured_arrow.map_map_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T T' : D} {S : C ⥤ D} (f : T ⟶ T') (X Y : category_theory.comma S (category_theory.functor.from_punit T)) (f_1 : X ⟶ Y) :
((category_theory.costructured_arrow.map f).map f_1).left = f_1.left
source
@[simp]
theorem category_theory.costructured_arrow.map_obj_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T T' : D} {S : C ⥤ D} (f : T ⟶ T') (X : category_theory.comma S (category_theory.functor.from_punit T)) :
((category_theory.costructured_arrow.map f).obj X).left = X.left
source
@[simp]
theorem category_theory.costructured_arrow.map_mk {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T T' : D} {Y : C} {S : C ⥤ D} {f : S.obj Y ⟶ T} (g : T ⟶ T') :
(category_theory.costructured_arrow.map g).obj (category_theory.costructured_arrow.mk f) = category_theory.costructured_arrow.mk (f ≫ g)
source
@[simp]
theorem category_theory.costructured_arrow.map_id {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} :
(category_theory.costructured_arrow.map (𝟙 T)).obj f = f
source
@[simp]
theorem category_theory.costructured_arrow.map_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T T' T'' : D} {S : C ⥤ D} {f : T ⟶ T'} {f' : T' ⟶ T''} {h : category_theory.costructured_arrow S T} :
(category_theory.costructured_arrow.map (f ≫ f')).obj h = (category_theory.costructured_arrow.map f').obj ((category_theory.costructured_arrow.map f).obj h)
source
@[protected, instance]
def category_theory.costructured_arrow.proj_reflects_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T : D} {S : C ⥤ D} :
category_theory.reflects_isomorphisms (category_theory.costructured_arrow.proj S T)
source
def category_theory.costructured_arrow.mk_id_terminal {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {Y : C} {S : C ⥤ D} [category_theory.full S] [category_theory.faithful S] :
category_theory.limits.is_terminal (category_theory.costructured_arrow.mk (𝟙 (S.obj Y)))

The identity costructured arrow is terminal.

Equations
source
@[simp]
theorem category_theory.costructured_arrow.pre_obj_hom {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 : category_theory.comma (F ⋙ G) (category_theory.functor.from_punit S)) :
((category_theory.costructured_arrow.pre F G S).obj X).hom = X.hom
source
@[simp]
theorem category_theory.costructured_arrow.pre_obj_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 : D) (X : category_theory.comma (F ⋙ G) (category_theory.functor.from_punit S)) :
((category_theory.costructured_arrow.pre F G S).obj X).right = X.right
source
def category_theory.costructured_arrow.pre {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) :
category_theory.costructured_arrow (F ⋙ G) S ⥤ category_theory.costructured_arrow G S

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

Equations
source
@[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) :
((category_theory.costructured_arrow.pre F G S).map f).left = F.map f.left
source
@[simp]
theorem category_theory.costructured_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] (F : B ⥤ C) (G : C ⥤ D) (S : D) (X Y : category_theory.comma (F ⋙ G) (category_theory.functor.from_punit S)) (f : X ⟶ Y) :
((category_theory.costructured_arrow.pre F G S).map f).right = f.right
source
@[simp]
theorem category_theory.costructured_arrow.pre_obj_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 : category_theory.comma (F ⋙ G) (category_theory.functor.from_punit S)) :
((category_theory.costructured_arrow.pre F G S).obj X).left = F.obj X.left
source
@[simp]
theorem category_theory.costructured_arrow.post_map {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 = category_theory.costructured_arrow.hom_mk f.left _
source
def category_theory.costructured_arrow.post {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) :
category_theory.costructured_arrow F S ⥤ category_theory.costructured_arrow (F ⋙ G) (G.obj S)

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

Equations
source
@[simp]
theorem category_theory.costructured_arrow.post_obj {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 : category_theory.costructured_arrow F S) :
(category_theory.costructured_arrow.post F G S).obj X = category_theory.costructured_arrow.mk (G.map X.hom)
source
@[protected, instance]
def category_theory.costructured_arrow.small_proj_preimage_of_locally_small {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {T : D} {S : C ⥤ D} {𝒢 : set C} [small ↥𝒢] [category_theory.locally_small D] :
small ↥((category_theory.costructured_arrow.proj S T).obj ⁻¹' 𝒢)
source
@[simp]
theorem category_theory.structured_arrow.to_costructured_arrow_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) (X : (category_theory.structured_arrow d F)ᵒᵖ) :
(category_theory.structured_arrow.to_costructured_arrow F d).obj X = category_theory.costructured_arrow.mk (opposite.unop X).hom.op
source
@[simp]
theorem category_theory.structured_arrow.to_costructured_arrow_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) (X Y : (category_theory.structured_arrow d F)ᵒᵖ) (f : X ⟶ Y) :
(category_theory.structured_arrow.to_costructured_arrow F d).map f = category_theory.costructured_arrow.hom_mk f.unop.right.op _
source
def category_theory.structured_arrow.to_costructured_arrow {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) :
(category_theory.structured_arrow d F)ᵒᵖ ⥤ category_theory.costructured_arrow F.op (opposite.op 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
source
@[simp]
theorem category_theory.structured_arrow.to_costructured_arrow'_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) (X Y : (category_theory.structured_arrow (opposite.op d) F.op)ᵒᵖ) (f : X ⟶ Y) :
(category_theory.structured_arrow.to_costructured_arrow' F d).map f = category_theory.costructured_arrow.hom_mk f.unop.right.unop _
source
@[simp]
theorem category_theory.structured_arrow.to_costructured_arrow'_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) (X : (category_theory.structured_arrow (opposite.op d) F.op)ᵒᵖ) :
(category_theory.structured_arrow.to_costructured_arrow' F d).obj X = category_theory.costructured_arrow.mk (opposite.unop X).hom.unop
source
def category_theory.structured_arrow.to_costructured_arrow' {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) :
(category_theory.structured_arrow (opposite.op d) F.op)ᵒᵖ ⥤ category_theory.costructured_arrow F 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
source
@[simp]
theorem category_theory.costructured_arrow.to_structured_arrow_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) (X Y : (category_theory.costructured_arrow F d)ᵒᵖ) (f : X ⟶ Y) :
(category_theory.costructured_arrow.to_structured_arrow F d).map f = category_theory.structured_arrow.hom_mk f.unop.left.op _
source
def category_theory.costructured_arrow.to_structured_arrow {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) :
(category_theory.costructured_arrow F d)ᵒᵖ ⥤ category_theory.structured_arrow (opposite.op d) F.op

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
source
@[simp]
theorem category_theory.costructured_arrow.to_structured_arrow_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) (X : (category_theory.costructured_arrow F d)ᵒᵖ) :
(category_theory.costructured_arrow.to_structured_arrow F d).obj X = category_theory.structured_arrow.mk (opposite.unop X).hom.op
source
def category_theory.costructured_arrow.to_structured_arrow' {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) :
(category_theory.costructured_arrow F.op (opposite.op d))ᵒᵖ ⥤ category_theory.structured_arrow d F

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
source
@[simp]
theorem category_theory.costructured_arrow.to_structured_arrow'_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) (X : (category_theory.costructured_arrow F.op (opposite.op d))ᵒᵖ) :
(category_theory.costructured_arrow.to_structured_arrow' F d).obj X = category_theory.structured_arrow.mk (opposite.unop X).hom.unop
source
@[simp]
theorem category_theory.costructured_arrow.to_structured_arrow'_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) (X Y : (category_theory.costructured_arrow F.op (opposite.op d))ᵒᵖ) (f : X ⟶ Y) :
(category_theory.costructured_arrow.to_structured_arrow' F d).map f = category_theory.structured_arrow.hom_mk f.unop.left.unop _
source
def category_theory.structured_arrow_op_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) :
(category_theory.structured_arrow d F)ᵒᵖ ≌ category_theory.costructured_arrow F.op (opposite.op 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
source
def category_theory.costructured_arrow_op_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (d : D) :
(category_theory.costructured_arrow F d)ᵒᵖ ≌ category_theory.structured_arrow (opposite.op d) F.op

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