Transfer to the pro-p class module

For a finite-index subgroup V of a topological group G, the transfer to V^ab(p) is Mathlib's MonoidHom.transfer applied to the canonical map V → V^ab(p). It is continuous when V is open; for profinite G it then kills the kernel of G → G^ab(p). For normal V, its restriction to V is the norm for the conjugation action of G ⧸ V. Its value on a quotient representative is the sum of the factor set abelianizationProPFactorSet in the first variable.

These formulas connect the group-theoretic transfer with the extension class abelianizationProPClass: in particular, they identify the norm and the representative sum that occur in the cyclic-quotient calculation of that class. No cohomological-dimension hypothesis is needed for the formulas, and no claim of injectivity or surjectivity is made.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.9) and the transfer diagram (3.6.2).
• Transfer API: TauCeti.transfer_eq_prod_lWord, TauCeti.continuous_transfer, and MonoidHom.transfer_eq_prod_mul_out.

noncomputable def TauCeti.abelianizationProPTransfer (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.FiniteIndex] : G →* abelianizationProP p G V

The transfer G → V^ab(p) induced by the canonical map V → V^ab(p).

theorem TauCeti.abelianizationProPTransfer_def (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.FiniteIndex] : abelianizationProPTransfer p G V = (abelianizationProPMk p G V).transfer

The transfer to V^ab(p) is Mathlib's transfer of the canonical map V → V^ab(p).

theorem TauCeti.abelianizationProPTransfer_eq_prod_lWord (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.FiniteIndex] (t : G ⧸ V → G) (ht : ∀ (q : G ⧸ V), ↑(t q) = q) (g : G) : (abelianizationProPTransfer p G V) g = ∏ q : G ⧸ V, (abelianizationProPMk p G V) ⟨lWord V t q g, ⋯⟩

The transfer is the product of the classes of the transversal words, for every transversal. The representatives are arbitrary; the transfer itself does not depend on them.

theorem TauCeti.continuous_abelianizationProPTransfer (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.FiniteIndex] (hV : IsOpen ↑V) : Continuous ⇑(abelianizationProPTransfer p G V)

Transfer to V^ab(p) is continuous when V is open. Compactness and primality of p are not required.

theorem TauCeti.abelianizationProPTransfer_eq_one_of_mk_eq_one {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V : Subgroup G} [V.FiniteIndex] [CompactSpace G] [TotallyDisconnectedSpace G] (hV : IsOpen ↑V) {g : G} (hg : (maximalProPQuotient.mk p (TopologicalAbelianization G)) ↑g = 1) : (abelianizationProPTransfer p G V) g = 1

The transfer Ver : G → V^ab(p) kills the kernel of the canonical map G → G^ab(p). It is a continuous homomorphism to the abelian pro-p group V^ab(p), so it factors through G^ab(p). No hypothesis on the cohomological dimension of G is needed.

theorem TauCeti.abelianizationProPTransfer_apply_of_mem (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.FiniteIndex] [V.Normal] (v : ↥V) : (abelianizationProPTransfer p G V) ↑v = ∏ q : G ⧸ V, q • (abelianizationProPMk p G V) v

On V, transfer is the norm of the conjugation action of G ⧸ V.

theorem TauCeti.abelianizationProPTransfer_out (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.FiniteIndex] [V.Normal] (q : G ⧸ V) : Additive.ofMul ((abelianizationProPTransfer p G V) (Quotient.out q)) = ∑ r : G ⧸ V, abelianizationProPFactorSet p G V (r, q)

At a quotient representative, transfer is the sum of the factor set in its first variable. This is the additive form of the transfer formula used to evaluate the extension class.

@[simp]

theorem TauCeti.smul_abelianizationProPTransfer (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.FiniteIndex] [V.Normal] (q : G ⧸ V) (g : G) : q • (abelianizationProPTransfer p G V) g = (abelianizationProPTransfer p G V) g

The image of transfer is fixed by the conjugation action of G ⧸ V. This is a containment in the invariants; equality with the invariants requires additional cohomological hypotheses.

@[simp]

theorem TauCeti.abelianizationProPTransfer_top (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : (abelianizationProPTransfer p G ⊤) g = (abelianizationProPMk p G ⊤) ⟨g, ⋯⟩

Transfer from the whole group is the canonical map to its pro-p abelianization.