mathlib documentation

group_theory.transfer

The Transfer Homomorphism #

In this file we construct the transfer homomorphism.

Main definitions #

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)) [fintype (G H)] :
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)) [fintype (G H)] :
A

The difference of two left transversals

Equations
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)) [fintype (G H)] :
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)) [fintype (G H)] (g : G) :
noncomputable def monoid_hom.transfer {G : Type u_1} [group G] {H : subgroup G} {A : Type u_2} [comm_group A] (ϕ : H →* A) [fintype (G H)] :
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) [fintype (G H)] :
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)) [fintype (G H)] (g : G) :
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)) [fintype (G H)] (g : G) :

Explicit computation of the transfer homomorphism.

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₀ Hg₀⁻¹ * 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) [fintype (G H)] (g : G) (key : ∀ (k : ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ Hg₀⁻¹ * g ^ k * g₀ = g ^ k) :
(ϕ.transfer) g = ϕ g ^ H.index, _⟩
noncomputable def monoid_hom.transfer_center_pow {G : Type u_1} [group G] [fintype (G subgroup.center G)] :

The transfer homomorphism G →* center G.

Equations
noncomputable def monoid_hom.transfer_center_pow' {G : Type u_1} [group G] (h : (subgroup.center G).index 0) :

The transfer homomorphism G →* center G.

Equations