The action of trifunctors on graded objects #
Given a trifunctor F. C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ and types I₁, I₂ and I₃, we define a functor
GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject (I₁ × I₂ × I₃) C₄
(see mapTrifunctor). When we have a map p : I₁ × I₂ × I₃ → J and suitable coproducts
exists, we define a functor
GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject J C₄
(see mapTrifunctorMap) which sends graded objects X₁, X₂, X₃ to the graded object
which sets j to the coproduct of the objects ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃)
for p ⟨i₁, i₂, i₃⟩ = j.
This shall be used in order to construct the associator isomorphism for the monoidal
category structure on GradedObject I C induced by a monoidal structure on C and
an additive monoid structure on I (TODO @joelriou).
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorObj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_10, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(I₂ : Type u_7)
(I₃ : Type u_8)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
(x : I₁ × I₂ × I₃)
:
((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).toPrefunctor.obj X₂).toPrefunctor.obj X₃ x = ((F.toPrefunctor.obj (X₁ x.1)).toPrefunctor.obj (X₂ x.2.1)).toPrefunctor.obj (X₃ x.2.2)
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorObj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_10, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(I₂ : Type u_7)
(I₃ : Type u_8)
{X₂ : CategoryTheory.GradedObject I₂ C₂}
{Y₂ : CategoryTheory.GradedObject I₂ C₂}
(φ : X₂ ⟶ Y₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
(x : I₁ × I₂ × I₃)
:
((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).toPrefunctor.map φ).app X₃ x = ((F.toPrefunctor.obj (X₁ x.1)).toPrefunctor.map (φ x.2.1)).app (X₃ x.2.2)
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorObj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_10, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(I₂ : Type u_7)
(I₃ : Type u_8)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
{X₃ : CategoryTheory.GradedObject I₃ C₃}
{Y₃ : CategoryTheory.GradedObject I₃ C₃}
(φ : X₃ ⟶ Y₃)
(x : I₁ × I₂ × I₃)
:
((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).toPrefunctor.obj X₂).toPrefunctor.map φ x = ((F.toPrefunctor.obj (X₁ x.1)).toPrefunctor.obj (X₂ x.2.1)).toPrefunctor.map (φ x.2.2)
def
CategoryTheory.GradedObject.mapTrifunctorObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_10, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(I₂ : Type u_7)
(I₃ : Type u_8)
:
CategoryTheory.Functor (CategoryTheory.GradedObject I₂ C₂)
(CategoryTheory.Functor (CategoryTheory.GradedObject I₃ C₃) (CategoryTheory.GradedObject (I₁ × I₂ × I₃) C₄))
Auxiliary definition for mapTrifunctor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctor_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_10, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
(I₁ : Type u_6)
(I₂ : Type u_7)
(I₃ : Type u_8)
{X₁ : CategoryTheory.GradedObject I₁ C₁}
{Y₁ : CategoryTheory.GradedObject I₁ C₁}
(φ : X₁ ⟶ Y₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
(x : I₁ × I₂ × I₃)
:
(((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.map φ).app X₂).app X₃ x = ((F.toPrefunctor.map (φ x.1)).app (X₂ x.2.1)).app (X₃ x.2.2)
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctor_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_10, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
(I₁ : Type u_6)
(I₂ : Type u_7)
(I₃ : Type u_8)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
:
(CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁ = CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃
def
CategoryTheory.GradedObject.mapTrifunctor
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_10, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
(I₁ : Type u_6)
(I₂ : Type u_7)
(I₃ : Type u_8)
:
CategoryTheory.Functor (CategoryTheory.GradedObject I₁ C₁)
(CategoryTheory.Functor (CategoryTheory.GradedObject I₂ C₂)
(CategoryTheory.Functor (CategoryTheory.GradedObject I₃ C₃) (CategoryTheory.GradedObject (I₁ × I₂ × I₃) C₄)))
Given a trifunctor F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ and types I₁, I₂, I₃,
this is the obvious functor
GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject (I₁ × I₂ × I₃) C₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMapNatTrans_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_10, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
{F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
{F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
(α : F ⟶ F')
(I₁ : Type u_6)
(I₂ : Type u_7)
(I₃ : Type u_8)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
(i : I₁ × I₂ × I₃)
:
(((CategoryTheory.GradedObject.mapTrifunctorMapNatTrans α I₁ I₂ I₃).app X₁).app X₂).app X₃ i = ((α.app (X₁ i.1)).app (X₂ i.2.1)).app (X₃ i.2.2)
def
CategoryTheory.GradedObject.mapTrifunctorMapNatTrans
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_10, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
{F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
{F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
(α : F ⟶ F')
(I₁ : Type u_6)
(I₂ : Type u_7)
(I₃ : Type u_8)
:
CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃ ⟶ CategoryTheory.GradedObject.mapTrifunctor F' I₁ I₂ I₃
The natural transformation mapTrifunctor F I₁ I₂ I₃ ⟶ mapTrifunctor F' I₁ I₂ I₃
induced by a natural transformation F ⟶ F of trifunctors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMapIso_hom
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_10, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
{F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
{F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
(e : F ≅ F')
(I₁ : Type u_6)
(I₂ : Type u_7)
(I₃ : Type u_8)
:
(CategoryTheory.GradedObject.mapTrifunctorMapIso e I₁ I₂ I₃).hom = CategoryTheory.GradedObject.mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMapIso_inv
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_10, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
{F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
{F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
(e : F ≅ F')
(I₁ : Type u_6)
(I₂ : Type u_7)
(I₃ : Type u_8)
:
(CategoryTheory.GradedObject.mapTrifunctorMapIso e I₁ I₂ I₃).inv = CategoryTheory.GradedObject.mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃
def
CategoryTheory.GradedObject.mapTrifunctorMapIso
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_10, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
{F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
{F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
(e : F ≅ F')
(I₁ : Type u_6)
(I₂ : Type u_7)
(I₃ : Type u_8)
:
CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃ ≅ CategoryTheory.GradedObject.mapTrifunctor F' I₁ I₂ I₃
The natural isomorphism mapTrifunctor F I₁ I₂ I₃ ≅ mapTrifunctor F' I₁ I₂ I₃
induced by a natural isomorphism F ≅ F of trifunctors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.GradedObject.mapTrifunctorMapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
[CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
:
Given a trifunctor F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₃, graded objects X₁ : GradedObject I₁ C₁,
X₂ : GradedObject I₂ C₂, X₃ : GradedObject I₃ C₃, and a map p : I₁ × I₂ × I₃ → J,
this is the J-graded object sending j to the coproduct of
((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) for p ⟨i₁, i₂, i₃⟩ = k.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.GradedObject.ιMapTrifunctorMapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : p (i₁, i₂, i₃) = j)
[CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
:
((F.toPrefunctor.obj (X₁ i₁)).toPrefunctor.obj (X₂ i₂)).toPrefunctor.obj (X₃ i₃) ⟶ CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ j
The obvious inclusion
((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p X₁ X₂ X₃ j when
p ⟨i₁, i₂, i₃⟩ = j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.GradedObject.mapTrifunctorMapMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
{X₁ : CategoryTheory.GradedObject I₁ C₁}
{Y₁ : CategoryTheory.GradedObject I₁ C₁}
(f₁ : X₁ ⟶ Y₁)
{X₂ : CategoryTheory.GradedObject I₂ C₂}
{Y₂ : CategoryTheory.GradedObject I₂ C₂}
(f₂ : X₂ ⟶ Y₂)
{X₃ : CategoryTheory.GradedObject I₃ C₃}
{Y₃ : CategoryTheory.GradedObject I₃ C₃}
(f₃ : X₃ ⟶ Y₃)
[CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
[CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj Y₁).toPrefunctor.obj Y₂).toPrefunctor.obj
Y₃)
p]
:
CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ ⟶ CategoryTheory.GradedObject.mapTrifunctorMapObj F p Y₁ Y₂ Y₃
The maps mapTrifunctorMapObj F p X₁ X₂ X₃ ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ which
express the functoriality of mapTrifunctorMapObj, see mapTrifunctorMap
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapTrifunctorMapMap_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
{X₁ : CategoryTheory.GradedObject I₁ C₁}
{Y₁ : CategoryTheory.GradedObject I₁ C₁}
(f₁ : X₁ ⟶ Y₁)
{X₂ : CategoryTheory.GradedObject I₂ C₂}
{Y₂ : CategoryTheory.GradedObject I₂ C₂}
(f₂ : X₂ ⟶ Y₂)
{X₃ : CategoryTheory.GradedObject I₃ C₃}
{Y₃ : CategoryTheory.GradedObject I₃ C₃}
(f₃ : X₃ ⟶ Y₃)
[CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
[CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj Y₁).toPrefunctor.obj Y₂).toPrefunctor.obj
Y₃)
p]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : p (i₁, i₂, i₃) = j)
{Z : C₄}
(h : CategoryTheory.GradedObject.mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h✝)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapTrifunctorMapMap F p f₁ f₂ f₃ j) h) = CategoryTheory.CategoryStruct.comp (((F.toPrefunctor.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃))
(CategoryTheory.CategoryStruct.comp (((F.toPrefunctor.obj (Y₁ i₁)).toPrefunctor.map (f₂ i₂)).app (X₃ i₃))
(CategoryTheory.CategoryStruct.comp
(((F.toPrefunctor.obj (Y₁ i₁)).toPrefunctor.obj (Y₂ i₂)).toPrefunctor.map (f₃ i₃))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h✝) h)))
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapTrifunctorMapMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
{X₁ : CategoryTheory.GradedObject I₁ C₁}
{Y₁ : CategoryTheory.GradedObject I₁ C₁}
(f₁ : X₁ ⟶ Y₁)
{X₂ : CategoryTheory.GradedObject I₂ C₂}
{Y₂ : CategoryTheory.GradedObject I₂ C₂}
(f₂ : X₂ ⟶ Y₂)
{X₃ : CategoryTheory.GradedObject I₃ C₃}
{Y₃ : CategoryTheory.GradedObject I₃ C₃}
(f₃ : X₃ ⟶ Y₃)
[CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
[CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj Y₁).toPrefunctor.obj Y₂).toPrefunctor.obj
Y₃)
p]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : p (i₁, i₂, i₃) = j)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
(CategoryTheory.GradedObject.mapTrifunctorMapMap F p f₁ f₂ f₃ j) = CategoryTheory.CategoryStruct.comp (((F.toPrefunctor.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃))
(CategoryTheory.CategoryStruct.comp (((F.toPrefunctor.obj (Y₁ i₁)).toPrefunctor.map (f₂ i₂)).app (X₃ i₃))
(CategoryTheory.CategoryStruct.comp
(((F.toPrefunctor.obj (Y₁ i₁)).toPrefunctor.obj (Y₂ i₂)).toPrefunctor.map (f₃ i₃))
(CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)))
theorem
CategoryTheory.GradedObject.mapTrifunctorMapObj_ext
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_13, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
{X₁ : CategoryTheory.GradedObject I₁ C₁}
{X₂ : CategoryTheory.GradedObject I₂ C₂}
{X₃ : CategoryTheory.GradedObject I₃ C₃}
{Y : C₄}
(j : J)
[CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
{φ : CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y}
{φ' : CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y}
(h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) φ')
:
φ = φ'
instance
CategoryTheory.GradedObject.instHasMapProdProdObjGradedObjectToQuiverToCategoryStructCategoryOfGradedObjectsGradedObjectToQuiverToCategoryStructCategoryOfGradedObjectsToPrefunctorObjGradedObjectToQuiverToCategoryStructCategoryOfGradedObjectsFunctorToQuiverToCategoryStructCategoryToPrefunctorMapTrifunctorObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
[h : CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
:
CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).toPrefunctor.obj X₂).toPrefunctor.obj X₃) p
Equations
- (_ : CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).toPrefunctor.obj X₂).toPrefunctor.obj X₃) p) = h
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
[∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
(X₂ : CategoryTheory.GradedObject I₂ C₂)
{X₃ : CategoryTheory.GradedObject I₃ C₃}
{Y₃ : CategoryTheory.GradedObject I₃ C₃}
(φ : X₃ ⟶ Y₃)
(i : J)
:
((CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁).toPrefunctor.obj X₂).toPrefunctor.map φ i = CategoryTheory.GradedObject.mapTrifunctorMapMap F p (CategoryTheory.CategoryStruct.id X₁)
(CategoryTheory.CategoryStruct.id X₂) φ i
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
[∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
{X₂ : CategoryTheory.GradedObject I₂ C₂}
{Y₂ : CategoryTheory.GradedObject I₂ C₂}
(φ : X₂ ⟶ Y₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
(i : J)
:
((CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁).toPrefunctor.map φ).app X₃ i = CategoryTheory.GradedObject.mapTrifunctorMapMap F p (CategoryTheory.CategoryStruct.id X₁) φ
(CategoryTheory.CategoryStruct.id X₃) i
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
[∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
:
((CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁).toPrefunctor.obj X₂).toPrefunctor.obj X₃ = CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃
noncomputable def
CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
[∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
:
Given a trifunctor F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄, a map p : I₁ × I₂ × I₃ → J, and
graded objects X₁ : GradedObject I₁ C₁, X₂ : GradedObject I₂ C₂ and X₃ : GradedObject I₃ C₃,
this is the J-graded object sending j to the coproduct of
((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) for p ⟨i₁, i₂, i₃⟩ = j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMap_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
[∀ (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃),
CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
(X₁ : CategoryTheory.GradedObject I₁ C₁)
:
(CategoryTheory.GradedObject.mapTrifunctorMap F p).toPrefunctor.obj X₁ = CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMap_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
[∀ (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃),
CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
{X₁ : CategoryTheory.GradedObject I₁ C₁}
{Y₁ : CategoryTheory.GradedObject I₁ C₁}
(φ : X₁ ⟶ Y₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
(i : J)
:
(((CategoryTheory.GradedObject.mapTrifunctorMap F p).toPrefunctor.map φ).app X₂).app X₃ i = CategoryTheory.GradedObject.mapTrifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id X₂)
(CategoryTheory.CategoryStruct.id X₃) i
noncomputable def
CategoryTheory.GradedObject.mapTrifunctorMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(p : I₁ × I₂ × I₃ → J)
[∀ (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃),
CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).toPrefunctor.obj X₁).toPrefunctor.obj X₂).toPrefunctor.obj
X₃)
p]
:
Given a trifunctor F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ and a map p : I₁ × I₂ × I₃ → J,
this is the functor
GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject J C₄
sending X₁ : GradedObject I₁ C₁, X₂ : GradedObject I₂ C₂ and X₃ : GradedObject I₃ C₃
to the J-graded object sending j to the coproduct of
((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) for p ⟨i₁, i₂, i₃⟩ = j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
CategoryTheory.GradedObject.BifunctorComp₁₂IndexData
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
(r : I₁ × I₂ × I₃ → J)
:
Type (max (max (max (max (u_10 + 1) u_6) u_7) u_8) u_9)
Given a map r : I₁ × I₂ × I₃ → J, a BifunctorComp₁₂IndexData r consists of the data
of a type I₁₂, maps p : I₁ × I₂ → I₁₂ and q : I₁₂ × I₃ → J, such that r is obtained
by composition of p and q.
- I₁₂ : Type u_10
an auxiliary type
- p : I₁ × I₂ → self.I₁₂
a map
I₁ × I₂ → I₁₂ - q : self.I₁₂ × I₃ → J
a map
I₁₂ × I₃ → J
Instances For
@[inline, reducible]
abbrev
CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
[CategoryTheory.Category.{u_14, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
:
Type (max (max (max (max (max (max u_8 u_15) u_4) u_5) u_13) u_14) u_6 u_7)
Given bifunctors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂, G : C₁₂ ⥤ C₃ ⥤ C₄, graded objects
X₁ : GradedObject I₁ C₁, X₂ : GradedObject I₂ C₂, X₃ : GradedObject I₃ C₃ and
ρ₁₂ : BifunctorComp₁₂IndexData r, this asserts that for all i₁₂ : ρ₁₂.I₁₂ and i₃ : I₃,
the functor G(-, X₃ i₃) commutes wich the coproducts of the F₁₂(X₁ i₁, X₂ i₂)
such that ρ₁₂.p ⟨i₁, i₂⟩ = i₁₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
[CategoryTheory.Category.{u_14, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).toPrefunctor.obj X₁).toPrefunctor.obj X₂) ρ₁₂.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).toPrefunctor.obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).toPrefunctor.obj
X₃)
ρ₁₂.q]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
:
(G.toPrefunctor.obj ((F₁₂.toPrefunctor.obj (X₁ i₁)).toPrefunctor.obj (X₂ i₂))).toPrefunctor.obj (X₃ i₃) ⟶ CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j
The inclusion of (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) in
mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j
when r (i₁, i₂, i₃) = j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.GradedObject.cofan₃MapBifunctor₁₂BifunctorMapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
[CategoryTheory.Category.{u_14, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).toPrefunctor.obj X₁).toPrefunctor.obj X₂) ρ₁₂.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).toPrefunctor.obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).toPrefunctor.obj
X₃)
ρ₁₂.q]
(j : J)
:
CategoryTheory.GradedObject.CofanMapObjFun
((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).toPrefunctor.obj
X₁).toPrefunctor.obj
X₂).toPrefunctor.obj
X₃)
r j
The cofan consisting of the inclusions given by ιMapBifunctor₁₂BifunctorMapObj.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.GradedObject.isColimitCofan₃MapBifunctor₁₂BifunctorMapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
[CategoryTheory.Category.{u_14, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).toPrefunctor.obj X₁).toPrefunctor.obj X₂) ρ₁₂.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).toPrefunctor.obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).toPrefunctor.obj
X₃)
ρ₁₂.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
(j : J)
:
CategoryTheory.Limits.IsColimit (CategoryTheory.GradedObject.cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
The cofan cofan₃MapBifunctor₁₂BifunctorMapObj is a colimit, see the induced isomorphism
mapBifunctorComp₁₂MapObjIso.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj.hasMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_13, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_10, u_4} C₄]
[CategoryTheory.Category.{u_14, u_5} C₁₂]
{F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
{G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
{r : I₁ × I₂ × I₃ → J}
{ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r}
{X₁ : CategoryTheory.GradedObject I₁ C₁}
{X₂ : CategoryTheory.GradedObject I₂ C₂}
{X₃ : CategoryTheory.GradedObject I₃ C₃}
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).toPrefunctor.obj X₁).toPrefunctor.obj X₂) ρ₁₂.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).toPrefunctor.obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).toPrefunctor.obj
X₃)
ρ₁₂.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
:
CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).toPrefunctor.obj
X₁).toPrefunctor.obj
X₂).toPrefunctor.obj
X₃)
r
noncomputable def
CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[CategoryTheory.Category.{u_10, u_1} C₁]
[CategoryTheory.Category.{u_11, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_13, u_4} C₄]
[CategoryTheory.Category.{u_14, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_6}
{I₂ : Type u_7}
{I₃ : Type u_8}
{J : Type u_9}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).toPrefunctor.obj X₁).toPrefunctor.obj X₂) ρ₁₂.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).toPrefunctor.obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).toPrefunctor.obj
X₃)
ρ₁₂.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
[CategoryTheory.GradedObject.HasMap
((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).toPrefunctor.obj
X₁).toPrefunctor.obj
X₂).toPrefunctor.obj
X₃)
r]
:
CategoryTheory.GradedObject.mapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ ≅ CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃
The action on graded objects of a trifunctor obtained by composition of two bifunctors can be computed as a composition of the actions of these two bifunctors.
Equations
- One or more equations did not get rendered due to their size.