The relative norm and the relative transfer of a subgroup

Let ρ : Representation R G V and let H ≤ G be a subgroup of finite index. Summing the action over a left transversal of H gives two endomorphisms of V,

relNorm ρ H = ∑ q : G ⧸ H, ρ q.out and relTransfer ρ H = ∑ q : G ⧸ H, ρ q.out⁻¹,

which refine the norm Representation.norm ρ = ∑ g : G, ρ g of a finite group: the norm of G is the relative norm composed with the norm of H, and it is also the norm of H composed with the relative transfer.

Neither endomorphism is canonical — each depends on the chosen transversal, here Quotient.out — but each becomes canonical on an appropriate submodule or quotient. The relative norm is independent of the transversal on the invariants V^H, where it takes values in V^G and restricts to multiplication by [G : H] on V^G; the relative transfer is independent of the transversal modulo the augmentation submodule of H, into which it carries the augmentation submodule of G. Modulo the larger augmentation submodule of G, the relative transfer is multiplication by [G : H].

These are the two maps that give restriction and corestriction on the Tate cohomology of a subgroup in the two degrees where Tate cohomology is not ordinary group cohomology or homology.

Main definitions

• Representation.relNorm: the relative norm ∑ q : G ⧸ H, ρ q.out.
• Representation.relTransfer: the relative transfer ∑ q : G ⧸ H, ρ q.out⁻¹.

Main results

• Representation.relNorm_comp_norm: N_{G/H} ∘ N_H = N_G.
• Representation.norm_comp_relTransfer: N_H ∘ N_{G/H}' = N_G.
• Representation.relNorm_apply_eq_self: the relative norm carries H-fixed vectors to G-fixed vectors, over any semiring.
• Representation.relNorm_apply_of_forall_apply_eq: on G-fixed vectors the relative norm is [G : H] • ·, over any semiring.
• Representation.relTransfer_mem_coinvariantsKer: the relative transfer carries the augmentation submodule of G into the augmentation submodule of H.
• Representation.relTransfer_sub_index_nsmul_mem: modulo the augmentation submodule of G the relative transfer is [G : H] • ·.
• Representation.relTransfer_sub_sum_mem: modulo the augmentation submodule of H the relative transfer is the sum over any transversal of H.
• Representation.relTransfer_map_sub_mem: modulo the augmentation submodule of H' the relative transfer commutes with a map of representations along a group isomorphism carrying H to H'.
• Representation.relTransfer_relTransfer_sub_relTransfer_mem: modulo the augmentation submodule of K the relative transfer is transitive along a tower K ≤ H ≤ G.

References

• K. S. Brown, Cohomology of Groups, Chapter III, §9.
• J. S. Milne, Class Field Theory, v4.03, Chapter II, §1.

noncomputable def Representation.relNorm {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] (ρ : Representation R G V) (H : Subgroup G) [Fintype (G ⧸ H)] : Module.End R V

The relative norm of a finite-index subgroup H ≤ G: the sum of ρ over the transversal of H given by Quotient.out. On the H-invariants it does not depend on that choice and lands in the G-invariants; see Representation.relNorm_apply_eq_self.

Equations

• ρ.relNorm H = ∑ q : G ⧸ H, ρ (Quotient.out q)

noncomputable def Representation.relTransfer {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] (ρ : Representation R G V) (H : Subgroup G) [Fintype (G ⧸ H)] : Module.End R V

The relative transfer of a finite-index subgroup H ≤ G: the sum of ρ over the inverses of the transversal of H given by Quotient.out, which form a transversal of the right cosets. Modulo the augmentation submodule of H it does not depend on that choice; see Representation.relTransfer_sub_sum_mem.

Equations

• ρ.relTransfer H = ∑ q : G ⧸ H, ρ (Quotient.out q)⁻¹

theorem Representation.relNorm_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype (G ⧸ H)] (x : V) : (ρ.relNorm H) x = ∑ q : G ⧸ H, (ρ (Quotient.out q)) x

The relative norm sends x to ∑_{q ∈ G ⧸ H} ρ(q.out) x, a sum over the chosen coset representatives.

theorem Representation.relTransfer_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype (G ⧸ H)] (x : V) : (ρ.relTransfer H) x = ∑ q : G ⧸ H, (ρ (Quotient.out q)⁻¹) x

The relative transfer sends x to ∑_{q ∈ G ⧸ H} ρ(q.out⁻¹) x, a sum over the inverses of the chosen coset representatives.

theorem Representation.relNorm_norm_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype G] (x : V) : (ρ.relNorm H) ((norm (MonoidHom.comp ρ H.subtype)) x) = ρ.norm x

The norm of G is the relative norm of H evaluated on the norm of H.

theorem Representation.relNorm_comp_norm {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype G] : ρ.relNorm H ∘ₗ norm (MonoidHom.comp ρ H.subtype) = ρ.norm

The norm of G is the relative norm of H composed with the norm of H.

theorem Representation.norm_relTransfer_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype G] (x : V) : (norm (MonoidHom.comp ρ H.subtype)) ((ρ.relTransfer H) x) = ρ.norm x

The norm of G is the norm of H evaluated on the relative transfer of H.

theorem Representation.norm_comp_relTransfer {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype G] : norm (MonoidHom.comp ρ H.subtype) ∘ₗ ρ.relTransfer H = ρ.norm

The norm of G is the norm of H composed with the relative transfer of H.

theorem Representation.range_norm_le_range_norm_comp_subtype {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype G] : LinearMap.range ρ.norm ≤ LinearMap.range (norm (MonoidHom.comp ρ H.subtype))

The image of the norm of G is contained in the image of the norm of H.

theorem Representation.ker_norm_comp_subtype_le_ker_norm {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype G] : LinearMap.ker (norm (MonoidHom.comp ρ H.subtype)) ≤ LinearMap.ker ρ.norm

The kernel of the norm of H is contained in the kernel of the norm of G.

noncomputable def Representation.relTransferKerNorm {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] (ρ : Representation R G V) (H : Subgroup G) [Fintype G] : ↥(LinearMap.ker ρ.norm) →ₗ[R] ↥(LinearMap.ker (norm (MonoidHom.comp ρ H.subtype)))

The relative transfer maps the kernel of the norm of G to the kernel of the norm of H.

Equations

• ρ.relTransferKerNorm H = LinearMap.restrict (ρ.relTransfer H) ⋯

@[simp]

theorem Representation.coe_relTransferKerNorm {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] (ρ : Representation R G V) (H : Subgroup G) [Fintype G] (x : ↥(LinearMap.ker ρ.norm)) : ↑((ρ.relTransferKerNorm H) x) = (ρ.relTransfer H) ↑x

On underlying elements, relTransferKerNorm is the relative transfer.

theorem Representation.relNorm_apply_eq_self {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] (ρ : Representation R G V) {H : Subgroup G} [Fintype (G ⧸ H)] {x : V} (hx : ∀ (h : ↥H), (ρ ↑h) x = x) (g : G) : (ρ g) ((ρ.relNorm H) x) = (ρ.relNorm H) x

The relative norm sends H-fixed vectors to G-fixed vectors.

theorem Representation.relNorm_apply_of_forall_apply_eq {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [Semiring R] [AddCommMonoid V] [Module R V] (ρ : Representation R G V) {H : Subgroup G} [Fintype (G ⧸ H)] {x : V} (hx : ∀ (g : G), (ρ g) x = x) : (ρ.relNorm H) x = H.index • x

On G-fixed vectors the relative norm is multiplication by the index.

noncomputable def Representation.relNormInvariants {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [CommRing R] [AddCommGroup V] [Module R V] (ρ : Representation R G V) (H : Subgroup G) [Fintype (G ⧸ H)] : ↥(invariants (MonoidHom.comp ρ H.subtype)) →ₗ[R] ↥ρ.invariants

The relative norm as a linear map from the H-invariants to the G-invariants.

Equations

• ρ.relNormInvariants H = LinearMap.restrict (ρ.relNorm H) ⋯

@[simp]

theorem Representation.coe_relNormInvariants {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [CommRing R] [AddCommGroup V] [Module R V] (ρ : Representation R G V) (H : Subgroup G) [Fintype (G ⧸ H)] (x : ↥(invariants (MonoidHom.comp ρ H.subtype))) : ↑((ρ.relNormInvariants H) x) = (ρ.relNorm H) ↑x

On underlying elements, relNormInvariants is the relative norm.

theorem Representation.relTransfer_sub_index_nsmul_mem {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [CommRing R] [AddCommGroup V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype (G ⧸ H)] (x : V) : (ρ.relTransfer H) x - H.index • x ∈ Coinvariants.ker ρ

Modulo the augmentation submodule of G, the relative transfer is multiplication by the index.

theorem Representation.relTransfer_mem_coinvariantsKer {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [CommRing R] [AddCommGroup V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype (G ⧸ H)] {x : V} (hx : x ∈ Coinvariants.ker ρ) : (ρ.relTransfer H) x ∈ Coinvariants.ker (MonoidHom.comp ρ H.subtype)

The relative transfer carries the augmentation submodule of G into the augmentation submodule of H; it is therefore the transfer of H on coinvariants.

theorem Representation.relTransfer_sub_sum_mem {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [CommRing R] [AddCommGroup V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype (G ⧸ H)] {ι : Type u_4} [Fintype ι] (f : ι → G) (hf : Function.Bijective fun (i : ι) => ↑(f i)) (x : V) : (ρ.relTransfer H) x - ∑ i : ι, (ρ (f i)⁻¹) x ∈ Coinvariants.ker (MonoidHom.comp ρ H.subtype)

The relative transfer is computed by any transversal, modulo the augmentation submodule of H. relTransfer sums ρ q.out⁻¹ over the transversal Quotient.out; any family f whose classes exhaust G ⧸ H bijectively computes the same element of the coinvariants.

theorem Representation.relTransfer_map_sub_mem {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [CommRing R] [AddCommGroup V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype (G ⧸ H)] {G' : Type u_4} {V' : Type u_5} [Group G'] [AddCommGroup V'] [Module R V'] {ρ' : Representation R G' V'} (e : G ≃* G') (φ : V →ₗ[R] V') (hφ : ∀ (g : G) (x : V), φ ((ρ g) x) = (ρ' (e g)) (φ x)) {H' : Subgroup G'} (he : Subgroup.map (↑e) H = H') [Fintype (G' ⧸ H')] (x : V) : φ ((ρ.relTransfer H) x) - (ρ'.relTransfer H') (φ x) ∈ Coinvariants.ker (MonoidHom.comp ρ' H'.subtype)

The relative transfer commutes with a map of representations along a group isomorphism, modulo the augmentation submodule of H'. Here e : G ≃* G' carries H onto H' and φ intertwines ρ with ρ' along e.

theorem Representation.relTransfer_relTransfer_sub_relTransfer_mem {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [CommRing R] [AddCommGroup V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} [Fintype (G ⧸ H)] {K : Subgroup G} (hKH : K ≤ H) [Fintype (G ⧸ K)] [Fintype (↥H ⧸ K.subgroupOf H)] (x : V) : (relTransfer (MonoidHom.comp ρ H.subtype) (K.subgroupOf H)) ((ρ.relTransfer H) x) - (ρ.relTransfer K) x ∈ Coinvariants.ker (MonoidHom.comp ρ K.subtype)

The relative transfer is transitive along a tower K ≤ H ≤ G, modulo the augmentation submodule of K. Transferring from G to H and then from H to K agrees with the transfer from G to K.