I am wondering how I might be able to express the following phenomenon, which is essentially equivalent to Artin's linear independence of characters, in Tannakian formalism. Any help would be much appreciated.
Let $k \text{-sep}$ be the category of finite étale $k$-algebras for a field $k$. Let $K$ be the separable closure of $k$, and let $G$ be the absolute Galois group of $k$, which is a profinite group.
From the fundamental theorem of Grothendieck's Galois theory, there is an essentially surjective, fully faithful functor $\Pi : k \text{-sep} \rightarrow G \text{-set}$ into the category of finite continuous $G$-sets. On objects, this functor can be defined by sending a finite étale $k$-algebra $A$ to the set $[A, K]_k$ of $k$-algebra maps from $A$ to $K$ with $G$ action given by sending $\sigma \in G$ and $\iota : A \rightarrow K$ to $\sigma \circ \iota$.
There is a covariant functor $T_{G \text{-set}} : G \text{-set} \rightarrow K \text{-vect}$ sending a $G$-set $X$ to $\oplus_{x \in X} K$. It sends a map $f : X \rightarrow Y$ of $G$-sets to the map $\oplus_{x \in X }K \rightarrow \oplus_{y \in Y} K$ sending the standard basis element corresponding to $x$ to the standard basis element corresponding to $y$.
There is a contravariant functor $T_{k \text{-sep}} : k \text{-sep} \rightarrow K \text{-vect}$ sending a finite étale $k$-algebra $A$ to $\text{Hom}_{k \text{-mod}} (A, K)$ ($k$-vector space maps). It sends a map of finite étale $k$-algebras $f : A \rightarrow B$ to the precomposition map $\text{Hom}_{k \text{-mod}} (B, K) \rightarrow \text{Hom}_{k \text{-mod}} (A, K)$ sending $\iota : B \rightarrow K$ to $\iota \circ f$.
$T_{k \text{-sep}}$ and $T_{G \text{-set}}$ factor through the forgetful functor $K[G] \text{-mod} \rightarrow K \text{-mod}$, just like in the reconstruction theorem of Tannakian formalism (but keep in mind that this doesn't meet the hypotheses of that theorem). We may view them as having target $K[G]$-mod then.
In this way $T_{k \text{-sep}} : k \text{-sep} \rightarrow k[G] \text{-mod}$ sends a finite étale $k$-algebra $A$ to $\text{Hom}_{k \text{-mod}} (A, K)$ with the $G$-action where, for $\sigma : K \rightarrow K$ and $\iota : A \rightarrow K$, $\sigma \cdot \iota = \sigma \circ \iota$.
This seems similar to some sort of Tannakian formalism setup, but maybe it's just coincidence. Anyways, this formality can be used to express Artin's linear independence of characters, albeit it is not obvious at first sight that they are essentially the same thing.
Theorem: The following diagram of functors commutes up to natural isomorphism:
That is, $T_{k \text{-sep}} : $ is naturally isomorphic to the composition $T_{G \text{-set}} \circ \Pi$ sending a finite ètale $k$-algebra $A$ to $\oplus_{\iota \in [A, K]_k } $, and this map is $G$-equivariant. More precisely, define a natural transformation $\epsilon : \Pi \rightarrow T_{k \text{-sep}} \rightarrow T_{G \text{-set}}$, where $\epsilon_A$ sends a formal sum $\sum_{\sigma : A \rightarrow K} c_{\sigma} \sigma$ in $\oplus_{x \in X} K$ to the $k$-linear map $A \rightarrow K$ in $\text{Hom}_{k \text{-mod}} (A, K)$ sending $a \in A$ to $\sum_{\sigma : A \rightarrow K} c_{\sigma} \sigma (a)$.
Proof: Take a finite étale $k$-algebra $A$. First we show that $\epsilon_A$ is injective (and this is the part which corresponds to linear independence of characters). For a contradiction, suppose $\epsilon_A$ is not injective, and take a nonzero element $\sum_{\sigma \in X} a_{\sigma} \sigma$ in the kernel of $\epsilon_A$, such that the amount of nonzero $a_{\sigma}$ is the least possible. Take $\tau \in X$, and take $y \in A$ such that $\tau(y) \neq \sigma(y)$ for some $\sigma \in X$ with $a_{\sigma} \neq 0$. Then $\sum_{i = 1} a_{\sigma} \sigma(y) \sigma (x) = \sum_{i = 1}^n a_{\sigma} \sigma (yx) = 0$ for each $x \in A$. And $\sum_{i = 1}^n a_{\sigma} \tau(y) \sigma(x) = 0$, so $\sum_{i = 1}^n (a_{\sigma} \tau(y) - a_{\sigma} \sigma(y)) \sigma$ is contained in the kernel of $\phi$. Yet this element is nonzero, as $\tau$ and $y$ were chosen so that $\tau(y) - \sigma(y) \neq 0$ for some $\sigma \in X$, and $a_{\sigma} \neq 0$. So we have a nonzero element of the kernel of $\epsilon_A$ with strictly fewer nonzero summands, a contradiction.
Now $\epsilon_A$ is injective, and it has target and cotarget with the same $K$-dimension, using the fact that $A$ is étale. So $\epsilon_A$ is an isomorphism.
So, I am asking whether this is related to Tannakian formalism. I don't see an abelian cotarget category anywhere, however.