All.lean

Étale cohomology and finite étale covers

Actual degree-one cohomology is identified with continuous finite-coefficient characters of the fundamental group and its topological abelianization. The coefficient-natural comparison identifies classical integral ℓ-adic H¹ with actual continuous p-adic characters, including their p-adic scalar action. Compactness identifies the scalar extension with actual continuous Qℓ-valued characters. The finite-coefficient direct limit retains torsion and reconstructs the full topological abelianization by Pontryagin duality.