Documentation

Mathlib.CategoryTheory.GradedObject.Bifunctor

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)

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 × JK) (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
    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 × JK) (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
      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 × JK) {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 × JK) {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) :
          @[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 × JK) {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) :
          noncomputable def CategoryTheory.GradedObject.mapBifunctorMapObjDesc {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 × JK} {X : CategoryTheory.GradedObject I C₁} {Y : CategoryTheory.GradedObject J C₂} {A : C₃} {k : K} [(((CategoryTheory.GradedObject.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
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.GradedObject.ι_mapBifunctorMapObjDesc_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, 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 × JK) {X : CategoryTheory.GradedObject I C₁} {Y : CategoryTheory.GradedObject J C₂} {A : C₃} {k : K} [(((CategoryTheory.GradedObject.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) :
            @[simp]
            theorem CategoryTheory.GradedObject.ι_mapBifunctorMapObjDesc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, 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 × JK) {X : CategoryTheory.GradedObject I C₁} {Y : CategoryTheory.GradedObject J C₂} {A : C₃} {k : K} [(((CategoryTheory.GradedObject.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.mapBifunctorMapMapIso_hom {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 × JK) {X₁ : CategoryTheory.GradedObject I C₁} {X₂ : CategoryTheory.GradedObject I C₁} {Y₁ : CategoryTheory.GradedObject J C₂} {Y₂ : CategoryTheory.GradedObject J C₂} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] [(((CategoryTheory.GradedObject.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} [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 × JK) {X₁ : CategoryTheory.GradedObject I C₁} {X₂ : CategoryTheory.GradedObject I C₁} {Y₁ : CategoryTheory.GradedObject J C₂} {Y₂ : CategoryTheory.GradedObject J C₂} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (e : X₁ X₂) (e' : Y₁ Y₂) (i : K) :
            noncomputable def CategoryTheory.GradedObject.mapBifunctorMapMapIso {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 × JK) {X₁ : CategoryTheory.GradedObject I C₁} {X₂ : CategoryTheory.GradedObject I C₁} {Y₁ : CategoryTheory.GradedObject J C₂} {Y₂ : CategoryTheory.GradedObject J C₂} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] [(((CategoryTheory.GradedObject.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
            • One or more equations did not get rendered due to their size.
            Instances For
              instance CategoryTheory.GradedObject.instIsIsoMapBifunctorMapMap {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 × JK) {X₁ : CategoryTheory.GradedObject I C₁} {X₂ : CategoryTheory.GradedObject I C₁} {Y₁ : CategoryTheory.GradedObject J C₂} {Y₂ : CategoryTheory.GradedObject J C₂} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (f : X₁ X₂) (g : Y₁ Y₂) [CategoryTheory.IsIso f] [CategoryTheory.IsIso g] :
              Equations
              • =

              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.
              Instances For