The index-two coefficient sequence in characteristic two

For an open subgroup U of index two and a discrete G-module M killed by two, the coinduction unit and trace form the short exact sequence

0 → M → Coind_U^G M → M → 0.

For trivial coefficients the unit is the inclusion of constant functions and the trace is the sum of the two coordinates. This is the coefficient sequence whose long exact sequence, under Shapiro's isomorphism, alternates restriction, corestriction and cup product with the character of G/U.

indexTwoShortExact_explicitDelta0 fixes the connecting-map normalization: an invariant m maps to the class of the cocycle that is zero on U and m off U. In particular, for trivial 𝔽₂ coefficients, the boundary of 1 is the nonzero character with kernel U. The coefficient sequence works for nontrivial actions as well.

References

• A. Kozlowski, The Evens–Kahn formula for the total Stiefel–Whitney class, Proc. Amer. Math. Soc. 91 (1984), Lemma 2.4.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.3.2), for the connecting-map convention.

theorem TauCeti.DiscreteCoind.trace_eq_add_of_index_two {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {U : Subgroup G} [U.FiniteIndex] {M : Type v} [AddCommGroup M] [DistribMulAction G M] (hU : U.index = 2) {s : G} (hs : s ∉ U) (f : DiscreteCoind G U M) : (trace G U M) f = f 1 + s • f s⁻¹

The trace at index two has the two terms at 1 and at an arbitrary outside representative. The action on the second term is retained even when the coefficients are nontrivial.

theorem TauCeti.DiscreteCoind.trace_eq_zero_iff_exists_unit_of_index_two {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {U : Subgroup G} [U.FiniteIndex] {M : Type v} [AddCommGroup M] [DistribMulAction G M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hU : U.index = 2) (hM : ∀ (m : M), 2 • m = 0) (f : DiscreteCoind G U M) : (trace G U M) f = 0 ↔ ∃ (m : M), (unit G U M) m = f

At index two, for coefficients killed by two, the kernel of the trace is the image of the coinduction unit. No triviality of the action is assumed.

noncomputable def TauCeti.DiscreteCoind.indexTwoShortExact (G : Type u) [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) [U.FiniteIndex] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hU : U.index = 2) (hUo : IsOpen ↑U) (hM : ∀ (m : M), 2 • m = 0) : ContCohomology.DiscreteShortExact G M (DiscreteCoind G U M) M

The short exact sequence 0 → M → Coind_U^G M → M → 0 for an open subgroup of index two and discrete coefficients killed by two. Its maps are the unit and trace.

Equations

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

@[simp]

theorem TauCeti.DiscreteCoind.indexTwoShortExact_incl (G : Type u) [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) [U.FiniteIndex] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hU : U.index = 2) (hUo : IsOpen ↑U) (hM : ∀ (m : M), 2 • m = 0) : (indexTwoShortExact G U M hU hUo hM).incl = (unit G U M).toAddMonoidHom

The first map of the index-two sequence is the coinduction unit.

@[simp]

theorem TauCeti.DiscreteCoind.indexTwoShortExact_proj (G : Type u) [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) [U.FiniteIndex] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hU : U.index = 2) (hUo : IsOpen ↑U) (hM : ∀ (m : M), 2 • m = 0) : (indexTwoShortExact G U M hU hUo hM).proj = (trace G U M).toAddMonoidHom

The second map of the index-two sequence is the trace.

noncomputable def TauCeti.ContCohomology.indexTwoConnectingCocycle {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} {M : Type v} [AddCommGroup M] [TopologicalSpace M] [DistribMulAction G M] [ContinuousMul G] [IsTopologicalAddGroup M] (hU : U.index = 2) (hUo : IsOpen ↑U) (c : ↥(H0 G M)) (hc2 : 2 • ↑c = 0) : ↥(Z1 G M)

The index-two connecting cocycle of an invariant c: zero on the subgroup, c off it.

Equations

• TauCeti.ContCohomology.indexTwoConnectingCocycle hU hUo c hc2 = ⟨fun (g : G) => if g ∈ U then 0 else ↑c, ⋯⟩

@[simp]

theorem TauCeti.ContCohomology.indexTwoConnectingCocycle_apply {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} {M : Type v} [AddCommGroup M] [TopologicalSpace M] [DistribMulAction G M] [ContinuousMul G] [IsTopologicalAddGroup M] (hU : U.index = 2) (hUo : IsOpen ↑U) (c : ↥(H0 G M)) (hc2 : 2 • ↑c = 0) (g : G) : ↑(indexTwoConnectingCocycle hU hUo c hc2) g = if g ∈ U then 0 else ↑c

The value formula of the connecting cocycle.

theorem TauCeti.ContCohomology.indexTwoShortExact_explicitDelta0 {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} [U.FiniteIndex] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [IsTopologicalGroup G] [CompactSpace G] (hU : U.index = 2) (hUo : IsOpen ↑U) (hM : ∀ (m : M), 2 • m = 0) (c : ↥(H0 G M)) : (DiscreteCoind.indexTwoShortExact G U M hU hUo hM).explicitDelta0 c = ↑(indexTwoConnectingCocycle hU hUo c ⋯)

The degree-zero connecting map of the index-two coefficient sequence is the class of the cocycle equal to c outside the subgroup and zero inside.

theorem TauCeti.ContCohomology.indexTwoShortExact_explicitDelta0_eq_zero_iff {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} [U.FiniteIndex] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [IsTopologicalGroup G] [CompactSpace G] (hU : U.index = 2) (hUo : IsOpen ↑U) (hM : ∀ (m : M), 2 • m = 0) (htriv : ∀ (g : G) (m : M), g • m = m) (c : ↥(H0 G M)) : (DiscreteCoind.indexTwoShortExact G U M hU hUo hM).explicitDelta0 c = 0 ↔ c = 0

For a trivial action the connecting map is injective: an invariant coefficient has zero boundary exactly when it is zero. Thus the boundary of 1 for trivial 𝔽₂ coefficients is nonzero, as required for the index-two character.