The action of bifunctors on graded objects #
Given a bifunctor F : C₁ ⥤ C₂ ⥤ C₃ and types I and J, we construct an obvious functor
mapBifunctor F I J : GradedObject I C₁ ⥤ GradedObject J C₂ ⥤ GradedObject (I × J) C₃.
When we have a map p : I × J → K and that suitable coproducts exists, we also get
a functor
mapBifunctorMap F p : GradedObject I C₁ ⥤ GradedObject J C₂ ⥤ GradedObject K C₃.
In case p : I × I → I is the addition on a monoid and F is the tensor product on a monoidal
category C, these definitions shall be used in order to construct a monoidal structure
on GradedObject I C (TODO @joelriou).
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctor_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_6, u_1} C₁]
[CategoryTheory.Category.{u_7, u_2} C₂]
[CategoryTheory.Category.{u_8, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
(I : Type u_4)
(J : Type u_5)
(X : CategoryTheory.GradedObject I C₁)
(Y : CategoryTheory.GradedObject J C₂)
(ij : I × J)
:
((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y ij = (F.obj (X ij.1)).obj (Y ij.2)
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctor_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_6, u_1} C₁]
[CategoryTheory.Category.{u_7, u_2} C₂]
[CategoryTheory.Category.{u_8, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
(I : Type u_4)
(J : Type u_5)
:
∀ {X Y : CategoryTheory.GradedObject I C₁} (φ : X ⟶ Y) (Y_1 : CategoryTheory.GradedObject J C₂) (ij : I × J),
((CategoryTheory.GradedObject.mapBifunctor F I J).map φ).app Y_1 ij = (F.map (φ ij.1)).app (Y_1 ij.2)
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctor_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_6, u_1} C₁]
[CategoryTheory.Category.{u_7, u_2} C₂]
[CategoryTheory.Category.{u_8, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
(I : Type u_4)
(J : Type u_5)
(X : CategoryTheory.GradedObject I C₁)
:
∀ {X_1 Y : CategoryTheory.GradedObject J C₂} (φ : X_1 ⟶ Y) (ij : I × J),
((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).map φ ij = (F.obj (X ij.1)).map (φ ij.2)
def
CategoryTheory.GradedObject.mapBifunctor
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_6, u_1} C₁]
[CategoryTheory.Category.{u_7, u_2} C₂]
[CategoryTheory.Category.{u_8, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
(I : Type u_4)
(J : Type u_5)
:
CategoryTheory.Functor (CategoryTheory.GradedObject I C₁)
(CategoryTheory.Functor (CategoryTheory.GradedObject J C₂) (CategoryTheory.GradedObject (I × J) C₃))
Given a bifunctor F : C₁ ⥤ C₂ ⥤ C₃ and types I and J, this is the obvious
functor GradedObject I C₁ ⥤ GradedObject J C₂ ⥤ GradedObject (I × J) C₃.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.GradedObject.mapBifunctorMapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
(X : CategoryTheory.GradedObject I C₁)
(Y : CategoryTheory.GradedObject J C₂)
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
:
Given a bifunctor F : C₁ ⥤ C₂ ⥤ C₃, graded objects X : GradedObject I C₁ and
Y : GradedObject J C₂ and a map p : I × J → K, this is the K-graded object sending
k to the coproduct of (F.obj (X i)).obj (Y j) for p ⟨i, j⟩ = k.
Equations
- CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y = (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).mapObj p
Instances For
noncomputable def
CategoryTheory.GradedObject.ιMapBifunctorMapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
(X : CategoryTheory.GradedObject I C₁)
(Y : CategoryTheory.GradedObject J C₂)
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
(i : I)
(j : J)
(k : K)
(h : p (i, j) = k)
:
(F.obj (X i)).obj (Y j) ⟶ CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y k
The inclusion of (F.obj (X i)).obj (Y j) in mapBifunctorMapObj F p X Y k
when i + j = k.
Equations
- CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k h = (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).ιMapObj p (i, j) k h
Instances For
noncomputable def
CategoryTheory.GradedObject.mapBifunctorMapMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X₁ : CategoryTheory.GradedObject I C₁}
{X₂ : CategoryTheory.GradedObject I C₁}
(f : X₁ ⟶ X₂)
{Y₁ : CategoryTheory.GradedObject J C₂}
{Y₂ : CategoryTheory.GradedObject J C₂}
(g : Y₁ ⟶ Y₂)
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p]
:
The maps mapBifunctorMapObj F p X₁ Y₁ ⟶ mapBifunctorMapObj F p X₂ Y₂ which express
the functoriality of mapBifunctorMapObj, see mapBifunctorMap.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorMapMap_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X₁ : CategoryTheory.GradedObject I C₁}
{X₂ : CategoryTheory.GradedObject I C₁}
(f : X₁ ⟶ X₂)
{Y₁ : CategoryTheory.GradedObject J C₂}
{Y₂ : CategoryTheory.GradedObject J C₂}
(g : Y₁ ⟶ Y₂)
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p]
(i : I)
(j : J)
(k : K)
(h : p (i, j) = k)
{Z : C₃}
(h : CategoryTheory.GradedObject.mapBifunctorMapObj F p X₂ Y₂ k ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₁ Y₁ i j k h✝)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p f g k) h) = CategoryTheory.CategoryStruct.comp ((F.map (f i)).app (Y₁ j))
(CategoryTheory.CategoryStruct.comp ((F.obj (X₂ i)).map (g j))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₂ Y₂ i j k h✝) h))
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorMapMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X₁ : CategoryTheory.GradedObject I C₁}
{X₂ : CategoryTheory.GradedObject I C₁}
(f : X₁ ⟶ X₂)
{Y₁ : CategoryTheory.GradedObject J C₂}
{Y₂ : CategoryTheory.GradedObject J C₂}
(g : Y₁ ⟶ Y₂)
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
[(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p]
(i : I)
(j : J)
(k : K)
(h : p (i, j) = k)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₁ Y₁ i j k h)
(CategoryTheory.GradedObject.mapBifunctorMapMap F p f g k) = CategoryTheory.CategoryStruct.comp ((F.map (f i)).app (Y₁ j))
(CategoryTheory.CategoryStruct.comp ((F.obj (X₂ i)).map (g j))
(CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₂ Y₂ i j k h))
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorMap_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
[∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂),
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
{X₁ : CategoryTheory.GradedObject I C₁}
{X₂ : CategoryTheory.GradedObject I C₁}
(φ : X₁ ⟶ X₂)
(Y : CategoryTheory.GradedObject J C₂)
(i : K)
:
((CategoryTheory.GradedObject.mapBifunctorMap F p).map φ).app Y i = CategoryTheory.GradedObject.mapBifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id Y) i
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorMap_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
[∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂),
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
(X : CategoryTheory.GradedObject I C₁)
(Y : CategoryTheory.GradedObject J C₂)
:
((CategoryTheory.GradedObject.mapBifunctorMap F p).obj X).obj Y = CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorMap_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
[∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂),
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
(X : CategoryTheory.GradedObject I C₁)
:
∀ {X_1 Y : CategoryTheory.GradedObject J C₂} (ψ : X_1 ⟶ Y) (i : K),
((CategoryTheory.GradedObject.mapBifunctorMap F p).obj X).map ψ i = CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id X) ψ i
noncomputable def
CategoryTheory.GradedObject.mapBifunctorMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} C₃]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
[∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂),
(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
:
Given a bifunctor F : C₁ ⥤ C₂ ⥤ C₃ and a map p : I × J → K, this is the
functor GradedObject I C₁ ⥤ GradedObject J C₂ ⥤ GradedObject K C₃ sending
X : GradedObject I C₁ and Y : GradedObject J C₂ to the K-graded object sending
k to the coproduct of (F.obj (X i)).obj (Y j) for p ⟨i, j⟩ = k.
Equations
- One or more equations did not get rendered due to their size.