[proofplan] We construct the isomorphism in both directions. A point derivation $D:A(X)\to k$ restricts to a functional on $\mathfrak m_p$, and the Leibniz rule forces it to vanish on $\mathfrak m_p^2$, so it descends to $\mathfrak m_p/\mathfrak m_p^2$. Conversely, a functional on $\mathfrak m_p/\mathfrak m_p^2$ defines a point derivation by applying it to the class of $f-f(p)1_{A(X)}$. The two constructions are then checked directly to be inverse $k$-linear maps. [/proofplan]

[step:Send a point derivation to its induced functional on $\mathfrak m_p/\mathfrak m_p^2$] Let $\operatorname{Der}_{k,p}(A(X),k)$ denote the $k$-[vector space](/page/Vector%20Space) of $k$-linear maps $D:A(X)\to k$ satisfying \begin{align*} D(fg)=f(p)D(g)+g(p)D(f) \end{align*} for all $f,g\in A(X)$. Fix $D\in \operatorname{Der}_{k,p}(A(X),k)$. Since $1_{A(X)}(p)=1$, applying the defining identity to $1_{A(X)}\cdot 1_{A(X)}$ gives \begin{align*} D(1_{A(X)})=D(1_{A(X)})+D(1_{A(X)}). \end{align*} Subtracting $D(1_{A(X)})$ in the field $k$, we get $D(1_{A(X)})=0$. Hence $D(c1_{A(X)})=cD(1_{A(X)})=0$ for every $c\in k$. If $a,b\in \mathfrak m_p$, then $a(p)=b(p)=0$, so the point-derivation identity gives \begin{align*} D(ab)=a(p)D(b)+b(p)D(a)=0. \end{align*} By $k$-linearity, $D$ vanishes on the ideal $\mathfrak m_p^2$, because $\mathfrak m_p^2$ consists of finite sums of products $ab$ with $a,b\in\mathfrak m_p$. Therefore the restriction $D|_{\mathfrak m_p}:\mathfrak m_p\to k$ descends to a well-defined $k$-[linear map](/page/Linear%20Map) \begin{align*} \Phi(D):\mathfrak m_p/\mathfrak m_p^2\to k \end{align*} defined by \begin{align*} \Phi(D)(\overline a):=D(a), \end{align*} where $a\in\mathfrak m_p$ and $\overline a$ denotes the class of $a$ modulo $\mathfrak m_p^2$. This defines a $k$-linear map \begin{align*} \Phi:\operatorname{Der}_{k,p}(A(X),k)\to \operatorname{Hom}_k(\mathfrak m_p/\mathfrak m_p^2,k). \end{align*} [/step]

[step:Build a point derivation from a functional on $\mathfrak m_p/\mathfrak m_p^2$]Let \begin{align*} \lambda:\mathfrak m_p/\mathfrak m_p^2\to k \end{align*} be a $k$-linear map. For $f\in A(X)$, the scalar $f(p)\in k$ is regarded as the constant function $f(p)1_{A(X)}\in A(X)$. Since \begin{align*} (f-f(p)1_{A(X)})(p)=0, \end{align*} we have $f-f(p)1_{A(X)}\in \mathfrak m_p$. Define a map \begin{align*} D_\lambda:A(X)\to k \end{align*} by \begin{align*} D_\lambda(f):=\lambda(\overline{f-f(p)1_{A(X)}}), \end{align*} where the bar denotes the class in $\mathfrak m_p/\mathfrak m_p^2$. Because evaluation at $p$, subtraction of the corresponding constant function, the quotient map $\mathfrak m_p\to\mathfrak m_p/\mathfrak m_p^2$, and $\lambda$ are all $k$-linear, the map $D_\lambda$ is $k$-linear.[/step]

[guided]Start with a functional \begin{align*} \lambda:\mathfrak m_p/\mathfrak m_p^2\to k. \end{align*} To turn $\lambda$ into a map on all of $A(X)$, we must first turn an arbitrary element $f\in A(X)$ into an element of $\mathfrak m_p$. The evaluation $f(p)\in k$ gives exactly the constant part of $f$ at the point $p$. We identify this scalar with the constant function $f(p)1_{A(X)}\in A(X)$ and define \begin{align*} f_0:=f-f(p)1_{A(X)}. \end{align*} Then \begin{align*} f_0(p)=f(p)-f(p)=0, \end{align*} so $f_0\in\mathfrak m_p$. Thus the class $\overline{f_0}\in\mathfrak m_p/\mathfrak m_p^2$ is a valid input for $\lambda$. We therefore define \begin{align*} D_\lambda:A(X)\to k \end{align*} by \begin{align*} D_\lambda(f):=\lambda(\overline{f-f(p)1_{A(X)}}). \end{align*} This formula is $k$-linear in $f$: evaluation $f\mapsto f(p)$ is a $k$-linear map, the assignment $f\mapsto f-f(p)1_{A(X)}$ is $k$-linear from $A(X)$ to $\mathfrak m_p$, the quotient map $\mathfrak m_p\to\mathfrak m_p/\mathfrak m_p^2$ is $k$-linear, and $\lambda$ is $k$-linear by hypothesis. Hence $D_\lambda$ is a $k$-linear map from $A(X)$ to $k$.[/guided]

[step:Verify the Leibniz rule for the constructed map] Let $f,g\in A(X)$. Define \begin{align*} f_0:=f-f(p)1_{A(X)} \end{align*} and \begin{align*} g_0:=g-g(p)1_{A(X)}. \end{align*} Then $f_0,g_0\in\mathfrak m_p$, and \begin{align*} f=f(p)1_{A(X)}+f_0 \end{align*} and \begin{align*} g=g(p)1_{A(X)}+g_0. \end{align*} Multiplying these decompositions in the $k$-algebra $A(X)$ gives \begin{align*} fg-f(p)g(p)1_{A(X)}=f(p)g_0+g(p)f_0+f_0g_0. \end{align*} Since $f_0g_0\in\mathfrak m_p^2$, its class in $\mathfrak m_p/\mathfrak m_p^2$ is zero. Therefore \begin{align*} D_\lambda(fg)=\lambda(\overline{f(p)g_0+g(p)f_0}). \end{align*} Using $k$-linearity of $\lambda$, we obtain \begin{align*} D_\lambda(fg)=f(p)\lambda(\overline{g_0})+g(p)\lambda(\overline{f_0}). \end{align*} By the definition of $D_\lambda$, this is \begin{align*} D_\lambda(fg)=f(p)D_\lambda(g)+g(p)D_\lambda(f). \end{align*} Thus $D_\lambda\in\operatorname{Der}_{k,p}(A(X),k)$. [/step]

[step:Check that the two constructions are inverse and $k$-linear] Define \begin{align*} \Psi:\operatorname{Hom}_k(\mathfrak m_p/\mathfrak m_p^2,k)\to \operatorname{Der}_{k,p}(A(X),k) \end{align*} by $\Psi(\lambda):=D_\lambda$. The construction of $D_\lambda$ is $k$-linear in $\lambda$, so $\Psi$ is a $k$-linear map. Let $D\in\operatorname{Der}_{k,p}(A(X),k)$ and $f\in A(X)$. Since $D$ vanishes on constant functions, we have \begin{align*} (\Psi(\Phi(D)))(f)=\Phi(D)(\overline{f-f(p)1_{A(X)}})=D(f-f(p)1_{A(X)})=D(f). \end{align*} Hence $\Psi\circ\Phi$ is the identity on $\operatorname{Der}_{k,p}(A(X),k)$. Conversely, let $\lambda\in\operatorname{Hom}_k(\mathfrak m_p/\mathfrak m_p^2,k)$ and let $a\in\mathfrak m_p$. Since $a(p)=0$, we have \begin{align*} (\Phi(\Psi(\lambda)))(\overline a)=D_\lambda(a)=\lambda(\overline{a-a(p)1_{A(X)}})=\lambda(\overline a). \end{align*} Thus $\Phi\circ\Psi$ is the identity on $\operatorname{Hom}_k(\mathfrak m_p/\mathfrak m_p^2,k)$. Therefore $\Phi$ and $\Psi$ are inverse $k$-linear isomorphisms. Since \begin{align*} T_pX=\operatorname{Hom}_k(\mathfrak m_p/\mathfrak m_p^2,k), \end{align*} this proves that $T_pX$ is naturally isomorphic to the $k$-vector space of point derivations $A(X)\to k$ at $p$. [/step]