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
- CategoryTheory.TwoSquare T L R B = (T.comp R ⟶ L.comp B)
@[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
- CategoryTheory.TwoSquare.mk T L R B α = α
@[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)
:
The natural transfomration associated to a 2-square.
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₄)
:
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
- CategoryTheory.TwoSquare.equivNatTrans T L R B = { toFun := CategoryTheory.TwoSquare.natTrans, invFun := CategoryTheory.TwoSquare.mk T L R B, left_inv := ⋯, right_inv := ⋯ }
@[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)
:
@[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)
:
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)
:
The opposite of a 2-square.
Equations
@[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)
:
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}
:
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
@[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
- CategoryTheory.TwoSquare.«term𝟙ₕ» = Lean.ParserDescr.node `CategoryTheory.TwoSquare.«term𝟙ₕ» 1024 (Lean.ParserDescr.symbol "𝟙ₕ")
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
@[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
- CategoryTheory.TwoSquare.«term𝟙ᵥ» = Lean.ParserDescr.node `CategoryTheory.TwoSquare.«term𝟙ᵥ» 1024 (Lean.ParserDescr.symbol "𝟙ᵥ")
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
- w.whiskerTop α = CategoryTheory.TwoSquare.mk T L R B (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight α R) w.natTrans)
@[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
- w.whiskerLeft α = CategoryTheory.TwoSquare.mk T L' R B (CategoryTheory.CategoryStruct.comp w.natTrans (CategoryTheory.whiskerRight α B))
@[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
- w.whiskerRight α = CategoryTheory.TwoSquare.mk T L R B (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft T α) w.natTrans)
@[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
- w.whiskerBottom α = CategoryTheory.TwoSquare.mk T L R B' (CategoryTheory.CategoryStruct.comp w.natTrans (CategoryTheory.whiskerLeft L α))
@[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')
:
The horizontal composition of 2-squares.
Equations
- One or more equations did not get rendered due to their size.
@[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₁)
:
Notation for the horizontal composition of 2-squares.
Equations
- One or more equations did not get rendered due to their size.
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'')
:
The vertical composition of 2-squares.
Equations
- One or more equations did not get rendered due to their size.
@[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₁)
:
Notation for the vertical composition of 2-squares.
Equations
- One or more equations did not get rendered due to their size.
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₃)
:
When composing 2-squares which form a diagram of grid, compositing horionzall first yields the same result as composing vertically first.