# Documentation

Mathlib.CategoryTheory.StructuredArrow

# 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 CategoryTheory.StructuredArrow {C : Type uā} {D : Type uā} (S : D) (T : ) :
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.

Instances For
instance CategoryTheory.instCategoryStructuredArrow {C : Type uā} {D : Type uā} (S : D) (T : ) :
@[simp]
theorem CategoryTheory.StructuredArrow.proj_map {C : Type uā} {D : Type uā} (S : D) (T : ) :
ā {X Y : } (f : X ā¶ Y), ().map f = f.right
@[simp]
theorem CategoryTheory.StructuredArrow.proj_obj {C : Type uā} {D : Type uā} (S : D) (T : ) :
().obj X = X.right
def CategoryTheory.StructuredArrow.proj {C : Type uā} {D : Type uā} (S : D) (T : ) :

The obvious projection functor from structured arrows.

Instances For
theorem CategoryTheory.StructuredArrow.hom_ext {C : Type uā} {D : Type uā} {S : D} {T : } {X : } {Y : } (f : X ā¶ Y) (g : X ā¶ Y) (h : f.right = g.right) :
f = g
@[simp]
theorem CategoryTheory.StructuredArrow.hom_eq_iff {C : Type uā} {D : Type uā} {S : D} {T : } {X : } {Y : } (f : X ā¶ Y) (g : X ā¶ Y) :
f = g ā f.right = g.right
def CategoryTheory.StructuredArrow.mk {C : Type uā} {D : Type uā} {S : D} {Y : C} {T : } (f : S ā¶ T.obj Y) :

Construct a structured arrow from a morphism.

Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.mk_left {C : Type uā} {D : Type uā} {S : D} {Y : C} {T : } (f : S ā¶ T.obj Y) :
().left = { as := PUnit.unit }
@[simp]
theorem CategoryTheory.StructuredArrow.mk_right {C : Type uā} {D : Type uā} {S : D} {Y : C} {T : } (f : S ā¶ T.obj Y) :
().right = Y
@[simp]
theorem CategoryTheory.StructuredArrow.mk_hom_eq_self {C : Type uā} {D : Type uā} {S : D} {Y : C} {T : } (f : S ā¶ T.obj Y) :
= f
@[simp]
theorem CategoryTheory.StructuredArrow.w_assoc {C : Type uā} {D : Type uā} {S : D} {T : } {A : } {B : } (f : A ā¶ B) {Z : D} (h : T.obj B.right ā¶ Z) :
@[simp]
theorem CategoryTheory.StructuredArrow.w {C : Type uā} {D : Type uā} {S : D} {T : } {A : } {B : } (f : A ā¶ B) :
CategoryTheory.CategoryStruct.comp A.hom (T.map f.right) = B.hom
@[simp]
theorem CategoryTheory.StructuredArrow.comp_right {C : Type uā} {D : Type uā} {S : D} {T : } {X : } {Y : } {Z : } (f : X ā¶ Y) (g : Y ā¶ Z) :
().right = CategoryTheory.CategoryStruct.comp f.right g.right
@[simp]
theorem CategoryTheory.StructuredArrow.id_right {C : Type uā} {D : Type uā} {S : D} {T : } (X : ) :
().right =
theorem CategoryTheory.StructuredArrow.eqToHom_right {C : Type uā} {D : Type uā} {S : D} {T : } {X : } {Y : } (h : X = Y) :
().right = CategoryTheory.eqToHom (_ : X.right = Y.right)
@[simp]
theorem CategoryTheory.StructuredArrow.left_eq_id {C : Type uā} {D : Type uā} {S : D} {T : } {X : } {Y : } (f : X ā¶ Y) :
f.left =
@[simp]
theorem CategoryTheory.StructuredArrow.homMk_right {C : Type uā} {D : Type uā} {S : D} {T : } {f : } {f' : } (g : f.right ā¶ f'.right) (w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom) _autoā) :
().right = g
@[simp]
theorem CategoryTheory.StructuredArrow.homMk_left {C : Type uā} {D : Type uā} {S : D} {T : } {f : } {f' : } (g : f.right ā¶ f'.right) (w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom) _autoā) :
().left = CategoryTheory.eqToHom (_ : f.left = f'.left)
def CategoryTheory.StructuredArrow.homMk {C : Type uā} {D : Type uā} {S : D} {T : } {f : } {f' : } (g : f.right ā¶ f'.right) (w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom) _autoā) :
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.

Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.homMk'_left {C : Type uā} {D : Type uā} {S : D} {Y' : C} {T : } (f : ) (g : f.right ā¶ Y') :
@[simp]
theorem CategoryTheory.StructuredArrow.homMk'_right {C : Type uā} {D : Type uā} {S : D} {Y' : C} {T : } (f : ) (g : f.right ā¶ Y') :
().right = g
def CategoryTheory.StructuredArrow.homMk' {C : Type uā} {D : Type uā} {S : D} {Y' : C} {T : } (f : ) (g : f.right ā¶ Y') :

Given a structured arrow X ā¶ T(Y), and an arrow Y ā¶ Y', we can construct a morphism of structured arrows given by (X ā¶ T(Y)) ā¶ (X ā¶ T(Y) ā¶ T(Y')).

Instances For
theorem CategoryTheory.StructuredArrow.homMk'_mk_id {C : Type uā} {D : Type uā} {S : D} {Y : C} {T : } (f : S ā¶ T.obj Y) :
@[simp]
theorem CategoryTheory.StructuredArrow.isoMk_hom_right {C : Type uā} {D : Type uā} {S : D} {T : } {f : } {f' : } (g : f.right ā f'.right) (w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom) _autoā) :
.right = g.hom
@[simp]
theorem CategoryTheory.StructuredArrow.isoMk_inv_left_down_down {C : Type uā} {D : Type uā} {S : D} {T : } {f : } {f' : } (g : f.right ā f'.right) (w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom) _autoā) :
(_ : f.left.as = f.left.as) = (_ : f.left.as = f.left.as)
@[simp]
theorem CategoryTheory.StructuredArrow.isoMk_inv_right {C : Type uā} {D : Type uā} {S : D} {T : } {f : } {f' : } (g : f.right ā f'.right) (w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom) _autoā) :
.right = g.inv
@[simp]
theorem CategoryTheory.StructuredArrow.isoMk_hom_left_down_down {C : Type uā} {D : Type uā} {S : D} {T : } {f : } {f' : } (g : f.right ā f'.right) (w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom) _autoā) :
(_ : f'.left.as = f'.left.as) = (_ : f'.left.as = f'.left.as)
def CategoryTheory.StructuredArrow.isoMk {C : Type uā} {D : Type uā} {S : D} {T : } {f : } {f' : } (g : f.right ā f'.right) (w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom) _autoā) :
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.

Instances For
theorem CategoryTheory.StructuredArrow.ext {C : Type uā} {D : Type uā} {S : D} {T : } {A : } {B : } (f : A ā¶ B) (g : A ā¶ B) :
f.right = g.right ā f = g
theorem CategoryTheory.StructuredArrow.ext_iff {C : Type uā} {D : Type uā} {S : D} {T : } {A : } {B : } (f : A ā¶ B) (g : A ā¶ B) :
f = g ā f.right = g.right
instance CategoryTheory.StructuredArrow.proj_faithful {C : Type uā} {D : Type uā} {S : D} {T : } :
theorem CategoryTheory.StructuredArrow.mono_of_mono_right {C : Type uā} {D : Type uā} {S : D} {T : } {A : } {B : } (f : A ā¶ B) [h : CategoryTheory.Mono f.right] :

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

theorem CategoryTheory.StructuredArrow.epi_of_epi_right {C : Type uā} {D : Type uā} {S : D} {T : } {A : } {B : } (f : A ā¶ B) [h : CategoryTheory.Epi f.right] :
instance CategoryTheory.StructuredArrow.mono_homMk {C : Type uā} {D : Type uā} {S : D} {T : } {A : } {B : } (f : A.right ā¶ B.right) (w : CategoryTheory.CategoryStruct.comp A.hom (T.map f) = B.hom) [h : ] :
instance CategoryTheory.StructuredArrow.epi_homMk {C : Type uā} {D : Type uā} {S : D} {T : } {A : } {B : } (f : A.right ā¶ B.right) (w : CategoryTheory.CategoryStruct.comp A.hom (T.map f) = B.hom) [h : ] :
theorem CategoryTheory.StructuredArrow.eq_mk {C : Type uā} {D : Type uā} {S : D} {T : } (f : ) :

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

@[simp]
theorem CategoryTheory.StructuredArrow.eta_inv_right {C : Type uā} {D : Type uā} {S : D} {T : } (f : ) :
.right =
@[simp]
theorem CategoryTheory.StructuredArrow.eta_hom_right {C : Type uā} {D : Type uā} {S : D} {T : } (f : ) :
.right =
@[simp]
theorem CategoryTheory.StructuredArrow.eta_hom_left_down_down {C : Type uā} {D : Type uā} {S : D} {T : } (f : ) :
(_ : ().left.as = ().left.as) = (_ : { as := PUnit.unit }.as = { as := PUnit.unit }.as)
@[simp]
theorem CategoryTheory.StructuredArrow.eta_inv_left_down_down {C : Type uā} {D : Type uā} {S : D} {T : } (f : ) :
(_ : f.left.as = f.left.as) = (_ : f.left.as = f.left.as)
def CategoryTheory.StructuredArrow.eta {C : Type uā} {D : Type uā} {S : D} {T : } (f : ) :

Eta rule for structured arrows.

Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.map_obj_right {C : Type uā} {D : Type uā} {S : D} {S' : D} {T : } (f : S ā¶ S') (X : ) :
(().obj X).right = X.right
@[simp]
theorem CategoryTheory.StructuredArrow.map_map_left {C : Type uā} {D : Type uā} {S : D} {S' : D} {T : } (f : S ā¶ S') :
ā {X Y : } (f : X ā¶ Y), (().map f).left =
@[simp]
theorem CategoryTheory.StructuredArrow.map_map_right {C : Type uā} {D : Type uā} {S : D} {S' : D} {T : } (f : S ā¶ S') :
ā {X Y : } (f : X ā¶ Y), (().map f).right = f.right
@[simp]
theorem CategoryTheory.StructuredArrow.map_obj_hom {C : Type uā} {D : Type uā} {S : D} {S' : D} {T : } (f : S ā¶ S') (X : ) :
(().obj X).hom =
@[simp]
theorem CategoryTheory.StructuredArrow.map_obj_left {C : Type uā} {D : Type uā} {S : D} {S' : D} {T : } (f : S ā¶ S') (X : ) :
(().obj X).left = X.left
def CategoryTheory.StructuredArrow.map {C : Type uā} {D : Type uā} {S : D} {S' : D} {T : } (f : S ā¶ S') :

A morphism between source objects S ā¶ S' contravariantly induces a functor between structured arrows, StructuredArrow S' T ā„¤ StructuredArrow 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.

Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.map_mk {C : Type uā} {D : Type uā} {S : D} {S' : D} {Y : C} {T : } {f : S' ā¶ T.obj Y} (g : S ā¶ S') :
@[simp]
theorem CategoryTheory.StructuredArrow.map_id {C : Type uā} {D : Type uā} {S : D} {T : } {f : } :
@[simp]
theorem CategoryTheory.StructuredArrow.map_comp {C : Type uā} {D : Type uā} {S : D} {S' : D} {S'' : D} {T : } {f : S ā¶ S'} {f' : S' ā¶ S''} {h : } :
= ().obj (().obj h)
def CategoryTheory.StructuredArrow.mapIso {C : Type uā} {D : Type uā} {S : D} {S' : D} {T : } (i : S ā S') :

An isomorphism S ā S' induces an equivalence StructuredArrow S T ā StructuredArrow S' T.

Instances For
def CategoryTheory.StructuredArrow.mapNatIso {C : Type uā} {D : Type uā} {S : D} {T : } {T' : } (i : T ā T') :

A natural isomorphism T ā T' induces an equivalence StructuredArrow S T ā StructuredArrow S T'.

Instances For
instance CategoryTheory.StructuredArrow.proj_reflectsIsomorphisms {C : Type uā} {D : Type uā} {S : D} {T : } :
def CategoryTheory.StructuredArrow.mkIdInitial {C : Type uā} {D : Type uā} {Y : C} {T : } :

The identity structured arrow is initial.

Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.pre_map_right {C : Type uā} {D : Type uā} {B : Type uā} (S : D) (F : ) (G : ) :
ā {X Y : } (f : X ā¶ Y), (().map f).right = F.map f.right
@[simp]
theorem CategoryTheory.StructuredArrow.pre_map_left {C : Type uā} {D : Type uā} {B : Type uā} (S : D) (F : ) (G : ) :
ā {X Y : } (f : X ā¶ Y), (().map f).left =
@[simp]
theorem CategoryTheory.StructuredArrow.pre_obj_left {C : Type uā} {D : Type uā} {B : Type uā} (S : D) (F : ) (G : ) :
(().obj X).left = X.left
@[simp]
theorem CategoryTheory.StructuredArrow.pre_obj_right {C : Type uā} {D : Type uā} {B : Type uā} (S : D) (F : ) (G : ) :
(().obj X).right = F.obj X.right
@[simp]
theorem CategoryTheory.StructuredArrow.pre_obj_hom {C : Type uā} {D : Type uā} {B : Type uā} (S : D) (F : ) (G : ) :
(().obj X).hom = X.hom
def CategoryTheory.StructuredArrow.pre {C : Type uā} {D : Type uā} {B : Type uā} (S : D) (F : ) (G : ) :

The functor (S, F ā G) ā„¤ (S, G).

Instances For
noncomputable def CategoryTheory.StructuredArrow.isEquivalencePre {C : Type uā} {D : Type uā} {B : Type uā} (S : D) (F : ) (G : ) :

If F is an equivalence, then so is the functor (S, F ā G) ā„¤ (S, G).

Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.post_obj {C : Type uā} {D : Type uā} {B : Type uā} (S : C) (F : ) (G : ) (X : ) :
().obj X = CategoryTheory.StructuredArrow.mk (G.map X.hom)
@[simp]
theorem CategoryTheory.StructuredArrow.post_map {C : Type uā} {D : Type uā} {B : Type uā} (S : C) (F : ) (G : ) :
ā {X Y : } (f : X ā¶ Y), ().map f =
def CategoryTheory.StructuredArrow.post {C : Type uā} {D : Type uā} {B : Type uā} (S : C) (F : ) (G : ) :

The functor (S, F) ā„¤ (G(S), F ā G).

Instances For
noncomputable def CategoryTheory.StructuredArrow.isEquivalencePost {C : Type uā} {D : Type uā} {B : Type uā} (S : C) (F : ) (G : ) :

If G is fully faithful, then post S F G : (S, F) ā„¤ (G(S), F ā G) is an equivalence.

Instances For
instance CategoryTheory.StructuredArrow.small_proj_preimage_of_locallySmall {C : Type uā} {D : Type uā} {S : D} {T : } {š¢ : Set C} [Small.{vā, uā} āš¢] :
Small.{vā, max uā vā} ā(().toPrefunctor.obj ā»Ā¹' š¢)
@[inline, reducible]
abbrev CategoryTheory.StructuredArrow.IsUniversal {C : Type uā} {D : Type uā} {S : D} {T : } (f : ) :
Type (max (max uā vā) vā)

A structured arrow is called universal if it is initial.

Instances For
theorem CategoryTheory.StructuredArrow.IsUniversal.uniq {C : Type uā} {D : Type uā} {S : D} {T : } {f : } {g : } (Ī· : f ā¶ g) :
def CategoryTheory.StructuredArrow.IsUniversal.desc {C : Type uā} {D : Type uā} {S : D} {T : } {f : } (g : ) :
f.right ā¶ g.right

The family of morphisms out of a universal arrow.

Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.IsUniversal.fac_assoc {C : Type uā} {D : Type uā} {S : D} {T : } {f : } (g : ) {Z : D} (h : T.obj g.right ā¶ Z) :
=
@[simp]
theorem CategoryTheory.StructuredArrow.IsUniversal.fac {C : Type uā} {D : Type uā} {S : D} {T : } {f : } (g : ) :
= g.hom

Any structured arrow factors through a universal arrow.

theorem CategoryTheory.StructuredArrow.IsUniversal.hom_desc {C : Type uā} {D : Type uā} {S : D} {T : } {f : } {c : C} (Ī· : f.right ā¶ c) :
Ī· =
theorem CategoryTheory.StructuredArrow.IsUniversal.hom_ext {C : Type uā} {D : Type uā} {S : D} {T : } {f : } {c : C} {Ī· : f.right ā¶ c} {Ī·' : f.right ā¶ c} (w : CategoryTheory.CategoryStruct.comp f.hom (T.map Ī·) = CategoryTheory.CategoryStruct.comp f.hom (T.map Ī·')) :
Ī· = Ī·'

Two morphisms out of a universal T-structured arrow are equal if their image under T are equal after precomposing the universal arrow.

theorem CategoryTheory.StructuredArrow.IsUniversal.existsUnique {C : Type uā} {D : Type uā} {S : D} {T : } {f : } (g : ) :
ā! Ī·, CategoryTheory.CategoryStruct.comp f.hom (T.map Ī·) = g.hom
def CategoryTheory.CostructuredArrow {C : Type uā} {D : Type uā} (S : ) (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.

Instances For
instance CategoryTheory.instCategoryCostructuredArrow {C : Type uā} {D : Type uā} (S : ) (T : D) :
@[simp]
theorem CategoryTheory.CostructuredArrow.proj_map {C : Type uā} {D : Type uā} (S : ) (T : D) :
ā {X Y : } (f : X ā¶ Y), ().map f = f.left
@[simp]
theorem CategoryTheory.CostructuredArrow.proj_obj {C : Type uā} {D : Type uā} (S : ) (T : D) :
().obj X = X.left
def CategoryTheory.CostructuredArrow.proj {C : Type uā} {D : Type uā} (S : ) (T : D) :

The obvious projection functor from costructured arrows.

Instances For
theorem CategoryTheory.CostructuredArrow.hom_ext {C : Type uā} {D : Type uā} {T : D} {S : } {X : } {Y : } (f : X ā¶ Y) (g : X ā¶ Y) (h : f.left = g.left) :
f = g
@[simp]
theorem CategoryTheory.CostructuredArrow.hom_eq_iff {C : Type uā} {D : Type uā} {T : D} {S : } {X : } {Y : } (f : X ā¶ Y) (g : X ā¶ Y) :
f = g ā f.left = g.left
def CategoryTheory.CostructuredArrow.mk {C : Type uā} {D : Type uā} {T : D} {Y : C} {S : } (f : S.obj Y ā¶ T) :

Construct a costructured arrow from a morphism.

Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.mk_left {C : Type uā} {D : Type uā} {T : D} {Y : C} {S : } (f : S.obj Y ā¶ T) :
().left = Y
@[simp]
theorem CategoryTheory.CostructuredArrow.mk_right {C : Type uā} {D : Type uā} {T : D} {Y : C} {S : } (f : S.obj Y ā¶ T) :
().right = { as := PUnit.unit }
@[simp]
theorem CategoryTheory.CostructuredArrow.mk_hom_eq_self {C : Type uā} {D : Type uā} {T : D} {Y : C} {S : } (f : S.obj Y ā¶ T) :
= f
theorem CategoryTheory.CostructuredArrow.w_assoc {C : Type uā} {D : Type uā} {T : D} {S : } {A : } {B : } (f : A ā¶ B) {Z : D} (h : ().obj B.right ā¶ Z) :
theorem CategoryTheory.CostructuredArrow.w {C : Type uā} {D : Type uā} {T : D} {S : } {A : } {B : } (f : A ā¶ B) :
CategoryTheory.CategoryStruct.comp (S.map f.left) B.hom = A.hom
@[simp]
theorem CategoryTheory.CostructuredArrow.comp_left {C : Type uā} {D : Type uā} {T : D} {S : } {X : } {Y : } {Z : } (f : X ā¶ Y) (g : Y ā¶ Z) :
@[simp]
theorem CategoryTheory.CostructuredArrow.id_left {C : Type uā} {D : Type uā} {T : D} {S : } (X : ) :
theorem CategoryTheory.CostructuredArrow.eqToHom_left {C : Type uā} {D : Type uā} {T : D} {S : } {X : } {Y : } (h : X = Y) :
().left = CategoryTheory.eqToHom (_ : X.left = Y.left)
@[simp]
theorem CategoryTheory.CostructuredArrow.right_eq_id {C : Type uā} {D : Type uā} {T : D} {S : } {X : } {Y : } (f : X ā¶ Y) :
f.right =
@[simp]
theorem CategoryTheory.CostructuredArrow.homMk_left {C : Type uā} {D : Type uā} {T : D} {S : } {f : } {f' : } (g : f.left ā¶ f'.left) (w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom) _autoā) :
= g
@[simp]
theorem CategoryTheory.CostructuredArrow.homMk_right_down_down {C : Type uā} {D : Type uā} {T : D} {S : } {f : } {f' : } (g : f.left ā¶ f'.left) (w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom) _autoā) :
(_ : f'.right.as = f'.right.as) = (_ : f'.right.as = f'.right.as)
def CategoryTheory.CostructuredArrow.homMk {C : Type uā} {D : Type uā} {T : D} {S : } {f : } {f' : } (g : f.left ā¶ f'.left) (w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom) _autoā) :
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.

Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.homMk'_right {C : Type uā} {D : Type uā} {T : D} {Y' : C} {S : } (f : ) (g : Y' ā¶ f.left) :
@[simp]
theorem CategoryTheory.CostructuredArrow.homMk'_left {C : Type uā} {D : Type uā} {T : D} {Y' : C} {S : } (f : ) (g : Y' ā¶ f.left) :
().left = g
def CategoryTheory.CostructuredArrow.homMk' {C : Type uā} {D : Type uā} {T : D} {Y' : C} {S : } (f : ) (g : Y' ā¶ f.left) :

Given a costructured arrow S(Y) ā¶ X, and an arrow Y' ā¶ Y', we can construct a morphism of costructured arrows given by (S(Y) ā¶ X) ā¶ (S(Y') ā¶ S(Y) ā¶ X).

Instances For
theorem CategoryTheory.CostructuredArrow.homMk'_mk_id {C : Type uā} {D : Type uā} {T : D} {Y : C} {S : } (f : S.obj Y ā¶ T) :
theorem CategoryTheory.CostructuredArrow.homMk'_mk_comp {C : Type uā} {D : Type uā} {T : D} {Y : C} {Y' : C} {Y'' : C} {S : } (f : S.obj Y ā¶ T) (g : Y' ā¶ Y) (g' : Y'' ā¶ Y') :
@[simp]
theorem CategoryTheory.CostructuredArrow.isoMk_hom_right_down_down {C : Type uā} {D : Type uā} {T : D} {S : } {f : } {f' : } (g : f.left ā f'.left) (w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom) _autoā) :
(_ : f'.right.as = f'.right.as) = (_ : f'.right.as = f'.right.as)
@[simp]
theorem CategoryTheory.CostructuredArrow.isoMk_inv_right_down_down {C : Type uā} {D : Type uā} {T : D} {S : } {f : } {f' : } (g : f.left ā f'.left) (w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom) _autoā) :
(_ : f.right.as = f.right.as) = (_ : f.right.as = f.right.as)
@[simp]
theorem CategoryTheory.CostructuredArrow.isoMk_inv_left {C : Type uā} {D : Type uā} {T : D} {S : } {f : } {f' : } (g : f.left ā f'.left) (w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom) _autoā) :
.left = g.inv
@[simp]
theorem CategoryTheory.CostructuredArrow.isoMk_hom_left {C : Type uā} {D : Type uā} {T : D} {S : } {f : } {f' : } (g : f.left ā f'.left) (w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom) _autoā) :
.left = g.hom
def CategoryTheory.CostructuredArrow.isoMk {C : Type uā} {D : Type uā} {T : D} {S : } {f : } {f' : } (g : f.left ā f'.left) (w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom) _autoā) :
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.

Instances For
theorem CategoryTheory.CostructuredArrow.ext {C : Type uā} {D : Type uā} {T : D} {S : } {A : } {B : } (f : A ā¶ B) (g : A ā¶ B) (h : f.left = g.left) :
f = g
theorem CategoryTheory.CostructuredArrow.ext_iff {C : Type uā} {D : Type uā} {T : D} {S : } {A : } {B : } (f : A ā¶ B) (g : A ā¶ B) :
f = g ā f.left = g.left
instance CategoryTheory.CostructuredArrow.proj_faithful {C : Type uā} {D : Type uā} {T : D} {S : } :
theorem CategoryTheory.CostructuredArrow.mono_of_mono_left {C : Type uā} {D : Type uā} {T : D} {S : } {A : } {B : } (f : A ā¶ B) [h : CategoryTheory.Mono f.left] :
theorem CategoryTheory.CostructuredArrow.epi_of_epi_left {C : Type uā} {D : Type uā} {T : D} {S : } {A : } {B : } (f : A ā¶ B) [h : CategoryTheory.Epi f.left] :

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

instance CategoryTheory.CostructuredArrow.mono_homMk {C : Type uā} {D : Type uā} {T : D} {S : } {A : } {B : } (f : A.left ā¶ B.left) (w : CategoryTheory.CategoryStruct.comp (S.map f) B.hom = A.hom) [h : ] :
instance CategoryTheory.CostructuredArrow.epi_homMk {C : Type uā} {D : Type uā} {T : D} {S : } {A : } {B : } (f : A.left ā¶ B.left) (w : CategoryTheory.CategoryStruct.comp (S.map f) B.hom = A.hom) [h : ] :
theorem CategoryTheory.CostructuredArrow.eq_mk {C : Type uā} {D : Type uā} {T : D} {S : } (f : ) :

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

@[simp]
theorem CategoryTheory.CostructuredArrow.eta_hom_right_down_down {C : Type uā} {D : Type uā} {T : D} {S : } (f : ) :
(_ : ().right.as = ().right.as) = (_ : { as := PUnit.unit }.as = { as := PUnit.unit }.as)
@[simp]
theorem CategoryTheory.CostructuredArrow.eta_inv_left {C : Type uā} {D : Type uā} {T : D} {S : } (f : ) :
.left =
@[simp]
theorem CategoryTheory.CostructuredArrow.eta_inv_right_down_down {C : Type uā} {D : Type uā} {T : D} {S : } (f : ) :
(_ : f.right.as = f.right.as) = (_ : f.right.as = f.right.as)
@[simp]
theorem CategoryTheory.CostructuredArrow.eta_hom_left {C : Type uā} {D : Type uā} {T : D} {S : } (f : ) :
.left =
def CategoryTheory.CostructuredArrow.eta {C : Type uā} {D : Type uā} {T : D} {S : } (f : ) :

Eta rule for costructured arrows.

Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.map_obj_left {C : Type uā} {D : Type uā} {T : D} {T' : D} {S : } (f : T ā¶ T') :
(().obj X).left = X.left
@[simp]
theorem CategoryTheory.CostructuredArrow.map_map_right {C : Type uā} {D : Type uā} {T : D} {T' : D} {S : } (f : T ā¶ T') :
ā {X Y : } (f : X ā¶ Y), (().map f).right =
@[simp]
theorem CategoryTheory.CostructuredArrow.map_obj_right {C : Type uā} {D : Type uā} {T : D} {T' : D} {S : } (f : T ā¶ T') :
(().obj X).right = X.right
@[simp]
theorem CategoryTheory.CostructuredArrow.map_obj_hom {C : Type uā} {D : Type uā} {T : D} {T' : D} {S : } (f : T ā¶ T') :
(().obj X).hom =
@[simp]
theorem CategoryTheory.CostructuredArrow.map_map_left {C : Type uā} {D : Type uā} {T : D} {T' : D} {S : } (f : T ā¶ T') :
ā {X Y : } (f : X ā¶ Y), (().map f).left = f.left
def CategoryTheory.CostructuredArrow.map {C : Type uā} {D : Type uā} {T : D} {T' : D} {S : } (f : T ā¶ T') :

A morphism between target objects T ā¶ T' covariantly induces a functor between costructured arrows, CostructuredArrow S T ā„¤ CostructuredArrow 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.

Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.map_mk {C : Type uā} {D : Type uā} {T : D} {T' : D} {Y : C} {S : } {f : S.obj Y ā¶ T} (g : T ā¶ T') :
@[simp]
theorem CategoryTheory.CostructuredArrow.map_id {C : Type uā} {D : Type uā} {T : D} {S : } {f : } :
@[simp]
theorem CategoryTheory.CostructuredArrow.map_comp {C : Type uā} {D : Type uā} {T : D} {T' : D} {T'' : D} {S : } {f : T ā¶ T'} {f' : T' ā¶ T''} {h : } :
= ().obj (().obj h)
def CategoryTheory.CostructuredArrow.mapIso {C : Type uā} {D : Type uā} {T : D} {T' : D} {S : } (i : T ā T') :

An isomorphism T ā T' induces an equivalence CostructuredArrow S T ā CostructuredArrow S T'.

Instances For
def CategoryTheory.CostructuredArrow.mapNatIso {C : Type uā} {D : Type uā} {T : D} {S : } {S' : } (i : S ā S') :

A natural isomorphism S ā S' induces an equivalence CostrucutredArrow S T ā CostructuredArrow S' T.

Instances For
instance CategoryTheory.CostructuredArrow.proj_reflectsIsomorphisms {C : Type uā} {D : Type uā} {T : D} {S : } :
def CategoryTheory.CostructuredArrow.mkIdTerminal {C : Type uā} {D : Type uā} {Y : C} {S : } :

The identity costructured arrow is terminal.

Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.pre_obj_left {C : Type uā} {D : Type uā} {B : Type uā} (F : ) (G : ) (S : D) :
(().obj X).left = F.obj X.left
@[simp]
theorem CategoryTheory.CostructuredArrow.pre_obj_hom {C : Type uā} {D : Type uā} {B : Type uā} (F : ) (G : ) (S : D) :
(().obj X).hom = X.hom
@[simp]
theorem CategoryTheory.CostructuredArrow.pre_obj_right {C : Type uā} {D : Type uā} {B : Type uā} (F : ) (G : ) (S : D) :
(().obj X).right = X.right
@[simp]
theorem CategoryTheory.CostructuredArrow.pre_map_right {C : Type uā} {D : Type uā} {B : Type uā} (F : ) (G : ) (S : D) :
ā {X Y : } (f : X ā¶ Y), (().map f).right =
@[simp]
theorem CategoryTheory.CostructuredArrow.pre_map_left {C : Type uā} {D : Type uā} {B : Type uā} (F : ) (G : ) (S : D) :
ā {X Y : } (f : X ā¶ Y), (().map f).left = F.map f.left
def CategoryTheory.CostructuredArrow.pre {C : Type uā} {D : Type uā} {B : Type uā} (F : ) (G : ) (S : D) :

The functor (F ā G, S) ā„¤ (G, S).

Instances For
noncomputable def CategoryTheory.CostructuredArrow.isEquivalencePre {C : Type uā} {D : Type uā} {B : Type uā} (F : ) (G : ) (S : D) :

If F is an equivalence, then so is the functor (F ā G, S) ā„¤ (G, S).

Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.post_map {C : Type uā} {D : Type uā} {B : Type uā} (F : ) (G : ) (S : C) :
ā {X Y : } (f : X ā¶ Y), ().map f =
@[simp]
theorem CategoryTheory.CostructuredArrow.post_obj {C : Type uā} {D : Type uā} {B : Type uā} (F : ) (G : ) (S : C) (X : ) :
().obj X = CategoryTheory.CostructuredArrow.mk (G.map X.hom)
def CategoryTheory.CostructuredArrow.post {C : Type uā} {D : Type uā} {B : Type uā} (F : ) (G : ) (S : C) :

The functor (F, S) ā„¤ (F ā G, G(S)).

Instances For
noncomputable def CategoryTheory.CostructuredArrow.isEquivalencePost {C : Type uā} {D : Type uā} {B : Type uā} (S : C) (F : ) (G : ) :

If G is fully faithful, then post F G S : (F, S) ā„¤ (F ā G, G(S)) is an equivalence.

Instances For
instance CategoryTheory.CostructuredArrow.small_proj_preimage_of_locallySmall {C : Type uā} {D : Type uā} {T : D} {S : } {š¢ : Set C} [Small.{vā, uā} āš¢] :
Small.{vā, max uā vā} ā(().toPrefunctor.obj ā»Ā¹' š¢)
@[inline, reducible]
abbrev CategoryTheory.CostructuredArrow.IsUniversal {C : Type uā} {D : Type uā} {T : D} {S : } (f : ) :
Type (max (max uā vā) vā)

A costructured arrow is called universal if it is terminal.

Instances For
theorem CategoryTheory.CostructuredArrow.IsUniversal.uniq {C : Type uā} {D : Type uā} {T : D} {S : } {f : } {g : } (Ī· : g ā¶ f) :
def CategoryTheory.CostructuredArrow.IsUniversal.lift {C : Type uā} {D : Type uā} {T : D} {S : } {f : } (g : ) :
g.left ā¶ f.left

The family of morphisms into a universal arrow.

Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.IsUniversal.fac_assoc {C : Type uā} {D : Type uā} {T : D} {S : } {f : } (g : ) {Z : D} (h : ().obj f.right ā¶ Z) :
=
@[simp]
theorem CategoryTheory.CostructuredArrow.IsUniversal.fac {C : Type uā} {D : Type uā} {T : D} {S : } {f : } (g : ) :
= g.hom

Any costructured arrow factors through a universal arrow.

theorem CategoryTheory.CostructuredArrow.IsUniversal.hom_desc {C : Type uā} {D : Type uā} {T : D} {S : } {f : } {c : C} (Ī· : c ā¶ f.left) :
Ī· =
theorem CategoryTheory.CostructuredArrow.IsUniversal.hom_ext {C : Type uā} {D : Type uā} {T : D} {S : } {f : } {c : C} {Ī· : c ā¶ f.left} {Ī·' : c ā¶ f.left} (w : CategoryTheory.CategoryStruct.comp (S.map Ī·) f.hom = CategoryTheory.CategoryStruct.comp (S.map Ī·') f.hom) :
Ī· = Ī·'

Two morphisms into a universal S-costructured arrow are equal if their image under S are equal after postcomposing the universal arrow.

theorem CategoryTheory.CostructuredArrow.IsUniversal.existsUnique {C : Type uā} {D : Type uā} {T : D} {S : } {f : } (g : ) :
ā! Ī·, CategoryTheory.CategoryStruct.comp (S.map Ī·) f.hom = g.hom
@[simp]
theorem CategoryTheory.Functor.toStructuredArrow_obj {C : Type uā} {D : Type uā} {E : Type uā} (G : ) (X : D) (F : ) (f : (Y : E) ā X ā¶ F.obj (G.obj Y)) (h : ā {Y Z : E} (g : Y ā¶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) (Y : E) :
().obj Y =
@[simp]
theorem CategoryTheory.Functor.toStructuredArrow_map {C : Type uā} {D : Type uā} {E : Type uā} (G : ) (X : D) (F : ) (f : (Y : E) ā X ā¶ F.obj (G.obj Y)) (h : ā {Y Z : E} (g : Y ā¶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) :
ā {X Y : E} (g : X ā¶ Y), ().map g = CategoryTheory.StructuredArrow.homMk (G.map g)
def CategoryTheory.Functor.toStructuredArrow {C : Type uā} {D : Type uā} {E : Type uā} (G : ) (X : D) (F : ) (f : (Y : E) ā X ā¶ F.obj (G.obj Y)) (h : ā {Y Z : E} (g : Y ā¶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) :

Given X : D and F : C ā„¤ D, to upgrade a functor G : E ā„¤ C to a functor E ā„¤ StructuredArrow X F, it suffices to provide maps X ā¶ F.obj (G.obj Y) for all Y making the obvious triangles involving all F.map (G.map g) commute.

This is of course the same as providing a cone over F ā G with cone point X, see Functor.toStructuredArrowIsoToStructuredArrow.

Instances For
def CategoryTheory.Functor.toStructuredArrowCompProj {C : Type uā} {D : Type uā} {E : Type uā} (G : ) (X : D) (F : ) (f : (Y : E) ā X ā¶ F.obj (G.obj Y)) (h : ā {Y Z : E} (g : Y ā¶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) :

Upgrading a functor E ā„¤ C to a functor E ā„¤ StructuredArrow X F and composing with the forgetful functor StructuredArrow X F ā„¤ C recovers the original functor.

Instances For
@[simp]
theorem CategoryTheory.Functor.toStructuredArrow_comp_proj {C : Type uā} {D : Type uā} {E : Type uā} (G : ) (X : D) (F : ) (f : (Y : E) ā X ā¶ F.obj (G.obj Y)) (h : ā {Y Z : E} (g : Y ā¶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) :
@[simp]
theorem CategoryTheory.Functor.toCostructuredArrow_obj {C : Type uā} {D : Type uā} {E : Type uā} (G : ) (F : ) (X : D) (f : (Y : E) ā F.obj (G.obj Y) ā¶ X) (h : ā {Y Z : E} (g : Y ā¶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) (Y : E) :
().obj Y =
@[simp]
theorem CategoryTheory.Functor.toCostructuredArrow_map {C : Type uā} {D : Type uā} {E : Type uā} (G : ) (F : ) (X : D) (f : (Y : E) ā F.obj (G.obj Y) ā¶ X) (h : ā {Y Z : E} (g : Y ā¶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) :
ā {X Y : E} (g : X ā¶ Y), ().map g =
def CategoryTheory.Functor.toCostructuredArrow {C : Type uā} {D : Type uā} {E : Type uā} (G : ) (F : ) (X : D) (f : (Y : E) ā F.obj (G.obj Y) ā¶ X) (h : ā {Y Z : E} (g : Y ā¶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) :

Given F : C ā„¤ D and X : D, to upgrade a functor G : E ā„¤ C to a functor E ā„¤ CostructuredArrow F X, it suffices to provide maps F.obj (G.obj Y) ā¶ X for all Y making the obvious triangles involving all F.map (G.map g) commute.

This is of course the same as providing a cocone over F ā G with cocone point X, see Functor.toCostructuredArrowIsoToCostructuredArrow.

Instances For
def CategoryTheory.Functor.toCostructuredArrowCompProj {C : Type uā} {D : Type uā} {E : Type uā} (G : ) (F : ) (X : D) (f : (Y : E) ā F.obj (G.obj Y) ā¶ X) (h : ā {Y Z : E} (g : Y ā¶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) :

Upgrading a functor E ā„¤ C to a functor E ā„¤ CostructuredArrow F X and composing with the forgetful functor CostructuredArrow F X ā„¤ C recovers the original functor.

Instances For
@[simp]
theorem CategoryTheory.Functor.toCostructuredArrow_comp_proj {C : Type uā} {D : Type uā} {E : Type uā} (G : ) (F : ) (X : D) (f : (Y : E) ā F.obj (G.obj Y) ā¶ X) (h : ā {Y Z : E} (g : Y ā¶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) :
@[simp]
theorem CategoryTheory.StructuredArrow.toCostructuredArrow_map {C : Type uā} {D : Type uā} (F : ) (d : D) :
ā {X Y : } (f : X ā¶ Y), = CategoryTheory.CostructuredArrow.homMk f.unop.right.op
@[simp]
theorem CategoryTheory.StructuredArrow.toCostructuredArrow_obj {C : Type uā} {D : Type uā} (F : ) (d : D) (X : ) :
def CategoryTheory.StructuredArrow.toCostructuredArrow {C : Type uā} {D : Type uā} (F : ) (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).

Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.toCostructuredArrow'_map {C : Type uā} {D : Type uā} (F : ) (d : D) :
ā {X Y : ()įµįµ} (f : X ā¶ Y), = CategoryTheory.CostructuredArrow.homMk f.unop.right.unop
@[simp]
theorem CategoryTheory.StructuredArrow.toCostructuredArrow'_obj {C : Type uā} {D : Type uā} (F : ) (d : D) (X : ()įµįµ) :
def CategoryTheory.StructuredArrow.toCostructuredArrow' {C : Type uā} {D : Type uā} (F : ) (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.

Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.toStructuredArrow_obj {C : Type uā} {D : Type uā} (F : ) (d : D) (X : ) :
@[simp]
theorem CategoryTheory.CostructuredArrow.toStructuredArrow_map {C : Type uā} {D : Type uā} (F : ) (d : D) :
ā {X Y : } (f : X ā¶ Y), = CategoryTheory.StructuredArrow.homMk f.unop.left.op
def CategoryTheory.CostructuredArrow.toStructuredArrow {C : Type uā} {D : Type uā} (F : ) (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.

Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.toStructuredArrow'_map {C : Type uā} {D : Type uā} (F : ) (d : D) :
ā {X Y : } (f : X ā¶ Y), = CategoryTheory.StructuredArrow.homMk f.unop.left.unop
@[simp]
theorem CategoryTheory.CostructuredArrow.toStructuredArrow'_obj {C : Type uā} {D : Type uā} (F : ) (d : D) (X : ) :
def CategoryTheory.CostructuredArrow.toStructuredArrow' {C : Type uā} {D : Type uā} (F : ) (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.

Instances For
def CategoryTheory.structuredArrowOpEquivalence {C : Type uā} {D : Type uā} (F : ) (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.

Instances For
def CategoryTheory.costructuredArrowOpEquivalence {C : Type uā} {D : Type uā} (F : ) (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.

Instances For