The left and right unitors #
Given a bifunctor F : C ⥤ D ⥤ D, an object X : C such that F.obj X ≅ 𝟭 D and a
map p : I × J → J such that hp : ∀ (j : J), p ⟨0, j⟩ = j,
we define an isomorphism of J-graded objects for any Y : GradedObject J D.
mapBifunctorLeftUnitor F X e p hp Y : mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y.
Under similar assumptions, we also obtain a right unitor isomorphism
mapBifunctorMapObj F p X ((single₀ I).obj Y) ≅ X. Finally,
the lemma mapBifunctor_triangle promotes a triangle identity involving functors
to a triangle identity for the induced functors on graded objects.
noncomputable def
CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
(Y : CategoryTheory.GradedObject J D)
(a : I × J)
(ha : a.1 = 0)
:
((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y a ≅ Y a.2
Given F : C ⥤ D ⥤ D, X : C, e : F.obj X ≅ 𝟭 D and Y : GradedObject J D,
this is the isomorphism ((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y a ≅ Y a.2
when a : I × J is such that a.1 = 0.
Equations
- CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso F X e Y a ha = (F.mapIso (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 X a.1 ha)).app (Y a.2) ≪≫ e.app (Y a.2)
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso_hom
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
(Y : CategoryTheory.GradedObject J D)
(a : I × J)
(ha : a.1 = 0)
:
(CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso F X e Y a ha).hom = CategoryTheory.CategoryStruct.comp
((F.map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 X a.1 ha).hom).app (Y a.2)) (e.hom.app (Y a.2))
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso_inv
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
(Y : CategoryTheory.GradedObject J D)
(a : I × J)
(ha : a.1 = 0)
:
(CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso F X e Y a ha).inv = CategoryTheory.CategoryStruct.comp (e.inv.app (Y a.2))
((F.map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 X a.1 ha).inv).app (Y a.2))
noncomputable def
CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIsInitial
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(Y : CategoryTheory.GradedObject J D)
(a : I × J)
(ha : a.1 ≠ 0)
:
CategoryTheory.Limits.IsInitial
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y a)
Given F : C ⥤ D ⥤ D, X : C and Y : GradedObject J D,
((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y a is an initial object
when a : I × J is such that a.1 ≠ 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
(j : J)
:
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
Y).CofanMapObjFun
p j
Given F : C ⥤ D ⥤ D, X : C, e : F.obj X ≅ 𝟭 D, Y : GradedObject J D and
p : I × J → J such that p ⟨0, j⟩ = j for all j,
this is the (colimit) cofan which shall be used to construct the isomorphism
mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y, see mapBifunctorLeftUnitor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan_inj
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
(j : J)
:
CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩ = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j))
(e.hom.app (Y j))
theorem
CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan_inj_assoc
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
(j : J)
{Z : D}
(h : (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j).pt ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j)
⟨(0, j), ⋯⟩)
h = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j))
(CategoryTheory.CategoryStruct.comp (e.hom.app (Y j)) h)
noncomputable def
CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofanIsColimit
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
(j : J)
:
The cofan mapBifunctorLeftUnitorCofan F X e p hp Y j is a colimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_hasMap
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
:
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p
noncomputable def
CategoryTheory.GradedObject.mapBifunctorLeftUnitor
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap
p]
:
CategoryTheory.GradedObject.mapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y ≅ Y
Given F : C ⥤ D ⥤ D, X : C, e : F.obj X ≅ 𝟭 D, Y : GradedObject J D and
p : I × J → J such that p ⟨0, j⟩ = j for all j,
this is the left unitor isomorphism mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorLeftUnitor_hom_apply
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap
p]
(j : J)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯)
((CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom j) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j))
(e.hom.app (Y j))
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorLeftUnitor_hom_apply_assoc
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap
p]
(j : J)
{Z : D}
(h : Y j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯)
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom j) h) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j))
(CategoryTheory.CategoryStruct.comp (e.hom.app (Y j)) h)
theorem
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_apply
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap
p]
(j : J)
:
(CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv j = CategoryTheory.CategoryStruct.comp (e.inv.app (Y j))
(CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).inv).app (Y j))
(CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯))
theorem
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_naturality
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
{Y Y' : CategoryTheory.GradedObject J D}
(φ : Y ⟶ Y')
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap
p]
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y').HasMap
p]
:
CategoryTheory.CategoryStruct.comp φ (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv
(CategoryTheory.GradedObject.mapBifunctorMapMap F p
(CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ)
theorem
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_naturality_assoc
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
{Y Y' : CategoryTheory.GradedObject J D}
(φ : Y ⟶ Y')
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap
p]
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y').HasMap
p]
{Z : CategoryTheory.GradedObject J D}
(h : CategoryTheory.GradedObject.mapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp φ
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.mapBifunctorMapMap F p
(CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ)
h)
theorem
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_naturality
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
{Y Y' : CategoryTheory.GradedObject J D}
(φ : Y ⟶ Y')
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap
p]
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y').HasMap
p]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.mapBifunctorMapMap F p
(CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ)
(CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom φ
theorem
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_naturality_assoc
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D D))
(X : C)
(e : F.obj X ≅ CategoryTheory.Functor.id D)
[∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
{Y Y' : CategoryTheory.GradedObject J D}
(φ : Y ⟶ Y')
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap
p]
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y').HasMap
p]
{Z : CategoryTheory.GradedObject J D}
(h : Y' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.mapBifunctorMapMap F p
(CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom
(CategoryTheory.CategoryStruct.comp φ h)
noncomputable def
CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
(X : CategoryTheory.GradedObject J D)
(a : J × I)
(ha : a.2 = 0)
:
((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y) a ≅ X a.1
Given F : D ⥤ C ⥤ D, Y : C, e : F.flip.obj X ≅ 𝟭 D and X : GradedObject J D,
this is the isomorphism ((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y) a ≅ Y a.2
when a : J × I is such that a.2 = 0.
Equations
- CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso F Y e X a ha = (F.obj (X a.1)).mapIso (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 Y a.2 ha) ≪≫ e.app (X a.1)
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso_inv
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
(X : CategoryTheory.GradedObject J D)
(a : J × I)
(ha : a.2 = 0)
:
(CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso F Y e X a ha).inv = CategoryTheory.CategoryStruct.comp (e.inv.app (X a.1))
((F.obj (X a.1)).map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 Y a.2 ha).inv)
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso_hom
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
(X : CategoryTheory.GradedObject J D)
(a : J × I)
(ha : a.2 = 0)
:
(CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso F Y e X a ha).hom = CategoryTheory.CategoryStruct.comp
((F.obj (X a.1)).map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 Y a.2 ha).hom) (e.hom.app (X a.1))
noncomputable def
CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀IsInitial
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(X : CategoryTheory.GradedObject J D)
(a : J × I)
(ha : a.2 ≠ 0)
:
CategoryTheory.Limits.IsInitial
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y) a)
Given F : D ⥤ C ⥤ D, Y : C and X : GradedObject J D,
((mapBifunctor F J I).obj X).obj ((single₀ I).obj X) a is an initial when a : J × I
is such that a.2 ≠ 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : CategoryTheory.GradedObject J D)
(j : J)
:
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
((CategoryTheory.GradedObject.single₀ I).obj Y)).CofanMapObjFun
p j
Given F : D ⥤ C ⥤ D, Y : C, e : F.flip.obj Y ≅ 𝟭 D, X : GradedObject J D and
p : J × I → J such that p ⟨j, 0⟩ = j for all j,
this is the (colimit) cofan which shall be used to construct the isomorphism
mapBifunctorMapObj F p X ((single₀ I).obj Y) ≅ X, see mapBifunctorRightUnitor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan_inj
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : CategoryTheory.GradedObject J D)
(j : J)
:
CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j, 0), ⋯⟩ = CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom)
(e.hom.app (X j))
theorem
CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan_inj_assoc
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : CategoryTheory.GradedObject J D)
(j : J)
{Z : D}
(h : (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j)
⟨(j, 0), ⋯⟩)
h = CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom)
(CategoryTheory.CategoryStruct.comp (e.hom.app (X j)) h)
noncomputable def
CategoryTheory.GradedObject.mapBifunctorRightUnitorCofanIsColimit
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : CategoryTheory.GradedObject J D)
(j : J)
:
The cofan mapBifunctorRightUnitorCofan F Y e p hp X j is a colimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.GradedObject.mapBifunctorRightUnitor_hasMap
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : CategoryTheory.GradedObject J D)
:
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p
noncomputable def
CategoryTheory.GradedObject.mapBifunctorRightUnitor
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : CategoryTheory.GradedObject J D)
[(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
p]
:
CategoryTheory.GradedObject.mapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) ≅ X
Given F : D ⥤ C ⥤ D, Y : C, e : F.flip.obj Y ≅ 𝟭 D, X : GradedObject J D and
p : J × I → J such that p ⟨j, 0⟩ = j for all j,
this is the right unitor isomorphism mapBifunctorMapObj F p X ((single₀ I).obj Y) ≅ X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorRightUnitor_hom_apply
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : CategoryTheory.GradedObject J D)
[(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
p]
(j : J)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) j 0 j ⋯)
((CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom j) = CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom)
(e.hom.app (X j))
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorRightUnitor_hom_apply_assoc
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : CategoryTheory.GradedObject J D)
[(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
p]
(j : J)
{Z : D}
(h : X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) j 0 j ⋯)
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom j) h) = CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom)
(CategoryTheory.CategoryStruct.comp (e.hom.app (X j)) h)
theorem
CategoryTheory.GradedObject.mapBifunctorRightUnitor_inv_apply
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : CategoryTheory.GradedObject J D)
[(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
p]
(j : J)
:
(CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).inv j = CategoryTheory.CategoryStruct.comp (e.inv.app (X j))
(CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).inv)
(CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) j 0 j ⋯))
theorem
CategoryTheory.GradedObject.mapBifunctorRightUnitor_inv_naturality
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
{Y : C}
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X X' : CategoryTheory.GradedObject J D)
(φ : X ⟶ X')
[(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
p]
[(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
p]
:
CategoryTheory.CategoryStruct.comp φ (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).inv
(CategoryTheory.GradedObject.mapBifunctorMapMap F p φ
(CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y)))
theorem
CategoryTheory.GradedObject.mapBifunctorRightUnitor_inv_naturality_assoc
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
{Y : C}
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X X' : CategoryTheory.GradedObject J D)
(φ : X ⟶ X')
[(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
p]
[(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
p]
{Z : CategoryTheory.GradedObject J D}
(h : CategoryTheory.GradedObject.mapBifunctorMapObj F p X' ((CategoryTheory.GradedObject.single₀ I).obj Y) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp φ
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.mapBifunctorMapMap F p φ
(CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y)))
h)
theorem
CategoryTheory.GradedObject.mapBifunctorRightUnitor_naturality
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
{Y : C}
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X X' : CategoryTheory.GradedObject J D)
(φ : X ⟶ X')
[(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
p]
[(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
p]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.mapBifunctorMapMap F p φ
(CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y)))
(CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom φ
theorem
CategoryTheory.GradedObject.mapBifunctorRightUnitor_naturality_assoc
{C : Type u_1}
{D : Type u_2}
{I : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[CategoryTheory.Limits.HasInitial C]
(F : CategoryTheory.Functor D (CategoryTheory.Functor C D))
{Y : C}
(e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
[∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X X' : CategoryTheory.GradedObject J D)
(φ : X ⟶ X')
[(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
p]
[(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
p]
{Z : CategoryTheory.GradedObject J D}
(h : X' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.mapBifunctorMapMap F p φ
(CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom
(CategoryTheory.CategoryStruct.comp φ h)
structure
CategoryTheory.GradedObject.TriangleIndexData
{I₁ : Type u_1}
{I₂ : Type u_2}
{I₃ : Type u_3}
{J : Type u_4}
[Zero I₂]
(r : I₁ × I₂ × I₃ → J)
(π : I₁ × I₃ → J)
:
Type (max (max u_1 u_2) u_3)
Given two maps r : I₁ × I₂ × I₃ → J and π : I₁ × I₃ → J, this structure is the
input in the formulation of the triangle equality mapBifunctor_triangle which
relates the left and right unitor and the associator for GradedObject.mapBifunctor.
- p₁₂ : I₁ × I₂ → I₁
a map
I₁ × I₂ → I₁ - p₂₃ : I₂ × I₃ → I₃
a map
I₂ × I₃ → I₃ - h₁ : ∀ (i₁ : I₁), self.p₁₂ (i₁, 0) = i₁
- h₃ : ∀ (i₃ : I₃), self.p₂₃ (0, i₃) = i₃
Instances For
@[reducible]
def
CategoryTheory.GradedObject.TriangleIndexData.ρ₁₂
{I₁ : Type u_1}
{I₂ : Type u_2}
{I₃ : Type u_3}
{J : Type u_4}
[Zero I₂]
{r : I₁ × I₂ × I₃ → J}
{π : I₁ × I₃ → J}
(τ : CategoryTheory.GradedObject.TriangleIndexData r π)
:
The BifunctorComp₁₂IndexData r attached to a TriangleIndexData r π.
Equations
- τ.ρ₁₂ = { I₁₂ := I₁, p := τ.p₁₂, q := π, hpq := ⋯ }
Instances For
@[reducible]
def
CategoryTheory.GradedObject.TriangleIndexData.ρ₂₃
{I₁ : Type u_1}
{I₂ : Type u_2}
{I₃ : Type u_3}
{J : Type u_4}
[Zero I₂]
{r : I₁ × I₂ × I₃ → J}
{π : I₁ × I₃ → J}
(τ : CategoryTheory.GradedObject.TriangleIndexData r π)
:
The BifunctorComp₂₃IndexData r attached to a TriangleIndexData r π.
Equations
- τ.ρ₂₃ = { I₂₃ := I₃, p := τ.p₂₃, q := π, hpq := ⋯ }
Instances For
theorem
CategoryTheory.GradedObject.mapBifunctor_triangle
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D : Type u_4}
{I₁ : Type u_5}
{I₂ : Type u_6}
{I₃ : Type u_7}
{J : Type u_8}
[CategoryTheory.Category.{u_12, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_10, u_3} C₃]
[CategoryTheory.Category.{u_9, u_4} D]
[Zero I₂]
[DecidableEq I₂]
[CategoryTheory.Limits.HasInitial C₂]
{F₁ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁)}
{F₂ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₃)}
{G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₃ D)}
(associator : CategoryTheory.bifunctorComp₁₂ F₁ G ≅ CategoryTheory.bifunctorComp₂₃ G F₂)
(X₂ : C₂)
(e₁ : F₁.flip.obj X₂ ≅ CategoryTheory.Functor.id C₁)
(e₂ : F₂.obj X₂ ≅ CategoryTheory.Functor.id C₃)
[∀ (X₁ : C₁), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C₂) (F₁.obj X₁)]
[∀ (X₃ : C₃), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C₂) (F₂.flip.obj X₃)]
{r : I₁ × I₂ × I₃ → J}
{π : I₁ × I₃ → J}
(τ : CategoryTheory.GradedObject.TriangleIndexData r π)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
[(((CategoryTheory.GradedObject.mapBifunctor F₁ I₁ I₂).obj X₁).obj
((CategoryTheory.GradedObject.single₀ I₂).obj X₂)).HasMap
τ.p₁₂]
[(((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁ τ.p₁₂ X₁
((CategoryTheory.GradedObject.single₀ I₂).obj X₂))).obj
X₃).HasMap
π]
[(((CategoryTheory.GradedObject.mapBifunctor F₂ I₂ I₃).obj ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)).obj
X₃).HasMap
τ.p₂₃]
[(((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₂ τ.p₂₃ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)
X₃)).HasMap
π]
[CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃]
[CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃]
[(((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π]
(triangle :
∀ (X₁ : C₁) (X₃ : C₃),
CategoryTheory.CategoryStruct.comp (((associator.hom.app X₁).app X₂).app X₃) ((G.obj X₁).map (e₂.hom.app X₃)) = (G.map (e₁.hom.app X₁)).app X₃)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁
((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃).hom
(CategoryTheory.GradedObject.mapBifunctorMapMap G π (CategoryTheory.CategoryStruct.id X₁)
(CategoryTheory.GradedObject.mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom) = CategoryTheory.GradedObject.mapBifunctorMapMap G π
(CategoryTheory.GradedObject.mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom (CategoryTheory.CategoryStruct.id X₃)