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).
def
CategoryTheory.GradedObject.mapBifunctor
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_6, u_1} C₁]
[Category.{u_7, u_2} C₂]
[Category.{u_8, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
(I : Type u_4)
(J : Type u_5)
:
Functor (GradedObject I C₁) (Functor (GradedObject J C₂) (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
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctor_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_6, u_1} C₁]
[Category.{u_7, u_2} C₂]
[Category.{u_8, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
(I : Type u_4)
(J : Type u_5)
(X : GradedObject I C₁)
{X✝ Y✝ : GradedObject J C₂}
(φ : X✝ ⟶ Y✝)
(ij : I × J)
:
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctor_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_6, u_1} C₁]
[Category.{u_7, u_2} C₂]
[Category.{u_8, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
(I : Type u_4)
(J : Type u_5)
(X : GradedObject I C₁)
(Y : GradedObject J C₂)
(ij : I × J)
:
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctor_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_6, u_1} C₁]
[Category.{u_7, u_2} C₂]
[Category.{u_8, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
(I : Type u_4)
(J : Type u_5)
{X✝ Y✝ : GradedObject I C₁}
(φ : X✝ ⟶ Y✝)
(Y : GradedObject J C₂)
(ij : I × J)
:
noncomputable def
CategoryTheory.GradedObject.mapBifunctorMapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
(X : GradedObject I C₁)
(Y : GradedObject J C₂)
[(((mapBifunctor F I J).obj X).obj Y).HasMap p]
:
GradedObject K C₃
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
Instances For
noncomputable def
CategoryTheory.GradedObject.ιMapBifunctorMapObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
(X : GradedObject I C₁)
(Y : GradedObject J C₂)
[(((mapBifunctor F I J).obj X).obj Y).HasMap p]
(i : I)
(j : J)
(k : K)
(h : p (i, j) = k)
:
The inclusion of (F.obj (X i)).obj (Y j) in mapBifunctorMapObj F p X Y k
when i + j = k.
Equations
Instances For
noncomputable def
CategoryTheory.GradedObject.mapBifunctorMapMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X₁ X₂ : GradedObject I C₁}
(f : X₁ ⟶ X₂)
{Y₁ Y₂ : GradedObject J C₂}
(g : Y₁ ⟶ Y₂)
[(((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
[(((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
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorMapMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X₁ X₂ : GradedObject I C₁}
(f : X₁ ⟶ X₂)
{Y₁ Y₂ : GradedObject J C₂}
(g : Y₁ ⟶ Y₂)
[(((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
[(((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p]
(i : I)
(j : J)
(k : K)
(h : p (i, j) = k)
:
CategoryStruct.comp (ιMapBifunctorMapObj F p X₁ Y₁ i j k h) (mapBifunctorMapMap F p f g k) = CategoryStruct.comp ((F.map (f i)).app (Y₁ j))
(CategoryStruct.comp ((F.obj (X₂ i)).map (g j)) (ιMapBifunctorMapObj F p X₂ Y₂ i j k h))
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorMapMap_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X₁ X₂ : GradedObject I C₁}
(f : X₁ ⟶ X₂)
{Y₁ Y₂ : GradedObject J C₂}
(g : Y₁ ⟶ Y₂)
[(((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
[(((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p]
(i : I)
(j : J)
(k : K)
(h : p (i, j) = k)
{Z : C₃}
(h✝ : mapBifunctorMapObj F p X₂ Y₂ k ⟶ Z)
:
CategoryStruct.comp (ιMapBifunctorMapObj F p X₁ Y₁ i j k h) (CategoryStruct.comp (mapBifunctorMapMap F p f g k) h✝) = CategoryStruct.comp ((F.map (f i)).app (Y₁ j))
(CategoryStruct.comp ((F.obj (X₂ i)).map (g j)) (CategoryStruct.comp (ιMapBifunctorMapObj F p X₂ Y₂ i j k h) h✝))
theorem
CategoryTheory.GradedObject.mapBifunctorMapObj_ext
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_9, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_7, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X : GradedObject I C₁}
{Y : GradedObject J C₂}
{A : C₃}
{k : K}
[(((mapBifunctor F I J).obj X).obj Y).HasMap p]
{f g : mapBifunctorMapObj F p X Y k ⟶ A}
(h :
∀ (i : I) (j : J) (hij : p (i, j) = k),
CategoryStruct.comp (ιMapBifunctorMapObj F p X Y i j k hij) f = CategoryStruct.comp (ιMapBifunctorMapObj F p X Y i j k hij) g)
:
theorem
CategoryTheory.GradedObject.mapBifunctorMapObj_ext_iff
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_9, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_7, u_3} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
{p : I × J → K}
{X : GradedObject I C₁}
{Y : GradedObject J C₂}
{A : C₃}
{k : K}
[(((mapBifunctor F I J).obj X).obj Y).HasMap p]
{f g : mapBifunctorMapObj F p X Y k ⟶ A}
:
f = g ↔ ∀ (i : I) (j : J) (hij : p (i, j) = k),
CategoryStruct.comp (ιMapBifunctorMapObj F p X Y i j k hij) f = CategoryStruct.comp (ιMapBifunctorMapObj F p X Y i j k hij) g
noncomputable def
CategoryTheory.GradedObject.mapBifunctorMapObjDesc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
{p : I × J → K}
{X : GradedObject I C₁}
{Y : GradedObject J C₂}
{A : C₃}
{k : K}
[(((mapBifunctor F I J).obj X).obj Y).HasMap p]
(f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A))
:
Constructor for morphisms from mapBifunctorMapObj F p X Y k.
Equations
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorMapObjDesc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_9, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_7, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X : GradedObject I C₁}
{Y : GradedObject J C₂}
{A : C₃}
{k : K}
[(((mapBifunctor F I J).obj X).obj Y).HasMap p]
(f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A))
(i : I)
(j : J)
(hij : p (i, j) = k)
:
@[simp]
theorem
CategoryTheory.GradedObject.ι_mapBifunctorMapObjDesc_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_9, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_7, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X : GradedObject I C₁}
{Y : GradedObject J C₂}
{A : C₃}
{k : K}
[(((mapBifunctor F I J).obj X).obj Y).HasMap p]
(f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A))
(i : I)
(j : J)
(hij : p (i, j) = k)
{Z : C₃}
(h : A ⟶ Z)
:
CategoryStruct.comp (ιMapBifunctorMapObj F p X Y i j k hij) (CategoryStruct.comp (mapBifunctorMapObjDesc f) h) = CategoryStruct.comp (f i j hij) h
noncomputable def
CategoryTheory.GradedObject.mapBifunctorMapMapIso
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X₁ X₂ : GradedObject I C₁}
{Y₁ Y₂ : GradedObject J C₂}
[(((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
[(((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p]
(e : X₁ ≅ X₂)
(e' : Y₁ ≅ Y₂)
:
The isomorphism mapBifunctorMapObj F p X₁ Y₁ ≅ mapBifunctorMapObj F p X₂ Y₂
induced by isomorphisms X₁ ≅ X₂ and Y₁ ≅ Y₂.
Equations
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorMapMapIso_hom
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X₁ X₂ : GradedObject I C₁}
{Y₁ Y₂ : GradedObject J C₂}
[(((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
[(((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p]
(e : X₁ ≅ X₂)
(e' : Y₁ ≅ Y₂)
(i : K)
:
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorMapMapIso_inv
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X₁ X₂ : GradedObject I C₁}
{Y₁ Y₂ : GradedObject J C₂}
[(((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
[(((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p]
(e : X₁ ≅ X₂)
(e' : Y₁ ≅ Y₂)
(i : K)
:
instance
CategoryTheory.GradedObject.instIsIsoMapBifunctorMapMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
{X₁ X₂ : GradedObject I C₁}
{Y₁ Y₂ : GradedObject J C₂}
[(((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
[(((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p]
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
[IsIso f]
[IsIso g]
:
IsIso (mapBifunctorMapMap F p f g)
noncomputable def
CategoryTheory.GradedObject.mapBifunctorMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
[∀ (X : GradedObject I C₁) (Y : GradedObject J C₂), (((mapBifunctor F I J).obj X).obj Y).HasMap p]
:
Functor (GradedObject I C₁) (Functor (GradedObject J C₂) (GradedObject K C₃))
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
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorMap_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
[∀ (X : GradedObject I C₁) (Y : GradedObject J C₂), (((mapBifunctor F I J).obj X).obj Y).HasMap p]
(X : GradedObject I C₁)
{X✝ Y✝ : GradedObject J C₂}
(ψ : X✝ ⟶ Y✝)
(i : K)
:
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorMap_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
[∀ (X : GradedObject I C₁) (Y : GradedObject J C₂), (((mapBifunctor F I J).obj X).obj Y).HasMap p]
(X : GradedObject I C₁)
(Y : GradedObject J C₂)
:
@[simp]
theorem
CategoryTheory.GradedObject.mapBifunctorMap_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
(F : Functor C₁ (Functor C₂ C₃))
{I : Type u_4}
{J : Type u_5}
{K : Type u_6}
(p : I × J → K)
[∀ (X : GradedObject I C₁) (Y : GradedObject J C₂), (((mapBifunctor F I J).obj X).obj Y).HasMap p]
{X₁ X₂ : GradedObject I C₁}
(φ : X₁ ⟶ X₂)
(Y : GradedObject J C₂)
(i : K)
: