I'm reading Jaroslav Ježek's "Universal algebra". There is a
Theorem. For a signature containing at least one symbol of positive arity, the lattice of varieties of that signature has no coatoms.
The proof is said to be easy, but I'm having hard times trying to prove this theorem. I've tried to prove it for particular signature to find some common pattern. Denote by $\text{Var}(K)$ the variety generated by class of algebras $K$ (if $K$ consists of a single algebra we omit brackets).
Let $\Omega = \{f\}$ be a signature consisting of one unary symbol $f$, and $\mathcal{L}$ be the corrseponding lattice of varieties. It is sufficient to prove that every variety $V$ is strictly contained in some variety $U$ which is not the variety of all $\Omega$-algebras (denote it by $V_\Omega$). Without loss of generality we may assume that $U = \text{Var}(V \cup \{\mathfrak{A}\})$ for some algebra $\mathfrak{A} \notin V$, because if $V \subset U$ for some variety $U$ and $\mathfrak{A} \in U \setminus V$ we have that $V = \text{Var}(V) \subset \text{Var}(V \cup \{\mathfrak{A}\}) \subseteq \text{Var}(U) = U.$
I undestand that we have to use the fact that we are considering the lattice of all varieties of a given signature. It allows us to find an algebra which doesn't satisfy any given non-trivial identity. Otherwise, for example, the lattice of all varieties of lattices belonging to $\text{Var}(N_5)$ (the lattice of all subvarieties of $\text{Var}(N_5)$), which is isomorphic to the chain with 3 elements, has the variety of distributive lattices as its dual atom (and atom also). Note that the lattice of all lattices varieties has no dual atoms.
Now we need to construct such an algebra and this is where I got stuck. Since theorem requires at least one symbol of positive arity I think we also need to use equational theory $E = \text{Eq}(V)$. Since $V \subset V_\Omega$ there is an identity $s \approx t \in E$ other than $x \approx x$. Now we need to find such an algebra $\mathfrak{A}$ which doesn't satisfy $s \approx t$, but satisfies some other non-trivial identity and there should exist a non-trivial identity satisfied both by $V$ and $\mathfrak{A}$. Let $s(x) = f^k(x)$ and $t(y) = f^m(y)$, where $f^n$ means $n$-fold composition of $f$ with itself. I don't understand how should I analyze this and get the desired identity. I'm not even sure if it is possible for a non-trivial variety to satisfy and identity of the form $s(x) \approx t(y)$, where $x, y$ are different variables. It seems that the answer is yes, for example, the identity $f(x) = f(y)$ is satisfied by algebras of arbitrary cardinality where $f$ is interpreted as an unary constant operation. But if it is so, it makes the situation even harder.
Can you give me a hint on how to proceed or offer another idea if my approach (if this word can be used to describe my weak attempts) is flawed? Thank you!
This is a rewrite of my original answer but the proof idea remains the same.
Recall that $s\approx t$ is an immediate consequence of $u \approx v$ if $s$ can be obtained from $t$ by replacing one occurence of a subterm $r(u)$, for some substitution $r$, with $r(v)$. Note that $\vert s\vert \geq \vert u \vert$ and $\vert t \vert \geq \vert v \vert$, since every substitution (a.k.a. term algebra endomorphism) is determined by where it sends the generators $x_i$ and each generator is of height 1. Hence, a substitution can only increase the height of a term. Theorem 3.1 in Ježek's notes says that $B\vdash u\approx v$ iff the is a finite sequence $u_0,\ldots,u_k$ such that $u=u_0$, $v=u_k$, and each $u_i\approx u_{i+1}$ is an immediate consequence of some equation in $B$.
Let $V$ be a proper subvariety of $V_\Omega$. So $\mathrm{Eq}(V)$ is a nontrivial equational theory. Since the lattice of equational theories is algebraic, $\mathrm{Eq}(V)$ is a join of compact equational theories. Choose nontrivial compact $B$ such that $B\subseteq \mathrm{Eq}(V)$. Then $V\subseteq\mathrm{Mod}(B)$. Consider $f(B)=\{f(u)\approx f(v):u\approx v \in B\}$ where $f$ is a unary symbol in $\Omega$.
Claim: $\mathrm{Mod}(B)\subsetneq\mathrm{Mod}(f(B))\subsetneq V_\Omega$.
To prove the claim, choose $s\approx t\in B$ such that $\vert s \vert + \vert t \vert$ is a minimum. Suppose, by way of contradiction, that $f(B)\vdash s\approx t$. Then there is sequence $s_0,\ldots,s_k$ such that $s=s_0$, $t=s_k$, and each $s_i\approx s_{i+1}$ is an immediate consequence of some $f(u)\approx f(v)$ in $f(B)$. Then $\vert s \vert \geq \vert f(u)\vert=\vert u\vert +1$ and $\vert t\vert\geq \vert f(v)\vert = \vert v \vert +1$. A contradiction, since $\vert s\vert + \vert t \vert$ was a minimum. Thus $f(B)\not\vdash s\approx t$ and $\mathrm{Mod}(B)\subsetneq\mathrm{Mod}(f(B))$. The other proper inclusion in the claim follows from the fact that $f(B)$ contains a nontrivial identity.