[proofplan] We split the proof into the base case $K = k(t)$ and the general separable extension case. In the base case, the chain rule (a property of the universal derivation $d$) shows that $dt$ generates $\Omega_{k(t)/k}$ over $k(t)$, so $\dim_{k(t)} \Omega_{k(t)/k} \leq 1$; we then exhibit the formal $t$-derivation $D_t: k(t) \to k(t)$ as a nonzero $k$-derivation, which by the universal property factors through a nonzero $k(t)$-linear map $\Omega_{k(t)/k} \to k(t)$, forcing $\dim \geq 1$. For the general case, we use the [Primitive Generator for Function Fields](/theorems/2153) to write $K = k(t)(\alpha)$ for some $\alpha$ algebraic over $k(t)$, and apply the chain rule to the minimal polynomial relation $h(\alpha) = 0$. Separability ensures $h'(\alpha) \neq 0$, allowing us to solve for $d\alpha$ in terms of $dt$. Nonvanishing of $\Omega_{K/k}$ comes from extending $D_t$ to a $k$-derivation $D: K \to K$, which factors through a nonzero map $\Omega_{K/k} \to K$. [/proofplan] [step:Establish the base case $K = k(t)$ by showing $dt$ generates $\Omega_{k(t)/k}$] Consider $K = k(t)$, the field of rational functions in one variable. Every element $f \in k(t)$ has the form $f = p(t)/q(t)$ for $p, q \in k[t]$ with $q \neq 0$, so $f$ is a rational expression in the single transcendental $t$ with coefficients in $k$. By the chain rule for the universal derivation $d: k(t) \to \Omega_{k(t)/k}$ established in [Differentials Are Well-Defined and Chain Rule Holds](/theorems/2150), for any $f = p(t)/q(t) \in k(t)$: \begin{align*} df = \frac{q(t) \cdot p'(t) - p(t) \cdot q'(t)}{q(t)^2} \, dt = D_t(f) \cdot dt, \end{align*} where $D_t: k(t) \to k(t)$ is the formal $t$-derivative — i.e., the $k$-linear map sending $\sum_i a_i t^i \mapsto \sum_i i a_i t^{i-1}$ on polynomials and extended to rational functions by the quotient rule. Hence every element of $\{df : f \in k(t)\}$ is a $k(t)$-multiple of $dt$. The image $d(k(t)) \subset \Omega_{k(t)/k}$ generates $\Omega_{k(t)/k}$ as a $k(t)$-module by the construction of Kähler differentials (or equivalently, by the universal property: $\Omega_{k(t)/k}$ is generated by symbols $df$ subject to the Leibniz and $k$-linearity relations). Therefore: \begin{align*} \Omega_{k(t)/k} = k(t) \cdot \{df : f \in k(t)\} = k(t) \cdot dt, \end{align*} which gives $\dim_{k(t)} \Omega_{k(t)/k} \leq 1$. [/step] [step:Show $\Omega_{k(t)/k} \neq 0$ via the formal derivation $D_t$] We exhibit $\Omega_{k(t)/k}$ as nonzero by producing a nonzero $k$-derivation $k(t) \to k(t)$. The formal $t$-derivation \begin{align*} D_t: k(t) &\to k(t) \\ f &\mapsto f'(t) \quad \text{(in the standard sense)} \end{align*} is a $k$-linear map satisfying the Leibniz rule $D_t(fg) = f \cdot D_t(g) + g \cdot D_t(f)$ and $D_t(c) = 0$ for $c \in k$. (This is verified directly on $k[t]$ by polynomial differentiation, then extended to $k(t)$ by the quotient rule, which preserves both properties.) Hence $D_t$ is a $k$-derivation $k(t) \to k(t)$ in the sense relevant for [Differentials Are Well-Defined and Chain Rule Holds](/theorems/2150). By the universal property of $\Omega_{k(t)/k}$, there exists a unique $k(t)$-linear map \begin{align*} \tilde{D}_t: \Omega_{k(t)/k} \to k(t) \end{align*} such that $\tilde{D}_t \circ d = D_t$. In particular $\tilde{D}_t(dt) = D_t(t) = 1 \in k(t)$. So $\tilde{D}_t$ is a nonzero $k(t)$-linear map, hence $\Omega_{k(t)/k} \neq 0$. Combining with the upper bound from the previous step: $\dim_{k(t)} \Omega_{k(t)/k} = 1$, with $dt$ a basis. This completes the base case. [guided] The strategy is the standard "produce a witness" technique: we know $\Omega$ is generated by one element (so $\dim \leq 1$); to show $\dim \geq 1$, we need $\Omega \neq 0$, which we get by exhibiting a nonzero linear functional on $\Omega$. \textbf{Why does $D_t$ factor through $\Omega$?} The Kähler differentials are defined by the universal property: for any $k$-algebra $A$, any $A$-module $M$, and any $k$-derivation $\delta: A \to M$, there is a unique $A$-linear map $\tilde{\delta}: \Omega_{A/k} \to M$ with $\tilde{\delta} \circ d = \delta$. Here $A = k(t)$, $M = k(t)$, $\delta = D_t$. The universal property gives the unique $\tilde{D}_t$ with $\tilde{D}_t(df) = D_t(f)$ for all $f \in k(t)$. \textbf{Why is $D_t$ a derivation?} By construction. On polynomials $f = \sum a_i t^i$, $D_t f = \sum i a_i t^{i-1}$, which is $k$-linear and satisfies Leibniz on monomials. Extending to $k(t)$ by the quotient rule preserves both properties — this is a standard verification. \textbf{Why is $\tilde{D}_t \neq 0$?} Because $\tilde{D}_t(dt) = D_t(t) = 1 \neq 0$. So $dt \neq 0$ in $\Omega_{k(t)/k}$, hence $\Omega_{k(t)/k} \neq 0$, hence $\dim_{k(t)} \Omega_{k(t)/k} \geq 1$. \textbf{Why exactly $1$?} From Step 1, $\Omega_{k(t)/k}$ is generated by $dt$ as a $k(t)$-module. From this step, $dt \neq 0$. A nonzero generator of a $k(t)$-module $M$ generated by one element gives $M \cong k(t)$, so $\dim = 1$. [/guided] [/step] [step:Reduce the general case to a primitive generator $K = k(t)(\alpha)$] Now suppose $K/k(t)$ is a finite separable extension. By [Primitive Generator for Function Fields](/theorems/2153), there exists $\alpha \in K$ such that $K = k(t)(\alpha)$. Let \begin{align*} h(W) \in k(t)[W] \end{align*} be the minimal polynomial of $\alpha$ over $k(t)$ — the monic polynomial of smallest positive degree with $h(\alpha) = 0$. Since $K/k(t)$ is separable and $\alpha$ generates $K$, $h$ is separable as a polynomial over $k(t)$, which is equivalent to $h'(\alpha) \neq 0$, where $h'$ denotes the formal $W$-derivative of $h$ (i.e., the polynomial derivative $\frac{d}{dW}$). Concretely: writing $h(W) = W^n + c_{n-1} W^{n-1} + \cdots + c_0$ with $c_i \in k(t)$, the derivative $h'(W) = n W^{n-1} + (n-1) c_{n-1} W^{n-2} + \cdots + c_1$, and the separability hypothesis ensures $\gcd(h, h') = 1$ in $k(t)[W]$, hence $h'(\alpha) \neq 0$ in $K$. [/step] [step:Apply the chain rule to the relation $h(\alpha) = 0$ to relate $d\alpha$ and $dt$] By [Differentials Are Well-Defined and Chain Rule Holds](/theorems/2150), the universal derivation $d: K \to \Omega_{K/k}$ is $k$-linear and satisfies the Leibniz and chain rules. Applying $d$ to the relation $h(\alpha) = 0$ in $K$, and using the chain rule for the polynomial expression $h(\alpha) = \alpha^n + c_{n-1}(t) \alpha^{n-1} + \cdots + c_0(t)$: \begin{align*} 0 = d\bigl(h(\alpha)\bigr) = (\partial_t h)(\alpha) \cdot dt + h'(\alpha) \cdot d\alpha, \end{align*} where: - $h'(W) = \frac{\partial h}{\partial W} \in k(t)[W]$ is the formal derivative in $W$, and $h'(\alpha) \in K$ denotes the evaluation; - $(\partial_t h)(W) := \sum_{i=0}^{n-1} D_t(c_i) \cdot W^i \in k(t)[W]$ is the polynomial obtained by differentiating each coefficient of $h$ with respect to $t$, and $(\partial_t h)(\alpha) \in K$ denotes the evaluation. (The chain rule expansion is: $d(c_i(t) \alpha^i) = D_t(c_i) \cdot dt \cdot \alpha^i + c_i \cdot i \alpha^{i-1} \cdot d\alpha$ for each $i$, then sum over $i$ and collect $dt$ and $d\alpha$ terms.) Since $h'(\alpha) \neq 0$ in $K$ (Step 3), it is invertible in $K$, and we can solve for $d\alpha$: \begin{align*} d\alpha = -\frac{(\partial_t h)(\alpha)}{h'(\alpha)} \cdot dt \in \Omega_{K/k}. \end{align*} [guided] The relation $h(\alpha) = 0$ is the defining equation of $\alpha$ over $k(t)$. Differentiating it via the chain rule gives a $K$-linear relation between $dt$ and $d\alpha$, which lets us eliminate $d\alpha$. \textbf{Why does the chain rule give this expression?} Write $h(\alpha) = \alpha^n + \sum_{i=0}^{n-1} c_i(t) \alpha^i$ where $c_i \in k(t)$. By Leibniz and the $k$-linearity of $d$: \begin{align*} d(h(\alpha)) = d(\alpha^n) + \sum_{i=0}^{n-1} d(c_i \alpha^i) = n \alpha^{n-1} d\alpha + \sum_{i=0}^{n-1} \bigl(\alpha^i \cdot dc_i + c_i \cdot i \alpha^{i-1} d\alpha\bigr). \end{align*} Collect $dt$ and $d\alpha$ terms, using $dc_i = D_t(c_i) \, dt$ from the base case (Step 1): \begin{align*} d(h(\alpha)) = \underbrace{\sum_{i=0}^{n-1} D_t(c_i) \alpha^i}_{(\partial_t h)(\alpha)} \cdot dt + \underbrace{\Bigl( n \alpha^{n-1} + \sum_{i=0}^{n-1} i c_i \alpha^{i-1} \Bigr)}_{h'(\alpha)} \cdot d\alpha. \end{align*} Setting this equal to $d(0) = 0$ and dividing through by $h'(\alpha) \neq 0$ gives the displayed expression for $d\alpha$. \textbf{Why is $h'(\alpha) \neq 0$ the consumed hypothesis?} If $\alpha$ were inseparable — i.e., $h'(\alpha) = 0$ — we could not solve for $d\alpha$. The relation $0 \cdot d\alpha = -(\partial_t h)(\alpha) \cdot dt$ would constrain $(\partial_t h)(\alpha) \cdot dt = 0$ in $\Omega_{K/k}$, but would say nothing about $d\alpha$. The space $\Omega_{K/k}$ would then be larger than one-dimensional. This is precisely how separability enters: it ensures the relation $d\alpha = $ (function) $\cdot dt$ is genuinely solvable. \textbf{Notation $\partial_t$ vs $D_t$.} We use $D_t: k(t) \to k(t)$ for the formal $t$-derivation on $k(t)$ (Step 2), and write $\partial_t h$ for the polynomial in $k(t)[W]$ obtained by applying $D_t$ to each coefficient of $h$. So $\partial_t h$ is a polynomial expression that we then evaluate at $\alpha$. [/guided] [/step] [step:Conclude that $dt$ generates $\Omega_{K/k}$ and $\dim_K \Omega_{K/k} \leq 1$] By the chain rule for the universal derivation, $\Omega_{K/k}$ is generated as a $K$-module by $\{df : f \in K\}$. Every $f \in K = k(t)(\alpha)$ is a polynomial expression in $\alpha$ and $t$ (and inverses), so by Leibniz and the chain rule, $df$ is a $K$-linear combination of $dt$ and $d\alpha$. By the previous step, $d\alpha = -(\partial_t h)(\alpha)/h'(\alpha) \cdot dt$ is itself a $K$-multiple of $dt$. Hence every $df$ is a $K$-multiple of $dt$, and: \begin{align*} \Omega_{K/k} = K \cdot dt. \end{align*} This gives $\dim_K \Omega_{K/k} \leq 1$. [/step] [step:Show $\Omega_{K/k} \neq 0$ by extending $D_t$ to a $k$-derivation $K \to K$] We construct a $k$-derivation $D: K \to K$ that restricts to $D_t$ on $k(t)$. Set \begin{align*} D|_{k(t)} := D_t, \qquad D(\alpha) := -\frac{(\partial_t h)(\alpha)}{h'(\alpha)} \in K. \end{align*} We must show that this prescription extends uniquely to a $k$-linear map $D: K \to K$ satisfying the Leibniz rule. Consider the polynomial ring $k(t)[W]$, equipped with the $k$-derivation \begin{align*} \tilde{D}: k(t)[W] &\to k(t)[W] \\ \sum_i c_i(t) W^i &\mapsto \sum_i D_t(c_i)(t) W^i + \sum_i c_i(t) \cdot i W^{i-1} \cdot \beta, \end{align*} where $\beta := -(\partial_t h)(W)/h'(W) \in k(t)(W)$ (extended through the quotient field; below we verify the construction lands in $K$ after passing to the quotient by $(h)$). Actually, the cleanest way: let \begin{align*} \tilde{D}: k(t)[W] &\to K \\ P(W) &\mapsto (\partial_t P)(\alpha) + P'(\alpha) \cdot \beta_0, \end{align*} where $\beta_0 := -(\partial_t h)(\alpha)/h'(\alpha) \in K$, $\partial_t P$ is coefficient-wise application of $D_t$, and $P'$ is the formal $W$-derivative. The map $\tilde{D}$ is $k$-linear and satisfies the Leibniz rule on $k(t)[W]$ (a direct computation: both $\partial_t$ and $P \mapsto P' \cdot \beta_0$ are derivations into $K$, and the sum of two derivations into the same module is a derivation). Compute $\tilde{D}(h)$: \begin{align*} \tilde{D}(h) = (\partial_t h)(\alpha) + h'(\alpha) \cdot \beta_0 = (\partial_t h)(\alpha) + h'(\alpha) \cdot \left(-\frac{(\partial_t h)(\alpha)}{h'(\alpha)}\right) = 0. \end{align*} Thus $\tilde{D}$ vanishes on the principal ideal $(h) \subset k(t)[W]$ (because $\tilde{D}(h \cdot Q) = \tilde{D}(h) Q(\alpha) + h(\alpha) \tilde{D}(Q) = 0 + 0 = 0$ for any $Q \in k(t)[W]$, using $h(\alpha) = 0$). Therefore $\tilde{D}$ descends to a well-defined $k$-linear map on the quotient $k(t)[W]/(h) \cong K$ — call this map $D: K \to K$. The descent $D$ is a $k$-derivation $K \to K$: $k$-linearity and Leibniz both descend through the quotient (since the ideal $(h)$ is closed under $\tilde{D}$, the quotient inherits the derivation structure). And $D(t) = D_t(t) = 1 \neq 0$, so $D$ is nonzero. By the universal property of $\Omega_{K/k}$, $D$ factors as $D = \tilde{D} \circ d$ for a unique $K$-linear map $\tilde{D}: \Omega_{K/k} \to K$, with $\tilde{D}(dt) = D(t) = 1 \neq 0$. Hence $\tilde{D}$ is nonzero, and $\Omega_{K/k} \neq 0$. Combined with the upper bound $\dim_K \Omega_{K/k} \leq 1$ from Step 5, we conclude $\dim_K \Omega_{K/k} = 1$ and $dt$ is a $K$-basis. This completes the proof. [guided] We have one inequality $\dim \leq 1$. To upgrade to equality, we must rule out $\Omega_{K/k} = 0$. The same strategy as the base case works: produce a nonzero $k$-derivation $K \to K$, which factors through a nonzero functional on $\Omega_{K/k}$, hence $\Omega_{K/k} \neq 0$. \textbf{Why is the construction of $D$ nontrivial?} On $k(t)$ we already have $D_t$. Extending to $K = k(t)(\alpha)$ requires choosing a value for $D(\alpha) \in K$ that is consistent with the relation $h(\alpha) = 0$ — i.e., that yields $D(h(\alpha)) = 0$ when computed via Leibniz. The chain rule applied to $h(\alpha) = 0$ forces $D(\alpha) = -(\partial_t h)(\alpha)/h'(\alpha)$, which is well-defined in $K$ because $h'(\alpha) \neq 0$ by separability. So separability is consumed both in constructing $D$ and in solving for $d\alpha$ in terms of $dt$ — the same fact wearing two hats. \textbf{The descent argument.} We define $\tilde{D}$ on the polynomial ring $k(t)[W]$, which is the "free version" before imposing the relation $h(\alpha) = 0$. We then check that $\tilde{D}(h) = 0$ — this is the key computation, made transparent by the prescribed formula for $\beta_0$. Since $(h) \subset \ker \tilde{D}$ (using $\tilde{D}(h \cdot Q) = h(\alpha) \tilde{D}(Q) + Q(\alpha) \tilde{D}(h) = 0$ — note this requires $\tilde{D}$ to be a derivation into $K$, with $h$ treated as a constant via evaluation $k(t)[W] \to K$, which equals zero), the map descends to the quotient $k(t)[W]/(h) = K$. \textbf{Why is $D(t) = 1$ enough?} We need $D \neq 0$ to conclude. Among the values $D$ takes, $D(t) = D_t(t) = 1 \neq 0$ is the simplest witness. The universal property then gives $\tilde{D}(dt) = 1 \neq 0$, so $dt \neq 0$ in $\Omega_{K/k}$, so $\Omega_{K/k} \neq 0$. \textbf{Where does separability fail?} If $\alpha$ were inseparable, $h'(\alpha) = 0$ and the formula for $D(\alpha)$ would involve dividing by zero. The construction of $D$ breaks, and indeed $\Omega_{K/k}$ can be larger than one-dimensional (or have torsion-like behaviour) in the inseparable case. This is the content of the separability hypothesis. [/guided] [/step]