Transitivity of all-degree corestriction

For open subgroups V ≤ U ≤ G of finite index, corestriction on canonical continuous cohomology is transitive in every degree:

cor_V^G = cor_U^G ∘ cor_V^U.

The relative map corestrictionLe first transports cohomology from V to its copy V.subgroupOf U inside U, then applies corestriction there. Transitivity gives all-degree corestriction coherent transfer maps along subgroup towers: a transfer may be assembled through intermediate open subgroups without depending on how the inclusion is factored.

Main definitions

• TauCeti.ContinuousCohomology.subgroupOfMap: transport from a subgroup to its canonical copy inside an intermediate subgroup.
• TauCeti.ContinuousCohomology.corestrictionLe: all-degree corestriction along an inclusion.

Main results

• TauCeti.ContinuousCohomology.shapiroMap_trans: transitivity of the Shapiro map.
• TauCeti.ContinuousCohomology.corestriction_trans: transitivity of corestriction in every degree.

noncomputable def TauCeti.ContinuousCohomology.subgroupOfMap {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U V : Subgroup G) (hVU : V ≤ U) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (n : ℕ) : continuousCohomology n (ofDiscreteModule ℤ (↥V) M) ⟶ continuousCohomology n (ofDiscreteModule ℤ (↥(V.subgroupOf U)) M)

Transport continuous cohomology from a subgroup V to its canonical copy V.subgroupOf U inside a larger subgroup U.

theorem TauCeti.ContinuousCohomology.subgroupOfMap_def {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U V : Subgroup G) (hVU : V ≤ U) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (n : ℕ) : subgroupOfMap U V hVU M n = ContinuousCohomology.map (↑(Subgroup.subgroupOfContinuousMulEquivOfLe hVU)) (ofDiscreteModulePair (↑(Subgroup.subgroupOfContinuousMulEquivOfLe hVU)) LinearMap.id ⋯) n

The defining equation for transport to the canonical copy V.subgroupOf U.

noncomputable def TauCeti.ContinuousCohomology.corestrictionLe {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U V : Subgroup G) (hVU : V ≤ U) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (hU : IsClosed ↑U) [(V.subgroupOf U).FiniteIndex] (hV : IsOpen ↑(V.subgroupOf U)) (n : ℕ) : continuousCohomology n (ofDiscreteModule ℤ (↥V) M) ⟶ continuousCohomology n (ofDiscreteModule ℤ (↥U) M)

All-degree corestriction along an inclusion V ≤ U: transport the cohomology of V to its canonical copy V.subgroupOf U, then apply corestriction inside U. The intermediate subgroup U need only be closed in the compact group G; the lower subgroup is required to be open in U and of finite index there.

theorem TauCeti.ContinuousCohomology.corestrictionLe_def {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U V : Subgroup G) (hVU : V ≤ U) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (hU : IsClosed ↑U) [(V.subgroupOf U).FiniteIndex] (hV : IsOpen ↑(V.subgroupOf U)) (n : ℕ) : corestrictionLe U V hVU M hU hV n = CategoryTheory.CategoryStruct.comp (subgroupOfMap U V hVU M n) (corestriction (V.subgroupOf U) M hV n)

The defining equation for relative corestriction: transport to V.subgroupOf U, then apply corestriction inside U.

theorem TauCeti.ContinuousCohomology.shapiroMap_trans {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U V : Subgroup G) (hVU : V ≤ U) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (n : ℕ) : have c := DiscreteCoind.transIso ⋯ ⋯ ⋯; CategoryTheory.CategoryStruct.comp (coeffMap c.inv n) (CategoryTheory.CategoryStruct.comp (shapiroMap U (DiscreteCoind (↥U) (V.subgroupOf U) M) n) (shapiroMap (V.subgroupOf U) M n)) = CategoryTheory.CategoryStruct.comp (shapiroMap V M n) (subgroupOfMap U V hVU M n)

Shapiro's map is transitive. For subgroups V ≤ U of a compact group G, the Shapiro map of V followed by the transport to the copy V.subgroupOf U of V inside U is the identification Coind_V^G M ≅ Coind_U^G (Coind_{V ⊓ U}^U M) of coinduced modules followed by the Shapiro maps of U in G and of V.subgroupOf U in U.

theorem TauCeti.ContinuousCohomology.corestriction_trans {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U V : Subgroup G) (hVU : V ≤ U) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (hU : IsOpen ↑U) (hV : IsOpen ↑V) [U.FiniteIndex] [(V.subgroupOf U).FiniteIndex] (n : ℕ) : corestriction V M hV n = CategoryTheory.CategoryStruct.comp (corestrictionLe U V hVU M ⋯ ⋯ n) (corestriction U M hU n)

Transitivity of corestriction in every degree. For open finite-index subgroups V ≤ U ≤ G, direct corestriction from V to G equals corestriction from V to U followed by corestriction from U to G.