To prove (1), we only need to check that
is an almost finite projective
-module, as
(24.3) already implies that
is an almost finite projective
-module. By
(24.3), the idempotent element of
that picks out the identity component is an almost element of
Consequently, for each
we may multiply by
to get a genuine element
satisfying
that kills the kernel of
and projects to
Write
for some
we then have
for
and
Define the trace map as the sum over -conjugates. Then
In other words, the composition
is multiplication by since was arbitrary, this proves that is an almost finite projective -module.
To prove (2), we first apply (1) to deduce that is almost finite étale. We then check that the canonical map is an almost isomorphism: we can check this after tensoring over with in which case we have almost isomorphisms
Thus the map
becomes almost finite étale after tensoring over
with
and so by
Remark 24.2.10 is itself almost finite étale. (Compare
[4], Proposition 9.1.)