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 : ↥(subgroup.left_transversals ↑H)) [H.finite_index] :

The difference of two left transversals

Equations

subgroup.left_transversals.diff ϕ S T = let α : G ⧸ H ≃ ↥(S.val) := subgroup.mem_left_transversals.to_equiv _, β : G ⧸ H ≃ ↥(T.val) := subgroup.mem_left_transversals.to_equiv _ in finset.univ.prod (λ (q : G ⧸ H), ⇑ϕ ⟨(↑(⇑α q))⁻¹ * ↑(⇑β q), _⟩)

source

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

The difference of two left transversals

Equations

add_subgroup.left_transversals.diff ϕ S T = let α : G ⧸ H ≃ ↥(S.val) := add_subgroup.mem_left_transversals.to_equiv _, β : G ⧸ H ≃ ↥(T.val) := add_subgroup.mem_left_transversals.to_equiv _ in finset.univ.sum (λ (q : G ⧸ H), ⇑ϕ ⟨-↑(⇑α q) + ↑(⇑β q), _⟩)

source

theorem add_subgroup.left_transversals.diff_add_diff {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} [add_comm_group A] (ϕ : ↥H →+ A) (R S T : ↥(add_subgroup.left_transversals ↑H)) [H.finite_index] :

add_subgroup.left_transversals.diff ϕ R S + add_subgroup.left_transversals.diff ϕ S T = add_subgroup.left_transversals.diff ϕ R T

source

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 : ↥(subgroup.left_transversals ↑H)) [H.finite_index] :

subgroup.left_transversals.diff ϕ R S * subgroup.left_transversals.diff ϕ S T = subgroup.left_transversals.diff ϕ R T

source

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 : ↥(subgroup.left_transversals ↑H)) [H.finite_index] :

subgroup.left_transversals.diff ϕ T T = 1

source

theorem add_subgroup.left_transversals.diff_self {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} [add_comm_group A] (ϕ : ↥H →+ A) (T : ↥(add_subgroup.left_transversals ↑H)) [H.finite_index] :

add_subgroup.left_transversals.diff ϕ T T = 0

source

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 : ↥(subgroup.left_transversals ↑H)) [H.finite_index] :

(subgroup.left_transversals.diff ϕ S T)⁻¹ = subgroup.left_transversals.diff ϕ T S

source

theorem add_subgroup.left_transversals.diff_neg {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} [add_comm_group A] (ϕ : ↥H →+ A) (S T : ↥(add_subgroup.left_transversals ↑H)) [H.finite_index] :

-add_subgroup.left_transversals.diff ϕ S T = add_subgroup.left_transversals.diff ϕ T S

source

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 : ↥(subgroup.left_transversals ↑H)) [H.finite_index] (g : G) :

subgroup.left_transversals.diff ϕ (g • S) (g • T) = subgroup.left_transversals.diff ϕ S T

source

theorem add_subgroup.left_transversals.vadd_diff_vadd {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} [add_comm_group A] (ϕ : ↥H →+ A) (S T : ↥(add_subgroup.left_transversals ↑H)) [H.finite_index] (g : G) :

add_subgroup.left_transversals.diff ϕ (g +ᵥ S) (g +ᵥ T) = add_subgroup.left_transversals.diff ϕ S T

source

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

ϕ.transfer = let T : ↥(subgroup.left_transversals ↑H) := inhabited.default in {to_fun := λ (g : G), subgroup.left_transversals.diff ϕ T (g • T), map_one' := _, map_mul' := _}

source

noncomputable def add_monoid_hom.transfer {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} [add_comm_group A] (ϕ : ↥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

ϕ.transfer = let T : ↥(add_subgroup.left_transversals ↑H) := inhabited.default in {to_fun := λ (g : G), add_subgroup.left_transversals.diff ϕ T (g +ᵥ T), map_zero' := _, map_add' := _}

source

theorem monoid_hom.transfer_def {G : Type u_1} [group G] {H : subgroup G} {A : Type u_2} [comm_group A] (ϕ : ↥H →* A) (T : ↥(subgroup.left_transversals ↑H)) [H.finite_index] (g : G) :

⇑(ϕ.transfer) g = subgroup.left_transversals.diff ϕ T (g • T)

source

theorem add_monoid_hom.transfer_def {G : Type u_1} [add_group G] {H : add_subgroup G} {A : Type u_2} [add_comm_group A] (ϕ : ↥H →+ A) (T : ↥(add_subgroup.left_transversals ↑H)) [H.finite_index] (g : G) :

⇑(ϕ.transfer) g = add_subgroup.left_transversals.diff ϕ T (g +ᵥ T)

source

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 (mul_action.orbit_rel ↥(subgroup.zpowers g) (G ⧸ H)))] :

⇑(ϕ.transfer) g = finset.univ.prod (λ (q : quotient (mul_action.orbit_rel ↥(subgroup.zpowers g) (G ⧸ H))), ⇑ϕ ⟨(quotient.out' q.out')⁻¹ * g ^ function.minimal_period (has_smul.smul g) q.out' * quotient.out' q.out', _⟩)

Explicit computation of the transfer homomorphism.

source

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.

source

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, _⟩

source

theorem monoid_hom.transfer_center_eq_pow {G : Type u_1} [group G] [(subgroup.center G).finite_index] (g : G) :

⇑((monoid_hom.id ↥(subgroup.center G)).transfer) g = ⟨g ^ (subgroup.center G).index, _⟩

source

noncomputable def monoid_hom.transfer_center_pow (G : Type u_1) [group G] [(subgroup.center G).finite_index] :

G →* ↥(subgroup.center G)

The transfer homomorphism G →* center G.

Equations

monoid_hom.transfer_center_pow G = {to_fun := λ (g : G), ⟨g ^ (subgroup.center G).index, _⟩, map_one' := _, map_mul' := _}

source

@[simp]

theorem monoid_hom.transfer_center_pow_apply {G : Type u_1} [group G] [(subgroup.center G).finite_index] (g : G) :

↑(⇑(monoid_hom.transfer_center_pow G) g) = g ^ (subgroup.center G).index

source

noncomputable def monoid_hom.transfer_sylow {G : Type u_1} [group G] {p : ℕ} (P : sylow p G) (hP : ↑P.normalizer ≤ subgroup.centralizer ↑P) [↑P.finite_index] :

G →* ↥↑P

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

Equations

monoid_hom.transfer_sylow P hP = (monoid_hom.id ↥P).transfer

source

theorem monoid_hom.transfer_sylow_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

Auxillary lemma in order to state transfer_sylow_eq_pow.

source

theorem monoid_hom.transfer_sylow_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.finite_index] (g : G) (hg : g ∈ P) :

⇑(monoid_hom.transfer_sylow P hP) g = ⟨g ^ ↑P.index, _⟩

source

theorem monoid_hom.transfer_sylow_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.finite_index] :

⇑((monoid_hom.transfer_sylow P hP).restrict ↑P) = λ (_x : ↥↑P), _x ^ ↑P.index

source

theorem monoid_hom.ker_transfer_sylow_is_complement' {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.finite_index] :

(monoid_hom.transfer_sylow P hP).ker.is_complement' ↑P

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

source

theorem monoid_hom.not_dvd_card_ker_transfer_sylow {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.finite_index] :

¬p ∣ nat.card ↥((monoid_hom.transfer_sylow P hP).ker)

source

theorem monoid_hom.ker_transfer_sylow_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.finite_index] (Q : subgroup G) (hQ : is_p_group p ↥Q) :

disjoint (monoid_hom.transfer_sylow P hP).ker Q