Fix a finite-dimensional representation $X$ of $G$. Let $\mathcal C_X$ be the strictly full subcategory of $\operatorname{Rep}_k(G)$ whose objects are subquotients of finite direct sums of tensor expressions in $X$ and $X^\vee$. For every $k$-algebra $R$, evaluation on $X$ is the homomorphism

$$ \operatorname{Aut}^{\otimes}(\omega_G|_{\mathcal C_X})(R) \longrightarrow\operatorname{GL}(\omega_G(X)\otimes_k R), \qquad \lambda\longmapsto\lambda_X. $$

It is injective. Indeed, tensor compatibility determines $\lambda$ on tensor powers of $X$ once $\lambda_X$ is known, and compatibility with the evaluation map determines $\lambda_{X^\vee}$. Naturality with respect to the inclusions and projections of finite direct sums then determines $\lambda$ on every finite direct sum of such tensor expressions. Finally, if $V$ is a subobject or quotient of one of these objects, naturality with respect to the inclusion or quotient map determines $\lambda_V$. Thus $\lambda_X$ determines the whole family $\lambda$. Let $G_X$ be the scheme-theoretic image of

$$ G\longrightarrow\operatorname{GL}(X). $$

Every object $V$ of $\mathcal C_X$ is constructed from $X$ by tensor products, duals, finite direct sums, subobjects, and quotients. Consequently, the action of $G$ on $V$ factors through $G_X$; write

$$ \rho_V:G_X\longrightarrow\operatorname{GL}(V) $$

for the resulting representation. For $g\in G_X(R)$, the map

$$ \rho_V(g):V\otimes_kR\xrightarrow{\sim}V\otimes_kR $$

is $R$-linear. If $f:V\to W$ is a morphism in $\mathcal C_X$, then

$$ (f\otimes\operatorname{id}_R)\circ\rho_V(g) =\rho_W(g)\circ(f\otimes\operatorname{id}_R). $$

Moreover,

$$ \rho_{V\otimes W}(g)=\rho_V(g)\otimes\rho_W(g), \qquad \rho_{\mathbf 1}(g)=\operatorname{id}_R. $$

Set $\omega_X:=\omega_G|_{\mathcal C_X}$. Thus $\omega_X$ forgets the group action but is defined only on objects of $\mathcal C_X$, and

$$ (\omega_X)_R(V)=V\otimes_kR. $$

By definition, an element of $\operatorname{Aut}^{\otimes}(\omega_X)(R)$ is a family $\lambda_V:(\omega_X)_R(V)\to(\omega_X)_R(V)$ that is natural in $V$, respects tensor products, and is the identity on $\mathbf 1$. Taking $\lambda_V=\rho_V(g)$, the preceding three displayed formulas verify exactly these conditions. Hence $g$ defines an element of $\operatorname{Aut}^{\otimes}(\omega_X)(R)$, giving the first inclusion

$$ G_X\subseteq\operatorname{Aut}^{\otimes}(\omega_G|_{\mathcal C_X}) \subseteq\operatorname{GL}(X). $$

We now prove the reverse inclusion. Let

$$ \lambda\in\operatorname{Aut}^{\otimes}(\omega_X)(R). $$

Because evaluation on $X$ is injective, it is enough to prove that $\lambda_X$ lies in $G_X(R)\subseteq\operatorname{GL}(X\otimes_kR)$. To show that $\lambda_X\in G_X(R)$, let $V\in\mathcal C_X$ and let $t\in V$ be fixed by $G_X$. Then the map

$$ k\longrightarrow V,\qquad a\longmapsto at, $$

is $G_X$-equivariant. After extension of scalars to $R$, naturality gives

$$ \lambda_V\circ(t\otimes-) =(t\otimes-)\circ\lambda_{\mathbf 1}. $$

Here $(t\otimes-):R\to V\otimes_kR$ sends $a$ to $t\otimes a$. Because $\lambda_{\mathbf 1}=\operatorname{id}_R$, evaluating this equality at $1\in R$ gives $\lambda_V(t_R)=t_R$. In particular, $\lambda_X$ fixes every tensor

$$ t\in\left(X^{\otimes m}\otimes(X^\vee)^{\otimes n}\right)^{G_X}. $$

By ⟦ref:lem-tensor-stabilizer⟧, an element of $\operatorname{GL}(X\otimes_kR)$ with this property belongs to $G_X(R)$. Therefore $\lambda_X\in G_X(R)$, as required. This proves

$$ G_X\xrightarrow{\sim}\operatorname{Aut}^{\otimes}(\omega_G|_{\mathcal C_X}). $$

If $X'=X\oplus Y$, then $\mathcal C_X\subseteq\mathcal C_{X'}$, and these isomorphisms commute with the restriction maps. Finally, finite-dimensional representations recover an affine group scheme from its finite-dimensional image groups:

$$ G\cong\varprojlim_XG_X. $$

Likewise, a tensor automorphism of $\omega_G$ is uniquely the compatible family of its restrictions to the $\mathcal C_X$, so

$$ \operatorname{Aut}^{\otimes}(\omega_G) \cong\varprojlim_X\operatorname{Aut}^{\otimes} (\omega_G|_{\mathcal C_X}). $$

Passing to the inverse limit of the preceding isomorphisms gives the result.

First, $\omega(Z)=0$ implies $Z=0$: faithfulness sends $\omega(\operatorname{id}_Z)=0$ back to $\operatorname{id}_Z=0$. Hence, if $U\subsetneq V$, exactness gives a strict inclusion $\omega(U)\subsetneq\omega(V)$. Every object of $\mathcal C$ is therefore Artinian and Noetherian, because strict chains of its subobjects give strict chains of subspaces of a finite-dimensional vector space. Thus both the largest subobject in (1) and the smallest subobject in (2) exist.

Let $P$ denote the subobject in (1). Since $\omega$ is exact, it carries a transporter to a transporter:

$$ \omega\bigl(Y:W\bigr)=\bigl(\omega(Y):W\bigr). $$

Consequently, $\omega(P)$ is the largest subalgebra of $\operatorname{End}_k(\omega(X))$ that stabilizes $\omega(Y)$ for every $Y\subseteq X^{\oplus n}$; this means that

$$ a^{\oplus n}\bigl(\omega(Y)\bigr)\subseteq\omega(Y) \qquad \text{for every }a\in\omega(P). $$

In particular, $\operatorname{id}_{\omega(X)}\in\omega(P)$, so the minimality of $P'$ gives $P'\subseteq P$.

Conversely, let $Q$ be any subobject as in (2). For every finite-dimensional vector space $V$, there is a natural map

$$ \underline{\operatorname{Hom}}(\omega(X),X) \longrightarrow \underline{\operatorname{Hom}}(\omega(V\otimes X),V\otimes X) $$

After applying $\omega$, this becomes the linear map

$$ \operatorname{End}_k\bigl(\omega(X)\bigr) \longrightarrow\operatorname{End}_k\bigl(V\otimes_k\omega(X)\bigr), \qquad a\longmapsto\operatorname{id}_V\otimes a, $$

where $(\operatorname{id}_V\otimes a)(v\otimes x)=v\otimes a(x)$. Choose an isomorphism $V\cong k^n$. The condition in (1) for the subobject $Y\subseteq V\otimes X\cong X^{\oplus n}$ is precisely

$$ \Delta_n(P)\subseteq\bigl(Y:\omega(Y)\bigr). $$

By the definition of the transporter, this says that the diagonal maps in $\Delta_n(P)$ carry $\omega(Y)$ into $Y$. After applying $\omega$, it says that for every $a\in\omega(P)$,

$$ (\operatorname{id}_V\otimes a)\bigl(\omega(Y)\bigr) \subseteq\omega(Y). $$

Thus $\omega(P)$ stabilizes $\omega(Y)$ for every subobject $Y\subseteq V\otimes X$. Take $V=\omega(X)^\vee$ and $Y=Q\subseteq \omega(X)^\vee\otimes X$. Under the identification $\omega(X)^\vee\otimes\omega(X)\cong\operatorname{End}_k(\omega(X))$, the map $\operatorname{id}_V\otimes a$ is left composition by $a$. Thus, applying the preceding stabilization condition to $\omega(Q)$ says that

$$ a\circ f\in\omega(Q) \qquad \text{for every }a\in\omega(P)\text{ and }f\in\omega(Q). $$

Since $\operatorname{id}_{\omega(X)}\in\omega(Q)$, every $a\in\omega(P)$ satisfies

$$ a=a\circ\operatorname{id}_{\omega(X)}\in\omega(Q). $$

Thus $\omega(P)\subseteq\omega(Q)$, and exactness and faithfulness imply $P\subseteq Q$. This holds for every $Q$ as in (2), so $P\subseteq P'$. Together with $P'\subseteq P$, this proves $P=P'$.

⟦ref:lem-tannakian-stabilizer⟧ says that $A_X$ is the largest subalgebra of $\operatorname{End}_k(\omega(X))$ that stabilizes $\omega(Y)$ for every $Y\subseteq X^{\oplus n}$. It therefore acts on every $\omega(Y)$ with $Y\in\langle X\rangle$.

The right action on $P_X$ is given by precomposition. It preserves $P_X$ because the composite of two maps that preserve every relevant subobject again preserves every relevant subobject. Thus, for a left $A_X$-module $M$ that is finite-dimensional as a $k$-vector space, the object

$$ P_X\otimes_{A_X}M $$

is defined in $\mathcal C$. It belongs to $\langle X\rangle$, since $P_X$ is a subobject of $\omega(X)^\vee\otimes X$ and $\langle X\rangle$ is closed under finite sums, subobjects, and quotients. Exactness of $\omega$ gives

$$ \omega\bigl(P_X\otimes_{A_X}M\bigr) \cong A_X\otimes_{A_X}M \cong M. $$

Thus $\overline\omega_X$ is essentially surjective. If $u:M\to N$ is an $A_X$-linear map, then

$$ \operatorname{id}_{P_X}\otimes_{A_X}u: P_X\otimes_{A_X}M\longrightarrow P_X\otimes_{A_X}N $$

is a morphism in $\langle X\rangle$. Applying $\omega$ identifies it with

$$ \operatorname{id}_{A_X}\otimes_{A_X}u=u, $$

so every $A_X$-linear map lifts; hence $\overline\omega_X$ is full. It is faithful because $\omega$ is. Therefore it is an equivalence.

Let $a\in A_X$. For every subobject $Y\subseteq X^{\oplus n}$, the defining property of $A_X$ gives

$$ a^{\oplus n}\bigl(\omega(Y)\bigr)\subseteq\omega(Y). $$

Thus $a^{\oplus n}$ restricts to $\omega(Y)$ and descends to the quotient of $\omega(Y)$ by the image of any subobject. It consequently defines an endomorphism of $\omega(Z)$ for every subquotient $Z$ of $X^{\oplus n}$. If $f:Z\to Z'$ is a morphism in $\langle X\rangle$, its graph is a subobject of $Z\oplus Z'$ and is preserved by these endomorphisms. Hence

$$ a_{Z'}\circ\omega(f)=\omega(f)\circ a_Z, $$

so the resulting family is a natural endomorphism of $\omega|_{\langle X\rangle}$.

Conversely, let $\eta$ be a natural endomorphism of $\omega|_{\langle X\rangle}$ and put $a:=\eta_X$. Naturality with the standard inclusions and projections of $X^{\oplus n}$ gives

$$ \eta_{X^{\oplus n}}=a^{\oplus n}. $$

For a subobject $i:Y\hookrightarrow X^{\oplus n}$, naturality of $\eta$ gives

$$ a^{\oplus n}\circ\omega(i)=\omega(i)\circ\eta_Y. $$

Therefore $a^{\oplus n}$ preserves $\omega(Y)$ for every $Y\subseteq X^{\oplus n}$, and ⟦ref:lem-tannakian-stabilizer⟧ implies that $a\in A_X$. The preceding construction then recovers $\eta$ from $a$, because every object of $\langle X\rangle$ is a subquotient of some $X^{\oplus n}$. This proves

$$ A_X=\operatorname{End}\bigl(\omega|_{\langle X\rangle}\bigr). $$

We now prove ⟦ref:thm-tannaka-reconstruction⟧. For every $X\in\mathcal C$, let $A_X$ be the algebra of ⟦ref:lem-tannakian-modules⟧ and put

$$ B_X:=A_X^\vee. $$

The equivalence in that lemma identifies finite-dimensional $A_X$-modules with finite-dimensional $B_X$-comodules. If $X$ is a subquotient of a finite direct sum of copies of $X'$, restriction gives a morphism $A_{X'}\to A_X$; dually, it gives a coalgebra morphism $B_X\to B_{X'}$. Define

$$ B:=\varinjlim_X B_X. $$

The objects $X\oplus X'$ show that this system is filtered. Every finite-dimensional $B$-comodule factors through some $B_X$, so the equivalences of ⟦ref:lem-tannakian-modules⟧ glue to an equivalence

$$ \mathcal C\xrightarrow{\sim}\operatorname{Comod}^{\mathrm{fd}}_B $$

that carries $\omega$ to the forgetful functor.

We now use the tensor structure. Let $V$ and $W$ be finite-dimensional left $B$-comodules, with coactions

$$ \delta_V:V\longrightarrow B\otimes_kV, \qquad \delta_W:W\longrightarrow B\otimes_kW. $$

A multiplication $m:B\otimes_kB\to B$ that is a coalgebra map gives a coaction on the ordinary tensor product $V\otimes_kW$: it is the composite

$$ \begin{aligned} V\otimes_kW &\xrightarrow{\ \delta_V\otimes\delta_W\ } B\otimes_kV\otimes_kB\otimes_kW \\ &\xrightarrow{\ \operatorname{id}_B\otimes\tau_{V,B}\otimes \operatorname{id}_W\ } B\otimes_kB\otimes_kV\otimes_kW \\ &\xrightarrow{\ m\otimes\operatorname{id}_{V\otimes W}\ } B\otimes_kV\otimes_kW, \end{aligned} $$

where

$$ \tau_{U,V}:U\otimes_kV\longrightarrow V\otimes_kU, \qquad u\otimes v\longmapsto v\otimes u, $$

is the symmetry of finite-dimensional vector spaces.

The condition that $m$ be a coalgebra map is exactly what makes this a coaction. Conversely, every tensor product on $\operatorname{Comod}^{\mathrm{fd}}_B$ whose underlying vector space is the ordinary tensor product arises in this way from a unique coalgebra map

$$ m:B\otimes_kB\longrightarrow B. $$

Transport the tensor product of $\mathcal C$ across the preceding equivalence. Its underlying vector space is the ordinary tensor product, because $\omega$ is a tensor functor, so it gives such a multiplication $m$. The associativity and symmetry constraints make $m$ associative and commutative, while the identity object gives a unit $k\to B$. Thus $B$ is a commutative bialgebra and

$$ M:=\operatorname{Spec}(B) $$

is an affine monoid scheme.

For every $k$-algebra $R$ and every $k$-algebra map $s:B\to R$, the coaction of a $B$-comodule $V$ defines an $R$-linear endomorphism of $V\otimes_kR$. It is the composite

$$ \begin{aligned} V\otimes_kR &\xrightarrow{\ \delta_V\otimes\operatorname{id}_R\ } B\otimes_kV\otimes_kR \\ &\xrightarrow{\ \operatorname{id}_B\otimes\tau_{V,R}\ } B\otimes_kR\otimes_kV \\ &\xrightarrow{\ s\otimes\operatorname{id}_R\otimes\operatorname{id}_V\ } R\otimes_kR\otimes_kV \\ &\xrightarrow{\ \mu_R\otimes\operatorname{id}_V\ } R\otimes_kV \xrightarrow{\ \tau_{R,V}\ }V\otimes_kR, \end{aligned} $$

where $\mu_R$ is multiplication in $R$.

This construction is natural in $V$. The displayed formula for the coaction on $V\otimes W$ shows that these endomorphisms respect tensor products exactly when

$$ s\circ m=\mu_R\circ(s\otimes s); $$

they preserve the identity object exactly when $s$ preserves the unit. Thus the preceding construction identifies the tensor-compatible endomorphisms of $\omega_R$ with the $k$-algebra maps $B\to R$. Write $\operatorname{End}^{\otimes}(\omega)(R)$ for these endomorphisms, without requiring them to be invertible. Hence

$$ \operatorname{End}^{\otimes}(\omega)(R) =\operatorname{Hom}_{k\text{-}\mathrm{alg}}(B,R) =M(R). $$

Rigidity makes every tensor-compatible endomorphism invertible: compatibility with the evaluation and coevaluation maps of $X$ and $X^\vee$ gives an inverse to its component on $X$. Therefore

$$ \operatorname{End}^{\otimes}(\omega) =\operatorname{Aut}^{\otimes}(\omega). $$

Thus $M$ is an affine group scheme; write it as $G$. Finally, finite-dimensional $B$-comodules are precisely finite-dimensional representations of $G$. Under the equivalence above, the coaction on $\omega(X)$ gives the representation $\rho_X$, so the equivalence is exactly $\widetilde\omega$ from the statement.