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) [fintype (G H)] (T : (subgroup.left_transversals 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) [fintype (G H)] (T : (add_subgroup.left_transversals H)) (g : G) :