IV.D250 — Profinite Limit hatalpha

The profinite limit hat{alpha} := varprojlim_n alpha_n is the set of coherent threads (x_1, x_2, ...) with x_n in alpha_n and rho_n(x_n) = x_{n+1}. It captures all levels simultaneously as a categorical limit in the category of directed systems, with omega as the formal boundary.