Continuous Shapiro isomorphism in degree two for open S
ProvedgroupCohomology.nonempty_continuousH2_coind_linearEquiv_continuousH2Let be a commutative ring and a group, let be a group homomorphism into the group of -algebra automorphisms of AlgebraicClosure ℚ, and let be a subgroup subject to the openness hypothesis hS: there is an intermediate field of , finite-dimensional over , whose fixing subgroup has -preimage contained in . Let be a -linear representation of (an object of Rep k S). Then the type of -linear equivalences between and is nonempty. Here, for a level map and a representation , is the quotient of the submodule levelCocycles₂ r M of inhomogeneous -cochains by the preimage in it of levelCoboundaries₂ r M; the first argument is formed for the representation of coinduced from along the inclusion , and the second for with the level map obtained by restricting to . Only the existence of such an equivalence is asserted, no particular map being named in the conclusion.
This is Shapiro's lemma in degree two for the continuous (level-wise) cohomology used in the project: coinduction from an open subgroup does not change . It is used in the inductive proof of the local Euler–Poincaré characteristic identity and in the finite-dimensionality of in the prime-local setting.
import Mathlib import Definitions.Def_GroupCohomology_ContinuousH2 import Definitions.Def_GroupCohomology_LevelSubgroup import Definitions.Def_GroupCohomology_ContinuousH2Map set_option maxHeartbeats 4000000 set_option synthInstance.maxHeartbeats 400000 set_option backward.isDefEq.respectTransparency.types false set_option autoImplicit false universe u open CategoryTheory
theorem groupCohomology.nonempty_continuousH2_coind_linearEquiv_continuousH2 {k G : Type u} [CommRing k] [Group G]
(r : G →* (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)) (S : Subgroup G)
(hS : ∃ F₀ : IntermediateField ℚ (AlgebraicClosure ℚ), FiniteDimensional ℚ F₀ ∧ F₀.fixingSubgroup.comap r ≤ S)
(N : Rep.{u} k S) :
Nonempty (groupCohomology.continuousH2 r (Rep.coind S.subtype N)
≃ₗ[k] groupCohomology.continuousH2 (r.comp S.subtype) N) := by sorry