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.
TODO (@joelriou): get the triangle identity.
@[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))
@[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))
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
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) ((CategoryTheory.Functor.flip F).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 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) ((CategoryTheory.Functor.flip F).obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
(j : J)
:
CategoryTheory.GradedObject.CofanMapObjFun
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) 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
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) ((CategoryTheory.Functor.flip F).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)
{ val := (0, j), property := ⋯ })
h = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j))
(CategoryTheory.CategoryStruct.comp (e.hom.app (Y j)) h)
@[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) ((CategoryTheory.Functor.flip F).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)
{ val := (0, j), property := ⋯ } = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j))
(e.hom.app (Y j))
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) ((CategoryTheory.Functor.flip F).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) ((CategoryTheory.Functor.flip F).obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
:
CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) 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) ((CategoryTheory.Functor.flip F).obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) 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_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) ((CategoryTheory.Functor.flip F).obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) 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)
@[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) ((CategoryTheory.Functor.flip F).obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) 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))
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) ((CategoryTheory.Functor.flip F).obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : CategoryTheory.GradedObject J D)
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) 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_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) ((CategoryTheory.Functor.flip F).obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
{Y : CategoryTheory.GradedObject J D}
{Y' : CategoryTheory.GradedObject J D}
(φ : Y ⟶ Y')
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y') 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_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) ((CategoryTheory.Functor.flip F).obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
{Y : CategoryTheory.GradedObject J D}
{Y' : CategoryTheory.GradedObject J D}
(φ : Y ⟶ Y')
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y') 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_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) ((CategoryTheory.Functor.flip F).obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
{Y : CategoryTheory.GradedObject J D}
{Y' : CategoryTheory.GradedObject J D}
(φ : Y ⟶ Y')
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y') 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)
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) ((CategoryTheory.Functor.flip F).obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
{Y : CategoryTheory.GradedObject J D}
{Y' : CategoryTheory.GradedObject J D}
(φ : Y ⟶ Y')
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y') 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 φ
@[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 : (CategoryTheory.Functor.flip F).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))
@[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 : (CategoryTheory.Functor.flip F).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)
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 : (CategoryTheory.Functor.flip F).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
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 : (CategoryTheory.Functor.flip F).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.CofanMapObjFun
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) 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
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 : (CategoryTheory.Functor.flip F).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)
{ val := (j, 0), property := ⋯ })
h = CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom)
(CategoryTheory.CategoryStruct.comp (e.hom.app (X j)) h)
@[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 : (CategoryTheory.Functor.flip F).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)
{ val := (j, 0), property := ⋯ } = CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom)
(e.hom.app (X j))
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 : (CategoryTheory.Functor.flip F).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 : (CategoryTheory.Functor.flip F).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.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) 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 : (CategoryTheory.Functor.flip F).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.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) 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_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 : (CategoryTheory.Functor.flip F).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.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) 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)
@[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 : (CategoryTheory.Functor.flip F).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.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) 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))
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 : (CategoryTheory.Functor.flip F).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.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) 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_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 : (CategoryTheory.Functor.flip F).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)
(X' : CategoryTheory.GradedObject J D)
(φ : X ⟶ X')
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) 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_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 : (CategoryTheory.Functor.flip F).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)
(X' : CategoryTheory.GradedObject J D)
(φ : X ⟶ X')
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) 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_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 : (CategoryTheory.Functor.flip F).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)
(X' : CategoryTheory.GradedObject J D)
(φ : X ⟶ X')
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) 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)
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 : (CategoryTheory.Functor.flip F).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)
(X' : CategoryTheory.GradedObject J D)
(φ : X ⟶ X')
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)) 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 φ