Pullback of corestriction along a transitive coset map

Let φ : H → G carry a finite-index subgroup V into U. If the induced map H / V → G / U is a bijection, pullback along a compatible coefficient map commutes with corestriction in degrees zero, one and two. Neither injectivity nor surjectivity of φ is needed. This includes inflation along a quotient and the transitive-orbit case of the Mackey formula. In localizing a corestricted Galois class, it allows passage from a local absolute Galois group to its image before applying the subgroup Mackey formula.

The coset bijection is supplied as an equivalence with its value on representatives. For compatible transversals the identity already holds on arbitrary cochains; independence of the transversal gives the public identities on cohomology. The action on the coefficients need not be trivial. The groups need not be compact and the coefficients need not be discrete: openness and finite index of the two subgroups suffice.

The bijection hypothesis is essential. For an inclusion whose image has several orbits on G / U, pullback of corestriction is a sum of corestrictions, not a single corestriction.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., I §5, especially (1.5.6).
• K. S. Brown, Cohomology of Groups, III §9.

theorem TauCeti.ContCohomology.explicitCor0_pullback {G : Type u} {H : Type v} [Group G] [Group H] {M : Type w} {N : Type z} [AddCommGroup M] [AddCommGroup N] [DistribMulAction G M] [DistribMulAction H N] (U : Subgroup G) (V : Subgroup H) [U.FiniteIndex] [V.FiniteIndex] (φ : H →* G) (κ : ↥V →* ↥U) (hκ : ∀ (v : ↥V), ↑(κ v) = φ ↑v) (e : H ⧸ V ≃ G ⧸ U) (he : ∀ (h : H), e ↑h = ↑(φ h)) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (m : ↥(H0 (↥U) M)) : (explicitMap0 G M φ f hf) ((explicitCor0 G M U) m) = (explicitCor0 H N V) ((explicitMap0 (↥U) M κ f ⋯) m)

Pullback commutes with the norm on invariants if it induces a bijection on coset spaces. No topology is required in degree zero.

theorem TauCeti.ContCohomology.cochainsCor1_pullback {G : Type u} {H : Type v} [Group G] [Group H] {M : Type w} {N : Type z} [AddCommGroup M] [AddCommGroup N] [DistribMulAction G M] [DistribMulAction H N] (U : Subgroup G) (V : Subgroup H) [U.FiniteIndex] [V.FiniteIndex] (φ : H →* G) (κ : ↥V →* ↥U) (hκ : ∀ (v : ↥V), ↑(κ v) = φ ↑v) (e : H ⧸ V ≃ G ⧸ U) (he : ∀ (h : H), e ↑h = ↑(φ h)) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (t : G ⧸ U → G) (ht : ∀ (q : G ⧸ U), ↑(t q) = q) (s : H ⧸ V → H) (hs : ∀ (q : H ⧸ V), ↑(s q) = q) (hst : ∀ (q : H ⧸ V), t (e q) = φ (s q)) (c : ↥U → M) (h : H) : f ((cochainsCor1 G M U t ht) c (φ h)) = (cochainsCor1 H N V s hs) (fun (v : ↥V) => f (c (κ v))) h

Pullback commutes with the degree-one corestriction cochain when the transversals agree under the induced coset bijection. No cocycle or continuity hypothesis is required.

theorem TauCeti.ContCohomology.cochainsCor2_pullback {G : Type u} {H : Type v} [Group G] [Group H] {M : Type w} {N : Type z} [AddCommGroup M] [AddCommGroup N] [DistribMulAction G M] [DistribMulAction H N] (U : Subgroup G) (V : Subgroup H) [U.FiniteIndex] [V.FiniteIndex] (φ : H →* G) (κ : ↥V →* ↥U) (hκ : ∀ (v : ↥V), ↑(κ v) = φ ↑v) (e : H ⧸ V ≃ G ⧸ U) (he : ∀ (h : H), e ↑h = ↑(φ h)) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (t : G ⧸ U → G) (ht : ∀ (q : G ⧸ U), ↑(t q) = q) (s : H ⧸ V → H) (hs : ∀ (q : H ⧸ V), ↑(s q) = q) (hst : ∀ (q : H ⧸ V), t (e q) = φ (s q)) (c : ↥U × ↥U → M) (h j : H) : f ((cochainsCor2 G M U t ht) c (φ h, φ j)) = (cochainsCor2 H N V s hs) (fun (p : ↥V × ↥V) => f (c (κ p.1, κ p.2))) (h, j)

Pullback commutes with the degree-two corestriction cochain when the transversals agree under the induced coset bijection. No cocycle or continuity hypothesis is required.

theorem TauCeti.ContCohomology.explicitCor1_pullback {G : Type u} {H : Type v} [Group G] [Group H] {M : Type w} {N : Type z} [AddCommGroup M] [AddCommGroup N] [DistribMulAction G M] [DistribMulAction H N] (U : Subgroup G) (V : Subgroup H) [U.FiniteIndex] [V.FiniteIndex] [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] [TopologicalSpace N] [IsTopologicalAddGroup N] [ContinuousSMul H N] (φ : H →ₜ* G) (κ : ↥V →ₜ* ↥U) (hκ : ∀ (v : ↥V), ↑(κ v) = φ ↑v) (e : H ⧸ V ≃ G ⧸ U) (he : ∀ (h : H), e ↑h = ↑(φ h)) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (hU : IsOpen ↑U) (hV : IsOpen ↑V) [SeparatelyContinuousMul G] [SeparatelyContinuousMul H] (x : H1 (↥U) M) : (explicitMap1 G M H N φ f hf hequiv) ((explicitCor1 G M U hU) x) = (explicitCor1 H N V hV) ((explicitMap1 (↥U) M (↥V) N κ f hf ⋯) x)

Pullback along a compatible pair commutes with degree-one corestriction if the induced map of coset spaces is bijective. The subgroup homomorphism κ is the restriction of φ.

theorem TauCeti.ContCohomology.explicitCor2_pullback {G : Type u} {H : Type v} [Group G] [Group H] {M : Type w} {N : Type z} [AddCommGroup M] [AddCommGroup N] [DistribMulAction G M] [DistribMulAction H N] (U : Subgroup G) (V : Subgroup H) [U.FiniteIndex] [V.FiniteIndex] [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] [TopologicalSpace N] [IsTopologicalAddGroup N] [ContinuousSMul H N] (φ : H →ₜ* G) (κ : ↥V →ₜ* ↥U) (hκ : ∀ (v : ↥V), ↑(κ v) = φ ↑v) (e : H ⧸ V ≃ G ⧸ U) (he : ∀ (h : H), e ↑h = ↑(φ h)) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (hU : IsOpen ↑U) (hV : IsOpen ↑V) [ContinuousMul G] [ContinuousMul H] (x : H2 (↥U) M) : (explicitMap2 G M H N φ f hf hequiv) ((explicitCor2 G M U hU) x) = (explicitCor2 H N V hV) ((explicitMap2 (↥U) M (↥V) N κ f hf ⋯) x)

Pullback along a compatible pair commutes with degree-two corestriction if the induced map of coset spaces is bijective. This permits replacing the source group by its image before using a subgroup Mackey formula.