# 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 ϕ.
• transferCenterPow: The transfer homomorphism G →* center G.

## Main results #

• transferCenterPow_apply: The transfer homomorphism G →* center G is given by g ↦ g ^ (center G).index.
• ker_transferSylow_isComplement': Burnside's transfer (or normal p-complement) theorem: If hP : N(P) ≤ C(P), then (transfer P hP).ker is a normal p-complement.
theorem AddSubgroup.leftTransversals.diff.proof_2 {G : Type u_1} [] {H : } (T : ) :
theorem AddSubgroup.leftTransversals.diff.proof_3 {G : Type u_1} [] {H : } (S : ) (T : ) (q : G H) :
H
noncomputable def AddSubgroup.leftTransversals.diff {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →+ A) (S : ) (T : ) [H.FiniteIndex] :
A

The difference of two left transversals

Equations
• = let α := ; let β := ; q : G H, ϕ -(α q) + (β q),
Instances For
theorem AddSubgroup.leftTransversals.diff.proof_1 {G : Type u_1} [] {H : } (S : ) :
noncomputable def Subgroup.leftTransversals.diff {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →* A) (S : ) (T : ) [H.FiniteIndex] :
A

The difference of two left transversals

Equations
• = let α := ; let β := ; q : G H, ϕ (↑(α q))⁻¹ * (β q),
Instances For
theorem AddSubgroup.leftTransversals.diff_add_diff {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →+ A) (R : ) (S : ) (T : ) [H.FiniteIndex] :
theorem Subgroup.leftTransversals.diff_mul_diff {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →* A) (R : ) (S : ) (T : ) [H.FiniteIndex] :
theorem AddSubgroup.leftTransversals.diff_self {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →+ A) (T : ) [H.FiniteIndex] :
theorem Subgroup.leftTransversals.diff_self {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →* A) (T : ) [H.FiniteIndex] :
theorem AddSubgroup.leftTransversals.diff_neg {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →+ A) (S : ) (T : ) [H.FiniteIndex] :
theorem Subgroup.leftTransversals.diff_inv {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →* A) (S : ) (T : ) [H.FiniteIndex] :
theorem AddSubgroup.leftTransversals.vadd_diff_vadd {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →+ A) (S : ) (T : ) [H.FiniteIndex] (g : G) :
theorem Subgroup.leftTransversals.smul_diff_smul {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →* A) (S : ) (T : ) [H.FiniteIndex] (g : G) :
noncomputable def AddMonoidHom.transfer {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →+ A) [H.FiniteIndex] :
G →+ A

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

Equations
• ϕ.transfer = let T := default; { toFun := fun (g : G) => , map_zero' := , map_add' := }
Instances For
theorem AddMonoidHom.transfer.proof_2 {G : Type u_2} [] {H : } {A : Type u_1} [] (ϕ : H →+ A) [H.FiniteIndex] (g : G) (h : G) :
{ toFun := fun (g : G) => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default), map_zero' := }.toFun (g + h) = { toFun := fun (g : G) => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default), map_zero' := }.toFun g + { toFun := fun (g : G) => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default), map_zero' := }.toFun h
theorem AddMonoidHom.transfer.proof_1 {G : Type u_2} [] {H : } {A : Type u_1} [] (ϕ : H →+ A) [H.FiniteIndex] :
(fun (g : G) => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default)) 0 = 0
noncomputable def MonoidHom.transfer {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →* A) [H.FiniteIndex] :
G →* A

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

Equations
Instances For
theorem AddMonoidHom.transfer_def {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →+ A) (T : ) [H.FiniteIndex] (g : G) :
ϕ.transfer g =
theorem MonoidHom.transfer_def {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →* A) (T : ) [H.FiniteIndex] (g : G) :
ϕ.transfer g = Subgroup.leftTransversals.diff ϕ T (g T)
theorem MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →* A) [H.FiniteIndex] (g : G) [Fintype (Quotient (MulAction.orbitRel (↥) (G H)))] :
ϕ.transfer g = q : Quotient (MulAction.orbitRel (↥) (G H)), ϕ (Quotient.out' q.out')⁻¹ * g ^ Function.minimalPeriod (fun (x : G H) => g x) q.out' * Quotient.out' q.out',

Explicit computation of the transfer homomorphism.

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

Auxiliary lemma in order to state transfer_eq_pow.

theorem MonoidHom.transfer_eq_pow {G : Type u_1} [] {H : } {A : Type u_2} [] (ϕ : H →* A) [H.FiniteIndex] (g : G) (key : ∀ (k : ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ Hg₀⁻¹ * g ^ k * g₀ = g ^ k) :
ϕ.transfer g = ϕ g ^ H.index,
theorem MonoidHom.transfer_center_eq_pow {G : Type u_1} [] [.FiniteIndex] (g : G) :
(MonoidHom.id ).transfer g = g ^ .index,
noncomputable def MonoidHom.transferCenterPow (G : Type u_1) [] [.FiniteIndex] :
G →*

The transfer homomorphism G →* center G.

Equations
• = { toFun := fun (g : G) => g ^ .index, , map_one' := , map_mul' := }
Instances For
@[simp]
theorem MonoidHom.transferCenterPow_apply {G : Type u_1} [] [.FiniteIndex] (g : G) :
( g) = g ^ .index
noncomputable def MonoidHom.transferSylow {G : Type u_1} [] {p : } (P : Sylow p G) (hP : (↑P).normalizer ) [(↑P).FiniteIndex] :
G →* P

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

Equations
Instances For
theorem MonoidHom.transferSylow_eq_pow_aux {G : Type u_1} [] {p : } (P : Sylow 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

Auxiliary lemma in order to state transferSylow_eq_pow.

theorem MonoidHom.transferSylow_eq_pow {G : Type u_1} [] {p : } (P : Sylow p G) (hP : (↑P).normalizer ) [Fact (Nat.Prime p)] [Finite (Sylow p G)] [(↑P).FiniteIndex] (g : G) (hg : g P) :
g = g ^ (↑P).index,
theorem MonoidHom.transferSylow_restrict_eq_pow {G : Type u_1} [] {p : } (P : Sylow p G) (hP : (↑P).normalizer ) [Fact (Nat.Prime p)] [Finite (Sylow p G)] [(↑P).FiniteIndex] :
(.restrict P) = fun (x : P) => x ^ (↑P).index
theorem MonoidHom.ker_transferSylow_isComplement' {G : Type u_1} [] {p : } (P : Sylow p G) (hP : (↑P).normalizer ) [Fact (Nat.Prime p)] [Finite (Sylow p G)] [(↑P).FiniteIndex] :
.ker.IsComplement' P

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

theorem MonoidHom.not_dvd_card_ker_transferSylow {G : Type u_1} [] {p : } (P : Sylow p G) (hP : (↑P).normalizer ) [Fact (Nat.Prime p)] [Finite (Sylow p G)] [(↑P).FiniteIndex] :
¬p Nat.card .ker
theorem MonoidHom.ker_transferSylow_disjoint {G : Type u_1} [] {p : } (P : Sylow p G) (hP : (↑P).normalizer ) [Fact (Nat.Prime p)] [Finite (Sylow p G)] [(↑P).FiniteIndex] (Q : ) (hQ : IsPGroup p Q) :
Disjoint .ker Q