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 (_ : ↑S ∈ AddSubgroup.leftTransversals ↑H)) q) + ↑((AddSubgroup.MemLeftTransversals.toEquiv (_ : ↑T ∈ AddSubgroup.leftTransversals ↑H)) 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)) [AddSubgroup.FiniteIndex H] : A

The difference of two left transversals

Equations

• One or more equations did not get rendered due to their size.

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)) [Subgroup.FiniteIndex H] : A

The difference of two left transversals

Equations

• One or more equations did not get rendered due to their size.

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)) [AddSubgroup.FiniteIndex H] : 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)) [Subgroup.FiniteIndex H] : 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)) [AddSubgroup.FiniteIndex H] : 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)) [Subgroup.FiniteIndex H] : 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)) [AddSubgroup.FiniteIndex H] : -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)) [Subgroup.FiniteIndex H] : (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)) [AddSubgroup.FiniteIndex H] (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)) [Subgroup.FiniteIndex H] (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) [AddSubgroup.FiniteIndex H] : G →+ A

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

Equations

• One or more equations did not get rendered due to their size.

theorem AddMonoidHom.transfer.proof_2 {G : Type u_2} [AddGroup G] {H : AddSubgroup G} {A : Type u_1} [AddCommGroup A] (ϕ : ↥H →+ A) [AddSubgroup.FiniteIndex H] (g : G) (h : G) : { toFun := fun (g : G) => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default), map_zero' := (_ : (fun (g : G) => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default)) 0 = 0) }.toFun (g + h) = { toFun := fun (g : G) => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default), map_zero' := (_ : (fun (g : G) => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default)) 0 = 0) }.toFun g + { toFun := fun (g : G) => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default), map_zero' := (_ : (fun (g : G) => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default)) 0 = 0) }.toFun h

theorem AddMonoidHom.transfer.proof_1 {G : Type u_2} [AddGroup G] {H : AddSubgroup G} {A : Type u_1} [AddCommGroup A] (ϕ : ↥H →+ A) [AddSubgroup.FiniteIndex H] : (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) [Subgroup.FiniteIndex H] : G →* A

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

Equations

• One or more equations did not get rendered due to their size.

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)) [AddSubgroup.FiniteIndex H] (g : G) : (AddMonoidHom.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)) [Subgroup.FiniteIndex H] (g : G) : (MonoidHom.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) [Subgroup.FiniteIndex H] (g : G) [Fintype (Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H)))] : (MonoidHom.transfer ϕ) g = Finset.prod Finset.univ fun (q : Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H))) => ϕ { val := (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q), property := (_ : (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q) ∈ H) }

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 ^ Subgroup.index H ∈ 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) [Subgroup.FiniteIndex H] (g : G) (key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k) : (MonoidHom.transfer ϕ) g = ϕ { val := g ^ Subgroup.index H, property := (_ : g ^ Subgroup.index H ∈ H) }

theorem MonoidHom.transfer_center_eq_pow {G : Type u_1} [Group G] [Subgroup.FiniteIndex (Subgroup.center G)] (g : G) : (MonoidHom.transfer (MonoidHom.id ↥(Subgroup.center G))) g = { val := g ^ Subgroup.index (Subgroup.center G), property := (_ : g ^ Subgroup.index (Subgroup.center G) ∈ Subgroup.center G) }

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

The transfer homomorphism G →* center G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

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

Equations

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

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

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

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

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