Diagonals of morphisms of arrows

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-30.
Last modified on 2024-04-25.

module foundation.diagonals-of-morphisms-arrows where

Imports

Idea

The diagonal^¶ of a morphism of arrows

        i
    A -----> X
    |        |
  f |        | g
    ∨        ∨
    B -----> Y
        j

is obtained by taking the diagonals of the maps i and j, which fit in a naturality square

       Δ i
    A -----> A ×_X A
    |           |
  f |           | functoriality Δ g
    ∨           ∨
    B -----> B ×_Y B.
       Δ j

In other words, the diagonal of a morphism of arrows h : hom-arrow f g is a morphism of arrows `Δ h : hom-arrow f (functoriality Δ g).

Note that this operation preserves cartesian squares. Furthermore, by a lemma of David Wärn it also follows that this operation perserves cocartesian morphisms of arrows out of embeddings.