Documentation

Mathlib.CategoryTheory.Functor.TwoSquare

2-squares of functors #

Given four functors T, L, R and B, a 2-square TwoSquare T L R B consists of a natural transformation w : T ⋙ R ⟶ L ⋙ B:

     T
  C₁ ⥤ C₂
L |     | R
  v     v
  C₃ ⥤ C₄
     B

We define operations to paste such squares horizontally and vertically and prove the interchange law of those two operations.

TODO #

Generalize all of this to double categories.

def CategoryTheory.TwoSquare {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] (T : Functor C₁ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : Functor C₃ C₄) :
Type (max u₁ v₄)

A 2-square consists of a natural transformation T ⋙ R ⟶ L ⋙ B involving fours functors T, L, R, B that are on the top/left/right/bottom sides of a square of categories.

Equations
Instances For
    @[reducible, inline]
    abbrev CategoryTheory.TwoSquare.mk {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] (T : Functor C₁ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : Functor C₃ C₄) (α : T.comp R L.comp B) :
    TwoSquare T L R B

    Constructor for TwoSquare.

    Equations
    Instances For
      @[reducible, inline]
      abbrev CategoryTheory.TwoSquare.natTrans {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} (w : TwoSquare T L R B) :
      T.comp R L.comp B

      The natural transfomration associated to a 2-square.

      Equations
      Instances For
        def CategoryTheory.TwoSquare.equivNatTrans {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] (T : Functor C₁ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : Functor C₃ C₄) :
        TwoSquare T L R B (T.comp R L.comp B)

        The type of 2-squares on functors T, L, R, and B is trivially equivalent to the type of natural transformations T ⋙ R ⟶ L ⋙ B.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.TwoSquare.equivNatTrans_symm_apply {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] (T : Functor C₁ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : Functor C₃ C₄) (α : T.comp R L.comp B) :
          (equivNatTrans T L R B).symm α = mk T L R B α
          @[simp]
          theorem CategoryTheory.TwoSquare.equivNatTrans_apply {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] (T : Functor C₁ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : Functor C₃ C₄) (w : TwoSquare T L R B) :
          (equivNatTrans T L R B) w = w.natTrans
          def CategoryTheory.TwoSquare.op {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} (α : TwoSquare T L R B) :
          TwoSquare L.op T.op B.op R.op

          The opposite of a 2-square.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.TwoSquare.natTrans_op {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} (α : TwoSquare T L R B) :
            theorem CategoryTheory.TwoSquare.ext {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} (w w' : TwoSquare T L R B) (h : ∀ (X : C₁), w.natTrans.app X = w'.natTrans.app X) :
            w = w'
            theorem CategoryTheory.TwoSquare.ext_iff {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {w w' : TwoSquare T L R B} :
            w = w' ∀ (X : C₁), w.natTrans.app X = w'.natTrans.app X
            def CategoryTheory.TwoSquare.hId {C₁ : Type u₁} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₃, u₃} C₃] (L : Functor C₁ C₃) :
            TwoSquare (Functor.id C₁) L L (Functor.id C₃)

            The hoizontal identity 2-square.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.TwoSquare.hId_app {C₁ : Type u₁} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₃, u₃} C₃] (L : Functor C₁ C₃) (X : C₁) :

              Notation for the horizontal identity 2-square.

              Equations
              Instances For
                def CategoryTheory.TwoSquare.vId {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] (T : Functor C₁ C₂) :
                TwoSquare T (Functor.id C₁) (Functor.id C₂) T

                The vertical identity 2-square.

                Equations
                Instances For
                  @[simp]
                  theorem CategoryTheory.TwoSquare.vId_app {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] (T : Functor C₁ C₂) (X : C₁) :

                  Notation for the vertical identity 2-square.

                  Equations
                  Instances For
                    def CategoryTheory.TwoSquare.whiskerTop {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor C₁ C₂} (w : TwoSquare T' L R B) (α : T T') :
                    TwoSquare T L R B

                    Whiskering a 2-square with a natural transformation at the top.

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.TwoSquare.whiskerTop_app {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor C₁ C₂} (w : TwoSquare T' L R B) (α : T T') (X : C₁) :
                      def CategoryTheory.TwoSquare.whiskerLeft {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {L' : Functor C₁ C₃} (w : TwoSquare T L R B) (α : L L') :
                      TwoSquare T L' R B

                      Whiskering a 2-square with a natural transformation at the left side.

                      Equations
                      Instances For
                        @[simp]
                        theorem CategoryTheory.TwoSquare.whiskerLeft_app {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {L' : Functor C₁ C₃} (w : TwoSquare T L R B) (α : L L') (X : C₁) :
                        def CategoryTheory.TwoSquare.whiskerRight {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {R' : Functor C₂ C₄} (w : TwoSquare T L R' B) (α : R R') :
                        TwoSquare T L R B

                        Whiskering a 2-square with a natural transformation at the right side.

                        Equations
                        Instances For
                          @[simp]
                          theorem CategoryTheory.TwoSquare.whiskerRight_app {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {R' : Functor C₂ C₄} (w : TwoSquare T L R' B) (α : R R') (X : C₁) :
                          def CategoryTheory.TwoSquare.whiskerBottom {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B B' : Functor C₃ C₄} (w : TwoSquare T L R B) (α : B B') :
                          TwoSquare T L R B'

                          Whiskering a 2-square with a natural transformation at the bottom.

                          Equations
                          Instances For
                            @[simp]
                            theorem CategoryTheory.TwoSquare.whiskerBottom_app {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B B' : Functor C₃ C₄} (w : TwoSquare T L R B) (α : B B') (X : C₁) :
                            def CategoryTheory.TwoSquare.hComp {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {C₅ : Type u₅} {C₆ : Type u₆} [Category.{v₅, u₅} C₅] [Category.{v₆, u₆} C₆] {T' : Functor C₂ C₅} {R' : Functor C₅ C₆} {B' : Functor C₄ C₆} (w : TwoSquare T L R B) (w' : TwoSquare T' R R' B') :
                            TwoSquare (T.comp T') L R' (B.comp B')

                            The horizontal composition of 2-squares.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem CategoryTheory.TwoSquare.hComp_app {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {C₅ : Type u₅} {C₆ : Type u₆} [Category.{v₅, u₅} C₅] [Category.{v₆, u₆} C₆] {T' : Functor C₂ C₅} {R' : Functor C₅ C₆} {B' : Functor C₄ C₆} (w : TwoSquare T L R B) (w' : TwoSquare T' R R' B') (X : C₁) :
                              (w.hComp w').app X = CategoryStruct.comp (w'.natTrans.app (T.obj X)) (B'.map (w.natTrans.app X))

                              Notation for the horizontal composition of 2-squares.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def CategoryTheory.TwoSquare.vComp {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {C₇ : Type u₇} {C₈ : Type u₈} [Category.{v₇, u₇} C₇] [Category.{v₈, u₈} C₈] {L' : Functor C₃ C₇} {R'' : Functor C₄ C₈} {B'' : Functor C₇ C₈} (w : TwoSquare T L R B) (w' : TwoSquare B L' R'' B'') :
                                TwoSquare T (L.comp L') (R.comp R'') B''

                                The vertical composition of 2-squares.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.TwoSquare.vComp_app {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {C₇ : Type u₇} {C₈ : Type u₈} [Category.{v₇, u₇} C₇] [Category.{v₈, u₈} C₈] {L' : Functor C₃ C₇} {R'' : Functor C₄ C₈} {B'' : Functor C₇ C₈} (w : TwoSquare T L R B) (w' : TwoSquare B L' R'' B'') (X : C₁) :
                                  (w.vComp w').app X = CategoryStruct.comp (R''.map (w.natTrans.app X)) (w'.natTrans.app (L.obj X))

                                  Notation for the vertical composition of 2-squares.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem CategoryTheory.TwoSquare.hCompVCompHComp {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} C₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {C₅ : Type u₅} {C₆ : Type u₆} {C₇ : Type u₇} {C₈ : Type u₈} [Category.{v₅, u₅} C₅] [Category.{v₆, u₆} C₆] [Category.{v₇, u₇} C₇] [Category.{v₈, u₈} C₈] {T' : Functor C₂ C₅} {R' : Functor C₅ C₆} {B' : Functor C₄ C₆} {L' : Functor C₃ C₇} {R'' : Functor C₄ C₈} {B'' : Functor C₇ C₈} {C₉ : Type u₉} [Category.{v₉, u₉} C₉] {R₃ : Functor C₆ C₉} {B₃ : Functor C₈ C₉} (w₁ : TwoSquare T L R B) (w₂ : TwoSquare T' R R' B') (w₃ : TwoSquare B L' R'' B'') (w₄ : TwoSquare B' R'' R₃ B₃) :
                                    (w₁.hComp w₂).vComp (w₃.hComp w₄) = (w₁.vComp w₃).hComp (w₂.vComp w₄)

                                    When composing 2-squares which form a diagram of grid, compositing horionzall first yields the same result as composing vertically first.