Uniqueness of continuous crossed homomorphisms

Two continuous crossed homomorphisms into a Hausdorff, additively cancellative semiring are equal if they have the same unit-valued twist and agree on a topological generating set. No multiplicativity or continuity of the twist, or continuity of the semiring operations, is needed. Their agreement propagates to the subgroup generated by the set and then to its topological closure by continuity.

The algebraic calculus is developed in TauCeti/Algebra/Group/CrossedHom.lean. For a continuous character χ : G →ₜ* ℤ_pˣ of a pro-p group, continuous crossed homomorphisms G → ℤ_p are the compatible systems of continuous 1-cocycles with values in the twisted coefficients I(χ)/pⁱ. Their values on a minimal generating tuple are what Labute's prescription property prescribes.

Main results

• TauCeti.IsCrossedHom.eq_of_eqOn_of_topologicalClosure_closure_eq_top: two continuous crossed homomorphisms agreeing on a topological generating set are equal.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §2.3.
• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, §2.

theorem TauCeti.IsCrossedHom.eq_of_eqOn_of_topologicalClosure_closure_eq_top {H : Type u_1} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {R : Type u_2} [Semiring R] [IsLeftCancelAdd R] [TopologicalSpace R] [T2Space R] {χ : H → Rˣ} {F₁ F₂ : H → R} (h₁ : IsCrossedHom χ F₁) (h₂ : IsCrossedHom χ F₂) (hc₁ : Continuous F₁) (hc₂ : Continuous F₂) {s : Set H} (hs : (Subgroup.closure s).topologicalClosure = ⊤) (h : Set.EqOn F₁ F₂ s) : F₁ = F₂

Two continuous crossed homomorphisms for the same unit-valued twist agreeing on a topological generating set are equal.