Documentation

Mathlib.CategoryTheory.GradedObject.Unitor

The left and right unitors #

Given a bifunctor F : C ⥤ D ⥤ D, an object X : C such that F.obj X ≅ 𝟭 D and a map p : I × J → J such that hp : ∀ (j : J), p ⟨0, j⟩ = j, we define an isomorphism of J-graded objects for any Y : GradedObject J D. mapBifunctorLeftUnitor F X e p hp Y : mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y. Under similar assumptions, we also obtain a right unitor isomorphism mapBifunctorMapObj F p X ((single₀ I).obj Y) ≅ X. Finally, the lemma mapBifunctor_triangle promotes a triangle identity involving functors to a triangle identity for the induced functors on graded objects.

Given F : C ⥤ D ⥤ D, X : C, e : F.obj X ≅ 𝟭 D and Y : GradedObject J D, this is the isomorphism ((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y a ≅ Y a.2 when a : I × J is such that a.1 = 0.

Equations
Instances For

    Given F : C ⥤ D ⥤ D, X : C and Y : GradedObject J D, ((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y a is an initial object when a : I × J is such that a.1 ≠ 0.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × JJ) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) (j : J) :
      (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).CofanMapObjFun p j

      Given F : C ⥤ D ⥤ D, X : C, e : F.obj X ≅ 𝟭 D, Y : GradedObject J D and p : I × J → J such that p ⟨0, j⟩ = j for all j, this is the (colimit) cofan which shall be used to construct the isomorphism mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y, see mapBifunctorLeftUnitor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The cofan mapBifunctorLeftUnitorCofan F X e p hp Y j is a colimit.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Given F : C ⥤ D ⥤ D, X : C, e : F.obj X ≅ 𝟭 D, Y : GradedObject J D and p : I × J → J such that p ⟨0, j⟩ = j for all j, this is the left unitor isomorphism mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Given F : D ⥤ C ⥤ D, Y : C, e : F.flip.obj X ≅ 𝟭 D and X : GradedObject J D, this is the isomorphism ((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y) a ≅ Y a.2 when a : J × I is such that a.2 = 0.

            Equations
            Instances For

              Given F : D ⥤ C ⥤ D, Y : C and X : GradedObject J D, ((mapBifunctor F J I).obj X).obj ((single₀ I).obj X) a is an initial when a : J × I is such that a.2 ≠ 0.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                noncomputable def CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y CategoryTheory.Functor.id D) [(X : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × IJ) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) (j : J) :
                (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).CofanMapObjFun p j

                Given F : D ⥤ C ⥤ D, Y : C, e : F.flip.obj Y ≅ 𝟭 D, X : GradedObject J D and p : J × I → J such that p ⟨j, 0⟩ = j for all j, this is the (colimit) cofan which shall be used to construct the isomorphism mapBifunctorMapObj F p X ((single₀ I).obj Y) ≅ X, see mapBifunctorRightUnitor.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The cofan mapBifunctorRightUnitorCofan F Y e p hp X j is a colimit.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Given F : D ⥤ C ⥤ D, Y : C, e : F.flip.obj Y ≅ 𝟭 D, X : GradedObject J D and p : J × I → J such that p ⟨j, 0⟩ = j for all j, this is the right unitor isomorphism mapBifunctorMapObj F p X ((single₀ I).obj Y) ≅ X.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      structure CategoryTheory.GradedObject.TriangleIndexData {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [Zero I₂] (r : I₁ × I₂ × I₃J) (π : I₁ × I₃J) :
                      Type (max (max u_1 u_2) u_3)

                      Given two maps r : I₁ × I₂ × I₃ → J and π : I₁ × I₃ → J, this structure is the input in the formulation of the triangle equality mapBifunctor_triangle which relates the left and right unitor and the associator for GradedObject.mapBifunctor.

                      • p₁₂ : I₁ × I₂I₁

                        a map I₁ × I₂ → I₁

                      • hp₁₂ : ∀ (i : I₁ × I₂ × I₃), π (self.p₁₂ (i.1, i.2.1), i.2.2) = r i
                      • p₂₃ : I₂ × I₃I₃

                        a map I₂ × I₃ → I₃

                      • hp₂₃ : ∀ (i : I₁ × I₂ × I₃), π (i.1, self.p₂₃ i.2) = r i
                      • h₁ : ∀ (i₁ : I₁), self.p₁₂ (i₁, 0) = i₁
                      • h₃ : ∀ (i₃ : I₃), self.p₂₃ (0, i₃) = i₃
                      Instances For
                        theorem CategoryTheory.GradedObject.TriangleIndexData.hp₁₂ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [Zero I₂] {r : I₁ × I₂ × I₃J} {π : I₁ × I₃J} (self : CategoryTheory.GradedObject.TriangleIndexData r π) (i : I₁ × I₂ × I₃) :
                        π (self.p₁₂ (i.1, i.2.1), i.2.2) = r i
                        theorem CategoryTheory.GradedObject.TriangleIndexData.hp₂₃ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [Zero I₂] {r : I₁ × I₂ × I₃J} {π : I₁ × I₃J} (self : CategoryTheory.GradedObject.TriangleIndexData r π) (i : I₁ × I₂ × I₃) :
                        π (i.1, self.p₂₃ i.2) = r i
                        @[simp]
                        theorem CategoryTheory.GradedObject.TriangleIndexData.h₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [Zero I₂] {r : I₁ × I₂ × I₃J} {π : I₁ × I₃J} (self : CategoryTheory.GradedObject.TriangleIndexData r π) (i₁ : I₁) :
                        self.p₁₂ (i₁, 0) = i₁
                        @[simp]
                        theorem CategoryTheory.GradedObject.TriangleIndexData.h₃ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [Zero I₂] {r : I₁ × I₂ × I₃J} {π : I₁ × I₃J} (self : CategoryTheory.GradedObject.TriangleIndexData r π) (i₃ : I₃) :
                        self.p₂₃ (0, i₃) = i₃
                        theorem CategoryTheory.GradedObject.TriangleIndexData.r_zero {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [Zero I₂] {r : I₁ × I₂ × I₃J} {π : I₁ × I₃J} (τ : CategoryTheory.GradedObject.TriangleIndexData r π) (i₁ : I₁) (i₃ : I₃) :
                        r (i₁, 0, i₃) = π (i₁, i₃)
                        @[reducible]
                        def CategoryTheory.GradedObject.TriangleIndexData.ρ₁₂ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [Zero I₂] {r : I₁ × I₂ × I₃J} {π : I₁ × I₃J} (τ : CategoryTheory.GradedObject.TriangleIndexData r π) :

                        The BifunctorComp₁₂IndexData r attached to a TriangleIndexData r π.

                        Equations
                        • τ.ρ₁₂ = { I₁₂ := I₁, p := τ.p₁₂, q := π, hpq := }
                        Instances For
                          @[reducible]
                          def CategoryTheory.GradedObject.TriangleIndexData.ρ₂₃ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [Zero I₂] {r : I₁ × I₂ × I₃J} {π : I₁ × I₃J} (τ : CategoryTheory.GradedObject.TriangleIndexData r π) :

                          The BifunctorComp₂₃IndexData r attached to a TriangleIndexData r π.

                          Equations
                          • τ.ρ₂₃ = { I₂₃ := I₃, p := τ.p₂₃, q := π, hpq := }
                          Instances For
                            theorem CategoryTheory.GradedObject.mapBifunctor_triangle {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D : Type u_4} {I₁ : Type u_5} {I₂ : Type u_6} {I₃ : Type u_7} {J : Type u_8} [CategoryTheory.Category.{u_12, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_9, u_4} D] [Zero I₂] [DecidableEq I₂] [CategoryTheory.Limits.HasInitial C₂] {F₁ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁)} {F₂ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₃)} {G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₃ D)} (associator : CategoryTheory.bifunctorComp₁₂ F₁ G CategoryTheory.bifunctorComp₂₃ G F₂) (X₂ : C₂) (e₁ : F₁.flip.obj X₂ CategoryTheory.Functor.id C₁) (e₂ : F₂.obj X₂ CategoryTheory.Functor.id C₃) [(X₁ : C₁) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C₂) (F₁.obj X₁)] [(X₃ : C₃) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C₂) (F₂.flip.obj X₃)] {r : I₁ × I₂ × I₃J} {π : I₁ × I₃J} (τ : CategoryTheory.GradedObject.TriangleIndexData r π) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁ I₁ I₂).obj X₁).obj ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)).HasMap τ.p₁₂] [(((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂))).obj X₃).HasMap π] [(((CategoryTheory.GradedObject.mapBifunctor F₂ I₂ I₃).obj ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃] [(((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₂ τ.p₂₃ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃)).HasMap π] [CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃] [CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃] [(((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π] (triangle : ∀ (X₁ : C₁) (X₃ : C₃), CategoryTheory.CategoryStruct.comp (((associator.hom.app X₁).app X₂).app X₃) ((G.obj X₁).map (e₂.hom.app X₃)) = (G.map (e₁.hom.app X₁)).app X₃) :