# mathlib3documentation

group_theory.transfer

# The Transfer Homomorphism #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

## Main results #

• transfer_center_pow_apply: The transfer homomorphism G →* center G is given by g ↦ g ^ (center G).index.
• ker_transfer_sylow_is_complement': Burnside's transfer (or normal p-complement) theorem: If hP : N(P) ≤ C(P), then (transfer P hP).ker is a normal p-complement.
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 : ) [H.finite_index] :
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 : ) [H.finite_index] :
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 : ) [H.finite_index] :
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 : ) [H.finite_index] :
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 : ) [H.finite_index] :
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 : ) [H.finite_index] :
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 : ) [H.finite_index] :
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 : ) [H.finite_index] :
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 : ) [H.finite_index] (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 : ) [H.finite_index] (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) [H.finite_index] :
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) [H.finite_index] :
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 : ) [H.finite_index] (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 : ) [H.finite_index] (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) [H.finite_index] (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₀ H g₀⁻¹ * 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) [H.finite_index] (g : G) (key : (k : ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ H g₀⁻¹ * g ^ k * g₀ = g ^ k) :
(ϕ.transfer) g = ϕ g ^ H.index, _⟩
theorem monoid_hom.transfer_center_eq_pow {G : Type u_1} [group G] [.finite_index] (g : G) :
.transfer) g = g ^ .index, _⟩
noncomputable def monoid_hom.transfer_center_pow (G : Type u_1) [group G] [.finite_index] :

The transfer homomorphism G →* center G.

Equations
@[simp]
theorem monoid_hom.transfer_center_pow_apply {G : Type u_1} [group G] [.finite_index] (g : G) :
noncomputable def monoid_hom.transfer_sylow {G : Type u_1} [group G] {p : } (P : G) (hP : P.normalizer ) [P.finite_index] :

The homomorphism G →* P in Burnside's transfer theorem.

Equations
theorem monoid_hom.transfer_sylow_eq_pow_aux {G : Type u_1} [group G] {p : } (P : G) (hP : P.normalizer ) [fact (nat.prime p)] [finite (sylow p G)] (g : G) (hg : g P) (k : ) (g₀ : G) (h : g₀⁻¹ * g ^ k * g₀ P) :
g₀⁻¹ * g ^ k * g₀ = g ^ k

Auxillary lemma in order to state transfer_sylow_eq_pow.

theorem monoid_hom.transfer_sylow_eq_pow {G : Type u_1} [group G] {p : } (P : G) (hP : P.normalizer ) [fact (nat.prime p)] [finite (sylow p G)] [P.finite_index] (g : G) (hg : g P) :
g = g ^ P.index, _⟩
theorem monoid_hom.transfer_sylow_restrict_eq_pow {G : Type u_1} [group G] {p : } (P : G) (hP : P.normalizer ) [fact (nat.prime p)] [finite (sylow p G)] [P.finite_index] :
hP).restrict P) = λ (_x : P), _x ^ P.index
theorem monoid_hom.ker_transfer_sylow_is_complement' {G : Type u_1} [group G] {p : } (P : G) (hP : P.normalizer ) [fact (nat.prime p)] [finite (sylow p G)] [P.finite_index] :

Burnside's normal p-complement theorem: If N(P) ≤ C(P), then P has a normal complement.

theorem monoid_hom.not_dvd_card_ker_transfer_sylow {G : Type u_1} [group G] {p : } (P : G) (hP : P.normalizer ) [fact (nat.prime p)] [finite (sylow p G)] [P.finite_index] :
theorem monoid_hom.ker_transfer_sylow_disjoint {G : Type u_1} [group G] {p : } (P : G) (hP : P.normalizer ) [fact (nat.prime p)] [finite (sylow p G)] [P.finite_index] (Q : subgroup G) (hQ : Q) :
Q