Relation-module maps on arithmetic extension kernels

Let L/K be a finite extension of local fields of characteristic zero, g a finite generating family of Gal(L/K), and R the kernel of the resulting free profinite presentation. An algebraic ℤ_p[Gal(L/K)]-linear map β : relationModule → A(L) defines a continuous homomorphism R^ab(p) → V^ab(p), where V is the subgroup of G_K fixing L.

The map is exactly β read through Lyndon's isomorphism and local reciprocity. It preserves surjectivity, and for normal L/K it is equivariant for the quotient actions when K and L have compatible ℚ_[p]-algebra structures forming a scalar tower, L is finite over ℚ_[p], and ValuativeExtension ℚ_[p] L holds. Thus the integral relation-module surjection can be used as a map of kernels of profinite group extensions. No compatibility of extension classes is asserted here.

Main declarations

• TauCeti.relationModuleToAbelianizationProP: the continuous transport of a relation-module map.
• TauCeti.relationModuleToAbelianizationProP_surjective_iff: surjectivity is preserved and reflected.
• TauCeti.relationModuleToAbelianizationProP_smul: the transport is equivariant.

References

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

noncomputable def TauCeti.relationModuleToAbelianizationProP (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero 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 →ₜ* abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j)

Read an algebraic relation-module map as a continuous homomorphism between the abelian pro-p kernels of the free profinite presentation and the arithmetic extension, using Lyndon's isomorphism and local reciprocity.

@[simp]

theorem TauCeti.relationModuleToAbelianizationProP_apply (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero 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) : (relationModuleToAbelianizationProP p K L hg β j) x = (padicCompletionUnitsEquivAbelianizationProP p K L j) (Additive.toMul (β ((freeProfiniteGroup.abelianizationProPEquivRelationModule p hg) (Additive.ofMul x))))

The transported map is β between Lyndon's coordinates and the reciprocity coordinates.

@[simp]

theorem TauCeti.relationModuleToAbelianizationProP_surjective_iff (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero 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 ⇑(relationModuleToAbelianizationProP p K L hg β j) ↔ Function.Surjective ⇑β

A relation-module map is surjective exactly when its continuous transport to the arithmetic extension kernel is surjective.

theorem TauCeti.relationModuleToAbelianizationProP_smul (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero 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) [Normal K L] [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] (f : ↑(freeProfiniteGroup ι).toProfinite.toTop) (s : AbsoluteGaloisGroup K) (hfs : (freeProfiniteGroup.lift g) f = j.restrictNormalHom s) (x : abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(freeProfiniteGroup.lift g)).ker) : (relationModuleToAbelianizationProP p K L hg β j) (↑f • x) = ↑s • (relationModuleToAbelianizationProP p K L hg β j) x

The transported relation-module map intertwines the quotient conjugation actions whenever f ∈ F and s ∈ G_K induce the same automorphism of L.