# mathlibdocumentation

group_theory.transfer

# The Transfer Homomorphism #

In this file we construct the transfer homomorphism.

## Main definitions #

• diff ϕ S T : The difference of two left transversals S and T under the homomorphism ϕ.
• transfer ϕ : The transfer homomorphism induced by ϕ.
• transfer_center_pow: The transfer homomorphism G →* center G.
noncomputable def subgroup.left_transversals.diff {G : Type u_1} [group G] {H : subgroup G} {A : Type u_2} [comm_group A] (ϕ : H →* A) (S T : ) [fintype (G H)] :
A

The difference of two left transversals

Equations
noncomputable def add_subgroup.left_transversals.diff {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} (ϕ : H →+ A) (S T : ) [fintype (G H)] :
A

The difference of two left transversals

Equations
theorem add_subgroup.left_transversals.diff_add_diff {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} (ϕ : H →+ A) (R S T : ) [fintype (G H)] :
theorem subgroup.left_transversals.diff_mul_diff {G : Type u_1} [group G] {H : subgroup G} {A : Type u_2} [comm_group A] (ϕ : H →* A) (R S T : ) [fintype (G H)] :
theorem subgroup.left_transversals.diff_self {G : Type u_1} [group G] {H : subgroup G} {A : Type u_2} [comm_group A] (ϕ : H →* A) (T : ) [fintype (G H)] :
theorem add_subgroup.left_transversals.diff_self {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} (ϕ : H →+ A) (T : ) [fintype (G H)] :
theorem subgroup.left_transversals.diff_inv {G : Type u_1} [group G] {H : subgroup G} {A : Type u_2} [comm_group A] (ϕ : H →* A) (S T : ) [fintype (G H)] :
theorem add_subgroup.left_transversals.diff_neg {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} (ϕ : H →+ A) (S T : ) [fintype (G H)] :
theorem subgroup.left_transversals.smul_diff_smul {G : Type u_1} [group G] {H : subgroup G} {A : Type u_2} [comm_group A] (ϕ : H →* A) (S T : ) [fintype (G H)] (g : G) :
(g S) (g T) =
theorem add_subgroup.left_transversals.vadd_diff_vadd {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} (ϕ : H →+ A) (S T : ) [fintype (G H)] (g : G) :
(g +ᵥ T) =
noncomputable def monoid_hom.transfer {G : Type u_1} [group G] {H : subgroup G} {A : Type u_2} [comm_group A] (ϕ : H →* A) [fintype (G H)] :
G →* A

Given ϕ : H →* A from H : subgroup G to a commutative group A, the transfer homomorphism is transfer ϕ : G →* A.

Equations
noncomputable def add_monoid_hom.transfer {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} (ϕ : H →+ A) [fintype (G H)] :
G →+ A

Given ϕ : H →+ A from H : add_subgroup G to an additive commutative group A, the transfer homomorphism is transfer ϕ : G →+ A.

Equations
theorem monoid_hom.transfer_def {G : Type u_1} [group G] {H : subgroup G} {A : Type u_2} [comm_group A] (ϕ : H →* A) (T : ) [fintype (G H)] (g : G) :
(ϕ.transfer) g = (g T)
theorem add_monoid_hom.transfer_def {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} (ϕ : H →+ A) (T : ) [fintype (G H)] (g : G) :
(ϕ.transfer) g = (g +ᵥ T)
theorem monoid_hom.transfer_eq_prod_quotient_orbit_rel_zpowers_quot {G : Type u_1} [group G] {H : subgroup G} {A : Type u_2} [comm_group A] (ϕ : H →* A) [fintype (G H)] (g : G) [fintype (quotient (G H)))] :
(ϕ.transfer) g = finset.univ.prod (λ (q : quotient (G H))), ϕ ⁻¹ * * , _⟩)

Explicit computation of the transfer homomorphism.

theorem monoid_hom.transfer_eq_pow_aux {G : Type u_1} [group G] {H : subgroup G} (g : G) (key : ∀ (k : ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ Hg₀⁻¹ * g ^ k * g₀ = g ^ k) :
g ^ H.index H

Auxillary lemma in order to state transfer_eq_pow.

theorem monoid_hom.transfer_eq_pow {G : Type u_1} [group G] {H : subgroup G} {A : Type u_2} [comm_group A] (ϕ : H →* A) [fintype (G H)] (g : G) (key : ∀ (k : ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ Hg₀⁻¹ * g ^ k * g₀ = g ^ k) :
(ϕ.transfer) g = ϕ g ^ H.index, _⟩
theorem monoid_hom.transfer_center_eq_pow {G : Type u_1} [group G] [fintype (G ] (g : G) :
.transfer) g = g ^ .index, _⟩
noncomputable def monoid_hom.transfer_center_pow {G : Type u_1} [group G] [fintype (G ] :

The transfer homomorphism G →* center G.

Equations
@[simp]
theorem monoid_hom.transfer_center_pow_apply {G : Type u_1} [group G] [fintype (G ] (g : G) :
noncomputable def monoid_hom.transfer_center_pow' {G : Type u_1} [group G] (h : .index 0) :

The transfer homomorphism G →* center G.

Equations
@[simp]
theorem monoid_hom.transfer_center_pow'_apply {G : Type u_1} [group G] (h : .index 0) (g : G) :
= g ^ .index