Second cohomology of transported arithmetic relation-module maps

The relation-module map transported through Lyndon and local reciprocity induces the same second-cohomology map as the original integral group-algebra map. In particular, a surjection with projective kernel gives a bijection on explicit continuous second cohomology. Using this with the tame-frame relation-module surjection supplies the cohomology input needed to lift the transported map to a surjection of profinite group extensions.

The two coordinate comparisons are freeProfiniteGroup.explicitH2EquivRelationModule and explicitH2EquivPadicCompletionUnits; the transported map is relationModuleToAbelianizationProPEquivariant.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.4.1).

theorem TauCeti.explicitH2EquivPadicCompletionUnits_explicitCoeff2_relationModule (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] {ι : Type} [Fintype ι] [DecidableEq ι] {g : ι → Gal(L/K)} (hg : Subgroup.closure (Set.range g) = ⊤) (β : ↥(MonoidAlgebra.relationModule ℤ_[p] Gal(L/K) g) →ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] Additive ↥(padicCompletionUnits p L)) (j : L →ₐ[K] SeparableClosure K) : have this := galoisClassModuleAction p K L j; ∀ (x : ContCohomology.H2 Gal(L/K) (Additive (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(freeProfiniteGroup.lift g)).ker))), (explicitH2EquivPadicCompletionUnits p K L j) ((ContCohomology.explicitCoeff2 Gal(L/K) (Additive (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(freeProfiniteGroup.lift g)).ker)) (relationModuleToAbelianizationProPEquivariant p K L hg β j).toAdditive ⋯) x) = (CategoryTheory.ConcreteCategory.hom ((groupCohomology.functor ℤ_[p] Gal(L/K) 2).map (Rep.ofModuleMonoidAlgebra.map (ModuleCat.ofHom β)))) ((freeProfiniteGroup.explicitH2EquivRelationModule p hg) x)

The explicit second-cohomology map on arithmetic kernels is the original algebraic relation-module map, in Lyndon and reciprocity coordinates.

theorem TauCeti.bijective_explicitCoeff2_relationModuleToAbelianizationProPEquivariant (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] {ι : Type} [Fintype ι] [DecidableEq ι] {g : ι → Gal(L/K)} (hg : Subgroup.closure (Set.range g) = ⊤) (β : ↥(MonoidAlgebra.relationModule ℤ_[p] Gal(L/K) g) →ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] Additive ↥(padicCompletionUnits p L)) (j : L →ₐ[K] SeparableClosure K) (hβ : Function.Surjective ⇑β) [Module.Projective (MonoidAlgebra ℤ_[p] Gal(L/K)) ↥β.ker] : have this := galoisClassModuleAction p K L j; Function.Bijective ⇑(ContCohomology.explicitCoeff2 Gal(L/K) (Additive (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(freeProfiniteGroup.lift g)).ker)) (relationModuleToAbelianizationProPEquivariant p K L hg β j).toAdditive ⋯)

A surjective arithmetic relation-module map with projective kernel induces a bijection on explicit second cohomology after transport through Lyndon and local reciprocity.