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).
def
CategoryTheory.GradedObject.mapTrifunctorObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_10, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_13, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
(X₁ : GradedObject I₁ C₁)
(I₂ : Type u_8)
(I₃ : Type u_9)
:
Functor (GradedObject I₂ C₂) (Functor (GradedObject I₃ C₃) (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.mapTrifunctorObj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_10, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_13, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
(X₁ : GradedObject I₁ C₁)
(I₂ : Type u_8)
(I₃ : Type u_9)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
(x : I₁ × I₂ × I₃)
:
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorObj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_10, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_13, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
(X₁ : GradedObject I₁ C₁)
(I₂ : Type u_8)
(I₃ : Type u_9)
(X₂ : GradedObject I₂ C₂)
{x✝ x✝¹ : GradedObject I₃ C₃}
(φ : x✝ ⟶ x✝¹)
(x : I₁ × I₂ × I₃)
:
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorObj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_10, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_13, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
(X₁ : GradedObject I₁ C₁)
(I₂ : Type u_8)
(I₃ : Type u_9)
{X₂ Y₂ : GradedObject I₂ C₂}
(φ : X₂ ⟶ Y₂)
(X₃ : GradedObject I₃ C₃)
(x : I₁ × I₂ × I₃)
:
def
CategoryTheory.GradedObject.mapTrifunctor
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_10, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_13, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
:
Functor (GradedObject I₁ C₁)
(Functor (GradedObject I₂ C₂) (Functor (GradedObject I₃ C₃) (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.mapTrifunctor_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_10, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_13, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
{X₁ Y₁ : GradedObject I₁ C₁}
(φ : X₁ ⟶ Y₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
(x : I₁ × I₂ × I₃)
:
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctor_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_10, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_13, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
(X₁ : GradedObject I₁ C₁)
:
def
CategoryTheory.GradedObject.mapTrifunctorMapNatTrans
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_10, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_13, u_4} C₄]
{F F' : Functor C₁ (Functor C₂ (Functor C₃ C₄))}
(α : F ⟶ F')
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
:
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.mapTrifunctorMapNatTrans_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_10, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_13, u_4} C₄]
{F F' : Functor C₁ (Functor C₂ (Functor C₃ C₄))}
(α : F ⟶ F')
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(x✝ : GradedObject I₃ C₃)
(x✝¹ : I₁ × I₂ × I₃)
:
def
CategoryTheory.GradedObject.mapTrifunctorMapIso
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_10, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_13, u_4} C₄]
{F F' : Functor C₁ (Functor C₂ (Functor C₃ C₄))}
(e : F ≅ F')
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
:
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
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMapIso_inv
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_10, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_13, u_4} C₄]
{F F' : Functor C₁ (Functor C₂ (Functor C₃ C₄))}
(e : F ≅ F')
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
:
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMapIso_hom
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_10, u_1} C₁]
[Category.{u_11, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_13, u_4} C₄]
{F F' : Functor C₁ (Functor C₂ (Functor C₃ C₄))}
(e : F ≅ F')
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
:
noncomputable def
CategoryTheory.GradedObject.mapTrifunctorMapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
:
GradedObject J C₄
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
- CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ = ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).mapObj p
Instances For
noncomputable def
CategoryTheory.GradedObject.ιMapTrifunctorMapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : p (i₁, i₂, i₃) = j)
[((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
:
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
Instances For
noncomputable def
CategoryTheory.GradedObject.mapTrifunctorMapMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
{X₁ Y₁ : GradedObject I₁ C₁}
(f₁ : X₁ ⟶ Y₁)
{X₂ Y₂ : GradedObject I₂ C₂}
(f₂ : X₂ ⟶ Y₂)
{X₃ Y₃ : GradedObject I₃ C₃}
(f₃ : X₃ ⟶ Y₃)
[((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
[((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p]
:
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
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
{X₁ Y₁ : GradedObject I₁ C₁}
(f₁ : X₁ ⟶ Y₁)
{X₂ Y₂ : GradedObject I₂ C₂}
(f₂ : X₂ ⟶ Y₂)
{X₃ Y₃ : GradedObject I₃ C₃}
(f₃ : X₃ ⟶ Y₃)
[((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
[((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : p (i₁, i₂, i₃) = j)
:
CategoryStruct.comp (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) (mapTrifunctorMapMap F p f₁ f₂ f₃ j) = CategoryStruct.comp (((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃))
(CategoryStruct.comp (((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃))
(CategoryStruct.comp (((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃))
(ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)))
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapTrifunctorMapMap_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
{X₁ Y₁ : GradedObject I₁ C₁}
(f₁ : X₁ ⟶ Y₁)
{X₂ Y₂ : GradedObject I₂ C₂}
(f₂ : X₂ ⟶ Y₂)
{X₃ Y₃ : GradedObject I₃ C₃}
(f₃ : X₃ ⟶ Y₃)
[((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
[((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : p (i₁, i₂, i₃) = j)
{Z : C₄}
(h✝ : mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j ⟶ Z)
:
CategoryStruct.comp (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
(CategoryStruct.comp (mapTrifunctorMapMap F p f₁ f₂ f₃ j) h✝) = CategoryStruct.comp (((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃))
(CategoryStruct.comp (((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃))
(CategoryStruct.comp (((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃))
(CategoryStruct.comp (ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h) h✝)))
theorem
CategoryTheory.GradedObject.mapTrifunctorMapObj_ext
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_14, u_1} C₁]
[Category.{u_13, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
{Y : C₄}
(j : J)
[((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
{φ φ' : mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y}
(h :
∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
CategoryStruct.comp (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) φ = CategoryStruct.comp (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) φ')
:
theorem
CategoryTheory.GradedObject.mapTrifunctorMapObj_ext_iff
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_14, u_1} C₁]
[Category.{u_13, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
{F : Functor C₁ (Functor C₂ (Functor C₃ C₄))}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{p : I₁ × I₂ × I₃ → J}
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
{Y : C₄}
{j : J}
[((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
{φ φ' : mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y}
:
φ = φ' ↔ ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
CategoryStruct.comp (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) φ = CategoryStruct.comp (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) φ'
instance
CategoryTheory.GradedObject.instHasMapProdObjFunctorMapTrifunctorObjOfMapTrifunctor
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_14, u_1} C₁]
[Category.{u_13, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[h : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
:
(((mapTrifunctorObj F X₁ I₂ I₃).obj X₂).obj X₃).HasMap p
noncomputable def
CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
(X₁ : GradedObject I₁ C₁)
[∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
:
Functor (GradedObject I₂ C₂) (Functor (GradedObject I₃ C₃) (GradedObject J C₄))
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.mapTrifunctorMapFunctorObj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
(X₁ : GradedObject I₁ C₁)
[∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
:
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
(X₁ : GradedObject I₁ C₁)
[∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
{X₂ Y₂ : GradedObject I₂ C₂}
(φ : X₂ ⟶ Y₂)
(X₃ : GradedObject I₃ C₃)
(i : J)
:
((mapTrifunctorMapFunctorObj F p X₁).map φ).app X₃ i = mapTrifunctorMapMap F p (CategoryStruct.id X₁) φ (CategoryStruct.id X₃) i
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
(X₁ : GradedObject I₁ C₁)
[∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
(X₂ : GradedObject I₂ C₂)
{x✝ x✝¹ : GradedObject I₃ C₃}
(φ : x✝ ⟶ x✝¹)
(i : J)
:
((mapTrifunctorMapFunctorObj F p X₁).obj X₂).map φ i = mapTrifunctorMapMap F p (CategoryStruct.id X₁) (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}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
[∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
:
Functor (GradedObject I₁ C₁) (Functor (GradedObject I₂ C₂) (Functor (GradedObject I₃ C₃) (GradedObject J C₄)))
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
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMap_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
[∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
{X₁ Y₁ : GradedObject I₁ C₁}
(φ : X₁ ⟶ Y₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
(i : J)
:
(((mapTrifunctorMap F p).map φ).app X₂).app X₃ i = mapTrifunctorMapMap F p φ (CategoryStruct.id X₂) (CategoryStruct.id X₃) i
@[simp]
theorem
CategoryTheory.GradedObject.mapTrifunctorMap_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
(F : Functor C₁ (Functor C₂ (Functor C₃ C₄)))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(p : I₁ × I₂ × I₃ → J)
[∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
(X₁ : GradedObject I₁ C₁)
:
structure
CategoryTheory.GradedObject.BifunctorComp₁₂IndexData
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(r : I₁ × I₂ × I₃ → J)
:
Type (max (max (max (max u_10 (u_11 + 1)) 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.
Instances For
@[reducible, inline]
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}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
[Category.{u_15, u_5} C₁₂]
(F₁₂ : Functor C₁ (Functor C₂ C₁₂))
(G : Functor C₁₂ (Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : BifunctorComp₁₂IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
:
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 with 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}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
[Category.{u_15, u_5} C₁₂]
(F₁₂ : Functor C₁ (Functor C₂ C₁₂))
(G : Functor C₁₂ (Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : BifunctorComp₁₂IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
:
(G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ mapBifunctorMapObj G ρ₁₂.q (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
theorem
CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj_eq
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[Category.{u_16, u_1} C₁]
[Category.{u_15, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_12, u_4} C₄]
[Category.{u_14, u_5} C₁₂]
(F₁₂ : Functor C₁ (Functor C₂ C₁₂))
(G : Functor C₁₂ (Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : BifunctorComp₁₂IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
(i₁₂ : ρ₁₂.I₁₂)
(h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂)
:
ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryStruct.comp ((G.map (ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃))
(ιMapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j ⋯)
theorem
CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj_eq_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[Category.{u_16, u_1} C₁]
[Category.{u_15, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_12, u_4} C₄]
[Category.{u_14, u_5} C₁₂]
(F₁₂ : Functor C₁ (Functor C₂ C₁₂))
(G : Functor C₁₂ (Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : BifunctorComp₁₂IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
(i₁₂ : ρ₁₂.I₁₂)
(h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂)
{Z : C₄}
(h✝ : mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ Z)
:
CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝ = CategoryStruct.comp ((G.map (ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃))
(CategoryStruct.comp (ιMapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j ⋯) h✝)
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}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
[Category.{u_15, u_5} C₁₂]
(F₁₂ : Functor C₁ (Functor C₂ C₁₂))
(G : Functor C₁₂ (Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : BifunctorComp₁₂IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
(j : J)
:
((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).CofanMapObjFun 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}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
[Category.{u_15, u_5} C₁₂]
(F₁₂ : Functor C₁ (Functor C₂ C₁₂))
(G : Functor C₁₂ (Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : BifunctorComp₁₂IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
[H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
(j : J)
:
Limits.IsColimit (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}
[Category.{u_14, u_1} C₁]
[Category.{u_13, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_15, u_5} C₁₂]
{F₁₂ : Functor C₁ (Functor C₂ C₁₂)}
{G : Functor C₁₂ (Functor C₃ C₄)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
{ρ₁₂ : BifunctorComp₁₂IndexData r}
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
[H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
:
((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap 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}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
[Category.{u_15, u_5} C₁₂]
(F₁₂ : Functor C₁ (Functor C₂ C₁₂))
(G : Functor C₁₂ (Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : BifunctorComp₁₂IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
[H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
[((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r]
:
mapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ ≅ mapBifunctorMapObj G ρ₁₂.q (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.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_hom
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[Category.{u_14, u_1} C₁]
[Category.{u_13, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_15, u_5} C₁₂]
(F₁₂ : Functor C₁ (Functor C₂ C₁₂))
(G : Functor C₁₂ (Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : BifunctorComp₁₂IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
[H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
[((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
:
CategoryStruct.comp (ιMapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
((mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).hom j) = ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_hom_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[Category.{u_14, u_1} C₁]
[Category.{u_13, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_15, u_5} C₁₂]
(F₁₂ : Functor C₁ (Functor C₂ C₁₂))
(G : Functor C₁₂ (Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : BifunctorComp₁₂IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
[H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
[((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
{Z : C₄}
(h✝ : mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ Z)
:
CategoryStruct.comp (ιMapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
(CategoryStruct.comp ((mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).hom j) h✝) = CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_inv
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[Category.{u_15, u_1} C₁]
[Category.{u_14, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_13, u_5} C₁₂]
(F₁₂ : Functor C₁ (Functor C₂ C₁₂))
(G : Functor C₁₂ (Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : BifunctorComp₁₂IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
[H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
[((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
:
CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
((mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).inv j) = ιMapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_inv_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[Category.{u_15, u_1} C₁]
[Category.{u_14, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_13, u_5} C₁₂]
(F₁₂ : Functor C₁ (Functor C₂ C₁₂))
(G : Functor C₁₂ (Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₁₂ : BifunctorComp₁₂IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
[H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
[((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
{Z : C₄}
(h✝ : mapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ j ⟶ Z)
:
CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
(CategoryStruct.comp ((mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).inv j) h✝) = CategoryStruct.comp (ιMapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝
theorem
CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorMapObj_ext
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[Category.{u_15, u_1} C₁]
[Category.{u_16, u_2} C₂]
[Category.{u_14, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_13, u_5} C₁₂]
{F₁₂ : Functor C₁ (Functor C₂ C₁₂)}
{G : Functor C₁₂ (Functor C₃ C₄)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
{ρ₁₂ : BifunctorComp₁₂IndexData r}
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
[H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
{j : J}
{A : C₄}
{f g : mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ A}
(h :
∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) g)
:
theorem
CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorMapObj_ext_iff
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[Category.{u_15, u_1} C₁]
[Category.{u_16, u_2} C₂]
[Category.{u_14, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_13, u_5} C₁₂]
{F₁₂ : Functor C₁ (Functor C₂ C₁₂)}
{G : Functor C₁₂ (Functor C₃ C₄)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
{ρ₁₂ : BifunctorComp₁₂IndexData r}
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
[H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
{j : J}
{A : C₄}
{f g : mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ A}
:
f = g ↔ ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) g
noncomputable def
CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDesc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
[Category.{u_15, u_5} C₁₂]
{F₁₂ : Functor C₁ (Functor C₂ C₁₂)}
{G : Functor C₁₂ (Functor C₃ C₄)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
{ρ₁₂ : BifunctorComp₁₂IndexData r}
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
[H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
{j : J}
{A : C₄}
(f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ A))
:
Constructor for morphisms from
mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctor₁₂BifunctorDesc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[Category.{u_15, u_1} C₁]
[Category.{u_14, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_13, u_5} C₁₂]
{F₁₂ : Functor C₁ (Functor C₂ C₁₂)}
{G : Functor C₁₂ (Functor C₃ C₄)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
{ρ₁₂ : BifunctorComp₁₂IndexData r}
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
[H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
{j : J}
{A : C₄}
(f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ A))
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(h : r (i₁, i₂, i₃) = j)
:
CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) (mapBifunctor₁₂BifunctorDesc f) = f i₁ i₂ i₃ h
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctor₁₂BifunctorDesc_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₁₂ : Type u_5}
[Category.{u_15, u_1} C₁]
[Category.{u_14, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_13, u_5} C₁₂]
{F₁₂ : Functor C₁ (Functor C₂ C₁₂)}
{G : Functor C₁₂ (Functor C₃ C₄)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
{ρ₁₂ : BifunctorComp₁₂IndexData r}
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
[(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q]
[H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
{j : J}
{A : C₄}
(f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ A))
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(h : r (i₁, i₂, i₃) = j)
{Z : C₄}
(h✝ : A ⟶ Z)
:
CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
(CategoryStruct.comp (mapBifunctor₁₂BifunctorDesc f) h✝) = CategoryStruct.comp (f i₁ i₂ i₃ h) h✝
structure
CategoryTheory.GradedObject.BifunctorComp₂₃IndexData
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
(r : I₁ × I₂ × I₃ → J)
:
Type (max (max (max (max u_10 (u_11 + 1)) 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.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
[Category.{u_15, u_6} C₂₃]
(F : Functor C₁ (Functor C₂₃ C₄))
(G₂₃ : Functor C₂ (Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₂₃ : BifunctorComp₂₃IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
:
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 F(X₁ i₁, _) commutes with the coproducts of the G₂₃(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.ιMapBifunctorBifunctor₂₃MapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
[Category.{u_15, u_6} C₂₃]
(F : Functor C₁ (Functor C₂₃ C₄))
(G₂₃ : Functor C₂ (Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₂₃ : BifunctorComp₂₃IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
:
(F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j
The inclusion of (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) in
mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j
when r (i₁, i₂, i₃) = j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj_eq
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_14, u_1} C₁]
[Category.{u_16, u_2} C₂]
[Category.{u_15, u_3} C₃]
[Category.{u_12, u_4} C₄]
[Category.{u_13, u_6} C₂₃]
(F : Functor C₁ (Functor C₂₃ C₄))
(G₂₃ : Functor C₂ (Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₂₃ : BifunctorComp₂₃IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
(i₂₃ : ρ₂₃.I₂₃)
(h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃)
:
ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryStruct.comp ((F.obj (X₁ i₁)).map (ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃))
(ιMapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j ⋯)
theorem
CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj_eq_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_14, u_1} C₁]
[Category.{u_16, u_2} C₂]
[Category.{u_15, u_3} C₃]
[Category.{u_12, u_4} C₄]
[Category.{u_13, u_6} C₂₃]
(F : Functor C₁ (Functor C₂₃ C₄))
(G₂₃ : Functor C₂ (Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₂₃ : BifunctorComp₂₃IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
(i₂₃ : ρ₂₃.I₂₃)
(h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃)
{Z : C₄}
(h✝ : mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ Z)
:
CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝ = CategoryStruct.comp ((F.obj (X₁ i₁)).map (ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃))
(CategoryStruct.comp (ιMapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j ⋯) h✝)
noncomputable def
CategoryTheory.GradedObject.cofan₃MapBifunctorBifunctor₂₃MapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
[Category.{u_15, u_6} C₂₃]
(F : Functor C₁ (Functor C₂₃ C₄))
(G₂₃ : Functor C₂ (Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₂₃ : BifunctorComp₂₃IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
(j : J)
:
((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).CofanMapObjFun r j
The cofan consisting of the inclusions given by ιMapBifunctorBifunctor₂₃MapObj.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
[Category.{u_15, u_6} C₂₃]
(F : Functor C₁ (Functor C₂₃ C₄))
(G₂₃ : Functor C₂ (Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₂₃ : BifunctorComp₂₃IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
[H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
(j : J)
:
Limits.IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
The cofan cofan₃MapBifunctorBifunctor₂₃MapObj 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_6}
[Category.{u_14, u_1} C₁]
[Category.{u_13, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_15, u_6} C₂₃]
(F : Functor C₁ (Functor C₂₃ C₄))
(G₂₃ : Functor C₂ (Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₂₃ : BifunctorComp₂₃IndexData r)
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
[H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
:
((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap 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_6}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
[Category.{u_15, u_6} C₂₃]
(F : Functor C₁ (Functor C₂₃ C₄))
(G₂₃ : Functor C₂ (Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₂₃ : BifunctorComp₂₃IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
[H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
[((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r]
:
mapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ ≅ mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p 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.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_hom
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_14, u_1} C₁]
[Category.{u_13, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_15, u_6} C₂₃]
(F : Functor C₁ (Functor C₂₃ C₄))
(G₂₃ : Functor C₂ (Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₂₃ : BifunctorComp₂₃IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
[H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
[((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
:
CategoryStruct.comp (ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
((mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j) = ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_hom_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_14, u_1} C₁]
[Category.{u_13, u_2} C₂]
[Category.{u_12, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_15, u_6} C₂₃]
(F : Functor C₁ (Functor C₂₃ C₄))
(G₂₃ : Functor C₂ (Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₂₃ : BifunctorComp₂₃IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
[H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
[((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
{Z : C₄}
(h✝ : mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ Z)
:
CategoryStruct.comp (ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
(CategoryStruct.comp ((mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j) h✝) = CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_inv
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_13, u_1} C₁]
[Category.{u_15, u_2} C₂]
[Category.{u_14, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_12, u_6} C₂₃]
(F : Functor C₁ (Functor C₂₃ C₄))
(G₂₃ : Functor C₂ (Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₂₃ : BifunctorComp₂₃IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
[H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
[((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
:
CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
((mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).inv j) = ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_inv_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_13, u_1} C₁]
[Category.{u_15, u_2} C₂]
[Category.{u_14, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_12, u_6} C₂₃]
(F : Functor C₁ (Functor C₂₃ C₄))
(G₂₃ : Functor C₂ (Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
(ρ₂₃ : BifunctorComp₂₃IndexData r)
(X₁ : GradedObject I₁ C₁)
(X₂ : GradedObject I₂ C₂)
(X₃ : GradedObject I₃ C₃)
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
[H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
[((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r]
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(j : J)
(h : r (i₁, i₂, i₃) = j)
{Z : C₄}
(h✝ : mapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ j ⟶ Z)
:
CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
(CategoryStruct.comp ((mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).inv j) h✝) = CategoryStruct.comp (ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝
theorem
CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃MapObj_ext
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_13, u_1} C₁]
[Category.{u_15, u_2} C₂]
[Category.{u_16, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_14, u_6} C₂₃]
{F : Functor C₁ (Functor C₂₃ C₄)}
{G₂₃ : Functor C₂ (Functor C₃ C₂₃)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
{ρ₂₃ : BifunctorComp₂₃IndexData r}
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
[H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
{j : J}
{A : C₄}
{f g : mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A}
(h :
∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) g)
:
theorem
CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃MapObj_ext_iff
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_13, u_1} C₁]
[Category.{u_15, u_2} C₂]
[Category.{u_16, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_14, u_6} C₂₃]
{F : Functor C₁ (Functor C₂₃ C₄)}
{G₂₃ : Functor C₂ (Functor C₃ C₂₃)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
{ρ₂₃ : BifunctorComp₂₃IndexData r}
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
[H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
{j : J}
{A : C₄}
{f g : mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A}
:
f = g ↔ ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) g
noncomputable def
CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃Desc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_11, u_1} C₁]
[Category.{u_12, u_2} C₂]
[Category.{u_13, u_3} C₃]
[Category.{u_14, u_4} C₄]
[Category.{u_15, u_6} C₂₃]
{F : Functor C₁ (Functor C₂₃ C₄)}
{G₂₃ : Functor C₂ (Functor C₃ C₂₃)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
{ρ₂₃ : BifunctorComp₂₃IndexData r}
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
[H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
{j : J}
{A : C₄}
(f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ A))
:
Constructor for morphisms from
mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorBifunctor₂₃Desc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_13, u_1} C₁]
[Category.{u_15, u_2} C₂]
[Category.{u_14, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_12, u_6} C₂₃]
{F : Functor C₁ (Functor C₂₃ C₄)}
{G₂₃ : Functor C₂ (Functor C₃ C₂₃)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
{ρ₂₃ : BifunctorComp₂₃IndexData r}
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
[H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
{j : J}
{A : C₄}
(f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ A))
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(h : r (i₁, i₂, i₃) = j)
:
CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (mapBifunctorBifunctor₂₃Desc f) = f i₁ i₂ i₃ h
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorBifunctor₂₃Desc_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[Category.{u_13, u_1} C₁]
[Category.{u_15, u_2} C₂]
[Category.{u_14, u_3} C₃]
[Category.{u_11, u_4} C₄]
[Category.{u_12, u_6} C₂₃]
{F : Functor C₁ (Functor C₂₃ C₄)}
{G₂₃ : Functor C₂ (Functor C₃ C₂₃)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{r : I₁ × I₂ × I₃ → J}
{ρ₂₃ : BifunctorComp₂₃IndexData r}
{X₁ : GradedObject I₁ C₁}
{X₂ : GradedObject I₂ C₂}
{X₃ : GradedObject I₃ C₃}
[(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q]
[H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
{j : J}
{A : C₄}
(f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ A))
(i₁ : I₁)
(i₂ : I₂)
(i₃ : I₃)
(h : r (i₁, i₂, i₃) = j)
{Z : C₄}
(h✝ : A ⟶ Z)
:
CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
(CategoryStruct.comp (mapBifunctorBifunctor₂₃Desc f) h✝) = CategoryStruct.comp (f i₁ i₂ i₃ h) h✝