Absolute Galois cohomology with trivial ZMod p coefficients

Zeroth continuous cohomology of the absolute Galois group with trivial coefficients has dimension one. The canonical coefficient identification is TauCeti.cohomFpZeroLinearEquiv p (Field.absoluteGaloisGroup K), and finite generation is provided by the corresponding Module.Finite instance. At prime p, this is the finite-dimensional 𝔽_p-vector space H⁰(G_K, 𝔽_p).

theorem TauCeti.finrank_cohomFp_zero_absoluteGaloisGroup (p : ℕ) (K : Type u) [Field K] : Module.finrank (ZMod p) ↑(cohomFp p (Field.absoluteGaloisGroup K) 0).toModuleCat = 1

Zeroth absolute Galois cohomology with trivial ZMod p coefficients has dimension one.