mathlib3 documentation

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 #

Main results #

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] :
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} [add_comm_group A] (ϕ : H →+ A) (S T : (add_subgroup.left_transversals H)) [H.finite_index] :
A

The difference of two left transversals

Equations
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} [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
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) :
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, _⟩

The transfer homomorphism G →* center G.

Equations
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] :

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 : 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.

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) :

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