Corestriction of continuous characters

For trivial coefficients, degree-one corestriction is the character-theoretic transfer. cochainsCor1_eq_transfer identifies the transversal sum with Mathlib's MonoidHom.transfer already on cochains, for every transversal. H1EquivOfSmulEqSelf_explicitCor1_eq_transfer states the commuting square between corestriction on continuous H¹ and transfer on characters, using the existing character equivalence H1EquivOfSmulEqSelf.

In particular, transfer of a character of an abelian quotient of an open subgroup is precomposition with the transfer into that quotient, by MonoidHom.transfer_comp. This is the bridge from cohomological corestriction to transfer on abelianizations. The character obtained by transfer is continuous by TauCeti.continuous_transfer.

The action must be trivial: otherwise the corestriction sum contains the factors t q •, and it is not the transfer of an ordinary homomorphism. The coefficients need not be discrete.

References

• Neukirch--Schmidt--Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.9).
• K. S. Brown, Cohomology of Groups, Chapter III, §9.

theorem TauCeti.ContCohomology.cochainsCor1_eq_transfer {G : Type u_1} {M : Type u_2} [Group G] [AddCommGroup M] [DistribMulAction G M] {U : Subgroup G} [U.FiniteIndex] (htriv : ∀ (g : G) (m : M), g • m = m) (t : G ⧸ U → G) (ht : ∀ (q : G ⧸ U), ↑(t q) = q) (φ : ↥U →* Multiplicative M) : ((cochainsCor1 G M U t ht) fun (u : ↥U) => Multiplicative.toAdd (φ u)) = fun (g : G) => Multiplicative.toAdd (φ.transfer g)

For trivial coefficients, the corestriction cochain of a homomorphism is its transfer, independently of the transversal. This identity needs no topology.

@[simp]

theorem TauCeti.ContCohomology.H1EquivOfSmulEqSelf_explicitCor1_eq_transfer {G : Type u_1} {M : Type u_2} [Group G] [AddCommGroup M] [DistribMulAction G M] {U : Subgroup G} [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (htriv : ∀ (g : G) (m : M), g • m = m) (hU : IsOpen ↑U) (x : H1 (↥U) M) : ↑(Additive.toMul ((H1EquivOfSmulEqSelf htriv) ((explicitCor1 G M U hU) x))) = (↑(Additive.toMul ((H1EquivOfSmulEqSelf ⋯) x))).transfer

Under the continuous-character description of H¹ for trivial coefficients, corestriction is Mathlib's transfer. This is an equality of homomorphisms, not just classes.