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
Instances For
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)
:
Equations
- CategoryTheory.instCategoryStructuredArrow S T = CategoryTheory.commaCategory
@[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
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)
:
The obvious projection functor from structured arrows.
Equations
Instances For
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 : CategoryTheory.StructuredArrow S T}
{Y : CategoryTheory.StructuredArrow S T}
(f : X ⟶ Y)
(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 : CategoryTheory.StructuredArrow S T}
{Y : CategoryTheory.StructuredArrow S T}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
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)
:
Construct a structured arrow from a morphism.
Equations
- CategoryTheory.StructuredArrow.mk f = { left := { as := PUnit.unit }, right := Y, hom := f }
Instances For
@[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_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 : CategoryTheory.StructuredArrow S T}
{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.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 : CategoryTheory.StructuredArrow S T}
{B : CategoryTheory.StructuredArrow S T}
(f : A ⟶ B)
:
CategoryTheory.CategoryStruct.comp A.hom (T.map f.right) = B.hom
@[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 : CategoryTheory.StructuredArrow S T}
{Y : CategoryTheory.StructuredArrow S T}
{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 : CategoryTheory.StructuredArrow S T}
{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 : CategoryTheory.StructuredArrow S T}
{Y : CategoryTheory.StructuredArrow S T}
(f : X ⟶ Y)
:
f.left = CategoryTheory.CategoryStruct.id X.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 : CategoryTheory.StructuredArrow S T}
{f' : CategoryTheory.StructuredArrow S T}
(g : f.right ⟶ f'.right)
(w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom) _auto✝)
:
(CategoryTheory.StructuredArrow.homMk g w).right = g
@[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 : CategoryTheory.StructuredArrow S T}
{f' : CategoryTheory.StructuredArrow S T}
(g : f.right ⟶ f'.right)
(w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom) _auto✝)
:
(CategoryTheory.StructuredArrow.homMk g w).left = CategoryTheory.CategoryStruct.id f.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 : CategoryTheory.StructuredArrow S T}
{f' : CategoryTheory.StructuredArrow S T}
(g : f.right ⟶ f'.right)
(w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom) _auto✝)
:
f ⟶ f'
To construct a morphism of structured arrows, we need a morphism of the objects underlying the target, and to check that the triangle commutes.
Equations
- CategoryTheory.StructuredArrow.homMk g w = { left := CategoryTheory.CategoryStruct.id f.left, right := g, w := ⋯ }
Instances For
@[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')
:
(CategoryTheory.StructuredArrow.homMk' f 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')
:
(CategoryTheory.StructuredArrow.homMk' f g).right = g
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
- CategoryTheory.StructuredArrow.homMk' f g = { left := CategoryTheory.CategoryStruct.id f.left, right := g, w := ⋯ }
Instances For
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)
:
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)
:
theorem
CategoryTheory.StructuredArrow.homMk'_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{Y' : C}
{Y'' : C}
{T : CategoryTheory.Functor C D}
(f : CategoryTheory.StructuredArrow S T)
(g : f.right ⟶ Y')
(g' : Y' ⟶ Y'')
:
CategoryTheory.StructuredArrow.homMk' f (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.homMk' f g)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.StructuredArrow.homMk'
(CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f.hom (T.map g))) 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 : C}
{Y' : C}
{Y'' : C}
{T : CategoryTheory.Functor C D}
(f : S ⟶ T.obj Y)
(g : Y ⟶ Y')
(g' : Y' ⟶ Y'')
:
CategoryTheory.StructuredArrow.homMk' (CategoryTheory.StructuredArrow.mk f) (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.homMk' (CategoryTheory.StructuredArrow.mk f) g)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.StructuredArrow.homMk'
(CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f (T.map g))) g')
(CategoryTheory.eqToHom ⋯))
@[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 : C}
{Y' : C}
{T : CategoryTheory.Functor C D}
(f : S ⟶ T.obj Y)
(g : Y ⟶ Y')
:
@[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 : C}
{Y' : C}
{T : CategoryTheory.Functor C D}
(f : S ⟶ T.obj Y)
(g : Y ⟶ Y')
:
(CategoryTheory.StructuredArrow.mkPostcomp f g).right = g
def
CategoryTheory.StructuredArrow.mkPostcomp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{Y : C}
{Y' : C}
{T : CategoryTheory.Functor C D}
(f : S ⟶ T.obj Y)
(g : Y ⟶ Y')
:
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 := ⋯ }
Instances For
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)
:
theorem
CategoryTheory.StructuredArrow.mkPostcomp_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{Y : C}
{Y' : C}
{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 ⋯))
@[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 : CategoryTheory.StructuredArrow S T}
{f' : CategoryTheory.StructuredArrow S T}
(g : f.right ≅ f'.right)
(w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom) _auto✝)
:
(CategoryTheory.StructuredArrow.isoMk g w).inv.right = g.inv
@[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 : CategoryTheory.StructuredArrow S T}
{f' : CategoryTheory.StructuredArrow S T}
(g : f.right ≅ f'.right)
(w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom) _auto✝)
:
(CategoryTheory.StructuredArrow.isoMk g w).hom.right = g.hom
@[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 : CategoryTheory.StructuredArrow S T}
{f' : CategoryTheory.StructuredArrow S T}
(g : f.right ≅ f'.right)
(w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom) _auto✝)
:
⋯ = ⋯
@[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 : CategoryTheory.StructuredArrow S T}
{f' : CategoryTheory.StructuredArrow S T}
(g : f.right ≅ f'.right)
(w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom) _auto✝)
:
⋯ = ⋯
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 : CategoryTheory.StructuredArrow S T}
{f' : CategoryTheory.StructuredArrow S T}
(g : f.right ≅ f'.right)
(w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom) _auto✝)
:
f ≅ f'
To construct an isomorphism of structured arrows, we need an isomorphism of the objects underlying the target, and to check that the triangle commutes.
Equations
Instances For
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 : CategoryTheory.StructuredArrow S T}
{B : CategoryTheory.StructuredArrow S T}
(f : A ⟶ B)
(g : A ⟶ B)
:
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 : CategoryTheory.StructuredArrow S T}
{B : CategoryTheory.StructuredArrow S T}
(f : A ⟶ B)
(g : A ⟶ B)
:
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}
:
Equations
- ⋯ = ⋯
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 : CategoryTheory.StructuredArrow S T}
{B : CategoryTheory.StructuredArrow S T}
(f : A ⟶ B)
[h : CategoryTheory.Mono f.right]
:
The converse of this is true with additional assumptions, see mono_iff_mono_right.
theorem
CategoryTheory.StructuredArrow.epi_of_epi_right
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{T : CategoryTheory.Functor C D}
{A : CategoryTheory.StructuredArrow S T}
{B : CategoryTheory.StructuredArrow S T}
(f : A ⟶ B)
[h : CategoryTheory.Epi f.right]
:
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 : CategoryTheory.StructuredArrow S T}
{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]
:
Equations
- ⋯ = ⋯
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 : CategoryTheory.StructuredArrow S T}
{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]
:
Equations
- ⋯ = ⋯
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.
@[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)
:
(CategoryTheory.StructuredArrow.eta f).inv.right = CategoryTheory.CategoryStruct.id 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_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)
:
(CategoryTheory.StructuredArrow.eta f).hom.right = CategoryTheory.CategoryStruct.id f.right
@[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)
:
⋯ = ⋯
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
Instances For
@[simp]
theorem
CategoryTheory.StructuredArrow.map_obj_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{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_left
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{S' : D}
{T : CategoryTheory.Functor C D}
(f : S ⟶ S')
:
∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T} (f_1 : X ⟶ Y),
((CategoryTheory.StructuredArrow.map f).map f_1).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]
{S : D}
{S' : D}
{T : CategoryTheory.Functor C D}
(f : S ⟶ S')
:
∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T} (f_1 : X ⟶ Y),
((CategoryTheory.StructuredArrow.map f).map f_1).right = f_1.right
@[simp]
theorem
CategoryTheory.StructuredArrow.map_obj_right
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{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_obj_left
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{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
def
CategoryTheory.StructuredArrow.map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{S' : D}
{T : CategoryTheory.Functor C D}
(f : S ⟶ S')
:
A morphism between source objects S ⟶ S'
contravariantly induces a functor between structured arrows,
StructuredArrow S' T ⥤ StructuredArrow S T.
Ideally this would be described as a 2-functor from D
(promoted to a 2-category with equations as 2-morphisms)
to Cat.
Equations
Instances For
@[simp]
theorem
CategoryTheory.StructuredArrow.map_mk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{S' : D}
{Y : C}
{T : CategoryTheory.Functor C D}
{f : S' ⟶ T.obj Y}
(g : S ⟶ S')
:
@[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}
:
@[simp]
theorem
CategoryTheory.StructuredArrow.map_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{S' : D}
{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 : D}
{S' : D}
{T : CategoryTheory.Functor C D}
(i : S ≅ S')
:
An isomorphism S ≅ S' induces an equivalence StructuredArrow S T ≌ StructuredArrow S' T.
Equations
Instances For
def
CategoryTheory.StructuredArrow.mapNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{T : CategoryTheory.Functor C D}
{T' : CategoryTheory.Functor C D}
(i : T ≅ T')
:
A natural isomorphism T ≅ T' induces an equivalence
StructuredArrow S T ≌ StructuredArrow S T'.
Equations
Instances For
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}
:
Equations
- ⋯ = ⋯
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}
[CategoryTheory.Full T]
[CategoryTheory.Faithful T]
:
The identity structured arrow is initial.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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) (CategoryTheory.Functor.comp F G))
:
((CategoryTheory.StructuredArrow.pre S F G).obj X).left = X.left
@[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) (CategoryTheory.Functor.comp F G))
:
((CategoryTheory.StructuredArrow.pre S F G).obj X).right = F.obj X.right
@[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) (CategoryTheory.Functor.comp F 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) (CategoryTheory.Functor.comp F G)} (f : X ⟶ Y),
((CategoryTheory.StructuredArrow.pre S F G).map f).left = CategoryTheory.CategoryStruct.id X.left
@[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) (CategoryTheory.Functor.comp F G)} (f : X ⟶ Y),
((CategoryTheory.StructuredArrow.pre S F G).map f).right = F.map f.right
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)
:
The functor (S, F ⋙ G) ⥤ (S, G).
Equations
Instances For
instance
CategoryTheory.StructuredArrow.instFaithfulStructuredArrowCompInstCategoryStructuredArrowStructuredArrowInstCategoryStructuredArrowPre
{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.Faithful F]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.StructuredArrow.instFullStructuredArrowCompInstCategoryStructuredArrowStructuredArrowInstCategoryStructuredArrowPre
{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.Full F]
:
Equations
- CategoryTheory.StructuredArrow.instFullStructuredArrowCompInstCategoryStructuredArrowStructuredArrowInstCategoryStructuredArrowPre S F G = let_fun this := inferInstance; this
instance
CategoryTheory.StructuredArrow.instEssSurjStructuredArrowCompStructuredArrowInstCategoryStructuredArrowInstCategoryStructuredArrowPre
{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.EssSurj F]
:
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.StructuredArrow.isEquivalencePre
{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.IsEquivalence F]
:
If F is an equivalence, then so is the functor (S, F ⋙ G) ⥤ (S, G).
Equations
Instances For
@[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 ⋯
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)
:
The functor (S, F) ⥤ (G(S), F ⋙ G).
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.StructuredArrow.instFaithfulStructuredArrowInstCategoryStructuredArrowStructuredArrowObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorCompInstCategoryStructuredArrowPost
{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)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.StructuredArrow.instFullStructuredArrowInstCategoryStructuredArrowStructuredArrowObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorCompInstCategoryStructuredArrowPost
{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.Faithful G]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.StructuredArrow.instEssSurjStructuredArrowStructuredArrowObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorCompInstCategoryStructuredArrowInstCategoryStructuredArrowPost
{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.Full G]
:
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.StructuredArrow.isEquivalencePost
{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.Full G]
[CategoryTheory.Faithful G]
:
If G is fully faithful, then post S F G : (S, F) ⥤ (G(S), F ⋙ G) is an equivalence.
Equations
Instances For
instance
CategoryTheory.StructuredArrow.small_proj_preimage_of_locallySmall
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S : D}
{T : CategoryTheory.Functor C D}
{𝒢 : Set C}
[Small.{v₁, u₁} ↑𝒢]
[CategoryTheory.LocallySmall.{v₁, v₂, u₂} D]
:
Small.{v₁, max u₁ v₂} ↑((CategoryTheory.StructuredArrow.proj S T).obj ⁻¹' 𝒢)
Equations
- ⋯ = ⋯
@[inline, reducible]
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.
Instances For
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 : CategoryTheory.StructuredArrow S T}
{g : CategoryTheory.StructuredArrow S T}
(h : CategoryTheory.StructuredArrow.IsUniversal f)
(η : f ⟶ 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 : CategoryTheory.StructuredArrow.IsUniversal f)
(g : CategoryTheory.StructuredArrow S T)
:
f.right ⟶ g.right
The family of morphisms out of a universal arrow.
Equations
Instances For
@[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 : CategoryTheory.StructuredArrow.IsUniversal f)
(g : CategoryTheory.StructuredArrow S T)
{Z : D}
(h : T.obj g.right ⟶ Z)
:
@[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 : CategoryTheory.StructuredArrow.IsUniversal f)
(g : CategoryTheory.StructuredArrow S T)
:
CategoryTheory.CategoryStruct.comp f.hom (T.map (CategoryTheory.StructuredArrow.IsUniversal.desc h g)) = g.hom
Any structured arrow factors through a universal arrow.
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 : CategoryTheory.StructuredArrow.IsUniversal f)
{c : C}
(η : f.right ⟶ c)
:
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 : CategoryTheory.StructuredArrow.IsUniversal f)
{c : C}
{η : f.right ⟶ c}
{η' : f.right ⟶ c}
(w : CategoryTheory.CategoryStruct.comp f.hom (T.map η) = CategoryTheory.CategoryStruct.comp f.hom (T.map η'))
:
η = η'
Two morphisms out of a universal T-structured arrow are equal if their image under T are
equal after precomposing the universal arrow.
theorem
CategoryTheory.StructuredArrow.IsUniversal.existsUnique
{C : Type u₁}
[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 : CategoryTheory.StructuredArrow.IsUniversal f)
(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
Instances For
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)
:
Equations
- CategoryTheory.instCategoryCostructuredArrow S T = CategoryTheory.commaCategory
@[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
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)
:
The obvious projection functor from costructured arrows.
Equations
Instances For
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 : CategoryTheory.CostructuredArrow S T}
{Y : CategoryTheory.CostructuredArrow S T}
(f : X ⟶ Y)
(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 : CategoryTheory.CostructuredArrow S T}
{Y : CategoryTheory.CostructuredArrow S T}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
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)
:
Construct a costructured arrow from a morphism.
Equations
- CategoryTheory.CostructuredArrow.mk f = { left := Y, right := { as := PUnit.unit }, hom := f }
Instances For
@[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_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 : CategoryTheory.CostructuredArrow S T}
{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
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 : CategoryTheory.CostructuredArrow S T}
{B : CategoryTheory.CostructuredArrow S T}
(f : A ⟶ B)
:
CategoryTheory.CategoryStruct.comp (S.map f.left) B.hom = A.hom
@[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 : CategoryTheory.CostructuredArrow S T}
{Y : CategoryTheory.CostructuredArrow S T}
{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 : CategoryTheory.CostructuredArrow S T}
{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 : CategoryTheory.CostructuredArrow S T}
{Y : CategoryTheory.CostructuredArrow S T}
(f : X ⟶ Y)
:
f.right = CategoryTheory.CategoryStruct.id X.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}
{S : CategoryTheory.Functor C D}
{f : CategoryTheory.CostructuredArrow S T}
{f' : CategoryTheory.CostructuredArrow S T}
(g : f.left ⟶ f'.left)
(w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom) _auto✝)
:
(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 : CategoryTheory.CostructuredArrow S T}
{f' : CategoryTheory.CostructuredArrow S T}
(g : f.left ⟶ f'.left)
(w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom) _auto✝)
:
⋯ = ⋯
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 : CategoryTheory.CostructuredArrow S T}
{f' : CategoryTheory.CostructuredArrow S T}
(g : f.left ⟶ f'.left)
(w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom) _auto✝)
:
f ⟶ f'
To construct a morphism of costructured arrows, we need a morphism of the objects underlying the source, and to check that the triangle commutes.
Equations
- CategoryTheory.CostructuredArrow.homMk g w = { left := g, right := CategoryTheory.CategoryStruct.id f.right, w := ⋯ }
Instances For
@[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)
:
(CategoryTheory.CostructuredArrow.homMk' f g).left = g
@[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)
:
(CategoryTheory.CostructuredArrow.homMk' f g).right = CategoryTheory.CategoryStruct.id
(CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom)).right
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
- One or more equations did not get rendered due to their size.
Instances For
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)
:
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)
:
theorem
CategoryTheory.CostructuredArrow.homMk'_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{T : D}
{Y' : C}
{Y'' : C}
{S : CategoryTheory.Functor C D}
(f : CategoryTheory.CostructuredArrow S T)
(g : Y' ⟶ f.left)
(g' : Y'' ⟶ Y')
:
CategoryTheory.CostructuredArrow.homMk' f (CategoryTheory.CategoryStruct.comp g' g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.CostructuredArrow.homMk'
(CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom)) g')
(CategoryTheory.CostructuredArrow.homMk' f 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 : C}
{Y' : C}
{Y'' : C}
{S : CategoryTheory.Functor C D}
(f : S.obj Y ⟶ T)
(g : Y' ⟶ Y)
(g' : Y'' ⟶ Y')
:
CategoryTheory.CostructuredArrow.homMk' (CategoryTheory.CostructuredArrow.mk f)
(CategoryTheory.CategoryStruct.comp g' g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.CostructuredArrow.homMk'
(CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f)) g')
(CategoryTheory.CostructuredArrow.homMk' (CategoryTheory.CostructuredArrow.mk f) g))
@[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 : C}
{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 : C}
{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
def
CategoryTheory.CostructuredArrow.mkPrecomp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{T : D}
{Y : C}
{Y' : C}
{S : CategoryTheory.Functor C D}
(f : S.obj Y ⟶ T)
(g : Y' ⟶ Y)
:
Variant of homMk' where both objects are applications of mk.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
theorem
CategoryTheory.CostructuredArrow.mkPrecomp_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{T : D}
{Y : C}
{Y' : C}
{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))
@[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 : CategoryTheory.CostructuredArrow S T}
{f' : CategoryTheory.CostructuredArrow S T}
(g : f.left ≅ f'.left)
(w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom) _auto✝)
:
(CategoryTheory.CostructuredArrow.isoMk g w).hom.left = g.hom
@[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 : CategoryTheory.CostructuredArrow S T}
{f' : CategoryTheory.CostructuredArrow S T}
(g : f.left ≅ f'.left)
(w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom) _auto✝)
:
(CategoryTheory.CostructuredArrow.isoMk g w).inv.left = g.inv
@[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 : CategoryTheory.CostructuredArrow S T}
{f' : CategoryTheory.CostructuredArrow S T}
(g : f.left ≅ f'.left)
(w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom) _auto✝)
:
⋯ = ⋯
@[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 : CategoryTheory.CostructuredArrow S T}
{f' : CategoryTheory.CostructuredArrow S T}
(g : f.left ≅ f'.left)
(w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom) _auto✝)
:
⋯ = ⋯
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 : CategoryTheory.CostructuredArrow S T}
{f' : CategoryTheory.CostructuredArrow S T}
(g : f.left ≅ f'.left)
(w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom) _auto✝)
:
f ≅ f'
To construct an isomorphism of costructured arrows, we need an isomorphism of the objects underlying the source, and to check that the triangle commutes.
Equations
Instances For
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 : CategoryTheory.CostructuredArrow S T}
{B : CategoryTheory.CostructuredArrow S T}
(f : A ⟶ B)
(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 : CategoryTheory.CostructuredArrow S T}
{B : CategoryTheory.CostructuredArrow S T}
(f : A ⟶ B)
(g : A ⟶ B)
:
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}
:
Equations
- ⋯ = ⋯
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 : CategoryTheory.CostructuredArrow S T}
{B : CategoryTheory.CostructuredArrow S T}
(f : A ⟶ B)
[h : CategoryTheory.Mono f.left]
:
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 : CategoryTheory.CostructuredArrow S T}
{B : CategoryTheory.CostructuredArrow S T}
(f : A ⟶ B)
[h : CategoryTheory.Epi f.left]
:
The converse of this is true with additional assumptions, see epi_iff_epi_left.
instance
CategoryTheory.CostructuredArrow.mono_homMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{T : D}
{S : CategoryTheory.Functor C D}
{A : CategoryTheory.CostructuredArrow S T}
{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]
:
Equations
- ⋯ = ⋯
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 : CategoryTheory.CostructuredArrow S T}
{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]
:
Equations
- ⋯ = ⋯
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.
@[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_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_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)
:
(CategoryTheory.CostructuredArrow.eta f).hom.left = CategoryTheory.CategoryStruct.id f.left
@[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)
:
(CategoryTheory.CostructuredArrow.eta f).inv.left = CategoryTheory.CategoryStruct.id f.left
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
Instances For
@[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}
{T' : D}
{S : CategoryTheory.Functor C D}
(f : T ⟶ T')
:
∀ {X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f_1 : X ⟶ Y),
((CategoryTheory.CostructuredArrow.map f).map f_1).left = f_1.left
@[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}
{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_left
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{T : D}
{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 : D}
{T' : D}
{S : CategoryTheory.Functor C D}
(f : T ⟶ T')
:
∀ {X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f_1 : X ⟶ Y),
((CategoryTheory.CostructuredArrow.map f).map f_1).right = CategoryTheory.CategoryStruct.id 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 : D}
{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
def
CategoryTheory.CostructuredArrow.map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{T : D}
{T' : D}
{S : CategoryTheory.Functor C D}
(f : T ⟶ T')
:
A morphism between target objects T ⟶ T'
covariantly induces a functor between costructured arrows,
CostructuredArrow S T ⥤ CostructuredArrow S T'.
Ideally this would be described as a 2-functor from D
(promoted to a 2-category with equations as 2-morphisms)
to Cat.
Equations
Instances For
@[simp]
theorem
CategoryTheory.CostructuredArrow.map_mk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{T : D}
{T' : D}
{Y : C}
{S : CategoryTheory.Functor C D}
{f : S.obj Y ⟶ T}
(g : T ⟶ T')
:
@[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}
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.map_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{T : D}
{T' : D}
{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 : D}
{T' : D}
{S : CategoryTheory.Functor C D}
(i : T ≅ T')
:
An isomorphism T ≅ T' induces an equivalence
CostructuredArrow S T ≌ CostructuredArrow S T'.
Equations
Instances For
def
CategoryTheory.CostructuredArrow.mapNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{T : D}
{S : CategoryTheory.Functor C D}
{S' : CategoryTheory.Functor C D}
(i : S ≅ S')
:
A natural isomorphism S ≅ S' induces an equivalence
CostrucutredArrow S T ≌ CostructuredArrow S' T.
Equations
Instances For
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}
:
Equations
- ⋯ = ⋯
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}
[CategoryTheory.Full S]
[CategoryTheory.Faithful S]
:
The identity costructured arrow is terminal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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 (CategoryTheory.Functor.comp F 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 (CategoryTheory.Functor.comp F 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 (CategoryTheory.Functor.comp F 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 (CategoryTheory.Functor.comp F 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 (CategoryTheory.Functor.comp F G) (CategoryTheory.Functor.fromPUnit S))
:
((CategoryTheory.CostructuredArrow.pre F G S).obj X).hom = X.hom
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)
:
The functor (F ⋙ G, S) ⥤ (G, S).
Equations
Instances For
instance
CategoryTheory.CostructuredArrow.instFaithfulCostructuredArrowCompInstCategoryCostructuredArrowCostructuredArrowInstCategoryCostructuredArrowPre
{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.Faithful F]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.CostructuredArrow.instFullCostructuredArrowCompInstCategoryCostructuredArrowCostructuredArrowInstCategoryCostructuredArrowPre
{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.Full F]
:
Equations
- CategoryTheory.CostructuredArrow.instFullCostructuredArrowCompInstCategoryCostructuredArrowCostructuredArrowInstCategoryCostructuredArrowPre F G S = let_fun this := inferInstance; this
instance
CategoryTheory.CostructuredArrow.instEssSurjCostructuredArrowCompCostructuredArrowInstCategoryCostructuredArrowInstCategoryCostructuredArrowPre
{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.EssSurj F]
:
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.CostructuredArrow.isEquivalencePre
{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.IsEquivalence F]
:
If F is an equivalence, then so is the functor (F ⋙ G, S) ⥤ (G, S).
Equations
Instances For
@[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)
@[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 ⋯
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)
:
The functor (F, S) ⥤ (F ⋙ G, G(S)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.CostructuredArrow.instFaithfulCostructuredArrowInstCategoryCostructuredArrowCostructuredArrowCompObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorInstCategoryCostructuredArrowPost
{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)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.CostructuredArrow.instFullCostructuredArrowInstCategoryCostructuredArrowCostructuredArrowCompObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorInstCategoryCostructuredArrowPost
{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.Faithful G]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.CostructuredArrow.instEssSurjCostructuredArrowCostructuredArrowCompObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorInstCategoryCostructuredArrowInstCategoryCostructuredArrowPost
{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.Full G]
:
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.CostructuredArrow.isEquivalencePost
{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.Full G]
[CategoryTheory.Faithful G]
:
If G is fully faithful, then post F G S : (F, S) ⥤ (F ⋙ G, G(S)) is an equivalence.
Equations
Instances For
instance
CategoryTheory.CostructuredArrow.small_proj_preimage_of_locallySmall
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{T : D}
{S : CategoryTheory.Functor C D}
{𝒢 : Set C}
[Small.{v₁, u₁} ↑𝒢]
[CategoryTheory.LocallySmall.{v₁, v₂, u₂} D]
:
Small.{v₁, max u₁ v₂} ↑((CategoryTheory.CostructuredArrow.proj S T).obj ⁻¹' 𝒢)
Equations
- ⋯ = ⋯
@[inline, reducible]
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.
Instances For
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 : CategoryTheory.CostructuredArrow S T}
{g : CategoryTheory.CostructuredArrow S T}
(h : CategoryTheory.CostructuredArrow.IsUniversal f)
(η : g ⟶ f)
:
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 : CategoryTheory.CostructuredArrow.IsUniversal f)
(g : CategoryTheory.CostructuredArrow S T)
:
g.left ⟶ f.left
The family of morphisms into a universal arrow.
Equations
Instances For
@[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 : CategoryTheory.CostructuredArrow.IsUniversal f)
(g : CategoryTheory.CostructuredArrow S T)
{Z : D}
(h : (CategoryTheory.Functor.fromPUnit T).obj f.right ⟶ Z)
:
@[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 : CategoryTheory.CostructuredArrow.IsUniversal f)
(g : CategoryTheory.CostructuredArrow S T)
:
CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.CostructuredArrow.IsUniversal.lift h g)) f.hom = g.hom
Any costructured arrow factors through a universal arrow.
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 : CategoryTheory.CostructuredArrow.IsUniversal f)
{c : C}
(η : c ⟶ f.left)
:
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 : CategoryTheory.CostructuredArrow.IsUniversal f)
{c : C}
{η : c ⟶ f.left}
{η' : c ⟶ f.left}
(w : CategoryTheory.CategoryStruct.comp (S.map η) f.hom = CategoryTheory.CategoryStruct.comp (S.map η') f.hom)
:
η = η'
Two morphisms into a universal S-costructured arrow are equal if their image under S are
equal after postcomposing the universal arrow.
theorem
CategoryTheory.CostructuredArrow.IsUniversal.existsUnique
{C : Type u₁}
[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 : CategoryTheory.CostructuredArrow.IsUniversal f)
(g : CategoryTheory.CostructuredArrow S T)
:
∃! (η : g.left ⟶ f.left), CategoryTheory.CategoryStruct.comp (S.map η) f.hom = g.hom
@[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)
:
(CategoryTheory.Functor.toStructuredArrow G 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_1 Y : E} (g : X_1 ⟶ Y),
(CategoryTheory.Functor.toStructuredArrow G X F f h).map g = CategoryTheory.StructuredArrow.homMk (G.map g) ⋯
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)
:
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.
Instances For
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)
:
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
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
@[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)
:
(CategoryTheory.Functor.toCostructuredArrow G F X f h).obj Y = CategoryTheory.CostructuredArrow.mk (f Y)
@[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_1 Y : E} (g : X_1 ⟶ Y),
(CategoryTheory.Functor.toCostructuredArrow G F X f h).map g = CategoryTheory.CostructuredArrow.homMk (G.map 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)
:
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.
Instances For
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)
:
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
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
@[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 X.unop.hom.op
@[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 ⋯
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)
:
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.
Instances For
@[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 X.unop.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.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)
:
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.
Instances For
@[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 ⋯
@[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 X.unop.hom.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)
:
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.
Instances For
@[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 X.unop.hom.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)
:
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.
Instances For
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)
:
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.
Instances For
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)
:
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.