OAI.FiniteCongruence.graph_criterion

The theorem states that, for any finite type Lat carrying a lattice structure with a least element ⊥, Lat is Representable if and only if it HasGraphWitness. Representable means that there is a positive size n and an algebra on Fin n (a finite list of operations, each of some finite arity, acting on the carrier) such that Lat is order-isomorphic to the poset of congruences of that algebra, where a congruence is an equivalence relation compatible with every operation: if corresponding arguments are related coordinatewise, the outputs are related; congruences are ordered by the inherited order on equivalence relations. HasGraphWitness means that there is a positive size n and a Lat-valued coloring color of ordered pairs from Fin n satisfying five conditions: color is symmetric; color(a,b)=⊥ exactly when a=b; color(a,b) ≤ color(a,m) ⊔ color(m,b) for all a, b, m; whenever lower ≰ upper in Lat, some pair has color ≤ lower but not ≤ upper; and for every nonempty finite set of seed pairs, any pair whose color is at most the join of the seed colors is connected to the seeds. Connected is the equivalence closure of the relation Marked, where a,b are Marked if some self-map p of the vertices satisfies color(p x,p y) ≤ color(x,y) for all x,y and sends some seed pair (s,t) to (a,b).