nLab composable pair

Redirected from "composable pair of morphisms".

Context

Category theory

(,1)(\infty,1)-Category theory

Internal (,1)(\infty,1)-Categories

Directed homotopy type theory

Contents

Definition

In category theory, a composable pair of morphisms in a given category CC consists of objects X,Y,ZX,Y,Z of CC and a pair of morphisms f:XYf\colon X \to Y and g:YZg\colon Y \to Z. The composite of this composable pair is the morphism gf:XZg \circ f\colon X \to Z.

A composable pair in CC is precisely a 2-simplex in the nerve of CC.

Sometimes one defines a composable pair to be a literal pair (f,g)(f,g) such that the target of ff is equal to the source of gg, but this violates the principle of equivalence.

The walking composable pair

The walking composable pair or (2,1)-horn category is the category Λ 1 2\Lambda_1^2 which consists of three objects 0,1,2Λ 1 20, 1, 2 \in \Lambda_1^2 and two morphisms h 01:hom Λ 1 2(0,1)h_{01}:\mathrm{hom}_{\Lambda_1^2}(0, 1) and h 12:hom Λ 1 2(1,2)h_{12}:\mathrm{hom}_{\Lambda_1^2}(1, 2).

The category Λ 1 2\Lambda_1^2 is also called the (2,1)-horn preorder or the (2,1)-horn poset because Λ 1 2\Lambda_1^2 can be shown to be a poset.

Every composable pair in a category CC is represented by a functor F:Λ 1 2CF:\Lambda_1^2 \to C from the walking composable pair to CC. By definition of a category, we have an equivalence of categories between the functor category C 1 Λ2C^\Lambda_1^2 of composable pairs in CC and the functor category C Δ2C^\Delta^2 of commutative triangles in CC.

In dependent type theory, given a directed interval 𝕀\mathbb{I}, the (2,1)-horn type representing the walking composable pair is defined as the type of pairs of elements i,j:𝕀i, j:\mathbb{I} such that i=1i = 1 or j=0j = 0.

Λ 1 2 i:𝕀 j:𝕀(i=1)(j=0)\Lambda_1^2 \coloneqq \sum_{i:\mathbb{I}} \sum_{j:\mathbb{I}} (i = 1) \vee (j = 0)

Unlike the case for the other horns representing the walking span and the walking cospan, the walking composable pair is only a category if there is an axiom stating that every type is a Segal type.

In simplicial type theory

In simplicial type theory, not every composable pair of morphisms has a unique composite forming a commutative triangle, so one has to distinguish between the notions.

Let AA be a type, and let 𝕀\mathbb{I} be the directed interval in simplicial type theory. Recall that the hom-type is defined as

hom A(x,y) f:𝕀A(f(0)=x)×(f(1)=y)\mathrm{hom}_A(x, y) \coloneqq \sum_{f:\mathbb{I} \to A} (f(0) = x) \times (f(1) = y)

A composable pair of morphisms is a record consisting of

  • elements x:Ax:A, y:Ay:A, and z:Az:A

  • a morphism f:hom A(x,y)f:\mathrm{hom}_A(x, y)

  • and a morphism g:hom A(y,z)g:\mathrm{hom}_A(y, z).

The type of composable pairs of morphisms is then the respective record type.

There is another definition involving the (2,1)(2,1)-horn type Λ 1 2\Lambda^2_1, defined from the directed interval as

Λ 1 2 i:𝕀 j:𝕀(i=0)(j=1)\Lambda^2_1 \coloneqq \sum_{i:\mathbb{I}} \sum_{j:\mathbb{I}} (i = 0) \vee (j = 1)

A composable pair of morphisms is simply a function f:Λ 1 2Af:\Lambda^2_1 \to A.

The type of composable pairs of morphisms is then the function type Λ 1 2A\Lambda^2_1 \to A.

References

Last revised on June 1, 2025 at 03:45:16. See the history of this page for a list of all contributions to it.