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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(S : D)
(T : 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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(S : D)
(T : Functor C D)
:
def
CategoryTheory.StructuredArrow.proj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(S : D)
(T : Functor C D)
:
Functor (StructuredArrow S T) C
The obvious projection functor from structured arrows.
@[simp]
theorem
CategoryTheory.StructuredArrow.proj_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(S : D)
(T : Functor C D)
(X : Comma (Functor.fromPUnit S) T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.proj_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(S : D)
(T : Functor C D)
{X✝ Y✝ : Comma (Functor.fromPUnit S) T}
(f : X✝ ⟶ Y✝)
:
theorem
CategoryTheory.StructuredArrow.hom_ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{X Y : StructuredArrow S T}
(f g : X ⟶ Y)
(h : f.right = g.right)
:
theorem
CategoryTheory.StructuredArrow.hom_ext_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{X Y : StructuredArrow S T}
{f g : X ⟶ Y}
:
@[simp]
theorem
CategoryTheory.StructuredArrow.hom_eq_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{X Y : StructuredArrow S T}
(f g : X ⟶ Y)
:
def
CategoryTheory.StructuredArrow.mk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y : C}
{T : Functor C D}
(f : S ⟶ T.obj Y)
:
StructuredArrow S T
Construct a structured arrow from a morphism.
Equations
- CategoryTheory.StructuredArrow.mk f = { left := { as := PUnit.unit }, right := Y, hom := f }
@[simp]
theorem
CategoryTheory.StructuredArrow.mk_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y : C}
{T : Functor C D}
(f : S ⟶ T.obj Y)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mk_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y : C}
{T : Functor C D}
(f : S ⟶ T.obj Y)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mk_hom_eq_self
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y : C}
{T : Functor C D}
(f : S ⟶ T.obj Y)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.w
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{A B : StructuredArrow S T}
(f : A ⟶ B)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.w_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{A B : StructuredArrow S T}
(f : A ⟶ B)
{Z : D}
(h : T.obj B.right ⟶ Z)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.comp_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{X Y Z : StructuredArrow S T}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.id_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
(X : StructuredArrow S T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.eqToHom_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{X Y : StructuredArrow S T}
(h : X = Y)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.left_eq_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{X Y : StructuredArrow S T}
(f : X ⟶ Y)
:
def
CategoryTheory.StructuredArrow.homMk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f f' : StructuredArrow S T}
(g : f.right ⟶ f'.right)
(w : CategoryStruct.comp f.hom (T.map g) = f'.hom := by aesop_cat)
:
To construct a morphism of structured arrows, we need a morphism of the objects underlying the target, and to check that the triangle commutes.
Equations
- CategoryTheory.StructuredArrow.homMk g w = { left := CategoryTheory.CategoryStruct.id f.left, right := g, w := ⋯ }
@[simp]
theorem
CategoryTheory.StructuredArrow.homMk_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f f' : StructuredArrow S T}
(g : f.right ⟶ f'.right)
(w : CategoryStruct.comp f.hom (T.map g) = f'.hom := by aesop_cat)
:
def
CategoryTheory.StructuredArrow.homMk'
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y' : C}
{T : Functor C D}
(f : StructuredArrow S T)
(g : f.right ⟶ Y')
:
Given a structured arrow X ⟶ T(Y), and an arrow Y ⟶ Y', we can construct a morphism of
structured arrows given by (X ⟶ T(Y)) ⟶ (X ⟶ T(Y) ⟶ T(Y')).
@[simp]
theorem
CategoryTheory.StructuredArrow.homMk'_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y' : C}
{T : Functor C D}
(f : StructuredArrow S T)
(g : f.right ⟶ Y')
:
@[simp]
theorem
CategoryTheory.StructuredArrow.homMk'_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y' : C}
{T : Functor C D}
(f : StructuredArrow S T)
(g : f.right ⟶ Y')
:
theorem
CategoryTheory.StructuredArrow.homMk'_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
(f : StructuredArrow S T)
:
theorem
CategoryTheory.StructuredArrow.homMk'_mk_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y : C}
{T : Functor C D}
(f : S ⟶ T.obj Y)
:
theorem
CategoryTheory.StructuredArrow.homMk'_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y' Y'' : C}
{T : Functor C D}
(f : StructuredArrow S T)
(g : f.right ⟶ Y')
(g' : Y' ⟶ Y'')
:
f.homMk' (CategoryStruct.comp g g') = CategoryStruct.comp (f.homMk' g)
(CategoryStruct.comp ((mk (CategoryStruct.comp f.hom (T.map g))).homMk' g') (eqToHom ⋯))
theorem
CategoryTheory.StructuredArrow.homMk'_mk_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y Y' Y'' : C}
{T : Functor C D}
(f : S ⟶ T.obj Y)
(g : Y ⟶ Y')
(g' : Y' ⟶ Y'')
:
(mk f).homMk' (CategoryStruct.comp g g') = CategoryStruct.comp ((mk f).homMk' g)
(CategoryStruct.comp ((mk (CategoryStruct.comp f (T.map g))).homMk' g') (eqToHom ⋯))
def
CategoryTheory.StructuredArrow.mkPostcomp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y Y' : C}
{T : 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 := ⋯ }
@[simp]
theorem
CategoryTheory.StructuredArrow.mkPostcomp_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y Y' : C}
{T : Functor C D}
(f : S ⟶ T.obj Y)
(g : Y ⟶ Y')
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mkPostcomp_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y Y' : C}
{T : Functor C D}
(f : S ⟶ T.obj Y)
(g : Y ⟶ Y')
:
theorem
CategoryTheory.StructuredArrow.mkPostcomp_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y : C}
{T : Functor C D}
(f : S ⟶ T.obj Y)
:
theorem
CategoryTheory.StructuredArrow.mkPostcomp_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{Y Y' Y'' : C}
{T : Functor C D}
(f : S ⟶ T.obj Y)
(g : Y ⟶ Y')
(g' : Y' ⟶ Y'')
:
mkPostcomp f (CategoryStruct.comp g g') = CategoryStruct.comp (mkPostcomp f g)
(CategoryStruct.comp (mkPostcomp (CategoryStruct.comp f (T.map g)) g') (eqToHom ⋯))
def
CategoryTheory.StructuredArrow.isoMk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f f' : StructuredArrow S T}
(g : f.right ≅ f'.right)
(w : CategoryStruct.comp f.hom (T.map g.hom) = f'.hom := by aesop_cat)
:
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
@[simp]
theorem
CategoryTheory.StructuredArrow.isoMk_hom_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f f' : StructuredArrow S T}
(g : f.right ≅ f'.right)
(w : CategoryStruct.comp f.hom (T.map g.hom) = f'.hom := by aesop_cat)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.isoMk_inv_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f f' : StructuredArrow S T}
(g : f.right ≅ f'.right)
(w : CategoryStruct.comp f.hom (T.map g.hom) = f'.hom := by aesop_cat)
:
theorem
CategoryTheory.StructuredArrow.obj_ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
(x y : StructuredArrow S T)
(hr : x.right = y.right)
(hh : CategoryStruct.comp x.hom (T.map (eqToHom hr)) = y.hom)
:
theorem
CategoryTheory.StructuredArrow.ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{A B : StructuredArrow S T}
(f g : A ⟶ B)
:
theorem
CategoryTheory.StructuredArrow.ext_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{A B : StructuredArrow S T}
(f g : A ⟶ B)
:
instance
CategoryTheory.StructuredArrow.proj_faithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
:
theorem
CategoryTheory.StructuredArrow.mono_of_mono_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{A B : StructuredArrow S T}
(f : A ⟶ B)
[h : Mono f.right]
:
Mono f
The converse of this is true with additional assumptions, see mono_iff_mono_right.
theorem
CategoryTheory.StructuredArrow.epi_of_epi_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{A B : StructuredArrow S T}
(f : A ⟶ B)
[h : Epi f.right]
:
Epi f
instance
CategoryTheory.StructuredArrow.mono_homMk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{A B : StructuredArrow S T}
(f : A.right ⟶ B.right)
(w : CategoryStruct.comp A.hom (T.map f) = B.hom)
[h : Mono f]
:
instance
CategoryTheory.StructuredArrow.epi_homMk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{A B : StructuredArrow S T}
(f : A.right ⟶ B.right)
(w : CategoryStruct.comp A.hom (T.map f) = B.hom)
[h : Epi f]
:
theorem
CategoryTheory.StructuredArrow.eq_mk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
(f : StructuredArrow S T)
:
Eta rule for structured arrows. Prefer StructuredArrow.eta for rewriting, since equality of
objects tends to cause problems.
def
CategoryTheory.StructuredArrow.eta
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
(f : StructuredArrow S T)
:
Eta rule for structured arrows.
Equations
@[simp]
theorem
CategoryTheory.StructuredArrow.eta_inv_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
(f : StructuredArrow S T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.eta_hom_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
(f : StructuredArrow S T)
:
def
CategoryTheory.StructuredArrow.map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(f : S ⟶ S')
:
Functor (StructuredArrow S' T) (StructuredArrow S T)
A morphism between source objects S ⟶ S'
contravariantly induces a functor between structured arrows,
StructuredArrow S' T ⥤ StructuredArrow S T.
Ideally this would be described as a 2-functor from D
(promoted to a 2-category with equations as 2-morphisms)
to Cat.
@[simp]
theorem
CategoryTheory.StructuredArrow.map_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(f : S ⟶ S')
{X✝ Y✝ : Comma (Functor.fromPUnit S') T}
(f✝ : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.map_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(f : S ⟶ S')
{X✝ Y✝ : Comma (Functor.fromPUnit S') T}
(f✝ : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.map_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(f : S ⟶ S')
(X : Comma (Functor.fromPUnit S') T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.map_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(f : S ⟶ S')
(X : Comma (Functor.fromPUnit S') T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.map_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(f : S ⟶ S')
(X : Comma (Functor.fromPUnit S') T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.map_mk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{Y : C}
{T : Functor C D}
{f : S' ⟶ T.obj Y}
(g : S ⟶ S')
:
@[simp]
theorem
CategoryTheory.StructuredArrow.map_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f : StructuredArrow S T}
:
@[simp]
theorem
CategoryTheory.StructuredArrow.map_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' S'' : D}
{T : Functor C D}
{f : S ⟶ S'}
{f' : S' ⟶ S''}
{h : StructuredArrow S'' T}
:
def
CategoryTheory.StructuredArrow.mapIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
:
An isomorphism S ≅ S' induces an equivalence StructuredArrow S T ≌ StructuredArrow S' T.
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_unitIso_inv_app_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
(X : Comma (Functor.fromPUnit S) T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_inverse_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
(X : Comma (Functor.fromPUnit S') T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_inverse_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
{X✝ Y✝ : Comma (Functor.fromPUnit S') T}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_functor_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
(X : Comma (Functor.fromPUnit S) T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_functor_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
{X✝ Y✝ : Comma (Functor.fromPUnit S) T}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_functor_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
{X✝ Y✝ : Comma (Functor.fromPUnit S) T}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_unitIso_hom_app_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
(X : Comma (Functor.fromPUnit S) T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_inverse_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
(X : Comma (Functor.fromPUnit S') T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_inverse_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
{X✝ Y✝ : Comma (Functor.fromPUnit S') T}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_counitIso_hom_app_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
(X : Comma (Functor.fromPUnit S') T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_functor_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
(X : Comma (Functor.fromPUnit S) T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_counitIso_inv_app_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
(X : Comma (Functor.fromPUnit S') T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_functor_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
(X : Comma (Functor.fromPUnit S) T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapIso_inverse_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S S' : D}
{T : Functor C D}
(i : S ≅ S')
(X : Comma (Functor.fromPUnit S') T)
:
def
CategoryTheory.StructuredArrow.mapNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
:
A natural isomorphism T ≅ T' induces an equivalence
StructuredArrow S T ≌ StructuredArrow S T'.
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_functor_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
(X : Comma (Functor.fromPUnit S) T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_functor_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
(X : Comma (Functor.fromPUnit S) T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_functor_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
{X✝ Y✝ : Comma (Functor.fromPUnit S) T}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_inverse_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
{X✝ Y✝ : Comma (Functor.fromPUnit S) T'}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_inverse_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
(X : Comma (Functor.fromPUnit S) T')
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_inverse_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
(X : Comma (Functor.fromPUnit S) T')
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_unitIso_hom_app_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
(X : Comma (Functor.fromPUnit S) T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_unitIso_inv_app_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
(X : Comma (Functor.fromPUnit S) T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_inverse_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
{X✝ Y✝ : Comma (Functor.fromPUnit S) T'}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_inverse_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
(X : Comma (Functor.fromPUnit S) T')
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_functor_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
(X : Comma (Functor.fromPUnit S) T)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_counitIso_inv_app_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
(X : Comma (Functor.fromPUnit S) T')
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_functor_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
{X✝ Y✝ : Comma (Functor.fromPUnit S) T}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.mapNatIso_counitIso_hom_app_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T T' : Functor C D}
(i : T ≅ T')
(X : Comma (Functor.fromPUnit S) T')
:
instance
CategoryTheory.StructuredArrow.proj_reflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
:
(proj S T).ReflectsIsomorphisms
noncomputable def
CategoryTheory.StructuredArrow.mkIdInitial
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{Y : C}
{T : Functor C D}
[T.Full]
[T.Faithful]
:
Limits.IsInitial (mk (CategoryStruct.id (T.obj Y)))
The identity structured arrow is initial.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.StructuredArrow.pre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : D)
(F : Functor B C)
(G : Functor C D)
:
Functor (StructuredArrow S (F.comp G)) (StructuredArrow S G)
The functor (S, F ⋙ G) ⥤ (S, G).
Equations
@[simp]
theorem
CategoryTheory.StructuredArrow.pre_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : D)
(F : Functor B C)
(G : Functor C D)
{X✝ Y✝ : Comma (Functor.fromPUnit S) (F.comp G)}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.pre_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : D)
(F : Functor B C)
(G : Functor C D)
(X : Comma (Functor.fromPUnit S) (F.comp G))
:
@[simp]
theorem
CategoryTheory.StructuredArrow.pre_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : D)
(F : Functor B C)
(G : Functor C D)
(X : Comma (Functor.fromPUnit S) (F.comp G))
:
@[simp]
theorem
CategoryTheory.StructuredArrow.pre_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : D)
(F : Functor B C)
(G : Functor C D)
{X✝ Y✝ : Comma (Functor.fromPUnit S) (F.comp G)}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.pre_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : D)
(F : Functor B C)
(G : Functor C D)
(X : Comma (Functor.fromPUnit S) (F.comp G))
:
instance
CategoryTheory.StructuredArrow.instFaithfulCompPre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : D)
(F : Functor B C)
(G : Functor C D)
[F.Faithful]
:
instance
CategoryTheory.StructuredArrow.instFullCompPre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : D)
(F : Functor B C)
(G : Functor C D)
[F.Full]
:
instance
CategoryTheory.StructuredArrow.instEssSurjCompPre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : D)
(F : Functor B C)
(G : Functor C D)
[F.EssSurj]
:
instance
CategoryTheory.StructuredArrow.isEquivalence_pre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : D)
(F : Functor B C)
(G : Functor C D)
[F.IsEquivalence]
:
(pre S F G).IsEquivalence
If F is an equivalence, then so is the functor (S, F ⋙ G) ⥤ (S, G).
def
CategoryTheory.StructuredArrow.post
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : C)
(F : Functor B C)
(G : Functor C D)
:
Functor (StructuredArrow S F) (StructuredArrow (G.obj S) (F.comp G))
The functor (S, F) ⥤ (G(S), F ⋙ G).
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.StructuredArrow.post_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : C)
(F : Functor B C)
(G : Functor C D)
{X✝ Y✝ : StructuredArrow S F}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.post_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : C)
(F : Functor B C)
(G : Functor C D)
(X : StructuredArrow S F)
:
instance
CategoryTheory.StructuredArrow.instFaithfulObjCompPost
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : C)
(F : Functor B C)
(G : Functor C D)
:
instance
CategoryTheory.StructuredArrow.instFullObjCompPostOfFaithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : C)
(F : Functor B C)
(G : Functor C D)
[G.Faithful]
:
instance
CategoryTheory.StructuredArrow.instEssSurjObjCompPostOfFull
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : C)
(F : Functor B C)
(G : Functor C D)
[G.Full]
:
instance
CategoryTheory.StructuredArrow.isEquivalence_post
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : C)
(F : Functor B C)
(G : Functor C D)
[G.Full]
[G.Faithful]
:
(post S F G).IsEquivalence
If G is fully faithful, then post S F G : (S, F) ⥤ (G(S), F ⋙ G) is an equivalence.
def
CategoryTheory.StructuredArrow.map₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{L : D}
{R : Functor C D}
{L' : B}
{R' : Functor A B}
{F : Functor C A}
{G : Functor D B}
(α : L' ⟶ G.obj L)
(β : R.comp G ⟶ F.comp R')
:
Functor (StructuredArrow L R) (StructuredArrow L' R')
The functor StructuredArrow L R ⥤ StructuredArrow L' R' that is deduced from
a natural transformation R ⋙ G ⟶ F ⋙ R' and a morphism L' ⟶ G.obj L.
Equations
@[simp]
theorem
CategoryTheory.StructuredArrow.map₂_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{L : D}
{R : Functor C D}
{L' : B}
{R' : Functor A B}
{F : Functor C A}
{G : Functor D B}
(α : L' ⟶ G.obj L)
(β : R.comp G ⟶ F.comp R')
(X : Comma (Functor.fromPUnit L) R)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.map₂_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{L : D}
{R : Functor C D}
{L' : B}
{R' : Functor A B}
{F : Functor C A}
{G : Functor D B}
(α : L' ⟶ G.obj L)
(β : R.comp G ⟶ F.comp R')
(X : Comma (Functor.fromPUnit L) R)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.map₂_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{L : D}
{R : Functor C D}
{L' : B}
{R' : Functor A B}
{F : Functor C A}
{G : Functor D B}
(α : L' ⟶ G.obj L)
(β : R.comp G ⟶ F.comp R')
(X : Comma (Functor.fromPUnit L) R)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.map₂_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{L : D}
{R : Functor C D}
{L' : B}
{R' : Functor A B}
{F : Functor C A}
{G : Functor D B}
(α : L' ⟶ G.obj L)
(β : R.comp G ⟶ F.comp R')
{X Y : Comma (Functor.fromPUnit L) R}
(φ : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.map₂_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{L : D}
{R : Functor C D}
{L' : B}
{R' : Functor A B}
{F : Functor C A}
{G : Functor D B}
(α : L' ⟶ G.obj L)
(β : R.comp G ⟶ F.comp R')
{X Y : Comma (Functor.fromPUnit L) R}
(φ : X ⟶ Y)
:
instance
CategoryTheory.StructuredArrow.faithful_map₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{L : D}
{R : Functor C D}
{L' : B}
{R' : Functor A B}
{F : Functor C A}
{G : Functor D B}
(α : L' ⟶ G.obj L)
(β : R.comp G ⟶ F.comp R')
[F.Faithful]
:
instance
CategoryTheory.StructuredArrow.full_map₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{L : D}
{R : Functor C D}
{L' : B}
{R' : Functor A B}
{F : Functor C A}
{G : Functor D B}
(α : L' ⟶ G.obj L)
(β : R.comp G ⟶ F.comp R')
[G.Faithful]
[F.Full]
[IsIso α]
[IsIso β]
:
instance
CategoryTheory.StructuredArrow.essSurj_map₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{L : D}
{R : Functor C D}
{L' : B}
{R' : Functor A B}
{F : Functor C A}
{G : Functor D B}
(α : L' ⟶ G.obj L)
(β : R.comp G ⟶ F.comp R')
[F.EssSurj]
[G.Full]
[IsIso α]
[IsIso β]
:
instance
CategoryTheory.StructuredArrow.isEquivalenceMap₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{L : D}
{R : Functor C D}
{L' : B}
{R' : Functor A B}
{F : Functor C A}
{G : Functor D B}
(α : L' ⟶ G.obj L)
(β : R.comp G ⟶ F.comp R')
[F.IsEquivalence]
[G.Faithful]
[G.Full]
[IsIso α]
[IsIso β]
:
(map₂ α β).IsEquivalence
def
CategoryTheory.StructuredArrow.map₂CompMap₂Iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{L : D}
{R : Functor C D}
{L' : B}
{R' : Functor A B}
{F : Functor C A}
{G : Functor D B}
(α : L' ⟶ G.obj L)
(β : R.comp G ⟶ F.comp R')
{C' : Type u₆}
[Category.{v₆, u₆} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{L'' : D'}
{R'' : Functor C' D'}
{F' : Functor C' C}
{G' : Functor D' D}
(α' : L ⟶ G'.obj L'')
(β' : R''.comp G' ⟶ F'.comp R)
:
(map₂ α' β').comp (map₂ α β) ≅ map₂ (CategoryStruct.comp α (G.map α'))
(CategoryStruct.comp (R''.associator G' G).inv
(CategoryStruct.comp (whiskerRight β' G)
(CategoryStruct.comp (F'.associator R G).hom
(CategoryStruct.comp (whiskerLeft F' β) (F'.associator F R').inv))))
The composition of two applications of map₂ is naturally isomorphic to a single such one.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.StructuredArrow.postIsoMap₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : C)
(F : Functor B C)
(G : Functor C D)
:
StructuredArrow.post is a special case of StructuredArrow.map₂ up to natural isomorphism.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.StructuredArrow.mapIsoMap₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Functor C D}
{S S' : D}
(f : S ⟶ S')
:
StructuredArrow.map is a special case of StructuredArrow.map₂ up to natural isomorphism.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.StructuredArrow.preIsoMap₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : D)
(F : Functor B C)
(G : Functor C D)
:
StructuredArrow.pre is a special case of StructuredArrow.map₂ up to natural isomorphism.
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev
CategoryTheory.StructuredArrow.IsUniversal
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
(f : StructuredArrow S T)
:
Type (max (max u₁ v₂) v₁)
A structured arrow is called universal if it is initial.
Equations
theorem
CategoryTheory.StructuredArrow.IsUniversal.uniq
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f g : StructuredArrow S T}
(h : f.IsUniversal)
(η : f ⟶ g)
:
def
CategoryTheory.StructuredArrow.IsUniversal.desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f : StructuredArrow S T}
(h : f.IsUniversal)
(g : StructuredArrow S T)
:
The family of morphisms out of a universal arrow.
Equations
- h.desc g = (CategoryTheory.Limits.IsInitial.to h g).right
@[simp]
theorem
CategoryTheory.StructuredArrow.IsUniversal.fac
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f : StructuredArrow S T}
(h : f.IsUniversal)
(g : StructuredArrow S T)
:
Any structured arrow factors through a universal arrow.
@[simp]
theorem
CategoryTheory.StructuredArrow.IsUniversal.fac_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f : StructuredArrow S T}
(h : f.IsUniversal)
(g : StructuredArrow S T)
{Z : D}
(h✝ : T.obj g.right ⟶ Z)
:
CategoryStruct.comp f.hom (CategoryStruct.comp (T.map (h.desc g)) h✝) = CategoryStruct.comp g.hom h✝
theorem
CategoryTheory.StructuredArrow.IsUniversal.hom_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f : StructuredArrow S T}
(h : f.IsUniversal)
{c : C}
(η : f.right ⟶ c)
:
theorem
CategoryTheory.StructuredArrow.IsUniversal.hom_ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f : StructuredArrow S T}
(h : f.IsUniversal)
{c : C}
{η η' : f.right ⟶ c}
(w : CategoryStruct.comp f.hom (T.map η) = 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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{S : D}
{T : Functor C D}
{f : StructuredArrow S T}
(h : f.IsUniversal)
(g : StructuredArrow S T)
:
def
CategoryTheory.CostructuredArrow
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(S : 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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(S : Functor C D)
(T : D)
:
def
CategoryTheory.CostructuredArrow.proj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(S : Functor C D)
(T : D)
:
Functor (CostructuredArrow S T) C
The obvious projection functor from costructured arrows.
@[simp]
theorem
CategoryTheory.CostructuredArrow.proj_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(S : Functor C D)
(T : D)
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.proj_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(S : Functor C D)
(T : D)
{X✝ Y✝ : Comma S (Functor.fromPUnit T)}
(f : X✝ ⟶ Y✝)
:
theorem
CategoryTheory.CostructuredArrow.hom_ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{X Y : CostructuredArrow S T}
(f g : X ⟶ Y)
(h : f.left = g.left)
:
theorem
CategoryTheory.CostructuredArrow.hom_ext_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{X Y : CostructuredArrow S T}
{f g : X ⟶ Y}
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.hom_eq_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{X Y : CostructuredArrow S T}
(f g : X ⟶ Y)
:
def
CategoryTheory.CostructuredArrow.mk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y : C}
{S : 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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y : C}
{S : Functor C D}
(f : S.obj Y ⟶ T)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mk_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y : C}
{S : Functor C D}
(f : S.obj Y ⟶ T)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mk_hom_eq_self
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y : C}
{S : Functor C D}
(f : S.obj Y ⟶ T)
:
theorem
CategoryTheory.CostructuredArrow.w
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A B : CostructuredArrow S T}
(f : A ⟶ B)
:
theorem
CategoryTheory.CostructuredArrow.w_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A B : CostructuredArrow S T}
(f : A ⟶ B)
{Z : D}
(h : (Functor.fromPUnit T).obj B.right ⟶ Z)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.comp_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{X Y Z : CostructuredArrow S T}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.id_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
(X : CostructuredArrow S T)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.eqToHom_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{X Y : CostructuredArrow S T}
(h : X = Y)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.right_eq_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{X Y : CostructuredArrow S T}
(f : X ⟶ Y)
:
def
CategoryTheory.CostructuredArrow.homMk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f f' : CostructuredArrow S T}
(g : f.left ⟶ f'.left)
(w : CategoryStruct.comp (S.map g) f'.hom = f.hom := by aesop_cat)
:
To construct a morphism of costructured arrows, we need a morphism of the objects underlying the source, and to check that the triangle commutes.
Equations
- CategoryTheory.CostructuredArrow.homMk g w = { left := g, right := CategoryTheory.CategoryStruct.id f.right, w := ⋯ }
@[simp]
theorem
CategoryTheory.CostructuredArrow.homMk_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f f' : CostructuredArrow S T}
(g : f.left ⟶ f'.left)
(w : CategoryStruct.comp (S.map g) f'.hom = f.hom := by aesop_cat)
:
def
CategoryTheory.CostructuredArrow.homMk'
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y' : C}
{S : Functor C D}
(f : CostructuredArrow S T)
(g : Y' ⟶ f.left)
:
Given a costructured arrow S(Y) ⟶ X, and an arrow Y' ⟶ Y', we can construct a morphism of
costructured arrows given by (S(Y) ⟶ X) ⟶ (S(Y') ⟶ S(Y) ⟶ X).
Equations
- f.homMk' g = { left := g, right := CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom)).right, w := ⋯ }
@[simp]
theorem
CategoryTheory.CostructuredArrow.homMk'_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y' : C}
{S : Functor C D}
(f : CostructuredArrow S T)
(g : Y' ⟶ f.left)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.homMk'_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y' : C}
{S : Functor C D}
(f : CostructuredArrow S T)
(g : Y' ⟶ f.left)
:
theorem
CategoryTheory.CostructuredArrow.homMk'_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
(f : CostructuredArrow S T)
:
theorem
CategoryTheory.CostructuredArrow.homMk'_mk_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y : C}
{S : Functor C D}
(f : S.obj Y ⟶ T)
:
theorem
CategoryTheory.CostructuredArrow.homMk'_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y' Y'' : C}
{S : Functor C D}
(f : CostructuredArrow S T)
(g : Y' ⟶ f.left)
(g' : Y'' ⟶ Y')
:
f.homMk' (CategoryStruct.comp g' g) = CategoryStruct.comp (eqToHom ⋯)
(CategoryStruct.comp ((mk (CategoryStruct.comp (S.map g) f.hom)).homMk' g') (f.homMk' g))
theorem
CategoryTheory.CostructuredArrow.homMk'_mk_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y Y' Y'' : C}
{S : Functor C D}
(f : S.obj Y ⟶ T)
(g : Y' ⟶ Y)
(g' : Y'' ⟶ Y')
:
(mk f).homMk' (CategoryStruct.comp g' g) = CategoryStruct.comp (eqToHom ⋯)
(CategoryStruct.comp ((mk (CategoryStruct.comp (S.map g) f)).homMk' g') ((mk f).homMk' g))
def
CategoryTheory.CostructuredArrow.mkPrecomp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y Y' : C}
{S : 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.
@[simp]
theorem
CategoryTheory.CostructuredArrow.mkPrecomp_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y Y' : C}
{S : Functor C D}
(f : S.obj Y ⟶ T)
(g : Y' ⟶ Y)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mkPrecomp_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y Y' : C}
{S : Functor C D}
(f : S.obj Y ⟶ T)
(g : Y' ⟶ Y)
:
theorem
CategoryTheory.CostructuredArrow.mkPrecomp_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y : C}
{S : Functor C D}
(f : S.obj Y ⟶ T)
:
theorem
CategoryTheory.CostructuredArrow.mkPrecomp_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{Y Y' Y'' : C}
{S : Functor C D}
(f : S.obj Y ⟶ T)
(g : Y' ⟶ Y)
(g' : Y'' ⟶ Y')
:
mkPrecomp f (CategoryStruct.comp g' g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (mkPrecomp (CategoryStruct.comp (S.map g) f) g') (mkPrecomp f g))
def
CategoryTheory.CostructuredArrow.isoMk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f f' : CostructuredArrow S T}
(g : f.left ≅ f'.left)
(w : CategoryStruct.comp (S.map g.hom) f'.hom = f.hom := by aesop_cat)
:
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
@[simp]
theorem
CategoryTheory.CostructuredArrow.isoMk_hom_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f f' : CostructuredArrow S T}
(g : f.left ≅ f'.left)
(w : CategoryStruct.comp (S.map g.hom) f'.hom = f.hom := by aesop_cat)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.isoMk_inv_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f f' : CostructuredArrow S T}
(g : f.left ≅ f'.left)
(w : CategoryStruct.comp (S.map g.hom) f'.hom = f.hom := by aesop_cat)
:
theorem
CategoryTheory.CostructuredArrow.obj_ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
(x y : CostructuredArrow S T)
(hl : x.left = y.left)
(hh : CategoryStruct.comp (S.map (eqToHom hl)) y.hom = x.hom)
:
theorem
CategoryTheory.CostructuredArrow.ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A B : CostructuredArrow S T}
(f g : A ⟶ B)
(h : f.left = g.left)
:
theorem
CategoryTheory.CostructuredArrow.ext_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A B : CostructuredArrow S T}
(f g : A ⟶ B)
:
instance
CategoryTheory.CostructuredArrow.proj_faithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
:
theorem
CategoryTheory.CostructuredArrow.mono_of_mono_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A B : CostructuredArrow S T}
(f : A ⟶ B)
[h : Mono f.left]
:
Mono f
theorem
CategoryTheory.CostructuredArrow.epi_of_epi_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A B : CostructuredArrow S T}
(f : A ⟶ B)
[h : Epi f.left]
:
Epi f
The converse of this is true with additional assumptions, see epi_iff_epi_left.
instance
CategoryTheory.CostructuredArrow.mono_homMk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A B : CostructuredArrow S T}
(f : A.left ⟶ B.left)
(w : CategoryStruct.comp (S.map f) B.hom = A.hom)
[h : Mono f]
:
instance
CategoryTheory.CostructuredArrow.epi_homMk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A B : CostructuredArrow S T}
(f : A.left ⟶ B.left)
(w : CategoryStruct.comp (S.map f) B.hom = A.hom)
[h : Epi f]
:
theorem
CategoryTheory.CostructuredArrow.eq_mk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
(f : CostructuredArrow S T)
:
Eta rule for costructured arrows. Prefer CostructuredArrow.eta for rewriting, as equality of
objects tends to cause problems.
def
CategoryTheory.CostructuredArrow.eta
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
(f : CostructuredArrow S T)
:
Eta rule for costructured arrows.
Equations
@[simp]
theorem
CategoryTheory.CostructuredArrow.eta_inv_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
(f : CostructuredArrow S T)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.eta_hom_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
(f : CostructuredArrow S T)
:
def
CategoryTheory.CostructuredArrow.map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(f : T ⟶ T')
:
Functor (CostructuredArrow S T) (CostructuredArrow S T')
A morphism between target objects T ⟶ T'
covariantly induces a functor between costructured arrows,
CostructuredArrow S T ⥤ CostructuredArrow S T'.
Ideally this would be described as a 2-functor from D
(promoted to a 2-category with equations as 2-morphisms)
to Cat.
@[simp]
theorem
CategoryTheory.CostructuredArrow.map_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(f : T ⟶ T')
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.map_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(f : T ⟶ T')
{X✝ Y✝ : Comma S (Functor.fromPUnit T)}
(f✝ : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.map_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(f : T ⟶ T')
{X✝ Y✝ : Comma S (Functor.fromPUnit T)}
(f✝ : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.map_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(f : T ⟶ T')
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.map_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(f : T ⟶ T')
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.map_mk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{Y : C}
{S : Functor C D}
{f : S.obj Y ⟶ T}
(g : T ⟶ T')
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.map_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f : CostructuredArrow S T}
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.map_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' T'' : D}
{S : Functor C D}
{f : T ⟶ T'}
{f' : T' ⟶ T''}
{h : CostructuredArrow S T}
:
def
CategoryTheory.CostructuredArrow.mapIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
:
An isomorphism T ≅ T' induces an equivalence
CostructuredArrow S T ≌ CostructuredArrow S T'.
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_counitIso_inv_app_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
(X : Comma S (Functor.fromPUnit T'))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_functor_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_inverse_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
(X : Comma S (Functor.fromPUnit T'))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_unitIso_hom_app_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_counitIso_hom_app_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
(X : Comma S (Functor.fromPUnit T'))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_functor_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
{X✝ Y✝ : Comma S (Functor.fromPUnit T)}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_inverse_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
(X : Comma S (Functor.fromPUnit T'))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_inverse_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
(X : Comma S (Functor.fromPUnit T'))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_functor_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
{X✝ Y✝ : Comma S (Functor.fromPUnit T)}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_inverse_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
{X✝ Y✝ : Comma S (Functor.fromPUnit T')}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_inverse_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
{X✝ Y✝ : Comma S (Functor.fromPUnit T')}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_functor_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_functor_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapIso_unitIso_inv_app_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T T' : D}
{S : Functor C D}
(i : T ≅ T')
(X : Comma S (Functor.fromPUnit T))
:
def
CategoryTheory.CostructuredArrow.mapNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
:
A natural isomorphism S ≅ S' induces an equivalence
CostrucutredArrow S T ≌ CostructuredArrow S' T.
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_inverse_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
(X : Comma S' (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_functor_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_counitIso_hom_app_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
(X : Comma S' (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_counitIso_inv_app_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
(X : Comma S' (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_functor_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
{X✝ Y✝ : Comma S (Functor.fromPUnit T)}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_functor_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_functor_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
{X✝ Y✝ : Comma S (Functor.fromPUnit T)}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_inverse_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
(X : Comma S' (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_inverse_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
(X : Comma S' (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_unitIso_inv_app_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_inverse_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
{X✝ Y✝ : Comma S' (Functor.fromPUnit T)}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_inverse_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
{X✝ Y✝ : Comma S' (Functor.fromPUnit T)}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_functor_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.mapNatIso_unitIso_hom_app_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S S' : Functor C D}
(i : S ≅ S')
(X : Comma S (Functor.fromPUnit T))
:
instance
CategoryTheory.CostructuredArrow.proj_reflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
:
(proj S T).ReflectsIsomorphisms
noncomputable def
CategoryTheory.CostructuredArrow.mkIdTerminal
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{Y : C}
{S : Functor C D}
[S.Full]
[S.Faithful]
:
Limits.IsTerminal (mk (CategoryStruct.id (S.obj Y)))
The identity costructured arrow is terminal.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.CostructuredArrow.pre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : D)
:
Functor (CostructuredArrow (F.comp G) S) (CostructuredArrow G S)
The functor (F ⋙ G, S) ⥤ (G, S).
Equations
@[simp]
theorem
CategoryTheory.CostructuredArrow.pre_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : D)
(X : Comma (F.comp G) (Functor.fromPUnit S))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.pre_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : D)
{X✝ Y✝ : Comma (F.comp G) (Functor.fromPUnit S)}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.pre_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : D)
(X : Comma (F.comp G) (Functor.fromPUnit S))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.pre_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : D)
(X : Comma (F.comp G) (Functor.fromPUnit S))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.pre_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : D)
{X✝ Y✝ : Comma (F.comp G) (Functor.fromPUnit S)}
(f : X✝ ⟶ Y✝)
:
instance
CategoryTheory.CostructuredArrow.instFaithfulCompPre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : D)
[F.Faithful]
:
instance
CategoryTheory.CostructuredArrow.instFullCompPre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : D)
[F.Full]
:
instance
CategoryTheory.CostructuredArrow.instEssSurjCompPre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : D)
[F.EssSurj]
:
instance
CategoryTheory.CostructuredArrow.isEquivalence_pre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : D)
[F.IsEquivalence]
:
(pre F G S).IsEquivalence
If F is an equivalence, then so is the functor (F ⋙ G, S) ⥤ (G, S).
def
CategoryTheory.CostructuredArrow.post
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : C)
:
Functor (CostructuredArrow F S) (CostructuredArrow (F.comp G) (G.obj S))
The functor (F, S) ⥤ (F ⋙ G, G(S)).
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.CostructuredArrow.post_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : C)
(X : CostructuredArrow F S)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.post_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : C)
{X✝ Y✝ : CostructuredArrow F S}
(f : X✝ ⟶ Y✝)
:
instance
CategoryTheory.CostructuredArrow.instFaithfulCompObjPost
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : C)
:
instance
CategoryTheory.CostructuredArrow.instFullCompObjPostOfFaithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : C)
[G.Faithful]
:
instance
CategoryTheory.CostructuredArrow.instEssSurjCompObjPostOfFull
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
(S : C)
[G.Full]
:
instance
CategoryTheory.CostructuredArrow.isEquivalence_post
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : C)
(F : Functor B C)
(G : Functor C D)
[G.Full]
[G.Faithful]
:
(post F G S).IsEquivalence
If G is fully faithful, then post F G S : (F, S) ⥤ (F ⋙ G, G(S)) is an equivalence.
def
CategoryTheory.CostructuredArrow.map₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{U : Functor A B}
{V : B}
{F : Functor C A}
{G : Functor D B}
(α : F.comp U ⟶ S.comp G)
(β : G.obj T ⟶ V)
:
Functor (CostructuredArrow S T) (CostructuredArrow U V)
The functor CostructuredArrow S T ⥤ CostructuredArrow U V that is deduced from
a natural transformation F ⋙ U ⟶ S ⋙ G and a morphism G.obj T ⟶ V
Equations
@[simp]
theorem
CategoryTheory.CostructuredArrow.map₂_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{U : Functor A B}
{V : B}
{F : Functor C A}
{G : Functor D B}
(α : F.comp U ⟶ S.comp G)
(β : G.obj T ⟶ V)
{X Y : Comma S (Functor.fromPUnit T)}
(φ : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.map₂_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{U : Functor A B}
{V : B}
{F : Functor C A}
{G : Functor D B}
(α : F.comp U ⟶ S.comp G)
(β : G.obj T ⟶ V)
{X Y : Comma S (Functor.fromPUnit T)}
(φ : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.map₂_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{U : Functor A B}
{V : B}
{F : Functor C A}
{G : Functor D B}
(α : F.comp U ⟶ S.comp G)
(β : G.obj T ⟶ V)
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.map₂_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{U : Functor A B}
{V : B}
{F : Functor C A}
{G : Functor D B}
(α : F.comp U ⟶ S.comp G)
(β : G.obj T ⟶ V)
(X : Comma S (Functor.fromPUnit T))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.map₂_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{U : Functor A B}
{V : B}
{F : Functor C A}
{G : Functor D B}
(α : F.comp U ⟶ S.comp G)
(β : G.obj T ⟶ V)
(X : Comma S (Functor.fromPUnit T))
:
instance
CategoryTheory.CostructuredArrow.faithful_map₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{U : Functor A B}
{V : B}
{F : Functor C A}
{G : Functor D B}
(α : F.comp U ⟶ S.comp G)
(β : G.obj T ⟶ V)
[F.Faithful]
:
instance
CategoryTheory.CostructuredArrow.full_map₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{U : Functor A B}
{V : B}
{F : Functor C A}
{G : Functor D B}
(α : F.comp U ⟶ S.comp G)
(β : G.obj T ⟶ V)
[G.Faithful]
[F.Full]
[IsIso α]
[IsIso β]
:
instance
CategoryTheory.CostructuredArrow.essSurj_map₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{U : Functor A B}
{V : B}
{F : Functor C A}
{G : Functor D B}
(α : F.comp U ⟶ S.comp G)
(β : G.obj T ⟶ V)
[F.EssSurj]
[G.Full]
[IsIso α]
[IsIso β]
:
instance
CategoryTheory.CostructuredArrow.isEquivalenceMap₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{A : Type u₃}
[Category.{v₃, u₃} A]
{B : Type u₄}
[Category.{v₄, u₄} B]
{U : Functor A B}
{V : B}
{F : Functor C A}
{G : Functor D B}
(α : F.comp U ⟶ S.comp G)
(β : G.obj T ⟶ V)
[F.IsEquivalence]
[G.Faithful]
[G.Full]
[IsIso α]
[IsIso β]
:
(map₂ α β).IsEquivalence
def
CategoryTheory.CostructuredArrow.postIsoMap₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{B : Type u₄}
[Category.{v₄, u₄} B]
(S : C)
(F : Functor B C)
(G : Functor C D)
:
CostructuredArrow.post is a special case of CostructuredArrow.map₂ up to natural
isomorphism.
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev
CategoryTheory.CostructuredArrow.IsUniversal
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
(f : CostructuredArrow S T)
:
Type (max (max u₁ v₂) v₁)
A costructured arrow is called universal if it is terminal.
Equations
theorem
CategoryTheory.CostructuredArrow.IsUniversal.uniq
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f g : CostructuredArrow S T}
(h : f.IsUniversal)
(η : g ⟶ f)
:
def
CategoryTheory.CostructuredArrow.IsUniversal.lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f : CostructuredArrow S T}
(h : f.IsUniversal)
(g : CostructuredArrow S T)
:
The family of morphisms into a universal arrow.
Equations
- h.lift g = (CategoryTheory.Limits.IsTerminal.from h g).left
@[simp]
theorem
CategoryTheory.CostructuredArrow.IsUniversal.fac
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f : CostructuredArrow S T}
(h : f.IsUniversal)
(g : CostructuredArrow S T)
:
Any costructured arrow factors through a universal arrow.
@[simp]
theorem
CategoryTheory.CostructuredArrow.IsUniversal.fac_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f : CostructuredArrow S T}
(h : f.IsUniversal)
(g : CostructuredArrow S T)
{Z : D}
(h✝ : (Functor.fromPUnit T).obj f.right ⟶ Z)
:
CategoryStruct.comp (S.map (h.lift g)) (CategoryStruct.comp f.hom h✝) = CategoryStruct.comp g.hom h✝
theorem
CategoryTheory.CostructuredArrow.IsUniversal.hom_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f : CostructuredArrow S T}
(h : f.IsUniversal)
{c : C}
(η : c ⟶ f.left)
:
theorem
CategoryTheory.CostructuredArrow.IsUniversal.hom_ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f : CostructuredArrow S T}
(h : f.IsUniversal)
{c : C}
{η η' : c ⟶ f.left}
(w : CategoryStruct.comp (S.map η) f.hom = 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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : D}
{S : Functor C D}
{f : CostructuredArrow S T}
(h : f.IsUniversal)
(g : CostructuredArrow S T)
:
def
CategoryTheory.Functor.toStructuredArrow
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor E C)
(X : D)
(F : Functor C D)
(f : (Y : E) → X ⟶ F.obj (G.obj Y))
(h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z)
:
Functor E (StructuredArrow X F)
Given X : D and F : C ⥤ D, to upgrade a functor G : E ⥤ C to a functor
E ⥤ StructuredArrow X F, it suffices to provide maps X ⟶ F.obj (G.obj Y) for all Y making
the obvious triangles involving all F.map (G.map g) commute.
This is of course the same as providing a cone over F ⋙ G with cone point X, see
Functor.toStructuredArrowIsoToStructuredArrow.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Functor.toStructuredArrow_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor E C)
(X : D)
(F : Functor C D)
(f : (Y : E) → X ⟶ F.obj (G.obj Y))
(h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z)
(Y : E)
:
@[simp]
theorem
CategoryTheory.Functor.toStructuredArrow_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor E C)
(X : D)
(F : Functor C D)
(f : (Y : E) → X ⟶ F.obj (G.obj Y))
(h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z)
{X✝ Y✝ : E}
(g : X✝ ⟶ Y✝)
:
def
CategoryTheory.Functor.toStructuredArrowCompProj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor E C)
(X : D)
(F : Functor C D)
(f : (Y : E) → X ⟶ F.obj (G.obj Y))
(h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z)
:
Upgrading a functor E ⥤ C to a functor E ⥤ StructuredArrow X F and composing with the
forgetful functor StructuredArrow X F ⥤ C recovers the original functor.
Equations
- 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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor E C)
(X : D)
(F : Functor C D)
(f : (Y : E) → X ⟶ F.obj (G.obj Y))
(h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z)
:
def
CategoryTheory.Functor.toCostructuredArrow
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor E C)
(F : Functor C D)
(X : D)
(f : (Y : E) → F.obj (G.obj Y) ⟶ X)
(h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y)
:
Functor E (CostructuredArrow F X)
Given F : C ⥤ D and X : D, to upgrade a functor G : E ⥤ C to a functor
E ⥤ CostructuredArrow F X, it suffices to provide maps F.obj (G.obj Y) ⟶ X for all Y
making the obvious triangles involving all F.map (G.map g) commute.
This is of course the same as providing a cocone over F ⋙ G with cocone point X, see
Functor.toCostructuredArrowIsoToCostructuredArrow.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Functor.toCostructuredArrow_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor E C)
(F : Functor C D)
(X : D)
(f : (Y : E) → F.obj (G.obj Y) ⟶ X)
(h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y)
{X✝ Y✝ : E}
(g : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.toCostructuredArrow_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor E C)
(F : Functor C D)
(X : D)
(f : (Y : E) → F.obj (G.obj Y) ⟶ X)
(h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y)
(Y : E)
:
def
CategoryTheory.Functor.toCostructuredArrowCompProj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor E C)
(F : Functor C D)
(X : D)
(f : (Y : E) → F.obj (G.obj Y) ⟶ X)
(h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y)
:
Upgrading a functor E ⥤ C to a functor E ⥤ CostructuredArrow F X and composing with the
forgetful functor CostructuredArrow F X ⥤ C recovers the original functor.
Equations
- 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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor E C)
(F : Functor C D)
(X : D)
(f : (Y : E) → F.obj (G.obj Y) ⟶ X)
(h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y)
:
def
CategoryTheory.StructuredArrow.toCostructuredArrow
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(d : D)
:
Functor (StructuredArrow d F)ᵒᵖ (CostructuredArrow F.op (Opposite.op d))
For a functor F : C ⥤ D and an object d : D, we obtain a contravariant functor from the
category of structured arrows d ⟶ F.obj c to the category of costructured arrows
F.op.obj c ⟶ (op d).
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.StructuredArrow.toCostructuredArrow_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(d : D)
{X✝ Y✝ : (StructuredArrow d F)ᵒᵖ}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.toCostructuredArrow_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(d : D)
(X : (StructuredArrow d F)ᵒᵖ)
:
def
CategoryTheory.StructuredArrow.toCostructuredArrow'
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(d : D)
:
Functor (StructuredArrow (Opposite.op d) F.op)ᵒᵖ (CostructuredArrow F d)
For a functor F : C ⥤ D and an object d : D, we obtain a contravariant functor from the
category of structured arrows op d ⟶ F.op.obj c to the category of costructured arrows
F.obj c ⟶ d.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.StructuredArrow.toCostructuredArrow'_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(d : D)
(X : (StructuredArrow (Opposite.op d) F.op)ᵒᵖ)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.toCostructuredArrow'_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(d : D)
{X✝ Y✝ : (StructuredArrow (Opposite.op d) F.op)ᵒᵖ}
(f : X✝ ⟶ Y✝)
:
def
CategoryTheory.CostructuredArrow.toStructuredArrow
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(d : D)
:
Functor (CostructuredArrow F d)ᵒᵖ (StructuredArrow (Opposite.op d) F.op)
For a functor F : C ⥤ D and an object d : D, we obtain a contravariant functor from the
category of costructured arrows F.obj c ⟶ d to the category of structured arrows
op d ⟶ F.op.obj c.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.CostructuredArrow.toStructuredArrow_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(d : D)
{X✝ Y✝ : (CostructuredArrow F d)ᵒᵖ}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.toStructuredArrow_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(d : D)
(X : (CostructuredArrow F d)ᵒᵖ)
:
def
CategoryTheory.CostructuredArrow.toStructuredArrow'
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(d : D)
:
Functor (CostructuredArrow F.op (Opposite.op d))ᵒᵖ (StructuredArrow d F)
For a functor F : C ⥤ D and an object d : D, we obtain a contravariant functor from the
category of costructured arrows F.op.obj c ⟶ op d to the category of structured arrows
d ⟶ F.obj c.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.CostructuredArrow.toStructuredArrow'_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(d : D)
{X✝ Y✝ : (CostructuredArrow F.op (Opposite.op d))ᵒᵖ}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.toStructuredArrow'_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(d : D)
(X : (CostructuredArrow F.op (Opposite.op d))ᵒᵖ)
:
def
CategoryTheory.structuredArrowOpEquivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : 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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : 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.
def
CategoryTheory.StructuredArrow.preEquivalenceFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
:
Functor (StructuredArrow f (pre e F G)) (StructuredArrow f.right F)
The functor establishing the equivalence StructuredArrow.preEquivalence.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalenceFunctor_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
(g : StructuredArrow f (pre e F G))
:
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalenceFunctor_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
{X✝ Y✝ : StructuredArrow f (pre e F G)}
(φ : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalenceFunctor_obj_left_as
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
(g : StructuredArrow f (pre e F G))
:
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalenceFunctor_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
(g : StructuredArrow f (pre e F G))
:
def
CategoryTheory.StructuredArrow.preEquivalenceInverse
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
:
Functor (StructuredArrow f.right F) (StructuredArrow f (pre e F G))
The inverse functor establishing the equivalence StructuredArrow.preEquivalence.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_right_left_as
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
(g : StructuredArrow f.right F)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_left_as
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
(g : StructuredArrow f.right F)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_hom_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
(g : StructuredArrow f.right F)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_right_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
(g : StructuredArrow f.right F)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_right_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
(g : StructuredArrow f.right F)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalenceInverse_map_right_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
{X✝ Y✝ : StructuredArrow f.right F}
(φ : X✝ ⟶ Y✝)
:
def
CategoryTheory.StructuredArrow.preEquivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : 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.StructuredArrow.preEquivalence_counitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
:
(preEquivalence F f).counitIso = NatIso.ofComponents
(fun (x : StructuredArrow f.right F) =>
isoMk (Iso.refl (((preEquivalenceInverse F f).comp (preEquivalenceFunctor F f)).obj x).right) ⋯)
⋯
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence_unitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
:
(preEquivalence F f).unitIso = NatIso.ofComponents
(fun (x : StructuredArrow f (pre e F G)) =>
isoMk (isoMk (Iso.refl ((Functor.id (StructuredArrow f (pre e F G))).obj x).right.right) ⋯) ⋯)
⋯
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence_functor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.preEquivalence_inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : StructuredArrow e G)
:
def
CategoryTheory.StructuredArrow.map₂IsoPreEquivalenceInverseCompProj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{T : Functor C D}
{S : Functor D E}
{T' : Functor C E}
(d : D)
(e : E)
(u : e ⟶ S.obj d)
(α : T.comp S ⟶ T')
:
The functor StructuredArrow d T ⥤ StructuredArrow e (T ⋙ S) that u : e ⟶ S.obj d
induces via StructuredArrow.map₂ can be expressed up to isomorphism by
StructuredArrow.preEquivalence and StructuredArrow.proj.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.CostructuredArrow.preEquivalence.functor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : CostructuredArrow G e)
:
Functor (CostructuredArrow (pre F G e) f) (CostructuredArrow F f.left)
The functor establishing the equivalence CostructuredArrow.preEquivalence.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.CostructuredArrow.preEquivalence.functor_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : CostructuredArrow G e)
(g : CostructuredArrow (pre F G e) f)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.preEquivalence.functor_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : CostructuredArrow G e)
(g : CostructuredArrow (pre F G e) f)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.preEquivalence.functor_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : CostructuredArrow G e)
{X✝ Y✝ : CostructuredArrow (pre F G e) f}
(φ : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.preEquivalence.functor_obj_right_as
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : CostructuredArrow G e)
(g : CostructuredArrow (pre F G e) f)
:
def
CategoryTheory.CostructuredArrow.preEquivalence.inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : CostructuredArrow G e)
:
Functor (CostructuredArrow F f.left) (CostructuredArrow (pre F G e) f)
The inverse functor establishing the equivalence CostructuredArrow.preEquivalence.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_right_as
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : CostructuredArrow G e)
(g : CostructuredArrow F f.left)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_hom_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : CostructuredArrow G e)
(g : CostructuredArrow F f.left)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_left_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : CostructuredArrow G e)
(g : CostructuredArrow F f.left)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.preEquivalence.inverse_map_left_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : CostructuredArrow G e)
{X✝ Y✝ : CostructuredArrow F f.left}
(φ : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_left_right_as
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : CostructuredArrow G e)
(g : CostructuredArrow F f.left)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_left_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : CostructuredArrow G e)
(g : CostructuredArrow F f.left)
:
def
CategoryTheory.CostructuredArrow.preEquivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
{e : E}
(f : 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.
def
CategoryTheory.CostructuredArrow.map₂IsoPreEquivalenceInverseCompProj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(T : Functor C D)
(S : Functor D E)
(d : D)
(e : E)
(u : S.obj d ⟶ e)
:
The functor CostructuredArrow T d ⥤ CostructuredArrow (T ⋙ S) e that u : S.obj d ⟶ e
induces via CostructuredArrow.map₂ can be expressed up to isomorphism by
CostructuredArrow.preEquivalence and CostructuredArrow.proj.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.StructuredArrow.w_prod_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
{X Y : StructuredArrow (S, S') (T.prod T')}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.w_prod_fst_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
{X Y : StructuredArrow (S, S') (T.prod T')}
(f : X ⟶ Y)
{Z : D}
(h : T.obj Y.right.1 ⟶ Z)
:
CategoryStruct.comp X.hom.1 (CategoryStruct.comp (T.map f.right.1) h) = CategoryStruct.comp Y.hom.1 h
@[simp]
theorem
CategoryTheory.StructuredArrow.w_prod_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
{X Y : StructuredArrow (S, S') (T.prod T')}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.w_prod_snd_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
{X Y : StructuredArrow (S, S') (T.prod T')}
(f : X ⟶ Y)
{Z : D'}
(h : T'.obj Y.right.2 ⟶ Z)
:
CategoryStruct.comp X.hom.2 (CategoryStruct.comp (T'.map f.right.2) h) = CategoryStruct.comp Y.hom.2 h
def
CategoryTheory.StructuredArrow.prodFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
:
Functor (StructuredArrow (S, S') (T.prod T')) (StructuredArrow S T × StructuredArrow S' T')
Implementation; see StructuredArrow.prodEquivalence.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.StructuredArrow.prodFunctor_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
{X✝ Y✝ : StructuredArrow (S, S') (T.prod T')}
(η : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.prodFunctor_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
(f : StructuredArrow (S, S') (T.prod T'))
:
def
CategoryTheory.StructuredArrow.prodInverse
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
:
Functor (StructuredArrow S T × StructuredArrow S' T') (StructuredArrow (S, S') (T.prod T'))
Implementation; see StructuredArrow.prodEquivalence.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.StructuredArrow.prodInverse_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
{X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'}
(η : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.StructuredArrow.prodInverse_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
(f : StructuredArrow S T × StructuredArrow S' T')
:
def
CategoryTheory.StructuredArrow.prodEquivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
:
The natural equivalence
StructuredArrow (S, S') (T.prod T') ≌ StructuredArrow S T × StructuredArrow S' T'.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.StructuredArrow.prodEquivalence_unitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
:
(prodEquivalence S S' T T').unitIso = NatIso.ofComponents
(fun (f : StructuredArrow (S, S') (T.prod T')) =>
Iso.refl ((Functor.id (StructuredArrow (S, S') (T.prod T'))).obj f))
⋯
@[simp]
theorem
CategoryTheory.StructuredArrow.prodEquivalence_functor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
:
@[simp]
theorem
CategoryTheory.StructuredArrow.prodEquivalence_inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
:
@[simp]
theorem
CategoryTheory.StructuredArrow.prodEquivalence_counitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : D)
(S' : D')
(T : Functor C D)
(T' : Functor C' D')
:
(prodEquivalence S S' T T').counitIso = NatIso.ofComponents
(fun (f : StructuredArrow S T × StructuredArrow S' T') =>
Iso.refl (((prodInverse S S' T T').comp (prodFunctor S S' T T')).obj f))
⋯
@[simp]
theorem
CategoryTheory.CostructuredArrow.w_prod_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
{A B : CostructuredArrow (S.prod S') (T, T')}
(f : A ⟶ B)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.w_prod_fst_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
{A B : CostructuredArrow (S.prod S') (T, T')}
(f : A ⟶ B)
{Z : D}
(h : ((Functor.fromPUnit (T, T')).obj B.right).1 ⟶ Z)
:
CategoryStruct.comp (S.map f.left.1) (CategoryStruct.comp B.hom.1 h) = CategoryStruct.comp A.hom.1 h
@[simp]
theorem
CategoryTheory.CostructuredArrow.w_prod_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
{A B : CostructuredArrow (S.prod S') (T, T')}
(f : A ⟶ B)
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.w_prod_snd_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
{A B : CostructuredArrow (S.prod S') (T, T')}
(f : A ⟶ B)
{Z : D'}
(h : ((Functor.fromPUnit (T, T')).obj B.right).2 ⟶ Z)
:
CategoryStruct.comp (S'.map f.left.2) (CategoryStruct.comp B.hom.2 h) = CategoryStruct.comp A.hom.2 h
def
CategoryTheory.CostructuredArrow.prodFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
:
Functor (CostructuredArrow (S.prod S') (T, T')) (CostructuredArrow S T × CostructuredArrow S' T')
Implementation; see CostructuredArrow.prodEquivalence.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.CostructuredArrow.prodFunctor_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
(f : CostructuredArrow (S.prod S') (T, T'))
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.prodFunctor_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
{X✝ Y✝ : CostructuredArrow (S.prod S') (T, T')}
(η : X✝ ⟶ Y✝)
:
def
CategoryTheory.CostructuredArrow.prodInverse
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
:
Functor (CostructuredArrow S T × CostructuredArrow S' T') (CostructuredArrow (S.prod S') (T, T'))
Implementation; see CostructuredArrow.prodEquivalence.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.CostructuredArrow.prodInverse_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
(f : CostructuredArrow S T × CostructuredArrow S' T')
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.prodInverse_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
{X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'}
(η : X✝ ⟶ Y✝)
:
def
CategoryTheory.CostructuredArrow.prodEquivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
:
The natural equivalence
CostructuredArrow (S.prod S') (T, T') ≌ CostructuredArrow S T × CostructuredArrow S' T'.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.CostructuredArrow.prodEquivalence_counitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
:
(prodEquivalence S S' T T').counitIso = NatIso.ofComponents
(fun (f : CostructuredArrow S T × CostructuredArrow S' T') =>
Iso.refl (((prodInverse S S' T T').comp (prodFunctor S S' T T')).obj f))
⋯
@[simp]
theorem
CategoryTheory.CostructuredArrow.prodEquivalence_functor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.prodEquivalence_inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
:
@[simp]
theorem
CategoryTheory.CostructuredArrow.prodEquivalence_unitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(S : Functor C D)
(S' : Functor C' D')
(T : D)
(T' : D')
:
(prodEquivalence S S' T T').unitIso = NatIso.ofComponents
(fun (f : CostructuredArrow (S.prod S') (T, T')) =>
Iso.refl ((Functor.id (CostructuredArrow (S.prod S') (T, T'))).obj f))
⋯