doc-next-gen

Mathlib.CategoryTheory.Functor.TwoSquare

Module docstring

{"# 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.

"}

CategoryTheory.TwoSquare definition
Full source 
/-- 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. -/
def TwoSquare := T ⋙ RT ⋙ R ⟶ L ⋙ B
2-Square of Functors
Informal description
A 2-square `TwoSquare T L R B` is a natural transformation \( w : T \circ R \to L \circ B \) between the compositions of four functors \( T, L, R, B \) arranged as follows: ``` T C₁ ⥤ C₂ L | | R v v C₃ ⥤ C₄ B ``` Here, \( T \) is the top functor, \( L \) is the left functor, \( R \) is the right functor, and \( B \) is the bottom functor. The natural transformation \( w \) connects the compositions \( T \circ R \) and \( L \circ B \).
CategoryTheory.TwoSquare.mk abbrev
(α : T ⋙ R ⟶ L ⋙ B) : TwoSquare T L R B
Full source 
/-- Constructor for `TwoSquare`. -/
abbrev mk (α : T ⋙ RT ⋙ R ⟶ L ⋙ B) : TwoSquare T L R B := α
Constructor for 2-Square of Functors
Informal description
Given a natural transformation $\alpha \colon T \circ R \to L \circ B$ between the compositions of functors $T, R, L, B$, the constructor `TwoSquare.mk` forms a 2-square diagram: ``` T C₁ ⥤ C₂ L | | R v v C₃ ⥤ C₄ B ``` where $T$ is the top functor, $L$ is the left functor, $R$ is the right functor, and $B$ is the bottom functor.
CategoryTheory.TwoSquare.natTrans abbrev
(w : TwoSquare T L R B) : T ⋙ R ⟶ L ⋙ B
Full source 
/-- The natural transfomration associated to a 2-square. -/
abbrev natTrans (w : TwoSquare T L R B) : T ⋙ RT ⋙ R ⟶ L ⋙ B := w
Natural Transformation of a 2-Square
Informal description
Given a 2-square $w$ consisting of functors $T$, $L$, $R$, and $B$, the natural transformation associated to $w$ is a morphism $T \circ R \to L \circ B$ in the functor category, where $\circ$ denotes functor composition.
CategoryTheory.TwoSquare.equivNatTrans definition
: TwoSquare T L R B ≃ (T ⋙ R ⟶ L ⋙ B)
Full source 
/-- 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`. -/
@[simps]
def equivNatTrans : TwoSquareTwoSquare T L R B ≃ (T ⋙ R ⟶ L ⋙ B) where
  toFun := natTrans
  invFun := mk T L R B
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence between 2-squares and natural transformations
Informal description
The equivalence `TwoSquare T L R B ≃ (T ⋙ R ⟶ L ⋙ B)` establishes a bijection between the type of 2-squares of functors `T, L, R, B` and the type of natural transformations from the composition `T ⋙ R` to `L ⋙ B`. The bijection is given by extracting the natural transformation from a 2-square (via `natTrans`) and constructing a 2-square from a natural transformation (via `mk`), with both operations being mutual inverses.
CategoryTheory.TwoSquare.op definition
(α : TwoSquare T L R B) : TwoSquare L.op T.op B.op R.op
Full source 
/-- The opposite of a `2`-square. -/
def op (α : TwoSquare T L R B) : TwoSquare L.op T.op B.op R.op := NatTrans.op α
Opposite 2-square of functors
Informal description
Given a 2-square $\alpha$ consisting of four functors $T, L, R, B$ and a natural transformation $w : T \circ R \to L \circ B$, the opposite 2-square $\alpha^{\mathrm{op}}$ is the natural transformation obtained by applying the opposite operation to $w$, resulting in a 2-square with the functors $L^{\mathrm{op}}, T^{\mathrm{op}}, B^{\mathrm{op}}, R^{\mathrm{op}}$ arranged as follows: ``` L.op C₃ᵒᵖ ⥤ C₁ᵒᵖ T.op | | B.op v v C₂ᵒᵖ ⥤ C₄ᵒᵖ R.op ``` Here, the natural transformation $w^{\mathrm{op}} : L^{\mathrm{op}} \circ T^{\mathrm{op}} \to B^{\mathrm{op}} \circ R^{\mathrm{op}}$ is the opposite of the original natural transformation $w$.
CategoryTheory.TwoSquare.natTrans_op theorem
(α : TwoSquare T L R B) : α.op.natTrans = NatTrans.op α.natTrans
Full source 
@[simp]
lemma natTrans_op (α : TwoSquare T L R B) :
    α.op.natTrans = NatTrans.op α.natTrans := rfl
Natural Transformation of Opposite 2-Square Equals Opposite Natural Transformation
Informal description
For any 2-square $\alpha$ consisting of functors $T$, $L$, $R$, $B$ with natural transformation $w : T \circ R \to L \circ B$, the natural transformation of the opposite 2-square $\alpha^{\mathrm{op}}$ is equal to the opposite natural transformation of $w$, i.e., $\alpha^{\mathrm{op}}.\mathrm{natTrans} = w^{\mathrm{op}}$.
CategoryTheory.TwoSquare.ext theorem
(w w' : TwoSquare T L R B) (h : ∀ (X : C₁), w.natTrans.app X = w'.natTrans.app X) : w = w'
Full source 
@[ext]
lemma ext (w w' : TwoSquare T L R B) (h : ∀ (X : C₁), w.natTrans.app X = w'.natTrans.app X) :
    w = w' :=
  NatTrans.ext (funext h)
Extensionality of 2-Squares via Componentwise Equality
Informal description
Given two 2-squares $w$ and $w'$ consisting of functors $T$, $L$, $R$, $B$, if for every object $X$ in the source category $C_1$, the components of their natural transformations agree (i.e., $w.\mathrm{natTrans}.app(X) = w'.\mathrm{natTrans}.app(X)$), then $w = w'$.
CategoryTheory.TwoSquare.hId definition
(L : C₁ ⥤ C₃) : TwoSquare (𝟭 _) L L (𝟭 _)
Full source 
/-- The hoizontal identity 2-square. -/
@[simps!]
def hId (L : C₁ ⥤ C₃) : TwoSquare (𝟭 _) L L (𝟭 _) :=
  𝟙 _
Horizontal identity 2-square
Informal description
Given a functor \( L : C_1 \to C_3 \), the horizontal identity 2-square \( \text{hId} \) is the natural transformation between the compositions of the identity functors and \( L \), forming the following commutative diagram: ``` id C₁ ⥤ C₁ L | | L v v C₃ ⥤ C₃ id ``` Here, the natural transformation is the identity natural transformation \( \text{id} \), ensuring that the diagram commutes trivially.
CategoryTheory.TwoSquare.term𝟙ₕ definition
: Lean.ParserDescr✝
Full source 
/-- Notation for the horizontal identity 2-square. -/
scoped notation "𝟙ₕ" => hId
Horizontal identity 2-square notation
Informal description
The notation `𝟙ₕ` represents the horizontal identity 2-square, which is a natural transformation between functors that acts as the identity in the horizontal direction. Specifically, given a functor `L : C₁ ⥤ C₃`, the horizontal identity 2-square `𝟙ₕ` is defined as `TwoSquare (𝟭 _) L L (𝟭 _)`, where `𝟭 _` denotes the identity functor on the respective category.
CategoryTheory.TwoSquare.vId definition
(T : C₁ ⥤ C₂) : TwoSquare T (𝟭 _) (𝟭 _) T
Full source 
/-- The vertical identity 2-square. -/
@[simps!]
def vId (T : C₁ ⥤ C₂) : TwoSquare T (𝟭 _) (𝟭 _) T :=
  𝟙 _
Vertical identity 2-square
Informal description
The vertical identity 2-square for a functor \( T : C_1 \to C_2 \) is the natural transformation \( \text{id} : T \circ \text{id} \to \text{id} \circ T \) that forms the commutative square: ``` T C₁ ⥤ C₂ 𝟭 | | 𝟭 v v C₁ ⥤ C₂ T ``` Here, \( \text{id} \) denotes the identity functor, and the natural transformation is the identity transformation between the compositions \( T \circ \text{id} \) and \( \text{id} \circ T \).
CategoryTheory.TwoSquare.term𝟙ᵥ definition
: Lean.ParserDescr✝
Full source 
/-- Notation for the vertical identity 2-square. -/
scoped notation "𝟙ᵥ" => vId
Vertical identity 2-square notation
Informal description
The notation `𝟙ᵥ` represents the vertical identity 2-square, which is a natural transformation between functors forming a commutative square where the left and right functors are identity functors.
CategoryTheory.TwoSquare.whiskerTop definition
{T' : C₁ ⥤ C₂} (w : TwoSquare T' L R B) (α : T ⟶ T') : TwoSquare T L R B
Full source 
/-- Whiskering a 2-square with a natural transformation at the top. -/
@[simps!]
protected def whiskerTop {T' : C₁ ⥤ C₂} (w : TwoSquare T' L R B) (α : T ⟶ T') : TwoSquare T L R B :=
  .mk _ _ _ _ <| whiskerRightwhiskerRight α R ≫ w.natTrans
Top whiskering of a 2-square of functors
Informal description
Given a 2-square \( w \) of functors \( T', L, R, B \) and a natural transformation \( \alpha \colon T \to T' \), the whiskering \( w \circ \alpha \) at the top is the 2-square \( T, L, R, B \) obtained by composing the right whiskering of \( \alpha \) with \( R \) and the natural transformation of \( w \). In other words, the resulting 2-square has the natural transformation \( (\alpha \circ R) \cdot w \), where \( \cdot \) denotes vertical composition of natural transformations.
CategoryTheory.TwoSquare.whiskerLeft definition
{L' : C₁ ⥤ C₃} (w : TwoSquare T L R B) (α : L ⟶ L') : TwoSquare T L' R B
Full source 
/-- Whiskering a 2-square with a natural transformation at the left side. -/
@[simps!]
protected def whiskerLeft {L' : C₁ ⥤ C₃} (w : TwoSquare T L R B) (α : L ⟶ L') :
    TwoSquare T L' R B :=
  .mk _ _ _ _ <| w.natTrans ≫ whiskerRight α B
Left whiskering of a 2-square of functors
Informal description
Given a 2-square \( w \) of functors \( T, L, R, B \) and a natural transformation \( \alpha \colon L \to L' \), the left whiskering \( \text{whiskerLeft}\, w\, \alpha \) constructs a new 2-square with the left functor replaced by \( L' \). The natural transformation of the resulting 2-square is obtained by composing \( w \)'s natural transformation with the right whiskering of \( \alpha \) by \( B \).
CategoryTheory.TwoSquare.whiskerRight definition
{R' : C₂ ⥤ C₄} (w : TwoSquare T L R' B) (α : R ⟶ R') : TwoSquare T L R B
Full source 
/-- Whiskering a 2-square with a natural transformation at the right side. -/
@[simps!]
protected def whiskerRight {R' : C₂ ⥤ C₄} (w : TwoSquare T L R' B) (α : R ⟶ R') :
    TwoSquare T L R B :=
  .mk _ _ _ _ <| whiskerLeftwhiskerLeft T α ≫ w.natTrans
Right whiskering of a 2-square of functors
Informal description
Given a 2-square \( w \) of functors \( T, L, R', B \) and a natural transformation \( \alpha \colon R \to R' \), the right whiskering \( \text{whiskerRight}\, w\, \alpha \) constructs a new 2-square with the right functor replaced by \( R \). The natural transformation of the resulting 2-square is obtained by composing the left whiskering of \( \alpha \) by \( T \) with the natural transformation of \( w \). In other words, the resulting 2-square has the natural transformation \( (T \circ \alpha) \cdot w \), where \( \cdot \) denotes vertical composition of natural transformations.
CategoryTheory.TwoSquare.whiskerBottom definition
{B' : C₃ ⥤ C₄} (w : TwoSquare T L R B) (α : B ⟶ B') : TwoSquare T L R B'
Full source 
/-- Whiskering a 2-square with a natural transformation at the bottom. -/
@[simps!]
protected def whiskerBottom {B' : C₃ ⥤ C₄} (w : TwoSquare T L R B) (α : B ⟶ B') :
    TwoSquare T L R B' :=
  .mk _ _ _ _ <| w.natTrans ≫ whiskerLeft L α
Bottom whiskering of a 2-square of functors
Informal description
Given a 2-square \( w \) of functors \( T, L, R, B \) and a natural transformation \( \alpha \colon B \to B' \), the whiskering \( \text{whiskerBottom}\, w\, \alpha \) constructs a new 2-square with the bottom functor replaced by \( B' \). The natural transformation of the resulting 2-square is obtained by composing \( w \)'s natural transformation with the left whiskering of \( \alpha \) by \( L \).
CategoryTheory.TwoSquare.hComp definition
(w : TwoSquare T L R B) (w' : TwoSquare T' R R' B') : TwoSquare (T ⋙ T') L R' (B ⋙ B')
Full source 
/-- The horizontal composition of 2-squares. -/
@[simps!]
def hComp (w : TwoSquare T L R B) (w' : TwoSquare T' R R' B') :
    TwoSquare (T ⋙ T') L R' (B ⋙ B') :=
  .mk _ _ _ _ <| (Functor.associator _ _ _).hom ≫ (whiskerLeft T w'.natTrans) ≫
    (Functor.associator _ _ _).inv ≫ (whiskerRight w.natTrans B') ≫ (Functor.associator _ _ _).hom
Horizontal composition of 2-squares of functors
Informal description
Given two 2-squares of functors \( w : \text{TwoSquare}\, T\, L\, R\, B \) and \( w' : \text{TwoSquare}\, T'\, R\, R'\, B' \), their horizontal composition \( \text{hComp}\, w\, w' \) forms a new 2-square \( \text{TwoSquare}\, (T \circ T')\, L\, R'\, (B \circ B') \). The natural transformation of the resulting 2-square is constructed by composing the associator isomorphisms with the left and right whiskerings of the natural transformations from \( w \) and \( w' \).
CategoryTheory.TwoSquare.term_≫ₕ_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- Notation for the horizontal composition of 2-squares. -/
scoped infixr:80 " ≫ₕ " => hComp
Horizontal composition of 2-squares
Informal description
The notation `≫ₕ` represents the horizontal composition of 2-squares in category theory. Given two 2-squares `w : TwoSquare T L R B` and `w' : TwoSquare T' R R' B'`, the horizontal composition `w ≫ₕ w'` forms a new 2-square `TwoSquare (T ⋙ T') L R' (B ⋙ B')`.
CategoryTheory.TwoSquare.vComp definition
(w : TwoSquare T L R B) (w' : TwoSquare B L' R'' B'') : TwoSquare T (L ⋙ L') (R ⋙ R'') B''
Full source 
/-- The vertical composition of 2-squares. -/
@[simps!]
def vComp (w : TwoSquare T L R B) (w' : TwoSquare B L' R'' B'') :
    TwoSquare T (L ⋙ L') (R ⋙ R'') B'' :=
  .mk _ _ _ _ <| (Functor.associator _ _ _).hom ≫ (whiskerRight w.natTrans R'') ≫
    (Functor.associator _ _ _).inv ≫ (whiskerLeft L w'.natTrans) ≫ (Functor.associator _ _ _).hom
Vertical composition of 2-squares of functors
Informal description
Given two 2-squares of functors: 1. \( w : \text{TwoSquare}\, T\, L\, R\, B \) with natural transformation \( w : T \circ R \to L \circ B \) 2. \( w' : \text{TwoSquare}\, B\, L'\, R''\, B'' \) with natural transformation \( w' : B \circ R'' \to L' \circ B'' \) their vertical composition \( \text{vComp}\, w\, w' \) forms a new 2-square \( \text{TwoSquare}\, T\, (L \circ L')\, (R \circ R'')\, B'' \) with the composed natural transformation obtained by: 1. Applying the associator isomorphism \( (T \circ R) \circ R'' \cong T \circ (R \circ R'') \) 2. Right whiskering \( w \) with \( R'' \) 3. Applying the inverse associator \( L \circ (B \circ R'') \cong (L \circ B) \circ R'' \) 4. Left whiskering \( w' \) with \( L \) 5. Applying the associator \( (L \circ L') \circ B'' \cong L \circ (L' \circ B'') \)
CategoryTheory.TwoSquare.term_≫ᵥ_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- Notation for the vertical composition of 2-squares. -/
scoped infixr:80 " ≫ᵥ " => vComp
Vertical composition of 2-squares
Informal description
The notation `≫ᵥ` represents the vertical composition of 2-squares in category theory. Given two 2-squares `w : TwoSquare T L R B` and `w' : TwoSquare B L' R'' B''`, their vertical composition `w ≫ᵥ w'` forms a new 2-square `TwoSquare T (L ⋙ L') (R ⋙ R'') B''`.
CategoryTheory.TwoSquare.hCompVCompHComp theorem
(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₁ ≫ₕ w₂) ≫ᵥ (w₃ ≫ₕ w₄) = (w₁ ≫ᵥ w₃) ≫ₕ (w₂ ≫ᵥ w₄)
Full source 
/-- When composing 2-squares which form a diagram of grid, compositing horionzall first yields the
same result as composing vertically first. -/
lemma hCompVCompHComp (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₁ ≫ₕ w₂) ≫ᵥ (w₃ ≫ₕ w₄) = (w₁ ≫ᵥ w₃) ≫ₕ (w₂ ≫ᵥ w₄) := by
  unfold hComp vComp whiskerLeft whiskerRight
  ext c
  simp only [Functor.comp_obj, NatTrans.comp_app, Functor.associator_hom_app,
    Functor.associator_inv_app, comp_id, id_comp, Functor.map_comp, assoc]
  slice_rhs 2 3 =>
    rw [← Functor.comp_map _ B₃, ← w₄.naturality]
  simp
Interchange Law for Horizontal and Vertical Composition of 2-Squares
Informal description
Given four 2-squares of functors: 1. $w_1 : \text{TwoSquare}\, T\, L\, R\, B$ with natural transformation $w_1 : T \circ R \to L \circ B$ 2. $w_2 : \text{TwoSquare}\, T'\, R\, R'\, B'$ with natural transformation $w_2 : T' \circ R' \to R \circ B'$ 3. $w_3 : \text{TwoSquare}\, B\, L'\, R''\, B''$ with natural transformation $w_3 : B \circ R'' \to L' \circ B''$ 4. $w_4 : \text{TwoSquare}\, B'\, R''\, R_3\, B_3$ with natural transformation $w_4 : B' \circ R_3 \to R'' \circ B_3$ the following interchange law holds: $$(w_1 \text{≫ₕ} w_2) \text{≫ᵥ} (w_3 \text{≫ₕ} w_4) = (w_1 \text{≫ᵥ} w_3) \text{≫ₕ} (w_2 \text{≫ᵥ} w_4)$$ Here, $\text{≫ₕ}$ denotes horizontal composition and $\text{≫ᵥ}$ denotes vertical composition of 2-squares.