A new aspect of the cozero lattice in pointfree topology

The cozero part CozL of a frame L has been studied quite extensively, but invariably from the point of view that it is a σ-frame – a fact proved with the aid of the Axiom of Countable Choice. Here, it will be shown that, for certain purposes, the latter is not required. For this a new description is presented of the realcompletion of a completely regular frame in terms of CozL which does not involve any choice principle. The key to this is the introduction of a particular type of ideal in CozL which amounts to a choice-free form of the σ-ideals usually considered in this context.