The homogeneous cocycle of a character and its cup products

A continuous character χ : G → 𝔽_p of a topological group G is a homogeneous one-cocycle (g₀, g₁) ↦ χ (g₀⁻¹ g₁) with trivial 𝔽_p coefficients (TauCeti.characterCocycle), and its class is the class attached to χ by the identification TauCeti.cohomFpLinearEquivContinuousZModDual of H¹(G, 𝔽_p) with the continuous 𝔽_p-dual of G (TauCeti.cohomFpLinearEquivContinuousZModDual_symm_apply). This gives every class of H¹(G, 𝔽_p) an explicit representative on Mathlib's homogeneous cochains, on which the cup product H¹ × H¹ → H² of TauCeti.cupFp is computed by the Alexander–Whitney formula (χ ⌣ ψ) g₀ g₁ g₂ = χ (g₀⁻¹ g₁) ψ (g₁⁻¹ g₂).

The one consequence drawn here is a symmetry test for the vanishing of a cup product: the coboundary of an invariant one-cochain w, evaluated at (1, x, xy), is w 1 y - w 1 (xy) + w 1 x, which is unchanged by exchanging x and y when they commute. So if a ⌣ b = 0 in H²(G, 𝔽_p) for classes a, b of H¹(G, 𝔽_p) with characters χ, ψ, then χ(x) ψ(y) = χ(y) ψ(x) for all commuting x, y ∈ G (TauCeti.mul_eq_mul_of_cupFp_eq_zero). Contrapositively, two characters that are not proportional on a pair of commuting elements have a nonzero cup product; this is how the cup product of an abelian pro-p group such as ℤ_p × ℤ_p is shown to be nondegenerate.

Main definitions

• TauCeti.characterCochain, TauCeti.characterCocycle: the homogeneous one-cocycle (g₀, g₁) ↦ χ (g₀⁻¹ g₁) of a continuous character χ.

Main results

• TauCeti.cohomFpLinearEquivContinuousZModDual_symm_apply: the class attached to a character is the class of its homogeneous cocycle.
• TauCeti.cohomFpLinearEquivContinuousZModDual_cohomFpMap: pullback of degree-one classes is precomposition of their characters.
• TauCeti.mul_eq_mul_of_cupFp_eq_zero: if a ⌣ b = 0 then the characters χ, ψ of a, b satisfy χ(x) ψ(y) = χ(y) ψ(x) for commuting x and y.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., I §1.4.
• J.-P. Serre, Galois Cohomology, Springer (1997), Chapter I, §4.5.

Homogeneous cochains with trivial coefficients

theorem TauCeti.homogeneousCochains_trivialFp_one_apply_eq (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a : ↑((trivialFp p G).homogeneousCochains.X 1).toModuleCat) (g₀ g₁ : G) : (↑a g₀) g₁ = (↑a 1) (g₀⁻¹ * g₁)

A homogeneous one-cochain with trivial coefficients is determined by its values at (1, g): a g₀ g₁ = a 1 (g₀⁻¹ g₁).

The cocycle of a character

noncomputable def TauCeti.characterCochain (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : continuousZModDual p G) : ↑((trivialFp p G).homogeneousCochains.X 1).toModuleCat

The homogeneous one-cochain (g₀, g₁) ↦ χ (g₀⁻¹ g₁) of a continuous character χ : G → 𝔽_p, with trivial 𝔽_p coefficients.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.characterCochain_apply (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : continuousZModDual p G) (g₀ g₁ : G) : (↑(characterCochain p χ) g₀) g₁ = (trivialFpEquiv p G).symm (Multiplicative.toAdd ((Additive.toMul χ) (g₀⁻¹ * g₁)))

The value of the cochain of χ at (g₀, g₁) is χ (g₀⁻¹ g₁), lifted to the coefficients.

theorem TauCeti.d_characterCochain (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : continuousZModDual p G) : (TopModuleCat.Hom.hom ((trivialFp p G).homogeneousCochains.d 1 (1 + 1))) (characterCochain p χ) = 0

The cochain of a character is a cocycle.

noncomputable def TauCeti.characterCocycle (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : continuousZModDual p G) : ↑(ContinuousCohomology.cocycles (trivialFp p G) 1).toModuleCat

The homogeneous one-cocycle (g₀, g₁) ↦ χ (g₀⁻¹ g₁) of a continuous character χ : G → 𝔽_p.

Equations

• TauCeti.characterCocycle p χ = HomologicalComplex.cyclesMkOfEq (TauCeti.trivialFp p G).homogeneousCochains (TauCeti.characterCochain p χ) (1 + 1) TauCeti.characterCocycle._proof_2✝ ⋯

theorem TauCeti.iCycles_characterCocycle (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : continuousZModDual p G) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (trivialFp p G).homogeneousCochains 1)) (characterCocycle p χ) = characterCochain p χ

The underlying cochain of the cocycle of χ is characterCochain p χ.

The class of a character

@[simp]

theorem TauCeti.cohomFpLinearEquivContinuousZModDual_π_characterCocycle (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : continuousZModDual p G) : (cohomFpLinearEquivContinuousZModDual p G) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π (trivialFp p G) 1)) (characterCocycle p χ)) = χ

The character attached to the class of the homogeneous cocycle of χ is χ.

theorem TauCeti.cohomFpLinearEquivContinuousZModDual_symm_apply (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : continuousZModDual p G) : (cohomFpLinearEquivContinuousZModDual p G).symm χ = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π (trivialFp p G) 1)) (characterCocycle p χ)

The class of a character is the class of its homogeneous cocycle (g₀, g₁) ↦ χ (g₀⁻¹ g₁): the inverse of TauCeti.cohomFpLinearEquivContinuousZModDual, computed on Mathlib's homogeneous cochains, which is the form a cup-product computation consumes.

theorem TauCeti.cohomFpLinearEquivContinuousZModDual_cohomFpMap (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : H →ₜ* G) (x : ↑(cohomFp p G 1).toModuleCat) : (cohomFpLinearEquivContinuousZModDual p H) ((CategoryTheory.ConcreteCategory.hom (cohomFpMap p f 1)) x) = f.continuousZModDualMap ((cohomFpLinearEquivContinuousZModDual p G) x)

The identification of degree-one cohomology with continuous characters is natural in the group: pullback of cohomology classes corresponds to precomposition of characters.

The symmetry test for the cup product

theorem TauCeti.mul_eq_mul_of_cupFp_eq_zero (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {a b : ↑(cohomFp p G 1).toModuleCat} (h : ((cupFp p G) a) b = 0) {x y : G} (hxy : Commute x y) : Multiplicative.toAdd ((Additive.toMul ((cohomFpLinearEquivContinuousZModDual p G) a)) x) * Multiplicative.toAdd ((Additive.toMul ((cohomFpLinearEquivContinuousZModDual p G) b)) y) = Multiplicative.toAdd ((Additive.toMul ((cohomFpLinearEquivContinuousZModDual p G) a)) y) * Multiplicative.toAdd ((Additive.toMul ((cohomFpLinearEquivContinuousZModDual p G) b)) x)

A vanishing cup product forces a symmetry on commuting elements. Let χ and ψ be the characters of the classes a and b of H¹(G, 𝔽_p). If a ⌣ b = 0 in H²(G, 𝔽_p), then χ(x) ψ(y) = χ(y) ψ(x) for every pair of commuting elements x, y of G. Indeed the cup product is then the coboundary of an invariant one-cochain w, whose value at (1, x, xy) is w 1 y - w 1 (xy) + w 1 x, which is symmetric in x and y when xy = yx.