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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (S : D) (T : CategoryTheory.Functor 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

• CategoryTheory.StructuredArrow S T = CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T

instance CategoryTheory.instCategoryStructuredArrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (S : D) (T : CategoryTheory.Functor C D) : CategoryTheory.Category.{v₁, max u₁ v₂} (CategoryTheory.StructuredArrow S T)

Equations

• CategoryTheory.instCategoryStructuredArrow S T = CategoryTheory.commaCategory

def CategoryTheory.StructuredArrow.proj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (S : D) (T : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.StructuredArrow S T) C

The obvious projection functor from structured arrows.

Equations

• CategoryTheory.StructuredArrow.proj S T = CategoryTheory.Comma.snd (CategoryTheory.Functor.fromPUnit S) T

@[simp]

theorem CategoryTheory.StructuredArrow.proj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (S : D) (T : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T} (f : X✝ ⟶ Y✝) : (CategoryTheory.StructuredArrow.proj S T).map f = f.right

@[simp]

theorem CategoryTheory.StructuredArrow.proj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (S : D) (T : CategoryTheory.Functor C D) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T) : (CategoryTheory.StructuredArrow.proj S T).obj X = X.right

theorem CategoryTheory.StructuredArrow.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (f g : X ⟶ Y) (h : f.right = g.right) : f = g

@[simp]

theorem CategoryTheory.StructuredArrow.hom_eq_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (f g : X ⟶ Y) : f = g ↔ f.right = g.right

def CategoryTheory.StructuredArrow.mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) : CategoryTheory.StructuredArrow S T

Construct a structured arrow from a morphism.

Equations

• CategoryTheory.StructuredArrow.mk f = { left := { as := PUnit.unit }, right := Y, hom := f }

@[simp]

theorem CategoryTheory.StructuredArrow.mk_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) : (CategoryTheory.StructuredArrow.mk f).left = { as := PUnit.unit }

@[simp]

theorem CategoryTheory.StructuredArrow.mk_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) : (CategoryTheory.StructuredArrow.mk f).right = Y

@[simp]

theorem CategoryTheory.StructuredArrow.mk_hom_eq_self {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) : (CategoryTheory.StructuredArrow.mk f).hom = f

@[simp]

theorem CategoryTheory.StructuredArrow.w {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp A.hom (T.map f.right) = B.hom

@[simp]

theorem CategoryTheory.StructuredArrow.w_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f : A ⟶ B) {Z : D} (h : T.obj B.right ⟶ Z) : CategoryTheory.CategoryStruct.comp A.hom (CategoryTheory.CategoryStruct.comp (T.map f.right) h) = CategoryTheory.CategoryStruct.comp B.hom h

@[simp]

theorem CategoryTheory.StructuredArrow.comp_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {X Y Z : CategoryTheory.StructuredArrow S T} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.right

@[simp]

theorem CategoryTheory.StructuredArrow.id_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (X : CategoryTheory.StructuredArrow S T) : (CategoryTheory.CategoryStruct.id X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.StructuredArrow.eqToHom_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (h : X = Y) : (CategoryTheory.eqToHom h).right = CategoryTheory.eqToHom ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.left_eq_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (f : X ⟶ Y) : f.left = CategoryTheory.CategoryStruct.id X.left

def CategoryTheory.StructuredArrow.homMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g : f.right ⟶ f'.right) (w : CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom := by aesop_cat) : 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

• CategoryTheory.StructuredArrow.homMk g w = { left := CategoryTheory.CategoryStruct.id f.left, right := g, w := ⋯ }

@[simp]

theorem CategoryTheory.StructuredArrow.homMk_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g : f.right ⟶ f'.right) (w : CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom := by aesop_cat) : (CategoryTheory.StructuredArrow.homMk g w).left = CategoryTheory.CategoryStruct.id f.left

@[simp]

theorem CategoryTheory.StructuredArrow.homMk_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g : f.right ⟶ f'.right) (w : CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom := by aesop_cat) : (CategoryTheory.StructuredArrow.homMk g w).right = g

theorem CategoryTheory.StructuredArrow.homMk_surjective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (φ : f ⟶ f') : ∃ (ψ : f.right ⟶ f'.right), ∃ (hψ : CategoryTheory.CategoryStruct.comp f.hom (T.map ψ) = f'.hom), φ = CategoryTheory.StructuredArrow.homMk ψ hψ

def CategoryTheory.StructuredArrow.homMk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y' : C} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) (g : f.right ⟶ Y') : f ⟶ CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f.hom (T.map g))

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')).

Equations

• f.homMk' g = { left := CategoryTheory.CategoryStruct.id f.left, right := g, w := ⋯ }

@[simp]

theorem CategoryTheory.StructuredArrow.homMk'_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y' : C} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) (g : f.right ⟶ Y') : (f.homMk' g).left = CategoryTheory.CategoryStruct.id f.left

@[simp]

theorem CategoryTheory.StructuredArrow.homMk'_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y' : C} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) (g : f.right ⟶ Y') : (f.homMk' g).right = g

theorem CategoryTheory.StructuredArrow.homMk'_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) : f.homMk' (CategoryTheory.CategoryStruct.id f.right) = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.StructuredArrow.homMk'_mk_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) : (CategoryTheory.StructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.StructuredArrow.homMk'_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y' Y'' : C} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) (g : f.right ⟶ Y') (g' : Y' ⟶ Y'') : f.homMk' (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (f.homMk' g) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f.hom (T.map g))).homMk' g') (CategoryTheory.eqToHom ⋯))

theorem CategoryTheory.StructuredArrow.homMk'_mk_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y Y' Y'' : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') : (CategoryTheory.StructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.mk f).homMk' g) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f (T.map g))).homMk' g') (CategoryTheory.eqToHom ⋯))

def CategoryTheory.StructuredArrow.mkPostcomp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y Y' : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) (g : Y ⟶ Y') : CategoryTheory.StructuredArrow.mk f ⟶ CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f (T.map g))

Variant of homMk' where both objects are applications of mk.

Equations

• CategoryTheory.StructuredArrow.mkPostcomp f g = { left := CategoryTheory.CategoryStruct.id (CategoryTheory.StructuredArrow.mk f).left, right := g, w := ⋯ }

@[simp]

theorem CategoryTheory.StructuredArrow.mkPostcomp_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y Y' : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) (g : Y ⟶ Y') : (CategoryTheory.StructuredArrow.mkPostcomp f g).left = CategoryTheory.CategoryStruct.id (CategoryTheory.StructuredArrow.mk f).left

@[simp]

theorem CategoryTheory.StructuredArrow.mkPostcomp_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y Y' : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) (g : Y ⟶ Y') : (CategoryTheory.StructuredArrow.mkPostcomp f g).right = g

theorem CategoryTheory.StructuredArrow.mkPostcomp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) : CategoryTheory.StructuredArrow.mkPostcomp f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.StructuredArrow.mkPostcomp_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y Y' Y'' : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') : CategoryTheory.StructuredArrow.mkPostcomp f (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.mkPostcomp f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.mkPostcomp (CategoryTheory.CategoryStruct.comp f (T.map g)) g') (CategoryTheory.eqToHom ⋯))

def CategoryTheory.StructuredArrow.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g : f.right ≅ f'.right) (w : CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom := by aesop_cat) : 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

• CategoryTheory.StructuredArrow.isoMk g w = CategoryTheory.Comma.isoMk (CategoryTheory.eqToIso ⋯) g ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.isoMk_hom_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g : f.right ≅ f'.right) (w : CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom := by aesop_cat) : (CategoryTheory.StructuredArrow.isoMk g w).hom.right = g.hom

@[simp]

theorem CategoryTheory.StructuredArrow.isoMk_inv_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g : f.right ≅ f'.right) (w : CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom := by aesop_cat) : (CategoryTheory.StructuredArrow.isoMk g w).inv.right = g.inv

@[simp]

theorem CategoryTheory.StructuredArrow.isoMk_inv_left_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g : f.right ≅ f'.right) (w : CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom := by aesop_cat) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.isoMk_hom_left_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g : f.right ≅ f'.right) (w : CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom := by aesop_cat) : ⋯ = ⋯

theorem CategoryTheory.StructuredArrow.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f g : A ⟶ B) : f.right = g.right → f = g

theorem CategoryTheory.StructuredArrow.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f g : A ⟶ B) : f = g ↔ f.right = g.right

instance CategoryTheory.StructuredArrow.proj_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} : (CategoryTheory.StructuredArrow.proj S T).Faithful

theorem CategoryTheory.StructuredArrow.mono_of_mono_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f : A ⟶ B) [h : CategoryTheory.Mono f.right] : CategoryTheory.Mono f

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

theorem CategoryTheory.StructuredArrow.epi_of_epi_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f : A ⟶ B) [h : CategoryTheory.Epi f.right] : CategoryTheory.Epi f

instance CategoryTheory.StructuredArrow.mono_homMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f : A.right ⟶ B.right) (w : CategoryTheory.CategoryStruct.comp A.hom (T.map f) = B.hom) [h : CategoryTheory.Mono f] : CategoryTheory.Mono (CategoryTheory.StructuredArrow.homMk f w)

instance CategoryTheory.StructuredArrow.epi_homMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f : A.right ⟶ B.right) (w : CategoryTheory.CategoryStruct.comp A.hom (T.map f) = B.hom) [h : CategoryTheory.Epi f] : CategoryTheory.Epi (CategoryTheory.StructuredArrow.homMk f w)

theorem CategoryTheory.StructuredArrow.eq_mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) : f = CategoryTheory.StructuredArrow.mk f.hom

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

def CategoryTheory.StructuredArrow.eta {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) : f ≅ CategoryTheory.StructuredArrow.mk f.hom

Eta rule for structured arrows.

Equations

• f.eta = CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl f.right) ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.eta_hom_left_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.eta_inv_left_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.eta_inv_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) : f.eta.inv.right = CategoryTheory.CategoryStruct.id f.right

@[simp]

theorem CategoryTheory.StructuredArrow.eta_hom_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) : f.eta.hom.right = CategoryTheory.CategoryStruct.id f.right

theorem CategoryTheory.StructuredArrow.mk_surjective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) : ∃ (Y : C), ∃ (g : S ⟶ T.obj Y), f = CategoryTheory.StructuredArrow.mk g

def CategoryTheory.StructuredArrow.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S S' : D} {T : CategoryTheory.Functor C D} (f : S ⟶ S') : CategoryTheory.Functor (CategoryTheory.StructuredArrow S' T) (CategoryTheory.StructuredArrow S T)

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.

Equations

• CategoryTheory.StructuredArrow.map f = CategoryTheory.Comma.mapLeft T ((CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{1})).map f)

@[simp]

theorem CategoryTheory.StructuredArrow.map_obj_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S S' : D} {T : CategoryTheory.Functor C D} (f : S ⟶ S') (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T) : ((CategoryTheory.StructuredArrow.map f).obj X).hom = CategoryTheory.CategoryStruct.comp f X.hom

@[simp]

theorem CategoryTheory.StructuredArrow.map_map_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S S' : D} {T : CategoryTheory.Functor C D} (f : S ⟶ S') {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T} (f✝ : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.map f).map f✝).right = f✝.right

@[simp]

theorem CategoryTheory.StructuredArrow.map_obj_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S S' : D} {T : CategoryTheory.Functor C D} (f : S ⟶ S') (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T) : ((CategoryTheory.StructuredArrow.map f).obj X).left = X.left

@[simp]

theorem CategoryTheory.StructuredArrow.map_obj_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S S' : D} {T : CategoryTheory.Functor C D} (f : S ⟶ S') (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T) : ((CategoryTheory.StructuredArrow.map f).obj X).right = X.right

@[simp]

theorem CategoryTheory.StructuredArrow.map_map_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S S' : D} {T : CategoryTheory.Functor C D} (f : S ⟶ S') {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T} (f✝ : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.map f).map f✝).left = CategoryTheory.CategoryStruct.id X✝.left

@[simp]

theorem CategoryTheory.StructuredArrow.map_mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S S' : D} {Y : C} {T : CategoryTheory.Functor C D} {f : S' ⟶ T.obj Y} (g : S ⟶ S') : (CategoryTheory.StructuredArrow.map g).obj (CategoryTheory.StructuredArrow.mk f) = CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp g f)

@[simp]

theorem CategoryTheory.StructuredArrow.map_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} : (CategoryTheory.StructuredArrow.map (CategoryTheory.CategoryStruct.id S)).obj f = f

@[simp]

theorem CategoryTheory.StructuredArrow.map_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S S' S'' : D} {T : CategoryTheory.Functor C D} {f : S ⟶ S'} {f' : S' ⟶ S''} {h : CategoryTheory.StructuredArrow S'' T} : (CategoryTheory.StructuredArrow.map (CategoryTheory.CategoryStruct.comp f f')).obj h = (CategoryTheory.StructuredArrow.map f).obj ((CategoryTheory.StructuredArrow.map f').obj h)

def CategoryTheory.StructuredArrow.mapIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S') : CategoryTheory.StructuredArrow S T ≌ CategoryTheory.StructuredArrow S' T

An isomorphism S ≅ S' induces an equivalence StructuredArrow S T ≌ StructuredArrow S' T.

Equations

• CategoryTheory.StructuredArrow.mapIso i = CategoryTheory.Comma.mapLeftIso T ((CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{1})).mapIso i)

def CategoryTheory.StructuredArrow.mapNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T') : CategoryTheory.StructuredArrow S T ≌ CategoryTheory.StructuredArrow S T'

A natural isomorphism T ≅ T' induces an equivalence StructuredArrow S T ≌ StructuredArrow S T'.

Equations

• CategoryTheory.StructuredArrow.mapNatIso i = CategoryTheory.Comma.mapRightIso (CategoryTheory.Functor.fromPUnit S) i

instance CategoryTheory.StructuredArrow.proj_reflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} : (CategoryTheory.StructuredArrow.proj S T).ReflectsIsomorphisms

noncomputable def CategoryTheory.StructuredArrow.mkIdInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {Y : C} {T : CategoryTheory.Functor C D} [T.Full] [T.Faithful] : CategoryTheory.Limits.IsInitial (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (T.obj Y)))

The identity structured arrow is initial.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.StructuredArrow.pre {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.StructuredArrow S (F.comp G)) (CategoryTheory.StructuredArrow S G)

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

Equations

• CategoryTheory.StructuredArrow.pre S F G = CategoryTheory.Comma.preRight (CategoryTheory.Functor.fromPUnit S) F G

@[simp]

theorem CategoryTheory.StructuredArrow.pre_obj_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)) : ((CategoryTheory.StructuredArrow.pre S F G).obj X).right = F.obj X.right

@[simp]

theorem CategoryTheory.StructuredArrow.pre_map_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.pre S F G).map f).right = F.map f.right

@[simp]

theorem CategoryTheory.StructuredArrow.pre_obj_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)) : ((CategoryTheory.StructuredArrow.pre S F G).obj X).left = X.left

@[simp]

theorem CategoryTheory.StructuredArrow.pre_obj_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)) : ((CategoryTheory.StructuredArrow.pre S F G).obj X).hom = X.hom

@[simp]

theorem CategoryTheory.StructuredArrow.pre_map_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.pre S F G).map f).left = CategoryTheory.CategoryStruct.id X✝.left

instance CategoryTheory.StructuredArrow.instFaithfulCompPre {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) [F.Faithful] : (CategoryTheory.StructuredArrow.pre S F G).Faithful

instance CategoryTheory.StructuredArrow.instFullCompPre {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) [F.Full] : (CategoryTheory.StructuredArrow.pre S F G).Full

instance CategoryTheory.StructuredArrow.instEssSurjCompPre {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) [F.EssSurj] : (CategoryTheory.StructuredArrow.pre S F G).EssSurj

instance CategoryTheory.StructuredArrow.isEquivalence_pre {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) [F.IsEquivalence] : (CategoryTheory.StructuredArrow.pre S F G).IsEquivalence

If F is an equivalence, then so is the functor (S, F ⋙ G) ⥤ (S, G).

def CategoryTheory.StructuredArrow.post {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.StructuredArrow S F) (CategoryTheory.StructuredArrow (G.obj S) (F.comp G))

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.StructuredArrow.post_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (X : CategoryTheory.StructuredArrow S F) : (CategoryTheory.StructuredArrow.post S F G).obj X = CategoryTheory.StructuredArrow.mk (G.map X.hom)

@[simp]

theorem CategoryTheory.StructuredArrow.post_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.StructuredArrow S F} (f : X✝ ⟶ Y✝) : (CategoryTheory.StructuredArrow.post S F G).map f = CategoryTheory.StructuredArrow.homMk f.right ⋯

instance CategoryTheory.StructuredArrow.instFaithfulObjCompPost {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) : (CategoryTheory.StructuredArrow.post S F G).Faithful

instance CategoryTheory.StructuredArrow.instFullObjCompPostOfFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) [G.Faithful] : (CategoryTheory.StructuredArrow.post S F G).Full

instance CategoryTheory.StructuredArrow.instEssSurjObjCompPostOfFull {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) [G.Full] : (CategoryTheory.StructuredArrow.post S F G).EssSurj

instance CategoryTheory.StructuredArrow.isEquivalence_post {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) [G.Full] [G.Faithful] : (CategoryTheory.StructuredArrow.post S F G).IsEquivalence

If G is fully faithful, then post S F G : (S, F) ⥤ (G(S), F ⋙ G) is an equivalence.

def CategoryTheory.StructuredArrow.map₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L) (β : R.comp G ⟶ F.comp R') : CategoryTheory.Functor (CategoryTheory.StructuredArrow L R) (CategoryTheory.StructuredArrow L' R')

The functor StructuredArrow L R ⥤ StructuredArrow L' R' that is deduced from a natural transformation R ⋙ G ⟶ F ⋙ R' and a morphism L' ⟶ G.obj L.

Equations

• CategoryTheory.StructuredArrow.map₂ α β = CategoryTheory.Comma.map (CategoryTheory.Discrete.natTrans fun (x : CategoryTheory.Discrete PUnit.{1}) => α) β

@[simp]

theorem CategoryTheory.StructuredArrow.map₂_obj_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L) (β : R.comp G ⟶ F.comp R') (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R) : ((CategoryTheory.StructuredArrow.map₂ α β).obj X).hom = CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (G.map X.hom) (β.app X.right))

@[simp]

theorem CategoryTheory.StructuredArrow.map₂_obj_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L) (β : R.comp G ⟶ F.comp R') (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R) : ((CategoryTheory.StructuredArrow.map₂ α β).obj X).right = F.obj X.right

@[simp]

theorem CategoryTheory.StructuredArrow.map₂_map_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L) (β : R.comp G ⟶ F.comp R') {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R} (φ : X ⟶ Y) : ((CategoryTheory.StructuredArrow.map₂ α β).map φ).left = CategoryTheory.CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.StructuredArrow.map₂_map_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L) (β : R.comp G ⟶ F.comp R') {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R} (φ : X ⟶ Y) : ((CategoryTheory.StructuredArrow.map₂ α β).map φ).right = F.map φ.right

@[simp]

theorem CategoryTheory.StructuredArrow.map₂_obj_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L) (β : R.comp G ⟶ F.comp R') (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R) : ((CategoryTheory.StructuredArrow.map₂ α β).obj X).left = X.left

instance CategoryTheory.StructuredArrow.faithful_map₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L) (β : R.comp G ⟶ F.comp R') [F.Faithful] : (CategoryTheory.StructuredArrow.map₂ α β).Faithful

instance CategoryTheory.StructuredArrow.full_map₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L) (β : R.comp G ⟶ F.comp R') [G.Faithful] [F.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] : (CategoryTheory.StructuredArrow.map₂ α β).Full

instance CategoryTheory.StructuredArrow.essSurj_map₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L) (β : R.comp G ⟶ F.comp R') [F.EssSurj] [G.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] : (CategoryTheory.StructuredArrow.map₂ α β).EssSurj

instance CategoryTheory.StructuredArrow.isEquivalenceMap₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L) (β : R.comp G ⟶ F.comp R') [F.IsEquivalence] [G.Faithful] [G.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] : (CategoryTheory.StructuredArrow.map₂ α β).IsEquivalence

def CategoryTheory.StructuredArrow.postIsoMap₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) : CategoryTheory.StructuredArrow.post S F G ≅ CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (G.obj S)) (CategoryTheory.CategoryStruct.id (F.comp G))

StructuredArrow.post is a special case of StructuredArrow.map₂ up to natural isomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.StructuredArrow.IsUniversal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) : Type (max (max u₁ v₂) v₁)

A structured arrow is called universal if it is initial.

Equations

• f.IsUniversal = CategoryTheory.Limits.IsInitial f

theorem CategoryTheory.StructuredArrow.IsUniversal.uniq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f g : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) (η : f ⟶ g) : η = CategoryTheory.Limits.IsInitial.to h g

def CategoryTheory.StructuredArrow.IsUniversal.desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) (g : CategoryTheory.StructuredArrow S T) : f.right ⟶ g.right

The family of morphisms out of a universal arrow.

Equations

• h.desc g = (CategoryTheory.Limits.IsInitial.to h g).right

@[simp]

theorem CategoryTheory.StructuredArrow.IsUniversal.fac {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) (g : CategoryTheory.StructuredArrow S T) : CategoryTheory.CategoryStruct.comp f.hom (T.map (h.desc g)) = g.hom

Any structured arrow factors through a universal arrow.

@[simp]

theorem CategoryTheory.StructuredArrow.IsUniversal.fac_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) (g : CategoryTheory.StructuredArrow S T) {Z : D} (h✝ : T.obj g.right ⟶ Z) : CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (T.map (h.desc g)) h✝) = CategoryTheory.CategoryStruct.comp g.hom h✝

theorem CategoryTheory.StructuredArrow.IsUniversal.hom_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) {c : C} (η : f.right ⟶ c) : η = h.desc (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f.hom (T.map η)))

theorem CategoryTheory.StructuredArrow.IsUniversal.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) {c : 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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) (g : CategoryTheory.StructuredArrow S T) : ∃! η : f.right ⟶ g.right, CategoryTheory.CategoryStruct.comp f.hom (T.map η) = g.hom

def CategoryTheory.CostructuredArrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (S : CategoryTheory.Functor 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

• CategoryTheory.CostructuredArrow S T = CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)

instance CategoryTheory.instCategoryCostructuredArrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (S : CategoryTheory.Functor C D) (T : D) : CategoryTheory.Category.{v₁, max u₁ v₂} (CategoryTheory.CostructuredArrow S T)

Equations

• CategoryTheory.instCategoryCostructuredArrow S T = CategoryTheory.commaCategory

def CategoryTheory.CostructuredArrow.proj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (S : CategoryTheory.Functor C D) (T : D) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow S T) C

The obvious projection functor from costructured arrows.

Equations

• CategoryTheory.CostructuredArrow.proj S T = CategoryTheory.Comma.fst S (CategoryTheory.Functor.fromPUnit T)

@[simp]

theorem CategoryTheory.CostructuredArrow.proj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (S : CategoryTheory.Functor C D) (T : D) {X✝ Y✝ : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f : X✝ ⟶ Y✝) : (CategoryTheory.CostructuredArrow.proj S T).map f = f.left

@[simp]

theorem CategoryTheory.CostructuredArrow.proj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (S : CategoryTheory.Functor C D) (T : D) (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)) : (CategoryTheory.CostructuredArrow.proj S T).obj X = X.left

theorem CategoryTheory.CostructuredArrow.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {X Y : CategoryTheory.CostructuredArrow S T} (f g : X ⟶ Y) (h : f.left = g.left) : f = g

@[simp]

theorem CategoryTheory.CostructuredArrow.hom_eq_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {X Y : CategoryTheory.CostructuredArrow S T} (f g : X ⟶ Y) : f = g ↔ f.left = g.left

def CategoryTheory.CostructuredArrow.mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) : CategoryTheory.CostructuredArrow S T

Construct a costructured arrow from a morphism.

Equations

• CategoryTheory.CostructuredArrow.mk f = { left := Y, right := { as := PUnit.unit }, hom := f }

@[simp]

theorem CategoryTheory.CostructuredArrow.mk_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) : (CategoryTheory.CostructuredArrow.mk f).left = Y

@[simp]

theorem CategoryTheory.CostructuredArrow.mk_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) : (CategoryTheory.CostructuredArrow.mk f).right = { as := PUnit.unit }

@[simp]

theorem CategoryTheory.CostructuredArrow.mk_hom_eq_self {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) : (CategoryTheory.CostructuredArrow.mk f).hom = f

theorem CategoryTheory.CostructuredArrow.w {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (S.map f.left) B.hom = A.hom

theorem CategoryTheory.CostructuredArrow.w_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f : A ⟶ B) {Z : D} (h : (CategoryTheory.Functor.fromPUnit T).obj B.right ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.map f.left) (CategoryTheory.CategoryStruct.comp B.hom h) = CategoryTheory.CategoryStruct.comp A.hom h

@[simp]

theorem CategoryTheory.CostructuredArrow.comp_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {X Y Z : CategoryTheory.CostructuredArrow S T} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.left

@[simp]

theorem CategoryTheory.CostructuredArrow.id_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (X : CategoryTheory.CostructuredArrow S T) : (CategoryTheory.CategoryStruct.id X).left = CategoryTheory.CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.CostructuredArrow.eqToHom_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {X Y : CategoryTheory.CostructuredArrow S T} (h : X = Y) : (CategoryTheory.eqToHom h).left = CategoryTheory.eqToHom ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.right_eq_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {X Y : CategoryTheory.CostructuredArrow S T} (f : X ⟶ Y) : f.right = CategoryTheory.CategoryStruct.id X.right

def CategoryTheory.CostructuredArrow.homMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g : f.left ⟶ f'.left) (w : CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom := by aesop_cat) : 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

• CategoryTheory.CostructuredArrow.homMk g w = { left := g, right := CategoryTheory.CategoryStruct.id f.right, w := ⋯ }

@[simp]

theorem CategoryTheory.CostructuredArrow.homMk_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g : f.left ⟶ f'.left) (w : CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom := by aesop_cat) : (CategoryTheory.CostructuredArrow.homMk g w).left = g

@[simp]

theorem CategoryTheory.CostructuredArrow.homMk_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g : f.left ⟶ f'.left) (w : CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom := by aesop_cat) : ⋯ = ⋯

theorem CategoryTheory.CostructuredArrow.homMk_surjective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (φ : f ⟶ f') : ∃ (ψ : f.left ⟶ f'.left), ∃ (hψ : CategoryTheory.CategoryStruct.comp (S.map ψ) f'.hom = f.hom), φ = CategoryTheory.CostructuredArrow.homMk ψ hψ

def CategoryTheory.CostructuredArrow.homMk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y' : C} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) (g : Y' ⟶ f.left) : CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom) ⟶ f

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

Equations

• f.homMk' g = { left := g, right := CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom)).right, w := ⋯ }

@[simp]

theorem CategoryTheory.CostructuredArrow.homMk'_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y' : C} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) (g : Y' ⟶ f.left) : (f.homMk' g).right = CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom)).right

@[simp]

theorem CategoryTheory.CostructuredArrow.homMk'_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y' : C} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) (g : Y' ⟶ f.left) : (f.homMk' g).left = g

theorem CategoryTheory.CostructuredArrow.homMk'_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) : f.homMk' (CategoryTheory.CategoryStruct.id f.left) = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.CostructuredArrow.homMk'_mk_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) : (CategoryTheory.CostructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.CostructuredArrow.homMk'_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y' Y'' : C} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) (g : Y' ⟶ f.left) (g' : Y'' ⟶ Y') : f.homMk' (CategoryTheory.CategoryStruct.comp g' g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom)).homMk' g') (f.homMk' g))

theorem CategoryTheory.CostructuredArrow.homMk'_mk_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y Y' Y'' : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') : (CategoryTheory.CostructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.comp g' g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f)).homMk' g') ((CategoryTheory.CostructuredArrow.mk f).homMk' g))

def CategoryTheory.CostructuredArrow.mkPrecomp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y Y' : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) : CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f) ⟶ CategoryTheory.CostructuredArrow.mk f

Variant of homMk' where both objects are applications of mk.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.CostructuredArrow.mkPrecomp_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y Y' : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) : (CategoryTheory.CostructuredArrow.mkPrecomp f g).left = g

@[simp]

theorem CategoryTheory.CostructuredArrow.mkPrecomp_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y Y' : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) : (CategoryTheory.CostructuredArrow.mkPrecomp f g).right = CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f)).right

theorem CategoryTheory.CostructuredArrow.mkPrecomp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) : CategoryTheory.CostructuredArrow.mkPrecomp f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.CostructuredArrow.mkPrecomp_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y Y' Y'' : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') : CategoryTheory.CostructuredArrow.mkPrecomp f (CategoryTheory.CategoryStruct.comp g' g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CostructuredArrow.mkPrecomp (CategoryTheory.CategoryStruct.comp (S.map g) f) g') (CategoryTheory.CostructuredArrow.mkPrecomp f g))

def CategoryTheory.CostructuredArrow.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g : f.left ≅ f'.left) (w : CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom := by aesop_cat) : 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

• CategoryTheory.CostructuredArrow.isoMk g w = CategoryTheory.Comma.isoMk g (CategoryTheory.eqToIso ⋯) ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.isoMk_hom_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g : f.left ≅ f'.left) (w : CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom := by aesop_cat) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.isoMk_hom_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g : f.left ≅ f'.left) (w : CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom := by aesop_cat) : (CategoryTheory.CostructuredArrow.isoMk g w).hom.left = g.hom

@[simp]

theorem CategoryTheory.CostructuredArrow.isoMk_inv_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g : f.left ≅ f'.left) (w : CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom := by aesop_cat) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.isoMk_inv_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g : f.left ≅ f'.left) (w : CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom := by aesop_cat) : (CategoryTheory.CostructuredArrow.isoMk g w).inv.left = g.inv

theorem CategoryTheory.CostructuredArrow.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f g : A ⟶ B) (h : f.left = g.left) : f = g

theorem CategoryTheory.CostructuredArrow.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f g : A ⟶ B) : f = g ↔ f.left = g.left

instance CategoryTheory.CostructuredArrow.proj_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} : (CategoryTheory.CostructuredArrow.proj S T).Faithful

theorem CategoryTheory.CostructuredArrow.mono_of_mono_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f : A ⟶ B) [h : CategoryTheory.Mono f.left] : CategoryTheory.Mono f

theorem CategoryTheory.CostructuredArrow.epi_of_epi_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f : A ⟶ B) [h : CategoryTheory.Epi f.left] : CategoryTheory.Epi f

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

instance CategoryTheory.CostructuredArrow.mono_homMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f : A.left ⟶ B.left) (w : CategoryTheory.CategoryStruct.comp (S.map f) B.hom = A.hom) [h : CategoryTheory.Mono f] : CategoryTheory.Mono (CategoryTheory.CostructuredArrow.homMk f w)

instance CategoryTheory.CostructuredArrow.epi_homMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f : A.left ⟶ B.left) (w : CategoryTheory.CategoryStruct.comp (S.map f) B.hom = A.hom) [h : CategoryTheory.Epi f] : CategoryTheory.Epi (CategoryTheory.CostructuredArrow.homMk f w)

theorem CategoryTheory.CostructuredArrow.eq_mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) : f = CategoryTheory.CostructuredArrow.mk f.hom

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

def CategoryTheory.CostructuredArrow.eta {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) : f ≅ CategoryTheory.CostructuredArrow.mk f.hom

Eta rule for costructured arrows.

Equations

• f.eta = CategoryTheory.CostructuredArrow.isoMk (CategoryTheory.Iso.refl f.left) ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.eta_hom_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) : f.eta.hom.left = CategoryTheory.CategoryStruct.id f.left

@[simp]

theorem CategoryTheory.CostructuredArrow.eta_hom_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.eta_inv_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.eta_inv_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) : f.eta.inv.left = CategoryTheory.CategoryStruct.id f.left

theorem CategoryTheory.CostructuredArrow.mk_surjective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) : ∃ (Y : C), ∃ (g : S.obj Y ⟶ T), f = CategoryTheory.CostructuredArrow.mk g

def CategoryTheory.CostructuredArrow.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') : CategoryTheory.Functor (CategoryTheory.CostructuredArrow S T) (CategoryTheory.CostructuredArrow S 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.

Equations

• CategoryTheory.CostructuredArrow.map f = CategoryTheory.Comma.mapRight S ((CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{1})).map f)

@[simp]

theorem CategoryTheory.CostructuredArrow.map_map_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') {X✝ Y✝ : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f✝ : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.map f).map f✝).left = f✝.left

@[simp]

theorem CategoryTheory.CostructuredArrow.map_obj_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)) : ((CategoryTheory.CostructuredArrow.map f).obj X).left = X.left

@[simp]

theorem CategoryTheory.CostructuredArrow.map_map_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') {X✝ Y✝ : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f✝ : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.map f).map f✝).right = CategoryTheory.CategoryStruct.id X✝.right

@[simp]

theorem CategoryTheory.CostructuredArrow.map_obj_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)) : ((CategoryTheory.CostructuredArrow.map f).obj X).right = X.right

@[simp]

theorem CategoryTheory.CostructuredArrow.map_obj_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)) : ((CategoryTheory.CostructuredArrow.map f).obj X).hom = CategoryTheory.CategoryStruct.comp X.hom f

@[simp]

theorem CategoryTheory.CostructuredArrow.map_mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {Y : C} {S : CategoryTheory.Functor C D} {f : S.obj Y ⟶ T} (g : T ⟶ T') : (CategoryTheory.CostructuredArrow.map g).obj (CategoryTheory.CostructuredArrow.mk f) = CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.CostructuredArrow.map_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} : (CategoryTheory.CostructuredArrow.map (CategoryTheory.CategoryStruct.id T)).obj f = f

@[simp]

theorem CategoryTheory.CostructuredArrow.map_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' T'' : D} {S : CategoryTheory.Functor C D} {f : T ⟶ T'} {f' : T' ⟶ T''} {h : CategoryTheory.CostructuredArrow S T} : (CategoryTheory.CostructuredArrow.map (CategoryTheory.CategoryStruct.comp f f')).obj h = (CategoryTheory.CostructuredArrow.map f').obj ((CategoryTheory.CostructuredArrow.map f).obj h)

def CategoryTheory.CostructuredArrow.mapIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T') : CategoryTheory.CostructuredArrow S T ≌ CategoryTheory.CostructuredArrow S T'

An isomorphism T ≅ T' induces an equivalence CostructuredArrow S T ≌ CostructuredArrow S T'.

Equations

• CategoryTheory.CostructuredArrow.mapIso i = CategoryTheory.Comma.mapRightIso S ((CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{1})).mapIso i)

def CategoryTheory.CostructuredArrow.mapNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S') : CategoryTheory.CostructuredArrow S T ≌ CategoryTheory.CostructuredArrow S' T

A natural isomorphism S ≅ S' induces an equivalence CostrucutredArrow S T ≌ CostructuredArrow S' T.

Equations

• CategoryTheory.CostructuredArrow.mapNatIso i = CategoryTheory.Comma.mapLeftIso (CategoryTheory.Functor.fromPUnit T) i

instance CategoryTheory.CostructuredArrow.proj_reflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} : (CategoryTheory.CostructuredArrow.proj S T).ReflectsIsomorphisms

noncomputable def CategoryTheory.CostructuredArrow.mkIdTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {Y : C} {S : CategoryTheory.Functor C D} [S.Full] [S.Faithful] : CategoryTheory.Limits.IsTerminal (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (S.obj Y)))

The identity costructured arrow is terminal.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.CostructuredArrow.pre {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : D) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow (F.comp G) S) (CategoryTheory.CostructuredArrow G S)

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

Equations

• CategoryTheory.CostructuredArrow.pre F G S = CategoryTheory.Comma.preLeft F G (CategoryTheory.Functor.fromPUnit S)

@[simp]

theorem CategoryTheory.CostructuredArrow.pre_obj_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : D) (X : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)) : ((CategoryTheory.CostructuredArrow.pre F G S).obj X).right = X.right

@[simp]

theorem CategoryTheory.CostructuredArrow.pre_obj_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : D) (X : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)) : ((CategoryTheory.CostructuredArrow.pre F G S).obj X).left = F.obj X.left

@[simp]

theorem CategoryTheory.CostructuredArrow.pre_map_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : D) {X✝ Y✝ : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.pre F G S).map f).left = F.map f.left

@[simp]

theorem CategoryTheory.CostructuredArrow.pre_map_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : D) {X✝ Y✝ : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.pre F G S).map f).right = CategoryTheory.CategoryStruct.id X✝.right

@[simp]

theorem CategoryTheory.CostructuredArrow.pre_obj_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : D) (X : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)) : ((CategoryTheory.CostructuredArrow.pre F G S).obj X).hom = X.hom

instance CategoryTheory.CostructuredArrow.instFaithfulCompPre {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : D) [F.Faithful] : (CategoryTheory.CostructuredArrow.pre F G S).Faithful

instance CategoryTheory.CostructuredArrow.instFullCompPre {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : D) [F.Full] : (CategoryTheory.CostructuredArrow.pre F G S).Full

instance CategoryTheory.CostructuredArrow.instEssSurjCompPre {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : D) [F.EssSurj] : (CategoryTheory.CostructuredArrow.pre F G S).EssSurj

instance CategoryTheory.CostructuredArrow.isEquivalence_pre {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : D) [F.IsEquivalence] : (CategoryTheory.CostructuredArrow.pre F G S).IsEquivalence

If F is an equivalence, then so is the functor (F ⋙ G, S) ⥤ (G, S).

def CategoryTheory.CostructuredArrow.post {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : C) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow F S) (CategoryTheory.CostructuredArrow (F.comp G) (G.obj S))

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.CostructuredArrow.post_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : C) {X✝ Y✝ : CategoryTheory.CostructuredArrow F S} (f : X✝ ⟶ Y✝) : (CategoryTheory.CostructuredArrow.post F G S).map f = CategoryTheory.CostructuredArrow.homMk f.left ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.post_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : C) (X : CategoryTheory.CostructuredArrow F S) : (CategoryTheory.CostructuredArrow.post F G S).obj X = CategoryTheory.CostructuredArrow.mk (G.map X.hom)

instance CategoryTheory.CostructuredArrow.instFaithfulCompObjPost {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : C) : (CategoryTheory.CostructuredArrow.post F G S).Faithful

instance CategoryTheory.CostructuredArrow.instFullCompObjPostOfFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : C) [G.Faithful] : (CategoryTheory.CostructuredArrow.post F G S).Full

instance CategoryTheory.CostructuredArrow.instEssSurjCompObjPostOfFull {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : C) [G.Full] : (CategoryTheory.CostructuredArrow.post F G S).EssSurj

instance CategoryTheory.CostructuredArrow.isEquivalence_post {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) [G.Full] [G.Faithful] : (CategoryTheory.CostructuredArrow.post F G S).IsEquivalence

If G is fully faithful, then post F G S : (F, S) ⥤ (F ⋙ G, G(S)) is an equivalence.

def CategoryTheory.CostructuredArrow.map₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow S T) (CategoryTheory.CostructuredArrow U V)

The functor CostructuredArrow S T ⥤ CostructuredArrow U V that is deduced from a natural transformation F ⋙ U ⟶ S ⋙ G and a morphism G.obj T ⟶ V

Equations

• CategoryTheory.CostructuredArrow.map₂ α β = CategoryTheory.Comma.map α (CategoryTheory.Discrete.natTrans fun (x : CategoryTheory.Discrete PUnit.{1}) => β)

@[simp]

theorem CategoryTheory.CostructuredArrow.map₂_obj_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V) (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)) : ((CategoryTheory.CostructuredArrow.map₂ α β).obj X).hom = CategoryTheory.CategoryStruct.comp (α.app X.left) (CategoryTheory.CategoryStruct.comp (G.map X.hom) β)

@[simp]

theorem CategoryTheory.CostructuredArrow.map₂_obj_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V) (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)) : ((CategoryTheory.CostructuredArrow.map₂ α β).obj X).right = X.right

@[simp]

theorem CategoryTheory.CostructuredArrow.map₂_map_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V) {X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (φ : X ⟶ Y) : ((CategoryTheory.CostructuredArrow.map₂ α β).map φ).left = F.map φ.left

@[simp]

theorem CategoryTheory.CostructuredArrow.map₂_map_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V) {X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (φ : X ⟶ Y) : ((CategoryTheory.CostructuredArrow.map₂ α β).map φ).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.CostructuredArrow.map₂_obj_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V) (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)) : ((CategoryTheory.CostructuredArrow.map₂ α β).obj X).left = F.obj X.left

instance CategoryTheory.CostructuredArrow.faithful_map₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V) [F.Faithful] : (CategoryTheory.CostructuredArrow.map₂ α β).Faithful

instance CategoryTheory.CostructuredArrow.full_map₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V) [G.Faithful] [F.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] : (CategoryTheory.CostructuredArrow.map₂ α β).Full

instance CategoryTheory.CostructuredArrow.essSurj_map₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V) [F.EssSurj] [G.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] : (CategoryTheory.CostructuredArrow.map₂ α β).EssSurj

instance CategoryTheory.CostructuredArrow.isEquivalenceMap₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V) [F.IsEquivalence] [G.Faithful] [G.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] : (CategoryTheory.CostructuredArrow.map₂ α β).IsEquivalence

def CategoryTheory.CostructuredArrow.postIsoMap₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) : CategoryTheory.CostructuredArrow.post F G S ≅ CategoryTheory.CostructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (F.comp G)) (CategoryTheory.CategoryStruct.id (G.obj S))

CostructuredArrow.post is a special case of CostructuredArrow.map₂ up to natural isomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.CostructuredArrow.IsUniversal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) : Type (max (max u₁ v₂) v₁)

A costructured arrow is called universal if it is terminal.

Equations

• f.IsUniversal = CategoryTheory.Limits.IsTerminal f

theorem CategoryTheory.CostructuredArrow.IsUniversal.uniq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f g : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) (η : g ⟶ f) : η = CategoryTheory.Limits.IsTerminal.from h g

def CategoryTheory.CostructuredArrow.IsUniversal.lift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) (g : CategoryTheory.CostructuredArrow S T) : g.left ⟶ f.left

The family of morphisms into a universal arrow.

Equations

• h.lift g = (CategoryTheory.Limits.IsTerminal.from h g).left

@[simp]

theorem CategoryTheory.CostructuredArrow.IsUniversal.fac {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) (g : CategoryTheory.CostructuredArrow S T) : CategoryTheory.CategoryStruct.comp (S.map (h.lift g)) f.hom = g.hom

Any costructured arrow factors through a universal arrow.

@[simp]

theorem CategoryTheory.CostructuredArrow.IsUniversal.fac_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) (g : CategoryTheory.CostructuredArrow S T) {Z : D} (h✝ : (CategoryTheory.Functor.fromPUnit T).obj f.right ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.map (h.lift g)) (CategoryTheory.CategoryStruct.comp f.hom h✝) = CategoryTheory.CategoryStruct.comp g.hom h✝

theorem CategoryTheory.CostructuredArrow.IsUniversal.hom_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) {c : C} (η : c ⟶ f.left) : η = h.lift (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map η) f.hom))

theorem CategoryTheory.CostructuredArrow.IsUniversal.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) {c : C} {η η' : 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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) (g : CategoryTheory.CostructuredArrow S T) : ∃! η : g.left ⟶ f.left, CategoryTheory.CategoryStruct.comp (S.map η) f.hom = g.hom

def CategoryTheory.Functor.toStructuredArrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (X : D) (F : CategoryTheory.Functor C D) (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) : CategoryTheory.Functor E (CategoryTheory.StructuredArrow X F)

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.toStructuredArrow_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (X : D) (F : CategoryTheory.Functor C D) (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) : (G.toStructuredArrow X F f h).obj Y = CategoryTheory.StructuredArrow.mk (f Y)

@[simp]

theorem CategoryTheory.Functor.toStructuredArrow_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (X : D) (F : CategoryTheory.Functor C D) (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✝) : (G.toStructuredArrow X F f h).map g = CategoryTheory.StructuredArrow.homMk (G.map g) ⋯

def CategoryTheory.Functor.toStructuredArrowCompProj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (X : D) (F : CategoryTheory.Functor C D) (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) : (G.toStructuredArrow X F f ⋯).comp (CategoryTheory.StructuredArrow.proj X F) ≅ G

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.

Equations

• G.toStructuredArrowCompProj X F f h = CategoryTheory.Iso.refl ((G.toStructuredArrow X F f ⋯).comp (CategoryTheory.StructuredArrow.proj X F))

@[simp]

theorem CategoryTheory.Functor.toStructuredArrow_comp_proj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (X : D) (F : CategoryTheory.Functor C D) (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) : (G.toStructuredArrow X F f ⋯).comp (CategoryTheory.StructuredArrow.proj X F) = G

def CategoryTheory.Functor.toCostructuredArrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (F : CategoryTheory.Functor C D) (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) : CategoryTheory.Functor E (CategoryTheory.CostructuredArrow F X)

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.toCostructuredArrow_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (F : CategoryTheory.Functor C D) (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✝) : (G.toCostructuredArrow F X f h).map g = CategoryTheory.CostructuredArrow.homMk (G.map g) ⋯

@[simp]

theorem CategoryTheory.Functor.toCostructuredArrow_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (F : CategoryTheory.Functor C D) (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) : (G.toCostructuredArrow F X f h).obj Y = CategoryTheory.CostructuredArrow.mk (f Y)

def CategoryTheory.Functor.toCostructuredArrowCompProj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (F : CategoryTheory.Functor C D) (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) : (G.toCostructuredArrow F X f ⋯).comp (CategoryTheory.CostructuredArrow.proj F X) ≅ G

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.

Equations

• G.toCostructuredArrowCompProj F X f h = CategoryTheory.Iso.refl ((G.toCostructuredArrow F X f ⋯).comp (CategoryTheory.CostructuredArrow.proj F X))

@[simp]

theorem CategoryTheory.Functor.toCostructuredArrow_comp_proj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (F : CategoryTheory.Functor C D) (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) : (G.toCostructuredArrow F X f ⋯).comp (CategoryTheory.CostructuredArrow.proj F X) = G

def CategoryTheory.StructuredArrow.toCostructuredArrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) : CategoryTheory.Functor (CategoryTheory.StructuredArrow d F)ᵒᵖ (CategoryTheory.CostructuredArrow 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.StructuredArrow.toCostructuredArrow_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) {X✝ Y✝ : (CategoryTheory.StructuredArrow d F)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.StructuredArrow.toCostructuredArrow F d).map f = CategoryTheory.CostructuredArrow.homMk f.unop.right.op ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.toCostructuredArrow_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) (X : (CategoryTheory.StructuredArrow d F)ᵒᵖ) : (CategoryTheory.StructuredArrow.toCostructuredArrow F d).obj X = CategoryTheory.CostructuredArrow.mk (Opposite.unop X).hom.op

def CategoryTheory.StructuredArrow.toCostructuredArrow' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) : CategoryTheory.Functor (CategoryTheory.StructuredArrow (Opposite.op d) F.op)ᵒᵖ (CategoryTheory.CostructuredArrow 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.StructuredArrow.toCostructuredArrow'_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) (X : (CategoryTheory.StructuredArrow (Opposite.op d) F.op)ᵒᵖ) : (CategoryTheory.StructuredArrow.toCostructuredArrow' F d).obj X = CategoryTheory.CostructuredArrow.mk (Opposite.unop X).hom.unop

@[simp]

theorem CategoryTheory.StructuredArrow.toCostructuredArrow'_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) {X✝ Y✝ : (CategoryTheory.StructuredArrow (Opposite.op d) F.op)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.StructuredArrow.toCostructuredArrow' F d).map f = CategoryTheory.CostructuredArrow.homMk f.unop.right.unop ⋯

def CategoryTheory.CostructuredArrow.toStructuredArrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow F d)ᵒᵖ (CategoryTheory.StructuredArrow (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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.CostructuredArrow.toStructuredArrow_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) (X : (CategoryTheory.CostructuredArrow F d)ᵒᵖ) : (CategoryTheory.CostructuredArrow.toStructuredArrow F d).obj X = CategoryTheory.StructuredArrow.mk (Opposite.unop X).hom.op

@[simp]

theorem CategoryTheory.CostructuredArrow.toStructuredArrow_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) {X✝ Y✝ : (CategoryTheory.CostructuredArrow F d)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.CostructuredArrow.toStructuredArrow F d).map f = CategoryTheory.StructuredArrow.homMk f.unop.left.op ⋯

def CategoryTheory.CostructuredArrow.toStructuredArrow' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow F.op (Opposite.op d))ᵒᵖ (CategoryTheory.StructuredArrow 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.CostructuredArrow.toStructuredArrow'_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) {X✝ Y✝ : (CategoryTheory.CostructuredArrow F.op (Opposite.op d))ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.CostructuredArrow.toStructuredArrow' F d).map f = CategoryTheory.StructuredArrow.homMk f.unop.left.unop ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.toStructuredArrow'_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) (X : (CategoryTheory.CostructuredArrow F.op (Opposite.op d))ᵒᵖ) : (CategoryTheory.CostructuredArrow.toStructuredArrow' F d).obj X = CategoryTheory.StructuredArrow.mk (Opposite.unop X).hom.unop

def CategoryTheory.structuredArrowOpEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) : (CategoryTheory.StructuredArrow d F)ᵒᵖ ≌ CategoryTheory.CostructuredArrow 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

• One or more equations did not get rendered due to their size.

def CategoryTheory.costructuredArrowOpEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) : (CategoryTheory.CostructuredArrow F d)ᵒᵖ ≌ CategoryTheory.StructuredArrow (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

• One or more equations did not get rendered due to their size.

def CategoryTheory.StructuredArrow.preEquivalenceFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) : CategoryTheory.Functor (CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G)) (CategoryTheory.StructuredArrow f.right F)

The functor establishing the equivalence StructuredArrow.preEquivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceFunctor_obj_left_as {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) (g : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G)) : ((CategoryTheory.StructuredArrow.preEquivalenceFunctor F f).obj g).left.as = PUnit.unit

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceFunctor_obj_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) (g : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G)) : ((CategoryTheory.StructuredArrow.preEquivalenceFunctor F f).obj g).hom = g.hom.right

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceFunctor_obj_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) (g : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G)) : ((CategoryTheory.StructuredArrow.preEquivalenceFunctor F f).obj g).right = g.right.right

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceFunctor_map_left_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) {X✝ Y✝ : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G)} (φ : X✝ ⟶ Y✝) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceFunctor_map_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) {X✝ Y✝ : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G)} (φ : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.preEquivalenceFunctor F f).map φ).right = φ.right.right

def CategoryTheory.StructuredArrow.preEquivalenceInverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) : CategoryTheory.Functor (CategoryTheory.StructuredArrow f.right F) (CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G))

The inverse functor establishing the equivalence StructuredArrow.preEquivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceInverse_map_right_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) {X✝ Y✝ : CategoryTheory.StructuredArrow f.right F} (φ : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).map φ).right.right = φ.right

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceInverse_map_right_left_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) {X✝ Y✝ : CategoryTheory.StructuredArrow f.right F} (φ : X✝ ⟶ Y✝) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_hom_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) (g : CategoryTheory.StructuredArrow f.right F) : ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).obj g).hom.right = g.hom

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_left_as {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) (g : CategoryTheory.StructuredArrow f.right F) : ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).obj g).left.as = PUnit.unit

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_hom_left_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) (g : CategoryTheory.StructuredArrow f.right F) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_right_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) (g : CategoryTheory.StructuredArrow f.right F) : ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).obj g).right.hom = CategoryTheory.CategoryStruct.comp f.hom (G.map g.hom)

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceInverse_map_left_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) {X✝ Y✝ : CategoryTheory.StructuredArrow f.right F} (φ : X✝ ⟶ Y✝) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_right_left_as {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) (g : CategoryTheory.StructuredArrow f.right F) : ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).obj g).right.left.as = PUnit.unit

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_right_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) (g : CategoryTheory.StructuredArrow f.right F) : ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).obj g).right.right = g.right

def CategoryTheory.StructuredArrow.preEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G) ≌ CategoryTheory.StructuredArrow f.right F

A structured arrow category on a StructuredArrow.pre e F G functor is equivalent to the structured arrow category on F

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalence_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) : (CategoryTheory.StructuredArrow.preEquivalence F f).functor = CategoryTheory.StructuredArrow.preEquivalenceFunctor F f

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalence_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) : (CategoryTheory.StructuredArrow.preEquivalence F f).counitIso = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.StructuredArrow f.right F) => CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl (((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).comp (CategoryTheory.StructuredArrow.preEquivalenceFunctor F f)).obj x).right) ⋯) ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalence_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) : (CategoryTheory.StructuredArrow.preEquivalence F f).inverse = CategoryTheory.StructuredArrow.preEquivalenceInverse F f

@[simp]

theorem CategoryTheory.StructuredArrow.preEquivalence_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) : (CategoryTheory.StructuredArrow.preEquivalence F f).unitIso = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G)) => CategoryTheory.StructuredArrow.isoMk (CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G))).obj x).right.right) ⋯) ⋯) ⋯

def CategoryTheory.StructuredArrow.map₂IsoPreEquivalenceInverseCompProj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (T : CategoryTheory.Functor C D) (S : CategoryTheory.Functor D E) (d : D) (e : E) (u : e ⟶ S.obj d) : CategoryTheory.StructuredArrow.map₂ u (CategoryTheory.CategoryStruct.id (T.comp S)) ≅ (CategoryTheory.StructuredArrow.preEquivalence T (CategoryTheory.StructuredArrow.mk u)).inverse.comp (CategoryTheory.StructuredArrow.proj (CategoryTheory.StructuredArrow.mk u) (CategoryTheory.StructuredArrow.pre e T S))

The functor StructuredArrow d T ⥤ StructuredArrow e (T ⋙ S) that u : e ⟶ S.obj d induces via StructuredArrow.map₂ can be expressed up to isomorphism by StructuredArrow.preEquivalence and StructuredArrow.proj.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.CostructuredArrow.preEquivalence.functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f) (CategoryTheory.CostructuredArrow F f.left)

The functor establishing the equivalence CostructuredArrow.preEquivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.functor_obj_right_as {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) (g : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f) : ((CategoryTheory.CostructuredArrow.preEquivalence.functor F f).obj g).right.as = PUnit.unit

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.functor_map_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) {X✝ Y✝ : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f} (φ : X✝ ⟶ Y✝) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.functor_map_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) {X✝ Y✝ : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f} (φ : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.preEquivalence.functor F f).map φ).left = φ.left.left

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.functor_obj_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) (g : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f) : ((CategoryTheory.CostructuredArrow.preEquivalence.functor F f).obj g).left = g.left.left

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.functor_obj_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) (g : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f) : ((CategoryTheory.CostructuredArrow.preEquivalence.functor F f).obj g).hom = g.hom.left

def CategoryTheory.CostructuredArrow.preEquivalence.inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow F f.left) (CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f)

The inverse functor establishing the equivalence CostructuredArrow.preEquivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.inverse_map_left_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) {X✝ Y✝ : CategoryTheory.CostructuredArrow F f.left} (φ : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).map φ).left.left = φ.left

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_left_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) (g : CategoryTheory.CostructuredArrow F f.left) : ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).obj g).left.hom = CategoryTheory.CategoryStruct.comp (G.map g.hom) f.hom

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_left_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) (g : CategoryTheory.CostructuredArrow F f.left) : ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).obj g).left.left = g.left

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.inverse_map_left_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) {X✝ Y✝ : CategoryTheory.CostructuredArrow F f.left} (φ : X✝ ⟶ Y✝) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_right_as {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) (g : CategoryTheory.CostructuredArrow F f.left) : ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).obj g).right.as = PUnit.unit

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.inverse_map_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) {X✝ Y✝ : CategoryTheory.CostructuredArrow F f.left} (φ : X✝ ⟶ Y✝) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_hom_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) (g : CategoryTheory.CostructuredArrow F f.left) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_hom_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) (g : CategoryTheory.CostructuredArrow F f.left) : ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).obj g).hom.left = g.hom

@[simp]

theorem CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_left_right_as {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) (g : CategoryTheory.CostructuredArrow F f.left) : ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).obj g).left.right.as = PUnit.unit

def CategoryTheory.CostructuredArrow.preEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f ≌ CategoryTheory.CostructuredArrow F f.left

A costructured arrow category on a CostructuredArrow.pre F G e functor is equivalent to the costructured arrow category on F

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.CostructuredArrow.map₂IsoPreEquivalenceInverseCompProj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (T : CategoryTheory.Functor C D) (S : CategoryTheory.Functor D E) (d : D) (e : E) (u : S.obj d ⟶ e) : CategoryTheory.CostructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (T.comp S)) u ≅ (CategoryTheory.CostructuredArrow.preEquivalence T (CategoryTheory.CostructuredArrow.mk u)).inverse.comp (CategoryTheory.CostructuredArrow.proj (CategoryTheory.CostructuredArrow.pre T S e) (CategoryTheory.CostructuredArrow.mk u))

The functor CostructuredArrow T d ⥤ CostructuredArrow (T ⋙ S) e that u : S.obj d ⟶ e induces via CostructuredArrow.map₂ can be expressed up to isomorphism by CostructuredArrow.preEquivalence and CostructuredArrow.proj.

Equations

• One or more equations did not get rendered due to their size.