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ϕ
.transferCenterPow
: The transfer homomorphismG →* center G
.
Main results #
transferCenterPow_apply
: The transfer homomorphismG →* center G
is given byg ↦ g ^ (center G).index
.ker_transferSylow_isComplement'
: Burnside's transfer (or normalp
-complement) theorem: IfhP : N(P) ≤ C(P)
, then(transfer P hP).ker
is a normalp
-complement.
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 = ∑ q : G ⧸ H, ϕ ⟨-↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) q) + ↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) q), ⋯⟩
Instances For
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 = ∏ q : G ⧸ H, ϕ ⟨(↑((Subgroup.MemLeftTransversals.toEquiv ⋯) q))⁻¹ * ↑((Subgroup.MemLeftTransversals.toEquiv ⋯) q), ⋯⟩
Instances For
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]
:
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]
:
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]
:
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 = { toFun := fun (g : G) => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default), map_zero' := ⋯, map_add' := ⋯ }
Instances For
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 = { toFun := fun (g : G) => Subgroup.leftTransversals.diff ϕ default (g • default), map_one' := ⋯, map_mul' := ⋯ }
Instances For
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_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' := ⋯ }
Instances For
@[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
Instances For
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)
:
Auxiliary lemma in order to state transferSylow_eq_pow
.
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.