Theorems · Theorem · group theory

MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot

∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
  [inst_2 : H.FiniteIndex] (g : G) [inst_3 : Fintype (Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H)))],
  ϕ.transfer g =
    ∏ q, ϕ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩

Explicit computation of the transfer homomorphism.

Defined in

Mathlib.GroupTheory.Transfer

Cited by

2 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupCommGroupSubgroup.FiniteIndexFintype