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_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_7}
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(I₂ : Type u_8)
(I₃ : Type u_9)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
(x : I₁ × I₂ × I₃)
:
((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).obj X₂).obj X₃ x = ((F.obj (X₁ x.1)).obj (X₂ x.2.1)).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_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_7}
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(I₂ : Type u_8)
(I₃ : Type u_9)
{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₃).map φ).app X₃ x = ((F.obj (X₁ x.1)).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_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_7}
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(I₂ : Type u_8)
(I₃ : Type u_9)
(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₃).obj X₂).map φ x = ((F.obj (X₁ x.1)).obj (X₂ x.2.1)).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_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_7}
(X₁ : CategoryTheory.GradedObject I₁ C₁)
(I₂ : Type u_8)
(I₃ : Type u_9)
:
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_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_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
{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₃).map φ).app X₂).app X₃ x = ((F.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_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_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
(X₁ : CategoryTheory.GradedObject I₁ C₁)
:
(CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).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_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_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
:
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_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₄))}
{F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
(α : F ⟶ F')
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
(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_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₄))}
{F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
(α : F ⟶ F')
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
:
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_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₄))}
{F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
(e : F ≅ F')
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
:
(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_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₄))}
{F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
(e : F ≅ F')
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
:
(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_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₄))}
{F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))}
(e : F ≅ F')
(I₁ : Type u_7)
(I₂ : Type u_8)
(I₃ : Type u_9)
:
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_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : CategoryTheory.GradedObject I₁ C₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
[((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap 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
- 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}
[CategoryTheory.Category.{u_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : 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.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
:
((F.obj (X₁ i₁)).obj (X₂ i₂)).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
- CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h = ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p (i₁, i₂, i₃) j h
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_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : 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.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
[((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap 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_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : 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.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
[((((CategoryTheory.GradedObject.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 : 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.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃))
(CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃))
(CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).obj (Y₂ i₂)).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_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : 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.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
[((((CategoryTheory.GradedObject.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)
:
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.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃))
(CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃))
(CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).obj (Y₂ i₂)).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_14, u_1} C₁]
[CategoryTheory.Category.{u_13, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : CategoryTheory.GradedObject I₁ C₁}
{X₂ : CategoryTheory.GradedObject I₂ C₂}
{X₃ : CategoryTheory.GradedObject I₃ C₃}
{Y : C₄}
(j : J)
[((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap 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.instHasMapProdObjFunctorMapTrifunctorObjOfMapTrifunctor
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_14, u_1} C₁]
[CategoryTheory.Category.{u_13, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : CategoryTheory.GradedObject I₁ C₁)
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
[h : ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
:
(((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).obj X₂).obj X₃).HasMap p
Equations
- ⋯ = 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_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : CategoryTheory.GradedObject I₁ C₁)
[∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap 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₁).obj X₂).map φ 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_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : CategoryTheory.GradedObject I₁ C₁)
[∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
(X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃)
:
((CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁).obj X₂).obj X₃ = CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃
@[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_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : CategoryTheory.GradedObject I₁ C₁)
[∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap 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₁).map φ).app X₃ i = CategoryTheory.GradedObject.mapTrifunctorMapMap F p (CategoryTheory.CategoryStruct.id X₁) φ
(CategoryTheory.CategoryStruct.id X₃) i
noncomputable def
CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[CategoryTheory.Category.{u_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : CategoryTheory.GradedObject I₁ C₁)
[∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap 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_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃),
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
(X₁ : CategoryTheory.GradedObject I₁ C₁)
:
@[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_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃),
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap 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).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_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
(X₃ : CategoryTheory.GradedObject I₃ C₃),
((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap 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_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.
- I₁₂ : Type u_11
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
@[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}
[CategoryTheory.Category.{u_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
[CategoryTheory.Category.{u_15, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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_9 u_16) u_4) u_5) u_14) u_15) u_7 u_8)
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_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
[CategoryTheory.Category.{u_15, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.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₃) ⟶ 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
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}
[CategoryTheory.Category.{u_16, u_1} C₁]
[CategoryTheory.Category.{u_15, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_12, 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_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.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 : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)
X₃ j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) h = CategoryTheory.CategoryStruct.comp
((G.map (CategoryTheory.GradedObject.ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctorMapObj G ρ₁₂.q
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j ⋯)
h)
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}
[CategoryTheory.Category.{u_16, u_1} C₁]
[CategoryTheory.Category.{u_15, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_12, 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_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.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₁₂)
:
CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryTheory.CategoryStruct.comp
((G.map (CategoryTheory.GradedObject.ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃))
(CategoryTheory.GradedObject.ιMapBifunctorMapObj G ρ₁₂.q
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j ⋯)
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_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
[CategoryTheory.Category.{u_15, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃).HasMap
ρ₁₂.q]
(j : J)
:
((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.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}
[CategoryTheory.Category.{u_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
[CategoryTheory.Category.{u_15, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃).HasMap
ρ₁₂.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_14, u_1} C₁]
[CategoryTheory.Category.{u_13, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
[CategoryTheory.Category.{u_15, u_5} C₁₂]
{F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
{G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃).HasMap
ρ₁₂.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
:
((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.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}
[CategoryTheory.Category.{u_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
[CategoryTheory.Category.{u_15, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃).HasMap
ρ₁₂.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
[((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj
X₃).HasMap
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.
Instances For
@[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}
[CategoryTheory.Category.{u_14, u_1} C₁]
[CategoryTheory.Category.{u_13, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
[CategoryTheory.Category.{u_15, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃).HasMap
ρ₁₂.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
[((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.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 : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)
X₃ j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h✝)
(CategoryTheory.CategoryStruct.comp
((CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).hom j) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) h
@[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}
[CategoryTheory.Category.{u_14, u_1} C₁]
[CategoryTheory.Category.{u_13, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
[CategoryTheory.Category.{u_15, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃).HasMap
ρ₁₂.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
[((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.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)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
((CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).hom j) = CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ 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}
[CategoryTheory.Category.{u_15, u_1} C₁]
[CategoryTheory.Category.{u_14, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
[CategoryTheory.Category.{u_13, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃).HasMap
ρ₁₂.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
[((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.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 : CategoryTheory.GradedObject.mapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h✝)
(CategoryTheory.CategoryStruct.comp
((CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).inv j) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r 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}
[CategoryTheory.Category.{u_15, u_1} C₁]
[CategoryTheory.Category.{u_14, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
[CategoryTheory.Category.{u_13, u_5} C₁₂]
(F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
(G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃).HasMap
ρ₁₂.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
[((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.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)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
((CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).inv j) = CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j 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}
[CategoryTheory.Category.{u_15, u_1} C₁]
[CategoryTheory.Category.{u_16, u_2} C₂]
[CategoryTheory.Category.{u_14, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
[CategoryTheory.Category.{u_13, u_5} C₁₂]
{F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
{G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
[(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃).HasMap
ρ₁₂.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
{j : J}
{A : C₄}
(f : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)
X₃ j ⟶ A)
(g : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)
X₃ j ⟶ A)
(h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) g)
:
f = g
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.
- I₂₃ : Type u_11
an auxiliary type
- p : I₂ × I₃ → self.I₂₃
a map
I₂ × I₃ → I₂₃ - q : I₁ × self.I₂₃ → J
a map
I₁ × I₂₃ → J
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}
[CategoryTheory.Category.{u_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
[CategoryTheory.Category.{u_15, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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_7 u_16) u_4) u_6) u_14) u_15) u_8 u_9)
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 wich 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}
[CategoryTheory.Category.{u_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
[CategoryTheory.Category.{u_15, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.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₃)) ⟶ CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
(CategoryTheory.GradedObject.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_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_14, u_1} C₁]
[CategoryTheory.Category.{u_16, u_2} C₂]
[CategoryTheory.Category.{u_15, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
[CategoryTheory.Category.{u_13, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.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 : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) h = CategoryTheory.CategoryStruct.comp
((F.obj (X₁ i₁)).map (CategoryTheory.GradedObject.ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctorMapObj F ρ₂₃.q X₁
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j ⋯)
h)
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}
[CategoryTheory.Category.{u_14, u_1} C₁]
[CategoryTheory.Category.{u_16, u_2} C₂]
[CategoryTheory.Category.{u_15, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} C₄]
[CategoryTheory.Category.{u_13, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.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₂₃)
:
CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryTheory.CategoryStruct.comp
((F.obj (X₁ i₁)).map (CategoryTheory.GradedObject.ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃))
(CategoryTheory.GradedObject.ιMapBifunctorMapObj F ρ₂₃.q X₁
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j ⋯)
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}
[CategoryTheory.Category.{u_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
[CategoryTheory.Category.{u_15, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
ρ₂₃.q]
(j : J)
:
((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.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}
[CategoryTheory.Category.{u_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
[CategoryTheory.Category.{u_15, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
ρ₂₃.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
(j : J)
:
CategoryTheory.Limits.IsColimit (CategoryTheory.GradedObject.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}
[CategoryTheory.Category.{u_14, u_1} C₁]
[CategoryTheory.Category.{u_13, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
[CategoryTheory.Category.{u_15, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
ρ₂₃.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
:
((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.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}
[CategoryTheory.Category.{u_11, u_1} C₁]
[CategoryTheory.Category.{u_12, u_2} C₂]
[CategoryTheory.Category.{u_13, u_3} C₃]
[CategoryTheory.Category.{u_14, u_4} C₄]
[CategoryTheory.Category.{u_15, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
ρ₂₃.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
[((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj
X₃).HasMap
r]
:
CategoryTheory.GradedObject.mapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ ≅ CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
(CategoryTheory.GradedObject.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_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{C₂₃ : Type u_6}
[CategoryTheory.Category.{u_14, u_1} C₁]
[CategoryTheory.Category.{u_13, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
[CategoryTheory.Category.{u_15, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
ρ₂₃.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
[((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.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 : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h✝)
(CategoryTheory.CategoryStruct.comp
((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) h
@[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}
[CategoryTheory.Category.{u_14, u_1} C₁]
[CategoryTheory.Category.{u_13, u_2} C₂]
[CategoryTheory.Category.{u_12, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
[CategoryTheory.Category.{u_15, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
ρ₂₃.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
[((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.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)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j) = CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ 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}
[CategoryTheory.Category.{u_13, u_1} C₁]
[CategoryTheory.Category.{u_15, u_2} C₂]
[CategoryTheory.Category.{u_14, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
[CategoryTheory.Category.{u_12, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
ρ₂₃.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
[((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.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 : CategoryTheory.GradedObject.mapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h✝)
(CategoryTheory.CategoryStruct.comp
((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).inv j) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r 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}
[CategoryTheory.Category.{u_13, u_1} C₁]
[CategoryTheory.Category.{u_15, u_2} C₂]
[CategoryTheory.Category.{u_14, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
[CategoryTheory.Category.{u_12, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
ρ₂₃.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
[((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.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)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).inv j) = CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j 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}
[CategoryTheory.Category.{u_13, u_1} C₁]
[CategoryTheory.Category.{u_15, u_2} C₂]
[CategoryTheory.Category.{u_16, u_3} C₃]
[CategoryTheory.Category.{u_11, u_4} C₄]
[CategoryTheory.Category.{u_14, u_6} C₂₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
(G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
{I₁ : Type u_7}
{I₂ : Type u_8}
{I₃ : Type u_9}
{J : Type u_10}
{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.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
[(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
ρ₂₃.q]
[H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
{j : J}
{A : C₄}
(f : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A)
(g : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A)
(h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) g)
:
f = g