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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
(Y : GradedObject J D)
(a : I × J)
(ha : a.1 = 0)
:
((mapBifunctor F I J).obj ((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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
(Y : GradedObject J D)
(a : I × J)
(ha : a.1 = 0)
:
(mapBifunctorObjSingle₀ObjIso F X e Y a ha).hom = CategoryStruct.comp ((F.map (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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
(Y : GradedObject J D)
(a : I × J)
(ha : a.1 = 0)
:
(mapBifunctorObjSingle₀ObjIso F X e Y a ha).inv = CategoryStruct.comp (e.inv.app (Y a.2)) ((F.map (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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(Y : GradedObject J D)
(a : I × J)
(ha : a.1 ≠ 0)
:
Limits.IsInitial (((mapBifunctor F I J).obj ((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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : GradedObject J D)
(j : J)
:
(((mapBifunctor F I J).obj ((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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : GradedObject J D)
(j : J)
:
Limits.Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩ = CategoryStruct.comp ((F.map (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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : GradedObject J D)
(j : J)
{Z : D}
(h : (mapBifunctorLeftUnitorCofan F X e p hp Y j).pt ⟶ Z)
:
CategoryStruct.comp (Limits.Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩) h = CategoryStruct.comp ((F.map (singleObjApplyIso 0 X).hom).app (Y j)) (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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : GradedObject J D)
(j : J)
:
Limits.IsColimit (mapBifunctorLeftUnitorCofan F X e p hp Y 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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : GradedObject J D)
:
(((mapBifunctor F I J).obj ((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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : GradedObject J D)
[(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p]
:
mapBifunctorMapObj F p ((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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : GradedObject J D)
[(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p]
(j : J)
:
CategoryStruct.comp (ιMapBifunctorMapObj F p ((single₀ I).obj X) Y 0 j j ⋯)
((mapBifunctorLeftUnitor F X e p hp Y).hom j) = CategoryStruct.comp ((F.map (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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : GradedObject J D)
[(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p]
(j : J)
{Z : D}
(h : Y j ⟶ Z)
:
CategoryStruct.comp (ιMapBifunctorMapObj F p ((single₀ I).obj X) Y 0 j j ⋯)
(CategoryStruct.comp ((mapBifunctorLeftUnitor F X e p hp Y).hom j) h) = CategoryStruct.comp ((F.map (singleObjApplyIso 0 X).hom).app (Y j)) (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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
(Y : GradedObject J D)
[(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p]
(j : J)
:
(mapBifunctorLeftUnitor F X e p hp Y).inv j = CategoryStruct.comp (e.inv.app (Y j))
(CategoryStruct.comp ((F.map (singleObjApplyIso 0 X).inv).app (Y j))
(ιMapBifunctorMapObj F p ((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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
{Y Y' : GradedObject J D}
(φ : Y ⟶ Y')
[(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p]
[(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p]
:
CategoryStruct.comp φ (mapBifunctorLeftUnitor F X e p hp Y').inv = CategoryStruct.comp (mapBifunctorLeftUnitor F X e p hp Y).inv
(mapBifunctorMapMap F p (CategoryStruct.id ((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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
{Y Y' : GradedObject J D}
(φ : Y ⟶ Y')
[(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p]
[(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p]
{Z : GradedObject J D}
(h : mapBifunctorMapObj F p ((single₀ I).obj X) Y' ⟶ Z)
:
CategoryStruct.comp φ (CategoryStruct.comp (mapBifunctorLeftUnitor F X e p hp Y').inv h) = CategoryStruct.comp (mapBifunctorLeftUnitor F X e p hp Y).inv
(CategoryStruct.comp (mapBifunctorMapMap F p (CategoryStruct.id ((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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
{Y Y' : GradedObject J D}
(φ : Y ⟶ Y')
[(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p]
[(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p]
:
CategoryStruct.comp (mapBifunctorMapMap F p (CategoryStruct.id ((single₀ I).obj X)) φ)
(mapBifunctorLeftUnitor F X e p hp Y').hom = CategoryStruct.comp (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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor C (Functor D D))
(X : C)
(e : F.obj X ≅ Functor.id D)
[∀ (Y : D), Limits.PreservesColimit (Functor.empty C) (F.flip.obj Y)]
(p : I × J → J)
(hp : ∀ (j : J), p (0, j) = j)
{Y Y' : GradedObject J D}
(φ : Y ⟶ Y')
[(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p]
[(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p]
{Z : GradedObject J D}
(h : Y' ⟶ Z)
:
CategoryStruct.comp (mapBifunctorMapMap F p (CategoryStruct.id ((single₀ I).obj X)) φ)
(CategoryStruct.comp (mapBifunctorLeftUnitor F X e p hp Y').hom h) = CategoryStruct.comp (mapBifunctorLeftUnitor F X e p hp Y).hom (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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ Functor.id D)
(X : GradedObject J D)
(a : J × I)
(ha : a.2 = 0)
:
((mapBifunctor F J I).obj X).obj ((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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ Functor.id D)
(X : GradedObject J D)
(a : J × I)
(ha : a.2 = 0)
:
(mapBifunctorObjObjSingle₀Iso F Y e X a ha).inv = CategoryStruct.comp (e.inv.app (X a.1)) ((F.obj (X a.1)).map (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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ Functor.id D)
(X : GradedObject J D)
(a : J × I)
(ha : a.2 = 0)
:
(mapBifunctorObjObjSingle₀Iso F Y e X a ha).hom = CategoryStruct.comp ((F.obj (X a.1)).map (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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(X : GradedObject J D)
(a : J × I)
(ha : a.2 ≠ 0)
:
Limits.IsInitial (((mapBifunctor F J I).obj X).obj ((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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : GradedObject J D)
(j : J)
:
(((mapBifunctor F J I).obj X).obj ((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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : GradedObject J D)
(j : J)
:
Limits.Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j, 0), ⋯⟩ = CategoryStruct.comp ((F.obj (X j)).map (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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : GradedObject J D)
(j : J)
{Z : D}
(h : (mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ Z)
:
CategoryStruct.comp (Limits.Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j, 0), ⋯⟩) h = CategoryStruct.comp ((F.obj (X j)).map (singleObjApplyIso 0 Y).hom) (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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : GradedObject J D)
(j : J)
:
Limits.IsColimit (mapBifunctorRightUnitorCofan F Y e p hp X 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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : GradedObject J D)
:
(((mapBifunctor F J I).obj X).obj ((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}
[Category.{u_5, u_1} C]
[Category.{u_6, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : GradedObject J D)
[(((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p]
:
mapBifunctorMapObj F p X ((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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : GradedObject J D)
[(((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p]
(j : J)
:
CategoryStruct.comp (ιMapBifunctorMapObj F p X ((single₀ I).obj Y) j 0 j ⋯)
((mapBifunctorRightUnitor F Y e p hp X).hom j) = CategoryStruct.comp ((F.obj (X j)).map (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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : GradedObject J D)
[(((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p]
(j : J)
{Z : D}
(h : X j ⟶ Z)
:
CategoryStruct.comp (ιMapBifunctorMapObj F p X ((single₀ I).obj Y) j 0 j ⋯)
(CategoryStruct.comp ((mapBifunctorRightUnitor F Y e p hp X).hom j) h) = CategoryStruct.comp ((F.obj (X j)).map (singleObjApplyIso 0 Y).hom) (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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
(Y : C)
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X : GradedObject J D)
[(((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p]
(j : J)
:
(mapBifunctorRightUnitor F Y e p hp X).inv j = CategoryStruct.comp (e.inv.app (X j))
(CategoryStruct.comp ((F.obj (X j)).map (singleObjApplyIso 0 Y).inv)
(ιMapBifunctorMapObj F p X ((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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
{Y : C}
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X X' : GradedObject J D)
(φ : X ⟶ X')
[(((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p]
[(((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p]
:
CategoryStruct.comp φ (mapBifunctorRightUnitor F Y e p hp X').inv = CategoryStruct.comp (mapBifunctorRightUnitor F Y e p hp X).inv
(mapBifunctorMapMap F p φ (CategoryStruct.id ((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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
{Y : C}
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X X' : GradedObject J D)
(φ : X ⟶ X')
[(((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p]
[(((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p]
{Z : GradedObject J D}
(h : mapBifunctorMapObj F p X' ((single₀ I).obj Y) ⟶ Z)
:
CategoryStruct.comp φ (CategoryStruct.comp (mapBifunctorRightUnitor F Y e p hp X').inv h) = CategoryStruct.comp (mapBifunctorRightUnitor F Y e p hp X).inv
(CategoryStruct.comp (mapBifunctorMapMap F p φ (CategoryStruct.id ((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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
{Y : C}
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X X' : GradedObject J D)
(φ : X ⟶ X')
[(((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p]
[(((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p]
:
CategoryStruct.comp (mapBifunctorMapMap F p φ (CategoryStruct.id ((single₀ I).obj Y)))
(mapBifunctorRightUnitor F Y e p hp X').hom = CategoryStruct.comp (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}
[Category.{u_6, u_1} C]
[Category.{u_5, u_2} D]
[Zero I]
[DecidableEq I]
[Limits.HasInitial C]
(F : Functor D (Functor C D))
{Y : C}
(e : F.flip.obj Y ≅ Functor.id D)
[∀ (X : D), Limits.PreservesColimit (Functor.empty C) (F.obj X)]
(p : J × I → J)
(hp : ∀ (j : J), p (j, 0) = j)
(X X' : GradedObject J D)
(φ : X ⟶ X')
[(((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p]
[(((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p]
{Z : GradedObject J D}
(h : X' ⟶ Z)
:
CategoryStruct.comp (mapBifunctorMapMap F p φ (CategoryStruct.id ((single₀ I).obj Y)))
(CategoryStruct.comp (mapBifunctorRightUnitor F Y e p hp X').hom h) = CategoryStruct.comp (mapBifunctorRightUnitor F Y e p hp X).hom (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}
(τ : 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}
(τ : 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}
[Category.{u_12, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_9, u_4} D]
[Zero I₂]
[DecidableEq I₂]
[Limits.HasInitial C₂]
{F₁ : Functor C₁ (Functor C₂ C₁)}
{F₂ : Functor C₂ (Functor C₃ C₃)}
{G : Functor C₁ (Functor C₃ D)}
(associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂)
(X₂ : C₂)
(e₁ : F₁.flip.obj X₂ ≅ Functor.id C₁)
(e₂ : F₂.obj X₂ ≅ Functor.id C₃)
[∀ (X₁ : C₁), Limits.PreservesColimit (Functor.empty C₂) (F₁.obj X₁)]
[∀ (X₃ : C₃), Limits.PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)]
{r : I₁ × I₂ × I₃ → J}
{π : I₁ × I₃ → J}
(τ : TriangleIndexData r π)
(X₁ : GradedObject I₁ C₁)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂]
[(((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π]
[(((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃]
[(((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π]
[HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃]
[HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃]
[(((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π]
(triangle :
∀ (X₁ : C₁) (X₃ : C₃),
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₃)
:
CategoryStruct.comp (mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃).hom
(mapBifunctorMapMap G π (CategoryStruct.id X₁) (mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom) = mapBifunctorMapMap G π (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom (CategoryStruct.id X₃)