Crux of Dwork's proof of rationality of the zeta function?

There is an excellent book by Neal Koblitz "p-adic numbers, p-adic analysis and zeta-functions" were the Dwork's proof is stated in a very detailed way, including all preliminaries from p-adic analysis. Let me sketch this proof in comparison with Weil's program of proving his conjecture.

First, any variety $X$ can be covered by affine charts $U_i$ with all intersections $U_{i_1}\cap \dots\cap U{i_k}$ being affine. The zeta-function of $X$ can be expressed in terms of zeta-functions of these affine varieties using inclusion-exclusion formula(I omit the base field and the formal variable to shorten notations) $$Z_X=\prod\limits_{i_1<\dots<i_k}Z_{U_{i_1}\cap\dots \cap U_{i_K}}^{(-1)^{k+1}}$$ Thus, it is enough to prove rationality for affine varieties. Next, any affine variety is an intersection of hypersurfaces and the union of hypersurfaces is a hypersurface, so again inclusion-exclusion formula(with $\cap$ and $\cup$ swapped) reduces the problem to hypersurfaces.

Now, the idea of Dwork is to prove first that $Z_X$ is $p$-adic meromorphic on $\mathbb{C}_p$ for a hypersurface $X\subset \mathbb{A}^n$. He proceeds by induction on dimension. We cut a hypersurface $f(X)=0$ into lower-dimensional hypersurfaces $f(X)=0,x_i=0$(to be precise, this variety may happen to be the whole $\mathbb{A}^{n-1}$ but this is even better since the rationality for affine space is obvious) and open subvariety $f(X),x_i\neq 0$ for all $i$. By the same inclusion-exclusion argument and induction, it is enough to prove rationality for this open variety.

As far as I understand, the following computation is the main insight of Dwork which resembles the Weil's idea. He expresses number of points of this variety over $\mathbb{F}_{q^k}$ in terms of trace of $\Psi^k$ where $\Psi$ is a certain linear operator. That gives an expression for zeta-function in terms of characteristic "polynomial" of $\Psi$. In contrast to Frobenius on Weil cohomology, $\Psi$ acts on an infinite-dimensional space, so its characteristic polynomial is not a polynomial, but rather a meromorphic series(one should do some work to make sense of determinant and trace of an infinite-dimensional operator -- this is perfectly carried out in Koblitz's book). This proves that $Z_X$ is $p$-adically meromorphic.

Finally, any meromorphic series with integral coefficients and properly bounded coefficients(for $Z_X$ the bound comes from $\# X(\mathbb{F}_{q^k})\leq q^{nk}$) is a rational function(this follows from p-adic Weierstrass preparation theorem and characterization of rational functions series as those admitting a linear recurrence relation on coefficients).

See Terry Tao's blog post. A very simple proof of a slightly weaker result is given by Mike Larsen.

Sasha has already pointed you to the primary source I used some years ago for my "expository" undergraduate thesis on Dwork's Theorem: Koblitz's p-adic Numbers, p-adic Analysis, and Zeta-Functions, which is available in 166 searchable pages here.

I've uploaded a copy of my thesis, which should constitute a relatively easy to digest ~ 50 page write-up of the proof. There is no significant difference from Koblitz's book; I worked out some of the pieces that were left as exercises or examples (e.g., showing that the zeta function for $f = x_1 x_4 - x_2 x_3 - 1$ is rational i.e. $\frac{1-qT}{1-q^3 T}$, which I re-produced in MO 117904) and omitted some of the proofs of cited theorems (e.g., the $p$-adic Weierstrass Preparation Theorem) with pointers to Koblitz's book or Gouvêa's intro to $p$-adic numbers when necessary.

As I understood matters almost a decade ago, there were a couple of important linear maps mentioned by Koblitz (included in my section 3.2) $G$ and $T_q$, which were composed to give the trace operator, $\Psi$, already mentioned. I introduce a slight bit of terminology ("admissible" in Definition 3.14) to discuss the trace of a linear operator from a certain infinite dimensional vector space to itself, and one of the key facts drawn upon in working towards the end of the proof is the power series identity:

$$ \det(1 - \psi T) = \exp \left(-\sum_{s=1}^{\infty} \text{Tr}(\psi^{s})T^{s}/s\right) $$

for a linear operator $\psi$ going from a vector space to itself. I re-mention that identity here, because I asked about its history in MSE 277124 for which Markus Scheuer gave a great answer. This identity arises in proving that a sufficient-to-consider modification of the zeta function $Z'(T)$ is $p$-adic meromorphic, which is established through a bit of induction, analysis of the above identity, and the inclusion/exclusion principle (the last of which re-arises, as Sasha mentions, in proving Dwork's theorem for affine hypersurfaces can be extended to projective varieties).

I do not believe that there is anything novel in my undergrad write-up, but I think it is possible that its presentation as being intended for college juniors/seniors could make the proof, hence the underlying intuition, easier to grok.