The Transfer Homomorphism #
In this file we construct the transfer homomorphism.
Main definitions #
diff ϕ S T
: The difference of two left transversalsS
andT
under the homomorphismϕ
.transfer ϕ
: The transfer homomorphism induced byϕ
.transfer_center_pow
: The transfer homomorphismG →* center G
.
Main results #
transfer_center_pow_apply
: The transfer homomorphismG →* center G
is given byg ↦ g ^ (center G).index
.ker_transfer_sylow_is_complement'
: Burnside's transfer (or normalp
-complement) theorem: IfhP : N(P) ≤ C(P)
, then(transfer P hP).ker
is a normalp
-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] :
A
The difference of two left transversals
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
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] :
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] :
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
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
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] :
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] :
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
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
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' := _}
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' := _}
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)
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)
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.
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, _⟩
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' := _}
@[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
noncomputable
def
monoid_hom.transfer_sylow
{G : Type u_1}
[group G]
{p : ℕ}
(P : sylow p G)
(hP : ↑P.normalizer ≤ ↑P.centralizer)
[↑P.finite_index] :
The homomorphism G →* P
in Burnside's transfer theorem.
Equations
- monoid_hom.transfer_sylow P hP = (monoid_hom.id ↥P).transfer
theorem
monoid_hom.transfer_sylow_eq_pow
{G : Type u_1}
[group G]
{p : ℕ}
(P : sylow p G)
(hP : ↑P.normalizer ≤ ↑P.centralizer)
[fact (nat.prime p)]
[finite (sylow p G)]
[↑P.finite_index]
(g : G)
(hg : g ∈ P) :
theorem
monoid_hom.ker_transfer_sylow_is_complement'
{G : Type u_1}
[group G]
{p : ℕ}
(P : sylow p G)
(hP : ↑P.normalizer ≤ ↑P.centralizer)
[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.
theorem
monoid_hom.not_dvd_card_ker_transfer_sylow
{G : Type u_1}
[group G]
{p : ℕ}
(P : sylow p G)
(hP : ↑P.normalizer ≤ ↑P.centralizer)
[fact (nat.prime p)]
[finite (sylow p G)]
[↑P.finite_index] :
theorem
monoid_hom.ker_transfer_sylow_disjoint
{G : Type u_1}
[group G]
{p : ℕ}
(P : sylow p G)
(hP : ↑P.normalizer ≤ ↑P.centralizer)
[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