The trace short exact sequence of an open subgroup

For an open subgroup U of finite index in a topological group G and a discrete G-module M, the trace Coind_U^G M → M of TauCeti.DiscreteCoind.trace is surjective (TauCeti.DiscreteCoind.trace_surjective). Its kernel TauCeti.DiscreteCoind.traceKer is a G-stable additive subgroup of the coinduced module, hence a discrete G-module in its own right, and the three fit into the short exact sequence

0 → traceKer G U M → Coind_U^G M → M → 0

of discrete G-modules, TauCeti.DiscreteCoind.traceShortExact. Its long exact cohomology sequence compares Hⁿ(G, Coind_U^G M) ≅ Hⁿ(U, M) with Hⁿ(G, M) through the cohomology of the kernel; this is how the cohomological dimension of G is bounded by that of an open subgroup (Serre, Galois Cohomology, Ch. I, §3.3, Prop. 14).

For a normal subgroup V, conjugation by g : G is a G-equivariant endomorphism TauCeti.DiscreteCoind.conj V V M g of Coind_V^G M, f ↦ (x ↦ g • f (g⁻¹ x)): under Coind_V^G M ≅ ℤ[G ⧸ V] ⊗ M it is right multiplication by g. It commutes with the trace, and the differences conj σ - 1 cover the kernel of the trace: the image of the G-equivariant map ∏_{x ∈ G ⧸ V} Coind_V^G M → Coind_V^G M, (φ_x)_x ↦ ∑_x (conj x.out⁻¹ - 1) φ_x, is exactly traceKer G V M. This is the cover ⊕_σ ℤ[G ⧸ V] ⊗ M → I ⊗ M, e_σ ⊗ m ↦ (σ - 1) ⊗ m, of NSW's proof of (3.3.11), I being the augmentation ideal of ℤ[G ⧸ V]. A preimage is computed from the decomposition into singles (TauCeti.DiscreteCoind.sum_single): conjugation by g moves the single at 1 to the single at g, and the singles at 1 add up to the single of the trace.

Main definitions

• TauCeti.DiscreteCoind.traceKer: the kernel of the trace, a G-stable additive subgroup of Coind_U^G M, with the restricted action of G and its continuity as instances.
• TauCeti.DiscreteCoind.traceShortExact: the short exact sequence 0 → traceKer G U M → Coind_U^G M → M → 0 for an open subgroup U.
• TauCeti.DiscreteCoind.traceKerCover: for a normal subgroup V, the cover ∏_{G ⧸ V} Coind_V^G M →+[G] Coind_V^G M by the conjugation differences conj σ - 1, whose image is traceKer G V M.
• TauCeti.DiscreteCoind.traceKerCoverShortExact: the short exact sequence 0 → traceKerCoverKer V M → ∏_{G ⧸ V} Coind_V^G M → traceKer G V M → 0 of the cover, whose second map is the codrestriction of traceKerCover to traceKer G V M.

Main results

• TauCeti.DiscreteCoind.isAddPGroup_traceKer: over a compact group the kernel of the trace of a p-primary torsion module is p-primary torsion.
• TauCeti.DiscreteCoind.conj_single_one: conjugation by g moves the single at 1 with value a to the single at g with value g • a.
• TauCeti.DiscreteCoind.range_traceKerCover: the image of the cover is exactly the kernel of the trace.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §3.3, Prop. 14.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (3.3.11).

The kernel of the trace

noncomputable def TauCeti.DiscreteCoind.traceKer (G : Type u) [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) [U.FiniteIndex] (M : Type v) [AddCommGroup M] [DistribMulAction G M] : AddSubgroup (DiscreteCoind G U M)

The kernel of the trace Coind_U^G M → M, as an additive subgroup of the coinduced module. It is G-stable (TauCeti.DiscreteCoind.smul_mem_traceKer), and carries the restricted action of G as an instance.

@[simp]

theorem TauCeti.DiscreteCoind.mem_traceKer_iff {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} : f ∈ traceKer G U M ↔ (trace G U M) f = 0

theorem TauCeti.DiscreteCoind.smul_mem_traceKer {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {U : Subgroup G} [U.FiniteIndex] {M : Type v} [AddCommGroup M] [DistribMulAction G M] (g : G) {f : DiscreteCoind G U M} (hf : f ∈ traceKer G U M) : g • f ∈ traceKer G U M

The kernel of the trace is stable under the action of G, the trace being equivariant.

@[instance_reducible]

noncomputable instance TauCeti.DiscreteCoind.instDistribMulActionSubtypeMemAddSubgroupTraceKer (G : Type u) [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) [U.FiniteIndex] (M : Type v) [AddCommGroup M] [DistribMulAction G M] : DistribMulAction G ↥(traceKer G U M)

The action of G on the kernel of the trace, by restriction.

@[simp]

theorem TauCeti.DiscreteCoind.coe_smul_traceKer (G : Type u) [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) [U.FiniteIndex] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (g : G) (f : ↥(traceKer G U M)) : ↑(g • f) = g • ↑f

The inclusion of the kernel of the trace in Coind_U^G M is equivariant.

theorem TauCeti.DiscreteCoind.isAddPGroup_traceKer (G : Type u) [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) [U.FiniteIndex] (M : Type v) [AddCommGroup M] [DistribMulAction G M] {p : ℕ} [CompactSpace G] (hM : IsAddPGroup p M) : IsAddPGroup p ↥(traceKer G U M)

Over a compact group, the kernel of the trace of a p-primary torsion module is p-primary torsion, as a subgroup of the p-primary torsion module Coind_U^G M.

The short exact sequence

noncomputable def TauCeti.DiscreteCoind.traceShortExact (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) : ContCohomology.DiscreteShortExact G (↥(traceKer G U M)) (DiscreteCoind G U M) M

The trace short exact sequence 0 → traceKer G U M → Coind_U^G M → M → 0 of discrete G-modules, for an open subgroup U of finite index and a discrete G-module M. The second map is the trace, surjective because U is open.

@[simp]

theorem TauCeti.DiscreteCoind.traceShortExact_incl (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) : (traceShortExact G U M hU).incl = (traceKer G U M).subtype

The first map of the trace short exact sequence is the inclusion of the kernel.

@[simp]

theorem TauCeti.DiscreteCoind.traceShortExact_proj (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) : (traceShortExact G U M hU).proj = (trace G U M).toAddMonoidHom

The second map of the trace short exact sequence is the trace.

instance TauCeti.DiscreteCoind.instContinuousSMulSubtypeMemAddSubgroupTraceKer (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) [U.FiniteIndex] (M : Type v) [AddCommGroup M] [DistribMulAction G M] : ContinuousSMul G ↥(traceKer G U M)

Over a compact group the restricted action on the kernel of the trace is continuous, the kernel being a discrete module.

The cover of the kernel of the trace of a normal subgroup

@[simp]

theorem TauCeti.DiscreteCoind.conj_single_one {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul (↥V) M] (hV : IsOpen ↑V) (g : G) (a : M) : (conj V V M g ⋯) ((single G V M hV 1) a) = (single G V M hV g) (g • a)

Conjugation moves singles: conjugation by g sends the single at 1 with value a to the single at g with value g • a.

noncomputable def TauCeti.DiscreteCoind.traceKerCover {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [V.FiniteIndex] : (G ⧸ V → DiscreteCoind G V M) →+[G] DiscreteCoind G V M

The cover of the kernel of the trace by conjugation differences: the G-equivariant map ∏_{x ∈ G ⧸ V} Coind_V^G M → Coind_V^G M sending (φ_x)_x to ∑_x (conj x.out⁻¹ - 1) φ_x. Its image is the kernel of the trace (range_traceKerCover).

@[simp]

theorem TauCeti.DiscreteCoind.traceKerCover_apply {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [V.FiniteIndex] (φ : G ⧸ V → DiscreteCoind G V M) : (traceKerCover V M) φ = ∑ x : G ⧸ V, ((conj V V M (Quotient.out x)⁻¹ ⋯) (φ x) - φ x)

The defining formula of traceKerCover.

theorem TauCeti.DiscreteCoind.traceKerCover_mem_traceKer {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [V.FiniteIndex] (φ : G ⧸ V → DiscreteCoind G V M) : (traceKerCover V M) φ ∈ traceKer G V M

The cover lands in the kernel of the trace, conjugation commuting with the trace.

theorem TauCeti.DiscreteCoind.range_traceKerCover {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [V.FiniteIndex] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul (↥V) M] (hV : IsOpen ↑V) : (traceKerCover V M).toAddMonoidHom.range = traceKer G V M

The image of the cover is the kernel of the trace. For f in the kernel of the trace, the family of singles at 1 with values x.out • f x.out⁻¹ is a preimage: conjugation moves them to the singles decomposing f, and they add up to the single of the trace of f, which is 0.

noncomputable def TauCeti.DiscreteCoind.traceKerCoverKer {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [V.FiniteIndex] : AddSubgroup (G ⧸ V → DiscreteCoind G V M)

The kernel of the cover traceKerCover, a G-stable additive subgroup of ∏_{G ⧸ V} Coind_V^G M.

@[simp]

theorem TauCeti.DiscreteCoind.mem_traceKerCoverKer_iff {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [V.FiniteIndex] {φ : G ⧸ V → DiscreteCoind G V M} : φ ∈ traceKerCoverKer V M ↔ (traceKerCover V M) φ = 0

theorem TauCeti.DiscreteCoind.smul_mem_traceKerCoverKer {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [V.FiniteIndex] (g : G) {φ : G ⧸ V → DiscreteCoind G V M} (hφ : φ ∈ traceKerCoverKer V M) : g • φ ∈ traceKerCoverKer V M

The kernel of the cover is stable under the action of G, the cover being equivariant.

@[instance_reducible]

noncomputable instance TauCeti.DiscreteCoind.instDistribMulActionSubtypeForallQuotientSubgroupMemAddSubgroupTraceKerCoverKer {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [V.FiniteIndex] : DistribMulAction G ↥(traceKerCoverKer V M)

The action of G on the kernel of the cover, by restriction.

@[simp]

theorem TauCeti.DiscreteCoind.coe_smul_traceKerCoverKer {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [V.FiniteIndex] (g : G) (φ : ↥(traceKerCoverKer V M)) : ↑(g • φ) = g • ↑φ

The inclusion of the kernel of the cover in ∏_{G ⧸ V} Coind_V^G M is equivariant.

instance TauCeti.DiscreteCoind.instContinuousSMulSubtypeForallQuotientSubgroupMemAddSubgroupTraceKerCoverKer {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (V : Subgroup G) [V.Normal] [V.FiniteIndex] (M : Type v) [AddCommGroup M] [DistribMulAction G M] : ContinuousSMul G ↥(traceKerCoverKer V M)

Over a compact group the restricted action on the kernel of the cover is continuous.

noncomputable def TauCeti.DiscreteCoind.traceKerCoverShortExact {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [V.FiniteIndex] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hV : IsOpen ↑V) : ContCohomology.DiscreteShortExact G (↥(traceKerCoverKer V M)) (G ⧸ V → DiscreteCoind G V M) ↥(traceKer G V M)

The short exact sequence of the cover 0 → traceKerCoverKer → ∏_{G ⧸ V} Coind_V^G M → traceKer G V M → 0 of discrete G-modules, for an open normal subgroup V of finite index.

@[simp]

theorem TauCeti.DiscreteCoind.traceKerCoverShortExact_incl {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [V.FiniteIndex] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hV : IsOpen ↑V) : (traceKerCoverShortExact V M hV).incl = (traceKerCoverKer V M).subtype

The first map of the cover short exact sequence is the inclusion of the kernel.

@[simp]

theorem TauCeti.DiscreteCoind.traceKerCoverShortExact_proj_apply {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (V : Subgroup G) [V.Normal] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [V.FiniteIndex] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hV : IsOpen ↑V) (φ : G ⧸ V → DiscreteCoind G V M) : ↑((traceKerCoverShortExact V M hV).proj φ) = (traceKerCover V M) φ

The second map of the cover short exact sequence, followed by the inclusion of the kernel of the trace, is the cover.