Commuting squares of identifications
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Raymond Baker and Tom de Jong.
Created on 2023-02-18.
Last modified on 2024-07-23.
module foundation.commuting-squares-of-identifications where open import foundation-core.commuting-squares-of-identifications public
Imports
open import foundation.dependent-pair-types open import foundation.path-algebra open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.identity-types
Idea
A square of identifications
top
x -------> y
| |
left | | right
∨ ∨
z -------> w
bottom
is said to be a
commuting square¶
if there is an identification left ∙ bottom ＝ top ∙ right. Such an
identification is called a
coherence¶
of the square.
Concatenating identifications of edges and coherences of commuting squares of identifications
Consider a commuting square of identifications and an identification of one of the four sides with another identification, as for example in the diagram below:
top
a ---------> b
| | |
left | right |=| right'
∨ ∨ ∨
c ---------> d.
bottom
Then any identification witnessing that the square commutes can be concatenated with the identification on the side, to obtain a new commuting square of identifications.
Concatenating identifications of the top edge with a coherence of a commuting square of identifications
Consider a commuting diagram of identifications
top'
------->
x -------> y
| top |
left | | right
∨ ∨
z -------> w.
bottom
with an identification top ＝ top'. Then we get an equivalence
top top'
x -------> y x -------> y
| | | |
left | | right ≃ left | | right
∨ ∨ ∨ ∨
z -------> w z -------> w.
bottom bottom
module _ {l : Level} {A : UU l} {x y z w : A} (top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) {top' : x ＝ y} (s : top ＝ top') where abstract is-equiv-concat-top-identification-coherence-square-identifications : is-equiv ( concat-top-identification-coherence-square-identifications top left right bottom s) is-equiv-concat-top-identification-coherence-square-identifications = is-equiv-is-invertible ( inv-concat-top-identification-coherence-square-identifications top left right bottom s) ( is-section-inv-concat-top-identification-coherence-square-identifications top left right bottom s) ( is-retraction-inv-concat-top-identification-coherence-square-identifications top left right bottom s) equiv-concat-top-identification-coherence-square-identifications : coherence-square-identifications top left right bottom ≃ coherence-square-identifications top' left right bottom pr1 equiv-concat-top-identification-coherence-square-identifications = concat-top-identification-coherence-square-identifications top left right bottom s pr2 equiv-concat-top-identification-coherence-square-identifications = is-equiv-concat-top-identification-coherence-square-identifications
Concatenating identifications of the left edge with a coherence of a commuting square of identifications
Consider a commuting diagram of identifications
top
x -------> y
| | |
left' | | left | right
∨ ∨ ∨
z -------> w.
bottom
with an identification left ＝ left'. Then we get an equivalence
top top
x -------> y x -------> y
| | | |
left | | right ≃ left' | | right
∨ ∨ ∨ ∨
z -------> w z -------> w.
bottom bottom
module _ {l : Level} {A : UU l} {x y z w : A} (top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) {left' : x ＝ z} (s : left ＝ left') where abstract is-equiv-concat-left-identification-coherence-square-identifications : is-equiv ( concat-left-identification-coherence-square-identifications top left right bottom s) is-equiv-concat-left-identification-coherence-square-identifications = is-equiv-is-invertible ( inv-concat-left-identification-coherence-square-identifications top left right bottom s) ( is-section-inv-concat-left-identification-coherence-square-identifications top left right bottom s) ( is-retraction-inv-concat-left-identification-coherence-square-identifications top left right bottom s) equiv-concat-left-identification-coherence-square-identifications : coherence-square-identifications top left right bottom ≃ coherence-square-identifications top left' right bottom pr1 equiv-concat-left-identification-coherence-square-identifications = concat-left-identification-coherence-square-identifications top left right bottom s pr2 equiv-concat-left-identification-coherence-square-identifications = is-equiv-concat-left-identification-coherence-square-identifications
Concatenating identifications of the right edge with a coherence of a commuting square of identifications
Consider a commuting diagram of identifications
top
x -------> y
| | |
left | right | | right'
∨ ∨ ∨
z -------> w.
bottom
with an identification right ＝ right'. Then we get an equivalence
top top
x -------> y x -------> y
| | | |
left | | right ≃ left | | right'
∨ ∨ ∨ ∨
z -------> w z -------> w.
bottom bottom
module _ {l : Level} {A : UU l} {x y z w : A} (top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) {right' : y ＝ w} (s : right ＝ right') where abstract is-equiv-concat-right-identification-coherence-square-identifications : is-equiv ( concat-right-identification-coherence-square-identifications top left right bottom s) is-equiv-concat-right-identification-coherence-square-identifications = is-equiv-is-invertible ( inv-concat-right-identification-coherence-square-identifications top left right bottom s) ( is-section-inv-concat-right-identification-coherence-square-identifications top left right bottom s) ( is-retraction-inv-concat-right-identification-coherence-square-identifications top left right bottom s) equiv-concat-right-identification-coherence-square-identifications : coherence-square-identifications top left right bottom ≃ coherence-square-identifications top left right' bottom pr1 equiv-concat-right-identification-coherence-square-identifications = concat-right-identification-coherence-square-identifications top left right bottom s pr2 equiv-concat-right-identification-coherence-square-identifications = is-equiv-concat-right-identification-coherence-square-identifications
Concatenating identifications of the bottom edge with a coherence of a commuting square of identifications
Consider a commuting diagram of identifications
top
x -------> y
| |
left | | right
∨ bottom ∨
z -------> w.
------->
bottom'
with an identification bottom ＝ bottom'. Then we get an equivalence
top top
x -------> y x -------> y
| | | |
left | | right ≃ left | | right
∨ ∨ ∨ ∨
z -------> w z -------> w.
bottom bottom'
module _ {l : Level} {A : UU l} {x y z w : A} (top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) {bottom' : z ＝ w} (s : bottom ＝ bottom') where is-equiv-concat-bottom-identification-coherence-square-identifications : is-equiv ( concat-bottom-identification-coherence-square-identifications top left right bottom s) is-equiv-concat-bottom-identification-coherence-square-identifications = is-equiv-is-invertible ( inv-concat-bottom-identification-coherence-square-identifications top left right bottom s) ( is-section-inv-concat-bottom-identification-coherence-square-identifications top left right bottom s) ( is-retraction-inv-concat-bottom-identification-coherence-square-identifications top left right bottom s) equiv-concat-bottom-identification-coherence-square-identifications : coherence-square-identifications top left right bottom ≃ coherence-square-identifications top left right bottom' pr1 equiv-concat-bottom-identification-coherence-square-identifications = concat-bottom-identification-coherence-square-identifications top left right bottom s pr2 equiv-concat-bottom-identification-coherence-square-identifications = is-equiv-concat-bottom-identification-coherence-square-identifications
Whiskering and splicing coherences of commuting squares of identifications
Given a commuting square of identifications
top
x -------> y
| |
left | | right
∨ ∨
z -------> w,
bottom
we may consider four ways of attaching new identifications to it:
-
Prepending
p : u ＝ xto the left gives us a commuting squarep ∙ top u -------> y | | p ∙ left | | right ∨ ∨ z -------> w. bottomMore precisely, we have an equivalence
(left ∙ bottom ＝ top ∙ right) ≃ ((p ∙ left) ∙ bottom ＝ (p ∙ top) ∙ right). -
Appending an identification
p : w ＝ uto the right gives a commuting square of identificationstop x ------------> y | | left | | right ∙ p ∨ ∨ z ------------> u. bottom ∙ pMore precisely, we have an equivalence
(left ∙ bottom ＝ top ∙ right) ≃ (left ∙ (bottom ∙ p) ＝ top ∙ (right ∙ p)). -
Splicing an identification
p : z ＝ uand its inverse into the middle gives a commuting square of identificationstop x --------------> y | | left ∙ p | | right ∨ ∨ u --------------> w. p⁻¹ ∙ bottomMore precisely, we have an equivalence
(left ∙ bottom ＝ top ∙ right) ≃ ((left ∙ p) ∙ (p⁻¹ ∙ bottom) ＝ top ∙ right).Similarly, we have an equivalence
(left ∙ bottom ＝ top ∙ right) ≃ ((left ∙ p⁻¹) ∙ (p ∙ bottom) ＝ top ∙ right). -
Splicing an identification
p : y ＝ uand its inverse into the middle gives a commuting square of identificationstop ∙ p x --------> u | | left | | p⁻¹ ∙ right ∨ ∨ z --------> w. bottomMore precisely, we have an equivalence
(left ∙ bottom ＝ top ∙ right) ≃ (left ∙ bottom ＝ (top ∙ p) ∙ (p⁻¹ ∙ right)).Similarly, we have an equivalence
(left ∙ bottom ＝ top ∙ right) ≃ (left ∙ bottom ＝ (top ∙ p⁻¹) ∙ (p ∙ right)).
These operations are useful in proofs involving path algebra, because taking
equiv-right-whisker-concat-coherence-square-identifications as an example, it
provides us with two maps: the forward direction states
(p ∙ r ＝ q ∙ s) → (p ∙ (r ∙ t)) ＝ q ∙ (s ∙ t)), which allows one to append
an identification without needing to reassociate on the right, and the backwards
direction conversely allows one to cancel out an identification in parentheses.
Left whiskering coherences of commuting squares of identifications
For any identification p : u ＝ x we obtain an equivalence
top p ∙ top
x -------> y u -------> y
| | | |
left | | right ≃ p ∙ left | | right
∨ ∨ ∨ ∨
z -------> w z -------> w
bottom bottom
of coherences of commuting squares of identifications.
module _ {l : Level} {A : UU l} {x y z w u : A} where equiv-left-whisker-concat-coherence-square-identifications : (p : u ＝ x) (top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) → coherence-square-identifications top left right bottom ≃ coherence-square-identifications (p ∙ top) (p ∙ left) right bottom equiv-left-whisker-concat-coherence-square-identifications refl top left right bottom = id-equiv
Right whiskering coherences of commuting squares of identifications
For any identification p : w ＝ u we obtain an equivalence
top top
x -------> y x ------------> y
| | | |
left | | right ≃ left | | right ∙ p
∨ ∨ ∨ ∨
z -------> w z ------------> w
bottom bottom ∙ p
of coherences of commuting squares of identifications.
module _ {l : Level} {A : UU l} {x y z w : A} (top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) where equiv-right-whisker-concat-coherence-square-identifications : {u : A} (p : w ＝ u) → coherence-square-identifications top left right bottom ≃ coherence-square-identifications top left (right ∙ p) (bottom ∙ p) equiv-right-whisker-concat-coherence-square-identifications refl = ( equiv-concat-bottom-identification-coherence-square-identifications ( top) ( left) ( right ∙ refl) ( bottom) ( inv right-unit)) ∘e ( equiv-concat-right-identification-coherence-square-identifications ( top) ( left) ( right) ( bottom) ( inv right-unit))
Left splicing coherences of commuting squares of identifications
For any inverse pair of identifications p : y ＝ u and q : u ＝ y equipped
with α : inv p ＝ q we obtain an equivalence
top top
x -------> y x -----------> y
| | | |
left | | right ≃ left ∙ p | | right
∨ ∨ ∨ ∨
z -------> w u -----------> w
bottom q ∙ bottom
of coherences of commuting squares of identifications.
module _ {l : Level} {A : UU l} {x y z w : A} (top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) where equiv-left-splice-coherence-square-identifications : {u : A} (p : z ＝ u) (q : u ＝ z) (α : inv p ＝ q) → coherence-square-identifications top left right bottom ≃ coherence-square-identifications top (left ∙ p) right (q ∙ bottom) equiv-left-splice-coherence-square-identifications refl .refl refl = equiv-concat-left-identification-coherence-square-identifications ( top) ( left) ( right) ( bottom) ( inv right-unit)
Right splicing coherences of commuting squares of identifications
For any inverse pair of identifications p : y ＝ u and q : u ＝ y equipped
with α : inv p ＝ q we obtain an equivalence
top top ∙ p
x -------> y x --------> u
| | | |
left | | right ≃ left | | q ∙ right
∨ ∨ ∨ ∨
z -------> w z --------> w
bottom bottom
of coherences of commuting squares of identifications.
module _ {l : Level} {A : UU l} {x y z w : A} (top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) where equiv-right-splice-coherence-square-identifications : {u : A} (p : y ＝ u) (q : u ＝ y) (α : inv p ＝ q) → coherence-square-identifications top left right bottom ≃ coherence-square-identifications (top ∙ p) left (inv p ∙ right) bottom equiv-right-splice-coherence-square-identifications refl .refl refl = equiv-concat-top-identification-coherence-square-identifications ( top) ( left) ( right) ( bottom) ( inv right-unit)
Double whiskering of commuting squares of identifications
module _ {l : Level} {A : UU l} {x y z u v w : A} where equiv-double-whisker-coherence-square-identifications : (p : x ＝ y) (top : y ＝ u) (left : y ＝ z) (right : u ＝ v) (bottom : z ＝ v) (s : v ＝ w) → coherence-square-identifications top left right bottom ≃ coherence-square-identifications ( p ∙ top) ( p ∙ left) ( right ∙ s) ( bottom ∙ s) equiv-double-whisker-coherence-square-identifications p top left right bottom q = equiv-left-whisker-concat-coherence-square-identifications p top left ( right ∙ q) ( bottom ∙ q) ∘e equiv-right-whisker-concat-coherence-square-identifications ( top) ( left) ( right) ( bottom) ( q)
Computing the pasting of squares with refl on opposite sides
Consider two squares of identifications as in the diagram
refl
a --------> a
| |
top-left | | top-right
∨ refl ∨
b --------> b
| |
bottom-left | | bottom-right
∨ ∨
c --------> c
refl
Then the pasted square can be computed in terms of the horizontal concatenation of the filler squares
module _ {l : Level} {A : UU l} {a b c : A} where vertical-pasting-coherence-square-identifications-horizontal-refl : (top-left : a ＝ b) (top-right : a ＝ b) (bottom-left : b ＝ c) (bottom-right : b ＝ c) (α : top-left ＝ top-right) (β : bottom-left ＝ bottom-right) → ( inv-coherence-square-identifications-horizontal-refl ( top-left ∙ bottom-left) ( top-right ∙ bottom-right) ( vertical-pasting-coherence-square-identifications ( refl) ( top-left) ( top-right) ( refl) ( bottom-left) ( bottom-right) ( refl) ( coherence-square-identifications-horizontal-refl ( top-left) ( top-right) ( α)) ( coherence-square-identifications-horizontal-refl ( bottom-left) ( bottom-right) ( β)))) ＝ ( horizontal-concat-Id² α β) vertical-pasting-coherence-square-identifications-horizontal-refl refl refl refl refl refl refl = refl vertical-pasting-inv-coherence-square-identifications-horizontal-refl : (top-left : a ＝ b) (top-right : a ＝ b) (bottom-left : b ＝ c) (bottom-right : b ＝ c) (α : coherence-square-identifications refl top-left top-right refl) (β : coherence-square-identifications refl bottom-left bottom-right refl) → ( inv-coherence-square-identifications-horizontal-refl ( top-left ∙ bottom-left) ( top-right ∙ bottom-right) ( vertical-pasting-coherence-square-identifications ( refl) ( top-left) ( top-right) ( refl) ( bottom-left) ( bottom-right) ( refl) ( α) ( β))) ＝ ( horizontal-concat-Id² ( inv-coherence-square-identifications-horizontal-refl ( top-left) ( top-right) ( α)) ( inv-coherence-square-identifications-horizontal-refl ( bottom-left) ( bottom-right) ( β))) vertical-pasting-inv-coherence-square-identifications-horizontal-refl refl refl refl refl refl refl = refl
Recent changes
- 2024-07-23. Raymond Baker. Eckmann-Hilton Updates (#1133).
- 2024-02-19. Fredrik Bakke. Additions for coherently invertible maps (#1024).
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
- 2023-11-05. Fredrik Bakke. Retracts of maps (#900).
- 2023-11-03. Tom de Jong and Fredrik Bakke. Functoriality of suspensions (#898).