The Lattice of Congruences of a Finite Line Frame

TL;DR

This paper studies the structure of the lattice of congruences in finite line frames, providing explicit descriptions of joins and meets, and revealing their embedding into divisor lattices.

Contribution

It offers concrete descriptions of the lattice operations and shows embeddings into divisor lattices for finite line frame congruences, advancing understanding of their algebraic structure.

Findings

Join and meet of congruences are explicitly characterized.

Intervals in the congruence lattice embed into divisor lattices.

Any two congruences with a nontrivial upper bound permute.

Abstract

Let $\mathbf{F}=\left\langle F,R\right\rangle $ be a finite Kripke frame. A congruence of $\mathbf{F}$ is a bisimulation of $\mathbf{F}$ that is also an equivalence relation on F. The set of all congruences of $\mathbf{F}$ is a lattice under the inclusion ordering. In this article we investigate this lattice in the case that $\mathbf{F}$ is a finite line frame. We give concrete descriptions of the join and meet of two congruences with a nontrivial upper bound. Through these descriptions we show that for every nontrivial congruence $\rho$, the interval $[\mathrm{Id_{F},\rho]}$ embeds into the lattice of divisors of a suitable positive integer. We also prove that any two congruences with a nontrivial upper bound permute.