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
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.
theorem
CategoryTheory.StructuredArrow.hom_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}
{X : CategoryTheory.StructuredArrow S T}
{Y : CategoryTheory.StructuredArrow S T}
{f : X ⟶ Y}
{g : X ⟶ Y}
:
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 }
@[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_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
@[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
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 := ⋯ }
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 : CategoryTheory.StructuredArrow S T}
{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ψ
@[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
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 := ⋯ }
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)
:
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'')
:
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 : C}
{Y' : C}
{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 ⋯))
@[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
@[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')
:
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 := ⋯ }
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_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_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_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✝)
:
⋯ = ⋯
@[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
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
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}
:
(CategoryTheory.StructuredArrow.proj S T).Faithful
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)
:
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
@[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)
:
⋯ = ⋯
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) ⋯
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
@[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
@[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_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_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_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
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.
@[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
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'.
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
Equations
- ⋯ = ⋯
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]
:
The identity structured arrow is initial.
Equations
- One or more equations did not get rendered due to their size.
@[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_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_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_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
@[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
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
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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).
Equations
- ⋯ = ⋯
@[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)
:
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.
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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.
Equations
- ⋯ = ⋯
@[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
@[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 : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R}
{Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R}
(φ : X ⟶ Y)
:
((CategoryTheory.StructuredArrow.map₂ α β).map φ).right = F.map φ.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 : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R}
{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₂_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
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')
:
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
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
noncomputable 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
Equations
- ⋯ = ⋯
@[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 : CategoryTheory.StructuredArrow S T}
{g : CategoryTheory.StructuredArrow S T}
(h : f.IsUniversal)
(η : 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 : 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_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
@[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.
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}
{η' : 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
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.
theorem
CategoryTheory.CostructuredArrow.hom_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}
{X : CategoryTheory.CostructuredArrow S T}
{Y : CategoryTheory.CostructuredArrow S T}
{f : X ⟶ Y}
{g : X ⟶ Y}
:
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 }
@[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_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✝)
:
⋯ = ⋯
@[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
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 := ⋯ }
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 : CategoryTheory.CostructuredArrow S T}
{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ψ
@[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
@[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
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 := ⋯ }
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)
:
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')
:
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 : C}
{Y' : C}
{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))
@[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.
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_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_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_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_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
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
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}
:
(CategoryTheory.CostructuredArrow.proj S T).Faithful
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)
:
f.eta.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)
:
f.eta.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
- f.eta = CategoryTheory.CostructuredArrow.isoMk (CategoryTheory.Iso.refl 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
@[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_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_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_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_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.
@[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
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.
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
Equations
- ⋯ = ⋯
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]
:
The identity costructured arrow is terminal.
Equations
- One or more equations did not get rendered due to their size.
@[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_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
@[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_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
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
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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).
Equations
- ⋯ = ⋯
@[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)
:
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.
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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.
Equations
- ⋯ = ⋯
@[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 : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)}
{Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)}
(φ : X ⟶ Y)
:
((CategoryTheory.CostructuredArrow.map₂ α β).map φ).left = F.map φ.left
@[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₂_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 : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)}
{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_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₂_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
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)
:
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
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
noncomputable 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
Equations
- ⋯ = ⋯
@[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 : CategoryTheory.CostructuredArrow S T}
{g : CategoryTheory.CostructuredArrow S T}
(h : f.IsUniversal)
(η : 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 : 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_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
@[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.
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}
{η' : 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
@[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), (G.toStructuredArrow X F f h).map g = CategoryTheory.StructuredArrow.homMk (G.map g) ⋯
@[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)
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.
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
@[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), (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.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.
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
@[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)
:
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 (Opposite.op d) F.op)ᵒᵖ} (f : X ⟶ Y),
(CategoryTheory.StructuredArrow.toCostructuredArrow' F d).map f = CategoryTheory.CostructuredArrow.homMk f.unop.right.unop ⋯
@[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
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.
@[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 (Opposite.unop X).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.
@[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.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.
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.
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.
@[simp]
theorem
CategoryTheory.StructuredArrow.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.StructuredArrow e G)
(g : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G))
:
((CategoryTheory.StructuredArrow.preEquivalence.functor F f).obj g).hom = g.hom.right
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence.functor_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.preEquivalence.functor_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.preEquivalence.functor F f).obj g).left.as = PUnit.unit
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence.functor_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.preEquivalence.functor F f).map φ).right = φ.right.right
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence.functor_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.preEquivalence.functor F f).obj g).right = g.right.right
def
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)
:
The functor establishing the equivalence StructuredArrow.preEquivalence.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence.inverse_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.preEquivalence.inverse F f).obj g).right.hom = CategoryTheory.CategoryStruct.comp f.hom (G.map g.hom)
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence.inverse_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.preEquivalence.inverse_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.preEquivalence.inverse F f).obj g).left.as = PUnit.unit
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence.inverse_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.preEquivalence.inverse F f).obj g).hom.right = g.hom
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence.inverse_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.preEquivalence.inverse F f).map φ).right.right = φ.right
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence.inverse_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.preEquivalence.inverse_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.preEquivalence.inverse F f).obj g).right.right = g.right
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence.inverse_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.preEquivalence.inverse F f).obj g).right.left.as = PUnit.unit
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence.inverse_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), ⋯ = ⋯
def
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)
:
The inverse functor establishing the equivalence StructuredArrow.preEquivalence.
Equations
- One or more equations did not get rendered due to their size.
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)
:
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.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_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
@[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_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_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
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)
:
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.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
@[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_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_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_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_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_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_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
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)
:
The inverse functor establishing the equivalence CostructuredArrow.preEquivalence.
Equations
- One or more equations did not get rendered due to their size.
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)
:
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.