Coinduction along a subgroup of finite index

For a subgroup U of a topological group G and a U-module A, an element of the coinduced module Coind_U^G A of TauCeti.DiscreteCoind is determined by its values on a right transversal of U, since f (u * g) = u • f g. When U has finite index and A is finite this makes Coind_U^G A finite. When moreover U is open and acts trivially on A, every function on the coset space extends: Coind_U^G A is the module of all functions G ⧸ U → A, read through g ↦ g⁻¹ because the coinduced functions are constant on right cosets while G ⧸ U is the space of left cosets. This is the permutation module A[G ⧸ U], of order |A| ^ [G : U].

Main definitions

• TauCeti.DiscreteCoind.quotientPiAddEquiv: for an open U acting trivially on A, the additive equivalence Coind_U^G A ≃+ (G ⧸ U → A); quotientPiAddEquiv_smul_apply records that it carries the action of G on Coind_U^G A to the permutation action on G ⧸ U → A.

Main results

• TauCeti.DiscreteCoind.instFinite: Coind_U^G A is finite for finite A and finite-index U, since restriction to a right transversal is injective.
• TauCeti.DiscreteCoind.sum_single: for an open finite-index U, a coinduced function is the sum of its singles TauCeti.DiscreteCoind.single over a right transversal, so Coind_U^G A is the direct sum of [G : U] copies of A.
• TauCeti.DiscreteCoind.natCard_of_isOpen: |Coind_U^G A| = |A| ^ [G : U] for an open finite-index U acting trivially on A.
• TauCeti.DiscreteCoind.trace_eq_inv_smul_apply: the trace of a coinduced function supported on the single right coset U * g is g⁻¹ • f g.
• TauCeti.DiscreteCoind.trace_single and TauCeti.DiscreteCoind.trace_surjective: for an open finite-index U and a discrete G-module M, the trace of single g m is g⁻¹ • m, so the trace Coind_U^G M → M is surjective.
• TauCeti.DiscreteCoind.trace_eq_relIndex_nsmul_of_forall_smul_eq, TauCeti.DiscreteCoind.trace_eq_zero_of_forall_smul_eq: on the G-invariants of Coind_V^G M, for V ≤ U with U acting trivially on M, the trace is [U : V] times the norm along G ⧸ U; in particular it vanishes when [U : V] kills M. This is the co-effaceability of H⁰ that Tate's duality argument for the cohomological dimension of a Demushkin group uses (Serre, Structure de certains pro-p-groupes, §9.1).

instance TauCeti.DiscreteCoind.instFinite {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} {A : Type v} [AddCommGroup A] [DistribMulAction (↥U) A] [Finite A] [U.FiniteIndex] : Finite (DiscreteCoind G U A)

Coind_U^G A is finite when A is finite and U has finite index.

theorem TauCeti.DiscreteCoind.sum_single {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {U : Subgroup G} [U.FiniteIndex] {A : Type v} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥U) A] [ContinuousSMul (↥U) A] (hU : IsOpen ↑U) (f : DiscreteCoind G U A) : ∑ x : G ⧸ U, (single G U A hU (Quotient.out x)⁻¹) (f (Quotient.out x)⁻¹) = f

A coinduced function is the sum of its singles over a right transversal. For an open subgroup U of finite index, f = ∑_{x : G ⧸ U} single x.out⁻¹ (f x.out⁻¹): the right cosets U * x.out⁻¹ partition G, and on each of them f agrees with the single of its value at the representative.

def TauCeti.DiscreteCoind.quotientPiAddEquiv (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : Type v) [AddCommGroup A] [DistribMulAction (↥U) A] (hU : IsOpen ↑U) (htriv : ∀ (u : ↥U) (a : A), u • a = a) : DiscreteCoind G U A ≃+ (G ⧸ U → A)

The coinduced module of a trivial module along an open subgroup is the permutation module. For an open subgroup U acting trivially on A, the coinduced module Coind_U^G A is the module of all functions G ⧸ U → A: a coinduced function is constant on the right cosets of U, and g ↦ g⁻¹ matches right cosets with the left cosets that make up G ⧸ U.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DiscreteCoind.quotientPiAddEquiv_apply_mk {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {U : Subgroup G} {A : Type v} [AddCommGroup A] [DistribMulAction (↥U) A] (hU : IsOpen ↑U) (htriv : ∀ (u : ↥U) (a : A), u • a = a) (f : DiscreteCoind G U A) (g : G) : (quotientPiAddEquiv G U A hU htriv) f ↑g = f g⁻¹

quotientPiAddEquiv reads a coinduced function at the inverse of a coset representative.

@[simp]

theorem TauCeti.DiscreteCoind.quotientPiAddEquiv_symm_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {U : Subgroup G} {A : Type v} [AddCommGroup A] [DistribMulAction (↥U) A] (hU : IsOpen ↑U) (htriv : ∀ (u : ↥U) (a : A), u • a = a) (φ : G ⧸ U → A) (g : G) : ((quotientPiAddEquiv G U A hU htriv).symm φ) g = φ ↑g⁻¹

The inverse of quotientPiAddEquiv sends φ : G ⧸ U → A to the coinduced function g ↦ φ (g⁻¹ U).

@[simp]

theorem TauCeti.DiscreteCoind.quotientPiAddEquiv_smul_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {U : Subgroup G} {A : Type v} [AddCommGroup A] [DistribMulAction (↥U) A] (hU : IsOpen ↑U) (htriv : ∀ (u : ↥U) (a : A), u • a = a) (g : G) (f : DiscreteCoind G U A) (y : G ⧸ U) : (quotientPiAddEquiv G U A hU htriv) (g • f) y = (quotientPiAddEquiv G U A hU htriv) f (g⁻¹ • y)

quotientPiAddEquiv is G-equivariant. The action (g • f) x = f (x * g) of G on Coind_U^G A corresponds to the permutation action (g • φ) y = φ (g⁻¹ • y) on G ⧸ U → A, for the translation action of G on the coset space G ⧸ U.

theorem TauCeti.DiscreteCoind.natCard_of_isOpen {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {U : Subgroup G} {A : Type v} [AddCommGroup A] [DistribMulAction (↥U) A] (hU : IsOpen ↑U) (htriv : ∀ (u : ↥U) (a : A), u • a = a) [U.FiniteIndex] : Nat.card (DiscreteCoind G U A) = Nat.card A ^ U.index

The order of the coinduced module of a trivial module. For an open subgroup U of finite index acting trivially on A, Coind_U^G A has |A| ^ [G : U] elements.

theorem TauCeti.DiscreteCoind.trace_eq_inv_smul_apply {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {U : Subgroup G} [U.FiniteIndex] {M : Type v} [AddCommGroup M] [DistribMulAction G M] (f : DiscreteCoind G U M) (g : G) (hf : ∀ (x : G), x * g⁻¹ ∉ U → f x = 0) : (trace G U M) f = g⁻¹ • f g

The trace of a function supported on one right coset: if f vanishes off U * g, then tr f = g⁻¹ • f g. In the trace ∑_{x : G ⧸ U} x.out • f x.out⁻¹ only the coset x = g⁻¹ U contributes, and there x.out⁻¹ = u * g with u = x.out⁻¹ * g⁻¹, so the term is x.out • u • f g = g⁻¹ • f g.

theorem TauCeti.DiscreteCoind.trace_single {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {U : Subgroup G} [U.FiniteIndex] {M : Type v} [AddCommGroup M] [DistribMulAction G M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hU : IsOpen ↑U) (g : G) (m : M) : (trace G U M) ((single G U M hU g) m) = g⁻¹ • m

The trace of a single: tr (single g m) = g⁻¹ • m, since single g m is supported on the right coset U * g with value m at g. Not a simp lemma, because TauCeti.DiscreteCoind.trace_apply already takes its left-hand side apart.

theorem TauCeti.DiscreteCoind.trace_surjective {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {U : Subgroup G} [U.FiniteIndex] {M : Type v} [AddCommGroup M] [DistribMulAction G M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hU : IsOpen ↑U) : Function.Surjective ⇑(trace G U M)

The trace Coind_U^G M → M of an open subgroup is surjective: m is the trace of single 1 m, the function that is g ↦ g • m on U and 0 off U.

theorem TauCeti.DiscreteCoind.trace_eq_relIndex_nsmul_of_forall_smul_eq {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {V U : Subgroup G} [V.FiniteIndex] [U.FiniteIndex] {M : Type v} [AddCommGroup M] [DistribMulAction G M] (hVU : V ≤ U) (htriv : ∀ u ∈ U, ∀ (m : M), u • m = m) {f : DiscreteCoind G V M} (hf : ∀ (g : G), g • f = f) : (trace G V M) f = V.relIndex U • ∑ q : G ⧸ U, Quotient.out q • f 1

The trace on invariants is a multiple of the norm. For finite-index subgroups V ≤ U with U acting trivially on M, the trace of a G-invariant element f of Coind_V^G M is [U : V] times the norm ∑_{q ∈ G ⧸ U} q.out • f 1 of its constant value.

theorem TauCeti.DiscreteCoind.trace_eq_zero_of_forall_smul_eq {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {V U : Subgroup G} [V.FiniteIndex] [U.FiniteIndex] {M : Type v} [AddCommGroup M] [DistribMulAction G M] (hVU : V ≤ U) (htriv : ∀ u ∈ U, ∀ (m : M), u • m = m) (hkill : ∀ (m : M), V.relIndex U • m = 0) {f : DiscreteCoind G V M} (hf : ∀ (g : G), g • f = f) : (trace G V M) f = 0

The trace kills the invariants once the relative index kills the module. For finite-index subgroups V ≤ U with U acting trivially on M and [U : V] • m = 0 for every m, the trace Coind_V^G M → M vanishes on the G-invariants: the map H⁰(G, Coind_V^G M) → H⁰(G, M) induced by trace is zero.