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
.
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
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
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))
[fintype (G ⧸ H)] :
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))
[fintype (G ⧸ H)] :
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)] :
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))
[fintype (G ⧸ H)] :
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))
[fintype (G ⧸ H)] :
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))
[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) :
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))
[fintype (G ⧸ H)]
(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)
[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
- ϕ.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)
[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
- ϕ.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))
[fintype (G ⧸ H)]
(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))
[fintype (G ⧸ H)]
(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)
[fintype (G ⧸ H)]
(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]
[fintype (G ⧸ subgroup.center G)]
(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]
[fintype (G ⧸ subgroup.center G)] :
G →* ↥(subgroup.center G)
The transfer homomorphism G →* center G
.
Equations
- monoid_hom.transfer_center_pow = {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]
[fintype (G ⧸ subgroup.center G)]
(g : G) :
↑(⇑monoid_hom.transfer_center_pow g) = g ^ (subgroup.center G).index
noncomputable
def
monoid_hom.transfer_center_pow'
{G : Type u_1}
[group G]
(h : (subgroup.center G).index ≠ 0) :
G →* ↥(subgroup.center G)
The transfer homomorphism G →* center G
.
@[simp]
theorem
monoid_hom.transfer_center_pow'_apply
{G : Type u_1}
[group G]
(h : (subgroup.center G).index ≠ 0)
(g : G) :
↑(⇑(monoid_hom.transfer_center_pow' h) g) = g ^ (subgroup.center G).index