Around the Stone space's construction for distributive lattices

Following George Grätzer [General Lattice Theory, Second Edition, 2003], we formalize the construction of a Stone space of a distributive lattice and the corresponding representation theorem. We fulfil all the proofs only in terms of an algebraic lattice (i.e., the lattice of all ideals of the underlying lattice) and realize the dual construction for coalgebraic lattices. Introducing the notions of a prime element and a cobase, we show that the Stone-type construction yields an i-topological space for an arbitrary cobase. It is the case of a topological space iff the cobase consists precisely of all prime elements, although an arbitrary cobase does not necessarily contain all prime elements.