CatDat

Implication Details

Assumptions: direct

Conclusions: sequential limits

Reason: Assume that A2A1A0\cdots \to A_2 \to A_1 \to A_0 is a sequence of morphisms. We will prove that almost all of them are identities, so that the sequence is eventually constant and the limit exists. Assume the opposite, i.e. that there are infinitely many AkAk1A_k \to A_{k-1} which are not the identity. Pick some n1n_1 such that An1An11A_{n_1} \to A_{n_1 - 1} is not the identity, and let n0:=n11n_0 := n_1 - 1. If AniAni1A_{n_i} \to A_{n_{i-1}} has been constructed, there is some ni+1>nin_{i+1} > n_i such that the composite Ani+1AniA_{n_{i+1}} \to A_{n_i} is not the identity, because otherwise it would follow inductively that all Ak+1AkA_{k+1} \to A_k, knik \geq n_i would be identities, which would contradict our infiniteness assumption. This way we construct an infinite sequence of non-identity morphisms Ani+1AniA_{n_{i+1}} \to A_{n_i}, a contradiction.