Lattice quotient descent, class intervals and monotone endpoints

Assume $x{\equiv }_{\theta }y$. Apply [F1] to the pairs $(x{\equiv }_{\theta }y,y{\equiv }_{\theta }y)$, the second entry being licensed by reflexivity in [F3]: this gives $x\wedge y{\equiv }_{\theta }y\wedge y$ and $x\vee y{\equiv }_{\theta }y\vee y$. By [F2] with antisymmetry, $y\wedge y=y=y\vee y$, so $x\wedge y{\equiv }_{\theta }y$ and $x\vee y{\equiv }_{\theta }y$.

$C$ is a subset of the finite set $L$, so $C$ is finite with $k:=\mathrm{\mid }C\mathrm{\mid }\le \mathrm{\mid }L\mathrm{\mid }$ by [F4]; since $x\in C$ by [F3], $C\mathrm{\ne }\mathrm{\varnothing }$, hence $k\ge 1$ and there is a bijection $\mathrm{\ell }:k\to C$. Put $z_i:=\mathrm{\ell }(i)$ for $i\in k$, so that $C=\{z_0,\dots ,z_{k-1}\}$. The bijection $\mathrm{\ell }$ is a single witness of an existence statement in the definition of $\mathrm{\mid }C\mathrm{\mid }$; no choice function on a family of sets is used.

Assume $x{\equiv }_{\theta }{x}^{\mathrm{\prime }}$ and $y{\equiv }_{\theta }{y}^{\mathrm{\prime }}$. By [F1], $x\vee y{\equiv }_{\theta }{x}^{\mathrm{\prime }}\vee y^{\mathrm{\prime }}$ and $x\wedge y{\equiv }_{\theta }{x}^{\mathrm{\prime }}\wedge y^{\mathrm{\prime }}$, so $[x\vee y{]}_{\theta }=[x^{\mathrm{\prime }}\vee y^{\mathrm{\prime }}{]}_{\theta }$ and $[x\wedge y{]}_{\theta }=[x^{\mathrm{\prime }}\wedge y^{\mathrm{\prime }}{]}_{\theta }$ by [F3]. Hence the proposed operations $[x{]}_{\theta }\vee [y{]}_{\theta }:=[x\vee y{]}_{\theta }$ and $[x{]}_{\theta }\wedge [y{]}_{\theta }:=[x\wedge y{]}_{\theta }$ do not depend on the chosen representatives, and the class of $x$, hence the proposed pair of endpoints of its class, depends only on $[x{]}_{\theta }$.

Let $z_1,\dots ,z_k$ be a listing of a nonempty finite subfamily of $C$ and define $m_1:=z_1$, $m_j:=m_{j-1}\wedge z_j$ for $2\le j\le k$. By induction on $j$ each $m_j$ lies in $C$: $m_1=z_1\in C$, and if $m_{j-1}\in C$ then $m_{j-1}{\equiv }_{\theta }{z}_j$ because any two members of a class are equivalent by [F3], so step 1.1 gives $m_j=m_{j-1}\wedge z_j{\equiv }_{\theta }{z}_j\in C$. The same induction with $\vee$ in place of $\wedge$ shows that the left-nested iterated join of $z_1,\dots ,z_k$ lies in $C$. The left-nested iterated meet $m_k$ is the meet of the subfamily: it is a common lower bound by [F2], and every common lower bound $w$ satisfies $w\le m_j$ for all $j\le k$ by induction, since $w\le m_{j-1}$ and $w\le z_j$ give $w\le m_{j-1}\wedge z_j=m_j$ by [F2]; dually the iterated join is the join of the subfamily. Hence each class is closed under the meet and the join of any nonempty finite subfamily of its members.

With the well-defined operations of step 1.3, the classes satisfy the lattice identities by transport along representatives: $[x]\wedge [x]=[x\wedge x]=[x]$ and $[x]\vee [x]=[x]$; commutativity $[x]\wedge [y]=[y]\wedge [x]$ and $[x]\vee [y]=[y]\vee [x]$; associativity, because $(x\wedge y)\wedge z$ and $x\wedge (y\wedge z)$ are both the greatest lower bound of $\{x,y,z\}$ — each is a common lower bound, and every common lower bound lies below both by [F2] — hence they are equal by antisymmetry, and dually for $\vee$; and absorption $[x]\wedge ([x]\vee [y])=[x\wedge (x\vee y)]=[x]$, since $x$ is the greatest lower bound of $\{x,x\vee y\}$ by [F2], together with the dual absorption. The projection $x\mapsto [x{]}_{\theta }$ preserves these operations by construction.

For classes $A,B$ define $A\le B$ to mean $A\vee B=B$. The identities of step 2.2 make this a partial order: idempotence gives $A\le A$; if $A\vee B=B$ and $B\vee A=A$, commutativity gives $A=B$; and if $A\vee B=B$ and $B\vee C=C$, then $A\vee C=A\vee (B\vee C)=(A\vee B)\vee C=B\vee C=C$. Moreover $A\le B$ if and only if $A\wedge B=A$: the forward direction is $A\wedge B=A\wedge (A\vee B)=A$ by absorption, and the reverse is $A\vee B=(A\wedge B)\vee B=B$ by commutativity and absorption.

Apply step 2.1 to the listing $z_0,\dots ,z_{k-1}$ of the nonempty finite class $C$ from step 1.2. Its iterated meet $m$ lies in $C$ and is a common lower bound of all its members, so it is a least member of $C$; its iterated join $b$ lies in $C$ and is a common upper bound, so it is a greatest member. Both are unique by [F5], independently of the chosen listing. Define ${\pi }_{\downarrow }(x):=m$ and ${\pi }_{\uparrow }(x):=b$.

The operations are the bounds for the order of step 3.1. Indeed $A\le A\vee B$ since $A\vee (A\vee B)=A\vee B$, and likewise $B\le A\vee B$. If $A\le C$ and $B\le C$, then $(A\vee B)\vee C=A\vee (B\vee C)=A\vee C=C$, so $A\vee B\le C$. Dually $(A\wedge B)\wedge A=A\wedge B$ and $(A\wedge B)\wedge B=A\wedge B$ show $A\wedge B\le A,B$; if $C\le A,B$, then $C\wedge (A\wedge B)=(C\wedge A)\wedge B=C\wedge B=C$, so $C\le A\wedge B$. Thus the classes form the lattice $L\mathrm{/}\theta$ in the order-theoretic sense of [F2].

By the quotient order constructed in step 3.1, $[x{]}_{\theta }\le [y{]}_{\theta }$ if and only if $[x{]}_{\theta }\vee [y{]}_{\theta }=[y{]}_{\theta }$. The operation of step 1.3 identifies the latter equality with $[x\vee y{]}_{\theta }=[y{]}_{\theta }$, which holds if and only if $x\vee y{\equiv }_{\theta }y$ by [F3].

Let $z\in L$. If $z\in C$ then ${\pi }_{\downarrow }(x)\le z\le {\pi }_{\uparrow }(x)$, since these are the least and the greatest member of $C$. Conversely assume ${\pi }_{\downarrow }(x)\le z\le {\pi }_{\uparrow }(x)$ and put $a:={\pi }_{\downarrow }(x)$, $b:={\pi }_{\uparrow }(x)$; both lie in $C$, so $a{\equiv }_{\theta }b$ by [F3]. Apply [F1] to the pairs $a{\equiv }_{\theta }b$ and $z{\equiv }_{\theta }z$: $a\wedge z{\equiv }_{\theta }b\wedge z$. Since $a\le z$ we have $a\wedge z=a$ by [F2], and since $z\le b$ we have $b\wedge z=z$ by [F2]; hence $a{\equiv }_{\theta }z$, so $z\in C$ by [F3]. Therefore $[x{]}_{\theta }=\{z\in L:{\pi }_{\downarrow }(x)\le z\le {\pi }_{\uparrow }(x)\}$, the asserted interval identity.

Monotonicity of the upper endpoint map. Assume $x\le y$. By [F3], ${\pi }_{\uparrow }(x){\equiv }_{\theta }x$ and ${\pi }_{\uparrow }(y){\equiv }_{\theta }y$, so [F1] gives ${\pi }_{\uparrow }(x)\vee {\pi }_{\uparrow }(y){\equiv }_{\theta }x\vee y=y{\equiv }_{\theta }{\pi }_{\uparrow }(y)$; thus ${\pi }_{\uparrow }(x)\vee {\pi }_{\uparrow }(y)$ lies in the class of $y$, whose greatest member is ${\pi }_{\uparrow }(y)$, so ${\pi }_{\uparrow }(x)\vee {\pi }_{\uparrow }(y)\le {\pi }_{\uparrow }(y)$. With ${\pi }_{\uparrow }(y)\le {\pi }_{\uparrow }(x)\vee {\pi }_{\uparrow }(y)$ from [F2], antisymmetry gives ${\pi }_{\uparrow }(x)\vee {\pi }_{\uparrow }(y)={\pi }_{\uparrow }(y)$, and then ${\pi }_{\uparrow }(x)\le {\pi }_{\uparrow }(x)\vee {\pi }_{\uparrow }(y)={\pi }_{\uparrow }(y)$ by [F2].

Monotonicity of the lower endpoint map. Assume $x\le y$. By [F3], ${\pi }_{\downarrow }(x){\equiv }_{\theta }x$ and ${\pi }_{\downarrow }(y){\equiv }_{\theta }y$, so [F1] gives ${\pi }_{\downarrow }(x)\wedge {\pi }_{\downarrow }(y){\equiv }_{\theta }x\wedge y=x{\equiv }_{\theta }{\pi }_{\downarrow }(x)$; thus ${\pi }_{\downarrow }(x)\wedge {\pi }_{\downarrow }(y)$ lies in the class of $x$, whose least member is ${\pi }_{\downarrow }(x)$, so ${\pi }_{\downarrow }(x)\le {\pi }_{\downarrow }(x)\wedge {\pi }_{\downarrow }(y)$. With ${\pi }_{\downarrow }(x)\wedge {\pi }_{\downarrow }(y)\le {\pi }_{\downarrow }(x)$ from [F2], antisymmetry gives equality, and then ${\pi }_{\downarrow }(x)={\pi }_{\downarrow }(x)\wedge {\pi }_{\downarrow }(y)\le {\pi }_{\downarrow }(y)$ by [F2].

Clause (i) is steps 1.1 and 2.1; clause (ii) is steps 1.2, 3.2 and 4.3, where finiteness enters only through the listing $z_0,\dots ,z_{k-1}$ of the finite class and the iterated meet is formed along that listing; clause (iii) is steps 1.3, 2.2, 3.1, 4.1 and 4.2; clause (iv) is steps 4.4 and 4.5. No choice principle is used: the listing is a bijection with a natural number, its existence is a single existential witness, and no family of nonempty sets is selected from.