Cup squares of classes of H¹(G, 𝔽₂) that lift to ℤ/4

Let G be a topological group and φ : G →ₜ* ℤ/4 a continuous character. Its reduction modulo 2 is the continuous character φ.zmodFourReduction : G → 𝔽₂, and the class of that character in H¹(G, 𝔽₂) under the identification TauCeti.cohomFpLinearEquivContinuousZModDual of H¹(G, 𝔽₂) with the continuous 𝔽₂-dual of G is φ.zmodFourReductionClass; it is represented by the homogeneous cocycle (g₀, g₁) ↦ φ(g₀⁻¹ g₁) mod 2 (TauCeti.characterCocycle). The cup square of this class vanishes: the carry ZMod.carryFour = ⌊·/2⌋ : ℤ/4 → 𝔽₂ satisfies ⌊(u + v)/2⌋ = ⌊u/2⌋ + ⌊v/2⌋ + (u mod 2)(v mod 2) (ZMod.carryFour_add), so the cup square (g₀, g₁, g₂) ↦ (φ(g₀⁻¹ g₁) mod 2)(φ(g₁⁻¹ g₂) mod 2) is the coboundary of the homogeneous one-cochain (g₀, g₁) ↦ ⌊φ(g₀⁻¹ g₁)/2⌋. Conversely, if the cup square of the class of a character χ : G → 𝔽₂ vanishes, then the cup cocycle (g₀, g₁, g₂) ↦ χ(g₀⁻¹ g₁) χ(g₁⁻¹ g₂) is the coboundary of a homogeneous one-cochain ψ, and g ↦ χ(g) + 2 ψ(1, g), with χ(g) ∈ {0, 1} lifted to ℤ/4, is a continuous character G → ℤ/4 reducing to χ: the carry identity makes the two-cocycle condition on ψ exactly the multiplicativity of this lift. Together these are the classical identification of the cup square on H¹(G, 𝔽₂) with the Bockstein of 0 → 𝔽₂ → ℤ/4 → 𝔽₂ → 0, whose kernel consists exactly of the classes that lift to ℤ/4. The class of a lift is nonzero as soon as φ takes an odd value.

Together with the nonvanishing of the cup square of the generator of H¹(ℤ/2, 𝔽₂), this is what distinguishes ℤ/2 from the cyclic groups ℤ/2ᵏ, k ≥ 2, whose mod-2 character lifts to ℤ/4: the cup pairing on H¹(ℤ/2ᵏ, 𝔽₂) vanishes for k ≥ 2.

Main declarations

• ContinuousMonoidHom.zmodFourReduction: the reduction modulo 2 of a continuous character φ : G →ₜ* ℤ/4, a continuous character G → 𝔽₂.
• ContinuousMonoidHom.zmodFourReductionClass: the class in H¹(G, 𝔽₂) of that reduction; ContinuousMonoidHom.cohomFpLinearEquivContinuousZModDual_zmodFourReductionClass recovers the reduction as its character.
• ContinuousMonoidHom.zmodFourReductionClass_ne_zero: the class is nonzero when φ takes an odd value.
• ContinuousMonoidHom.cupFp_zmodFourReductionClass_self_eq_zero: the cup square of the class vanishes.
• TauCeti.exists_zmodFourReductionClass_eq_of_cupFp_self_eq_zero, TauCeti.cupFp_self_eq_zero_iff_exists_zmodFourReductionClass_eq: a class of H¹(G, 𝔽₂) has vanishing cup square exactly when it is the class of the reduction of a character G → ℤ/4.
• TauCeti.forall_cupFp_self_eq_zero_iff_forall_exists_zmodFourReduction_eq: every cup square on H¹(G, 𝔽₂) vanishes exactly when every continuous character G → 𝔽₂ lifts to ℤ/4.
• TauCeti.forall_exists_zmodFourReduction_eq_iff_of_topologicalAbelianization: whether every continuous character G → 𝔽₂ lifts to ℤ/4 is decided on any model of the topological abelianization of G, since both kinds of characters factor through it.

References

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

The reduction modulo 2 and its class

def ContinuousMonoidHom.zmodFourReduction {G : Type u} [Group G] [TopologicalSpace G] (φ : G →ₜ* Multiplicative (ZMod 4)) : TauCeti.continuousZModDual 2 G

The reduction modulo 2 of a continuous character φ : G →ₜ* ℤ/4: the continuous character g ↦ φ g mod 2 of G with values in 𝔽₂, as an element of the continuous 𝔽₂-dual of G.

Equations

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

@[simp]

theorem ContinuousMonoidHom.zmodFourReduction_apply {G : Type u} [Group G] [TopologicalSpace G] (φ : G →ₜ* Multiplicative (ZMod 4)) (g : G) : Multiplicative.toAdd ((Additive.toMul φ.zmodFourReduction) g) = (ZMod.castHom zmodFourReduction_apply._proof_1 (ZMod 2)) (Multiplicative.toAdd (φ g))

The reduction of φ takes the value φ g mod 2 at g.

noncomputable def ContinuousMonoidHom.zmodFourReductionClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : G →ₜ* Multiplicative (ZMod 4)) : ↑(TauCeti.cohomFp 2 G 1).toModuleCat

The class in H¹(G, 𝔽₂) of the reduction modulo 2 of a continuous character φ : G →ₜ* ℤ/4: the class attached to the character φ.zmodFourReduction by the identification TauCeti.cohomFpLinearEquivContinuousZModDual of H¹(G, 𝔽₂) with the continuous 𝔽₂-dual of G.

Equations

• φ.zmodFourReductionClass = (TauCeti.cohomFpLinearEquivContinuousZModDual 2 G).symm φ.zmodFourReduction

@[simp]

theorem ContinuousMonoidHom.cohomFpLinearEquivContinuousZModDual_zmodFourReductionClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : G →ₜ* Multiplicative (ZMod 4)) : (TauCeti.cohomFpLinearEquivContinuousZModDual 2 G) φ.zmodFourReductionClass = φ.zmodFourReduction

The character of the class of the reduction of φ is the reduction of φ.

theorem ContinuousMonoidHom.zmodFourReduction_eq_iff {G : Type u} [Group G] [TopologicalSpace G] (φ : G →ₜ* Multiplicative (ZMod 4)) (χ : TauCeti.continuousZModDual 2 G) : φ.zmodFourReduction = χ ↔ ∀ (g : G), (ZMod.castHom zmodFourReduction_apply._proof_1 (ZMod 2)) (Multiplicative.toAdd (φ g)) = Multiplicative.toAdd ((Additive.toMul χ) g)

φ : G →ₜ* ℤ/4 reduces to the character χ : G → 𝔽₂ exactly when φ g mod 2 = χ g for every g.

theorem ContinuousMonoidHom.zmodFourReductionClass_ne_zero {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : G →ₜ* Multiplicative (ZMod 4)) {g : G} (hg : (ZMod.castHom zmodFourReduction_apply._proof_1 (ZMod 2)) (Multiplicative.toAdd (φ g)) ≠ 0) : φ.zmodFourReductionClass ≠ 0

The class of the reduction of φ is nonzero when φ takes an odd value: its character takes the value φ g mod 2 ≠ 0 at g.

The cup square

@[simp]

theorem ContinuousMonoidHom.cupFp_zmodFourReductionClass_self_eq_zero {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : G →ₜ* Multiplicative (ZMod 4)) : ((TauCeti.cupFp 2 G) φ.zmodFourReductionClass) φ.zmodFourReductionClass = 0

The cup square of a class of H¹(G, 𝔽₂) that lifts to ℤ/4 vanishes. The cup square of the cocycle (g₀, g₁) ↦ φ (g₀⁻¹ g₁) mod 2 is the coboundary of the homogeneous one-cochain (g₀, g₁) ↦ ⌊φ (g₀⁻¹ g₁) / 2⌋, by the carry identity ZMod.carryFour_add.

The converse: a class with vanishing cup square lifts to ℤ/4

theorem TauCeti.exists_zmodFourReductionClass_eq_of_cupFp_self_eq_zero {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {a : ↑(cohomFp 2 G 1).toModuleCat} (h : ((cupFp 2 G) a) a = 0) : ∃ (φ : G →ₜ* Multiplicative (ZMod 4)), φ.zmodFourReductionClass = a

A class of H¹(G, 𝔽₂) with vanishing cup square is the class of the reduction of a character G → ℤ/4. If the cup square of the class of χ : G → 𝔽₂ vanishes, its cup cocycle (g₀, g₁, g₂) ↦ χ(g₀⁻¹ g₁) χ(g₁⁻¹ g₂) is the coboundary of a homogeneous one-cochain ψ, and g ↦ χ(g) + 2 ψ(1, g) is a continuous character G → ℤ/4 reducing to χ.

theorem TauCeti.cupFp_self_eq_zero_iff_exists_zmodFourReductionClass_eq {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a : ↑(cohomFp 2 G 1).toModuleCat) : ((cupFp 2 G) a) a = 0 ↔ ∃ (φ : G →ₜ* Multiplicative (ZMod 4)), φ.zmodFourReductionClass = a

Bockstein exactness on H¹(G, 𝔽₂): a class has vanishing cup square exactly when it is the class of the reduction modulo 2 of a continuous character G → ℤ/4.

theorem TauCeti.forall_cupFp_self_eq_zero_iff_forall_exists_zmodFourReduction_eq {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : (∀ (a : ↑(cohomFp 2 G 1).toModuleCat), ((cupFp 2 G) a) a = 0) ↔ ∀ (χ : continuousZModDual 2 G), ∃ (φ : G →ₜ* Multiplicative (ZMod 4)), φ.zmodFourReduction = χ

Every cup square on H¹(G, 𝔽₂) vanishes exactly when every continuous character G → 𝔽₂ lifts to a continuous character G → ℤ/4.

Transport of lifting problems along the abelianization

theorem TauCeti.forall_exists_zmodFourReduction_eq_iff_of_topologicalAbelianization {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u_1} [Group A] [TopologicalSpace A] (e : TopologicalAbelianization G ≃ₜ* A) : (∀ (χ : continuousZModDual 2 G), ∃ (φ : G →ₜ* Multiplicative (ZMod 4)), φ.zmodFourReduction = χ) ↔ ∀ (χ : A →ₜ* Multiplicative (ZMod 2)), ∃ (φ : A →ₜ* Multiplicative (ZMod 4)), ∀ (a : A), (ZMod.castHom ContinuousMonoidHom.zmodFourReduction_apply._proof_1 (ZMod 2)) (Multiplicative.toAdd (φ a)) = Multiplicative.toAdd (χ a)

Lifting characters from 𝔽₂ to ℤ/4 is decided on the abelianization. For a model A ≅ G^{ab} of the topological abelianization of G, every continuous character G → 𝔽₂ lifts to a continuous character G → ℤ/4 exactly when every continuous character A → 𝔽₂ does: both kinds of characters factor through G^{ab}.