Transitivity of the transfer homomorphism

Let H be a subgroup of finite index of a group G and let ϕ : H →* A be a homomorphism to a commutative group. This file complements Mathlib's MonoidHom.transfer with the three structural properties of the transfer V_ϕ : G →* A:

• it can be computed from any family of coset representatives indexed by a finite type, with any compatible labelling of the permutation action of g: V_ϕ(g) = ∏ᵢ ϕ(t_{π i}⁻¹ g tᵢ) whenever g tᵢ H = t_{π i} H;
• it is natural in the commutative target and invariant under isomorphisms of the ambient group;
• it is transitive: for subgroups K ≤ H ≤ G with K of finite index, the transfer from G to K is the transfer from G to H followed by the transfer from H to K.

Finite indices that follow from the other hypotheses are not assumed: in the first property the index of H is finite because the family is finite, an isomorphism carries a subgroup of finite index to one of finite index, and in a tower K ≤ H the index of H divides that of K.

Main results

• MonoidHom.transfer_eq_prod_of_bijective: the transfer computed from an arbitrary indexed family of coset representatives.
• MonoidHom.transfer_eq_prod_mul_out: for a normal subgroup, computation by right multiplication of quotient representatives, matching the factor-set convention.
• MonoidHom.transfer_comp: the transfer is natural in the commutative target.
• MonoidHom.transfer_apply_of_mulEquiv: the transfer is invariant under an isomorphism of ambient groups carrying one subgroup onto the other.
• MonoidHom.transfer_transfer: transitivity of the transfer along a tower K ≤ H ≤ G.
• TauCeti.transfer_eq_prod_lWord: computation with the transversal words used by cohomological corestriction.

References

• K. S. Brown, Cohomology of Groups, Chapter III, §9.

theorem MonoidHom.transfer_eq_prod_of_bijective {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) {ι : Type u_3} [Fintype ι] (f : ι → G) (hf : Function.Bijective fun (i : ι) => ↑(f i)) (g : G) (π : ι → ι) (hπ : ∀ (i : ι), ↑(f (π i)) = ↑(g * f i)) : ϕ.transfer g = ∏ i : ι, ϕ ⟨(f (π i))⁻¹ * (g * f i), ⋯⟩

The transfer computed from coset representatives indexed by a finite type: if i ↦ f i H is a bijection onto G ⧸ H and π labels the action of g, in the sense that g (f i) H = f (π i) H, then transfer ϕ g = ∏ᵢ ϕ ((f (π i))⁻¹ g (f i)). Unlike transfer_def, which is phrased with a LeftTransversal indexed by G ⧸ H itself, the index type ι here is arbitrary; such a π is automatically a permutation of ι. The index of H is finite because ι is.

theorem MonoidHom.transfer_eq_prod_mul_out {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) [H.Normal] [H.FiniteIndex] (g : G) : ϕ.transfer g = ∏ q : G ⧸ H, ϕ ⟨Quotient.out q * g * (Quotient.out (q * ↑g))⁻¹, ⋯⟩

For a normal finite-index subgroup, the transfer may be computed by multiplying on the right of quotient representatives. This convention makes the transfer of a representative the product of the corresponding factor-set values.

@[simp]

theorem MonoidHom.transfer_comp {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) [H.FiniteIndex] {B : Type u_3} [CommGroup B] (χ : A →* B) : (χ.comp ϕ).transfer = χ.comp ϕ.transfer

The transfer is natural in the commutative target.

theorem MonoidHom.transfer_apply_of_mulEquiv {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) {G' : Type u_3} [Group G'] (e : G ≃* G') {H' : Subgroup G'} [H.FiniteIndex] (he : Subgroup.map (↑e) H = H') (ϕ' : ↥H' →* A) (hϕ : ∀ (h : ↥H), ϕ' ⟨e ↑h, ⋯⟩ = ϕ h) (g : G) : ϕ'.transfer (e g) = ϕ.transfer g

The transfer is invariant under an isomorphism e : G ≃* G' carrying H onto H' (which then also has finite index): if ϕ' : H' →* A corresponds to ϕ : H →* A along e, then transfer ϕ' (e g) = transfer ϕ g.

@[simp]

theorem MonoidHom.transfer_transfer {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] {K : Subgroup G} (hKH : K ≤ H) [K.FiniteIndex] (ϕ : ↥K →* A) : (ϕ.comp ↑(Subgroup.subgroupOfEquivOfLe hKH)).transfer.transfer = ϕ.transfer

Transitivity of the transfer. For subgroups K ≤ H ≤ G with K of finite index (so that H has finite index too), the transfer from G to K is the transfer from G to H of the transfer from H to K; the inner transfer is that of ϕ viewed on K.subgroupOf H via subgroupOfEquivOfLe.

theorem TauCeti.transfer_eq_prod_lWord {G : Type u_1} {A : Type u_2} [Group G] [CommGroup A] {U : Subgroup G} [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (q : G ⧸ U), ↑(t q) = q) (φ : ↥U →* A) (g : G) : φ.transfer g = ∏ q : G ⧸ U, φ ⟨lWord U t q g, ⋯⟩

The transfer is the product of the images of the transversal words, for any transversal. The index convention is the one used by cohomological corestriction.