Given an algebraic structure $F(K)$ freely generated by a set $K$ with underlying set $U(F(K))$, I'm trying to define a "support" map $\mathrm{supp} : U(F(K)) \rightarrow \mathcal{P}_\mathrm{fin}(K).$ The idea is that $\mathrm{supp}$ accepts a $u \in U(F(K))$ and returns the set of all $k \in K$ such that $k$ makes a "non-trivial" appearance in $u$.
For example. Suppose we're talking about group theory. Then $F$ is the free functor $$\mathbf{Set} \rightarrow \mathbf{Grp}.$$
Hence $y^2x$ represents an element of $F(\{x,y,z\}),$ and we should have $$\mathrm{supp}(y^2 x) = \{x,y\},$$
since $z$ makes no appearance in $y^2 x$ and both $x$ and $y$ make "non-trivial" appearances.
On the other hand, $yy^{-1}x$ also represents an element of $F(\{x,y,z\}),$ and we should have $$\mathrm{supp}(yy^{-1} x) =\{x\},$$ since $y$ only "features trivially" in the expression $yy^{-1} x.$
Question 0. How to define the function $\mathrm{supp}$ more precisely?
Question 1. Is there a sleek, category-theoretic definition of $\mathrm{supp}$?
My thoughts: Both $U \circ F$ and $\mathcal{P}_\mathrm{fin}$ can be viewed as monads on $\mathbf{Set}$. We're trying to define an "arrow" $\mathrm{supp} : U \circ F \rightarrow \mathcal{P}_\mathrm{fin}$ of some description. I'm not 100% sure what "arrow" should mean in this context; perhaps "natural transformation + some additional structure."
Question 0: Here's a reasonable definition.
For every finite subset $K'\subseteq K$, we can view $F(K')$ as a subalgebra of $F(K)$ (the inclusion map is obtained by applying the free functor to the inclusion map of sets $K'\hookrightarrow K$). For $t\in F(K)$, $\text{supp}(t)$ is the smallest subset $K'$ such that $t$ is in $F(K')$.
I'll leave it to you to verify that this definition makes sense. The main thing you have to check is that if $t\in F(K')$ and $t\in F(K'')$ (viewing both as subalgebras of $F(K)$), then $t\in F(K'\cap K'')$.
Question 1: How to categorify this? If you're familiar with adjunctions (specifically adjunctions between posets, or Galois connections), the definition above might have a familiar ring to it. But to really make it into an adjunction, we have to extend $\text{supp}$ to be a map on subsets of $F(K)$, not elements.
We view $\mathcal{P}(K)$ and $\mathcal{P}(F(K))$ as posets under $\subseteq$, i.e. categories in which there is at most one morphism between any pair of objects. Then $F$ is a functor from $\mathcal{P}(K)$ to $\mathcal{P}(F(K))$, sending $K'\subseteq K$ to $F(K')$ viewed as a subalgebra of $F(K)$.
Now we define $\text{supp}$ to be the left adjoint to this functor. Given a subset $T\subseteq F(K)$ and a subset $K'\subseteq K$, we want to have $T\subseteq F(K')$ if and only if $\text{supp}(T) \subseteq K'$. That is, $\text{supp}(T)$ is the smallest subset $K''\subseteq K$ such that every element of $T$ is in $F(K'')$. Then $\text{supp}(t)$ as defined above is just $\text{supp}(\{t\})$ as defined here.
It's worth noting that a functor between posets has a left adjoint if and only if it preserves meets (which are the products in the poset category). So we're guaranteed that the left adjoint to $F$ exists as long as $F(K')\cap F(K'') = F(K'\cap K'')$. This is exactly what we had to check, in the form $t\in F(K')\cap F(K'')$ iff $t\in F(K'\cap K'')$, to verify that the original definition made sense.
Edit: Oops, I just realized that the fact I didn't prove isn't true in general. Consider the algebraic theory in the language with a single binary operation axiomatized by $x\cdot x = y\cdot y$. In the free algebra on $\{x,y\}$, let $t = x^2 = y^2$. Then $t\in F(\{x\})\cap F(\{y\})$, but $t\notin F(\emptyset) = \emptyset$. It seems clear in this case that the $\text{supp}$ function is not well defined.
So I suggest that you should only define $\text{supp}$ for theories in which $F(K')\cap F(K'') = F(K'\cap K'')$ as subalgebras of $F(K)$ whenever $K',K''\subseteq K$.
This condition is equivalent to the following syntactic condition: Whenever $T$ implies the identity $t_1(\overline{x}) = t_2(\overline{y})$, $T$ also implies an identity of the form $t_1(\overline{x}) = t_3(\overline{z})$, where each variable in $\overline{z}$ occurs in both $\overline{x}$ and $\overline{y}$.