Corestriction at index two, and the conjugation res ∘ cor - id

Let U be an open subgroup of index two in a topological group G and let M be a topological G-module. On explicit H¹(U, M), the composite res_U ∘ cor_U of degree-one corestriction and restriction is 1 + s for any element s of the nontrivial coset: computed on the transversal {1, s}, the corestriction sum has two terms, the first restricts to the identity and the second to conjugation by s. The difference res ∘ cor - id is therefore the conjugation action of the nontrivial coset on explicit H¹(U, M), defined without choosing an element of that coset.

This is the conjugation evensConj of the index-two Evens norm, hence the name evensConj1; it is stated for an arbitrary topological coefficient module and uses only the corestriction and conjugation APIs. It supplies the conjugate class in the graph-cocycle restriction computation of TauCeti.RepresentationTheory.Homological.ContCohomology.Evens.Restriction. The theorem evensConj1_eq_explicitConj1 identifies it with conjugation by every element outside U, providing the comparison needed for computations using a chosen coset representative.

The computation is carried out on cochains for an arbitrary coefficient module, with no topology: cochainsCor1_indexTwoTransversal_apply_coe is the two-term formula for the corestriction cochain on the elements of U. The simp rule sum_indexTwoTransversal_smul_lWord evaluates the sum produced by cochainsCor1_apply; it only needs an additive commutative monoid of coefficients, and the named corestriction formula is also available for rewriting.

Main definitions

• TauCeti.ContCohomology.evensConj1: the map res ∘ cor - id on explicit H¹(U, M) for an open subgroup U of index two.

Main results

• TauCeti.ContCohomology.cochainsCor1_indexTwoTransversal_apply_coe: on γ ∈ U, the corestriction cochain over the transversal {1, s} is f γ + s • f (s⁻¹ γ s).
• TauCeti.ContCohomology.evensConj1_eq_explicitConj1: evensConj1 is conjugation by every element outside U.

References

• L. Evens, A generalization of the transfer map in the cohomology of groups, Trans. Amer. Math. Soc. 108 (1963), 54–65.
• A. Kozlowski, The Evens–Kahn formula for the total Stiefel–Whitney class, Proc. Amer. Math. Soc. 91 (1984), 309–313, Lemma 2.4.

@[simp]

theorem TauCeti.ContCohomology.sum_indexTwoTransversal_smul_lWord {G : Type u} [Group G] {M : Type v} {U : Subgroup G} [AddCommMonoid M] [DistribMulAction G M] (hU : U.index = 2) {s : G} (hs : s ∉ U) (f : ↥U → M) (γ : G) (hγ : γ ∈ U) : ∑ u : G ⧸ U, U.indexTwoTransversal s u • f ⟨lWord U (U.indexTwoTransversal s) u γ, ⋯⟩ = f ⟨γ, hγ⟩ + s • f ⟨s⁻¹ * γ * s, ⋯⟩

The corestriction sum on the transversal {1, s}, evaluated on an element of U, has the two terms f γ and s • f (s⁻¹ γ s).

theorem TauCeti.ContCohomology.cochainsCor1_indexTwoTransversal_apply_coe {G : Type u} [Group G] {M : Type v} {U : Subgroup G} [AddCommGroup M] [DistribMulAction G M] (hU : U.index = 2) {s : G} (hs : s ∉ U) (f : ↥U → M) (γ : ↥U) : (cochainsCor1 G M U (U.indexTwoTransversal s) ⋯) f ↑γ = f γ + s • f ⟨s⁻¹ * ↑γ * s, ⋯⟩

The corestriction cochain over the transversal {1, s}, on the subgroup. For U of index two, s ∉ U and γ ∈ U, the two terms of the corestriction sum of f : U → M are f γ at the trivial coset and s • f (s⁻¹ γ s) at the coset of s.

noncomputable def TauCeti.ContCohomology.evensConj1 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (U : Subgroup G) (hU : U.index = 2) (hUo : IsOpen ↑U) : H1 (↥U) M →+ H1 (↥U) M

The conjugation on H¹(U, M) of an open subgroup of index two, defined choice-free as res ∘ cor - id, with cor the degree-one corestriction TauCeti.ContCohomology.explicitCor1.

At index two res ∘ cor is 1 + s for every element s outside U, so this difference is conjugation by s for every s ∉ U (evensConj1_eq_explicitConj1) and depends on U alone. It is the conjugate α ↦ s · α appearing in the identities of the index-two Evens norm.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.evensConj1_apply (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (U : Subgroup G) (hU : U.index = 2) (hUo : IsOpen ↑U) (x : H1 (↥U) M) : (evensConj1 G M U hU hUo) x = (explicitRes1 G M U) ((explicitCor1 G M U hUo) x) - x

The defining formula of evensConj1: restriction of the corestriction, minus the identity.

theorem TauCeti.ContCohomology.evensConj1_eq_explicitConj1 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (U : Subgroup G) (hU : U.index = 2) (hUo : IsOpen ↑U) {s : G} (hs : s ∉ U) : evensConj1 G M U hU hUo = explicitConj1 U s

The choice-free conjugation is conjugation by every element outside U. For s ∉ U, evensConj1 is the conjugation map TauCeti.ContCohomology.explicitConj1 U s of the normal subgroup U.