Equivariant relation-module maps over a common Galois quotient

An algebraic relation-module map to the completed multiplicative group of a finite normal extension of p-adic fields gives a continuous homomorphism between the free and arithmetic pro-p class-module kernels via relationModuleToAbelianizationProP. Here that homomorphism is bundled as equivariant for Gal(L/K). The source uses the action of the presented group on its relation group, and the target uses the arithmetic conjugation action transported through the Galois correspondence.

Thus the map has the coefficient-map type required to lift a surjection between kernels to a surjection of profinite extensions. Continuity and surjectivity agree with the existing transport through Lyndon's isomorphism and local reciprocity; no condition on extension classes is imposed or proved here.

References

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

noncomputable def TauCeti.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) : abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(freeProfiniteGroup.lift g)).ker →*[Gal(L/K)] abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j)

A relation-module map, transported through Lyndon and reciprocity, as an equivariant homomorphism for the common quotient Gal(L/K) of the free and arithmetic extensions.

@[simp]

theorem TauCeti.relationModuleToAbelianizationProPEquivariant_apply (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) (x : abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(freeProfiniteGroup.lift g)).ker) : (relationModuleToAbelianizationProPEquivariant p K L hg β j) x = (relationModuleToAbelianizationProP p K L hg β j) x

The equivariant transport has the same underlying map as the continuous transport.

theorem TauCeti.ofMul_symm_apply_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) (x : Additive (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(freeProfiniteGroup.lift g)).ker)) : Additive.ofMul ((padicCompletionUnitsEquivAbelianizationProP p K L j).symm ((relationModuleToAbelianizationProPEquivariant p K L hg β j) (Additive.toMul x))) = β ((freeProfiniteGroup.abelianizationProPEquivRelationModule p hg) x)

The relation-module comparison map intertwines the Lyndon and reciprocity coordinates with the original algebraic map.

theorem TauCeti.continuous_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) : Continuous ⇑(relationModuleToAbelianizationProPEquivariant p K L hg β j)

The equivariant kernel transport is continuous.

@[simp]

theorem TauCeti.relationModuleToAbelianizationProPEquivariant_surjective_iff (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) : Function.Surjective ⇑(relationModuleToAbelianizationProPEquivariant p K L hg β j) ↔ Function.Surjective ⇑β

The equivariant kernel transport is surjective exactly when the algebraic relation-module map is surjective.