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} [AddGroup G] {H : AddSubgroup G} (T : ↑(AddSubgroup.leftTransversals ↑H)) : ↑T ∈ AddSubgroup.leftTransversals ↑H

theorem AddSubgroup.leftTransversals.diff.proof_3 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (S : ↑(AddSubgroup.leftTransversals ↑H)) (T : ↑(AddSubgroup.leftTransversals ↑H)) (q : G ⧸ H) : -↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) q) + ↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) q) ∈ H

noncomputable def AddSubgroup.leftTransversals.diff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {A : Type u_2} [AddCommGroup A] (ϕ : ↥H →+ A) (S : ↑(AddSubgroup.leftTransversals ↑H)) (T : ↑(AddSubgroup.leftTransversals ↑H)) [H.FiniteIndex] : A

The difference of two left transversals

Equations

• AddSubgroup.leftTransversals.diff ϕ S T = let α := AddSubgroup.MemLeftTransversals.toEquiv ⋯; let β := AddSubgroup.MemLeftTransversals.toEquiv ⋯; ∑ q : G ⧸ H, ϕ ⟨-↑(α q) + ↑(β q), ⋯⟩

theorem AddSubgroup.leftTransversals.diff.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (S : ↑(AddSubgroup.leftTransversals ↑H)) : ↑S ∈ AddSubgroup.leftTransversals ↑H

noncomputable def Subgroup.leftTransversals.diff {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) (S : ↑(Subgroup.leftTransversals ↑H)) (T : ↑(Subgroup.leftTransversals ↑H)) [H.FiniteIndex] : A

The difference of two left transversals

Equations

• Subgroup.leftTransversals.diff ϕ S T = let α := Subgroup.MemLeftTransversals.toEquiv ⋯; let β := Subgroup.MemLeftTransversals.toEquiv ⋯; ∏ q : G ⧸ H, ϕ ⟨(↑(α q))⁻¹ * ↑(β q), ⋯⟩

theorem AddSubgroup.leftTransversals.diff_add_diff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {A : Type u_2} [AddCommGroup A] (ϕ : ↥H →+ A) (R : ↑(AddSubgroup.leftTransversals ↑H)) (S : ↑(AddSubgroup.leftTransversals ↑H)) (T : ↑(AddSubgroup.leftTransversals ↑H)) [H.FiniteIndex] : AddSubgroup.leftTransversals.diff ϕ R S + AddSubgroup.leftTransversals.diff ϕ S T = AddSubgroup.leftTransversals.diff ϕ R T

theorem Subgroup.leftTransversals.diff_mul_diff {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) (R : ↑(Subgroup.leftTransversals ↑H)) (S : ↑(Subgroup.leftTransversals ↑H)) (T : ↑(Subgroup.leftTransversals ↑H)) [H.FiniteIndex] : Subgroup.leftTransversals.diff ϕ R S * Subgroup.leftTransversals.diff ϕ S T = Subgroup.leftTransversals.diff ϕ R T

theorem AddSubgroup.leftTransversals.diff_self {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {A : Type u_2} [AddCommGroup A] (ϕ : ↥H →+ A) (T : ↑(AddSubgroup.leftTransversals ↑H)) [H.FiniteIndex] : AddSubgroup.leftTransversals.diff ϕ T T = 0

theorem Subgroup.leftTransversals.diff_self {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) (T : ↑(Subgroup.leftTransversals ↑H)) [H.FiniteIndex] : Subgroup.leftTransversals.diff ϕ T T = 1

theorem AddSubgroup.leftTransversals.diff_neg {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {A : Type u_2} [AddCommGroup A] (ϕ : ↥H →+ A) (S : ↑(AddSubgroup.leftTransversals ↑H)) (T : ↑(AddSubgroup.leftTransversals ↑H)) [H.FiniteIndex] : -AddSubgroup.leftTransversals.diff ϕ S T = AddSubgroup.leftTransversals.diff ϕ T S

theorem Subgroup.leftTransversals.diff_inv {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) (S : ↑(Subgroup.leftTransversals ↑H)) (T : ↑(Subgroup.leftTransversals ↑H)) [H.FiniteIndex] : (Subgroup.leftTransversals.diff ϕ S T)⁻¹ = Subgroup.leftTransversals.diff ϕ T S

theorem AddSubgroup.leftTransversals.vadd_diff_vadd {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {A : Type u_2} [AddCommGroup A] (ϕ : ↥H →+ A) (S : ↑(AddSubgroup.leftTransversals ↑H)) (T : ↑(AddSubgroup.leftTransversals ↑H)) [H.FiniteIndex] (g : G) : AddSubgroup.leftTransversals.diff ϕ (g +ᵥ S) (g +ᵥ T) = AddSubgroup.leftTransversals.diff ϕ S T

theorem Subgroup.leftTransversals.smul_diff_smul {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) (S : ↑(Subgroup.leftTransversals ↑H)) (T : ↑(Subgroup.leftTransversals ↑H)) [H.FiniteIndex] (g : G) : Subgroup.leftTransversals.diff ϕ (g • S) (g • T) = Subgroup.leftTransversals.diff ϕ S T

noncomputable def AddMonoidHom.transfer {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {A : Type u_2} [AddCommGroup A] (ϕ : ↥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) => AddSubgroup.leftTransversals.diff ϕ T (g +ᵥ T), map_zero' := ⋯, map_add' := ⋯ }

theorem AddMonoidHom.transfer.proof_2 {G : Type u_2} [AddGroup G] {H : AddSubgroup G} {A : Type u_1} [AddCommGroup A] (ϕ : ↥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} [AddGroup G] {H : AddSubgroup G} {A : Type u_1} [AddCommGroup A] (ϕ : ↥H →+ A) [H.FiniteIndex] : (fun (g : G) => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default)) 0 = 0

noncomputable def MonoidHom.transfer {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥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

• ϕ.transfer = let T := default; { toFun := fun (g : G) => Subgroup.leftTransversals.diff ϕ T (g • T), map_one' := ⋯, map_mul' := ⋯ }

theorem AddMonoidHom.transfer_def {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {A : Type u_2} [AddCommGroup A] (ϕ : ↥H →+ A) (T : ↑(AddSubgroup.leftTransversals ↑H)) [H.FiniteIndex] (g : G) : ϕ.transfer g = AddSubgroup.leftTransversals.diff ϕ T (g +ᵥ T)

theorem MonoidHom.transfer_def {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) (T : ↑(Subgroup.leftTransversals ↑H)) [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} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) [H.FiniteIndex] (g : G) [Fintype (Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H)))] : ϕ.transfer g = ∏ q : Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (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} [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

Auxiliary lemma in order to state transfer_eq_pow.

theorem MonoidHom.transfer_eq_pow {G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) [H.FiniteIndex] (g : G) (key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k) : ϕ.transfer g = ϕ ⟨g ^ H.index, ⋯⟩

theorem MonoidHom.transfer_center_eq_pow {G : Type u_1} [Group G] [(Subgroup.center G).FiniteIndex] (g : G) : (MonoidHom.id ↥(Subgroup.center G)).transfer g = ⟨g ^ (Subgroup.center G).index, ⋯⟩

noncomputable def MonoidHom.transferCenterPow (G : Type u_1) [Group G] [(Subgroup.center G).FiniteIndex] : G →* ↥(Subgroup.center G)

The transfer homomorphism G →* center G.

Equations

• MonoidHom.transferCenterPow G = { toFun := fun (g : G) => ⟨g ^ (Subgroup.center G).index, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MonoidHom.transferCenterPow_apply {G : Type u_1} [Group G] [(Subgroup.center G).FiniteIndex] (g : G) : ↑((MonoidHom.transferCenterPow G) g) = g ^ (Subgroup.center G).index

noncomputable def MonoidHom.transferSylow {G : Type u_1} [Group G] {p : ℕ} (P : Sylow p G) (hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P) [(↑P).FiniteIndex] : G →* ↥↑P

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

Equations

• MonoidHom.transferSylow P hP = (MonoidHom.id ↥↑P).transfer

theorem MonoidHom.transferSylow_eq_pow_aux {G : Type u_1} [Group G] {p : ℕ} (P : Sylow p G) (hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P) [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} [Group G] {p : ℕ} (P : Sylow p G) (hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P) [Fact (Nat.Prime p)] [Finite (Sylow p G)] [(↑P).FiniteIndex] (g : G) (hg : g ∈ P) : (MonoidHom.transferSylow P hP) g = ⟨g ^ (↑P).index, ⋯⟩

theorem MonoidHom.transferSylow_restrict_eq_pow {G : Type u_1} [Group G] {p : ℕ} (P : Sylow p G) (hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P) [Fact (Nat.Prime p)] [Finite (Sylow p G)] [(↑P).FiniteIndex] : ⇑((MonoidHom.transferSylow P hP).restrict ↑P) = fun (x : ↥P) => x ^ (↑P).index

theorem MonoidHom.ker_transferSylow_isComplement' {G : Type u_1} [Group G] {p : ℕ} (P : Sylow p G) (hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P) [Fact (Nat.Prime p)] [Finite (Sylow p G)] [(↑P).FiniteIndex] : (MonoidHom.transferSylow P hP).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} [Group G] {p : ℕ} (P : Sylow p G) (hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P) [Fact (Nat.Prime p)] [Finite (Sylow p G)] [(↑P).FiniteIndex] : ¬p ∣ Nat.card ↥(MonoidHom.transferSylow P hP).ker

theorem MonoidHom.ker_transferSylow_disjoint {G : Type u_1} [Group G] {p : ℕ} (P : Sylow p G) (hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P) [Fact (Nat.Prime p)] [Finite (Sylow p G)] [(↑P).FiniteIndex] (Q : Subgroup G) (hQ : IsPGroup p ↥Q) : Disjoint (MonoidHom.transferSylow P hP).ker Q