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.

source

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)

Instances For

source

@[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 α = α

Instances For

source

@[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

w.natTrans = w

Instances For

source

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

CategoryTheory.TwoSquare.equivNatTrans T L R B = { toFun := CategoryTheory.TwoSquare.natTrans, invFun := CategoryTheory.TwoSquare.mk T L R B, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[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

source

@[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 α

source

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'

source

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

CategoryTheory.TwoSquare.hId L = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C₁).comp L)

Instances For

source

@[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₁) :

(hId L).app X = CategoryStruct.id (L.obj X)

source

def CategoryTheory.TwoSquare.«term𝟙ₕ» :

Lean.ParserDescr

Notation for the horizontal identity 2-square.

Equations

CategoryTheory.TwoSquare.«term𝟙ₕ» = Lean.ParserDescr.node `CategoryTheory.TwoSquare.«term𝟙ₕ» 1024 (Lean.ParserDescr.symbol "𝟙ₕ")

Instances For

source

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

CategoryTheory.TwoSquare.vId T = CategoryTheory.CategoryStruct.id (T.comp (CategoryTheory.Functor.id C₂))

Instances For

source

@[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₁) :

(vId T).app X = CategoryStruct.id (T.obj X)

source

def CategoryTheory.TwoSquare.«term𝟙ᵥ» :

Lean.ParserDescr

Notation for the vertical identity 2-square.

Equations

CategoryTheory.TwoSquare.«term𝟙ᵥ» = Lean.ParserDescr.node `CategoryTheory.TwoSquare.«term𝟙ᵥ» 1024 (Lean.ParserDescr.symbol "𝟙ᵥ")

Instances For

source

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)

Instances For

source

@[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₁) :

(w.whiskerTop α).app X = CategoryStruct.comp (R.map (α.app X)) (w.natTrans.app X)

source

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))

Instances For

source

@[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₁) :

(w.whiskerLeft α).app X = CategoryStruct.comp (w.natTrans.app X) (B.map (α.app X))

source

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)

Instances For

source

@[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₁) :

(w.whiskerRight α).app X = CategoryStruct.comp (α.app (T.obj X)) (w.natTrans.app X)

source

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 α))

Instances For

source

@[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₁) :

(w.whiskerBottom α).app X = CategoryStruct.comp (w.natTrans.app X) (α.app (L.obj X))

source

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

source

@[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))

source

def CategoryTheory.TwoSquare.«term_≫ₕ_» :

Lean.TrailingParserDescr

Notation for the horizontal composition of 2-squares.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

source

@[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))

source

def CategoryTheory.TwoSquare.«term_≫ᵥ_» :

Lean.TrailingParserDescr

Notation for the vertical composition of 2-squares.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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.

Documentation

Mathlib.CategoryTheory.Functor.TwoSquare

2-squares of functors #

TODO #