Acyclicity of Coind_1^G A in every degree

For a compact group G and a discrete module A over a topological ring R, the coinduced module Coind_1^G A = TauCeti.DiscreteCoind G ⊥ A of the trivial subgroup, the locally constant maps G → A under right translation, has vanishing continuous cohomology in every positive degree:

Hⁿ⁺¹(G, Coind_1^G A) = 0,

for Mathlib's canonical continuousCohomology. This is the all-degree form of TauCeti.ContCohomology.subsingleton_H1_discreteCoind_bot and TauCeti.ContCohomology.subsingleton_H2_discreteCoind_bot, and it is the input to dimension shifting in every degree.

The proof does not use Shapiro's lemma. Mathlib computes Hⁿ(G, X) as the homology of the G-invariants of the shifted coinduced resolution C(G, C(G, …, C(G, X))), whose differential is defined recursively by d (n + 1) F x = F - d n (F x). Two observations drive the argument.

• The full, non-invariant, coinduced resolution of any representation is contracted by evaluation at 1: d n (F 1) + (d (n + 1) F) 1 = F, the single-point case of TopRep.d_sum_apply_add_sum_d_apply in TauCeti/RepresentationTheory/Homological/ContCohomology/Resolution.lean. This is immediate from the recursion, but evaluation at 1 is not equivariant, so it does not act on the invariants.
• For the coefficients X = Coind_1^G A, an invariant element F of level m of the resolution is determined by evaluation at 1 inside every level, x₁ ↦ ⋯ ↦ xₘ ↦ F x₁ ⋯ xₘ 1, which lands in level m of the coinduced resolution of A with the trivial action (evalLevel). The inverse spreads a level Φ of that resolution back over G, as x₁ ↦ ⋯ ↦ xₘ ↦ (y ↦ Φ (y x₁) ⋯ (y xₘ)) (coindLevel). Evaluation is a chain map (evalLevel_d), because the differential is natural in the underlying modules and does not see the action.

A cocycle F of degree n + 1 is thus sent by evaluation to a cocycle Φ of the resolution of A, which is d (Φ 1) by the contraction; spreading Φ 1 back over G gives an invariant cochain whose differential is the spread of d (Φ 1) = Φ (d_coindLevel_const), which is F.

Compactness of G enters in two places. Every level of the resolution is discrete (TauCeti.discreteTopology_resolutionX), which makes evalLevel and coindLevel continuous, and G is locally compact, which makes evaluation C(G, Z) × G → Z continuous and hence lets the two-variable family ContinuousMap.compSwapShearMulRight be curried. Neither total disconnectedness of G nor any continuity of the action is needed. The coefficient ring R is arbitrary: evaluation at 1 is R-linear, and nothing else in the argument depends on the scalars.

Main definitions

• TauCeti.ContCohomology.evalLevel: evaluation at 1 inside every level of the coinduced resolution of Coind_1^G A.
• TauCeti.ContCohomology.coindLevel: spreading a level of the resolution of A over G, built from the family ContinuousMap.compSwapShearMulRight, x ↦ (y ↦ Ψ y (y * x)).

Main results

• TauCeti.ContCohomology.evalLevel_d: evaluation at 1 is a chain map.
• TauCeti.ContCohomology.eq_coindLevel_const_evalLevel and TauCeti.ContCohomology.eq_of_evalLevel_eq: an invariant element is recovered from, hence determined by, its evaluation at 1.
• TauCeti.ContCohomology.d_coindLevel_const: spreading a constant family commutes with the differentials.
• TauCeti.ContCohomology.subsingleton_continuousCohomology_discreteCoind_bot: Hⁿ⁺¹(G, Coind_1^G A) = 0 for every n, for a compact group G and a discrete R-module A; TauCeti.ContCohomology.subsingleton_continuousCohomology_discreteCoind_bot_int is its R = ℤ case for the integral module structure AddCommGroup.toIntModule on Coind_1^G A, the one Mathlib's instance search produces, and for an abelian group A without topology.
• TauCeti.ContCohomology.coindAcyclic: the same vanishing in the bundled language, Hⁿ(G, Coind_1^G A) is a zero object of TopModuleCat R for n > 0 and a smooth discrete representation A of the trivial subgroup, with Coind_1^G A = TauCeti.coindTopRep R G ⊥ A.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.3.7), whose proof through the standard resolution is the one written here on Mathlib's coinduced resolution. NSW write Ind for the coinduced module.
• L. Ribes, P. Zalesskii, Profinite Groups, Thm. 6.10.5 and Cor. 6.10.6.

Evaluation at 1 inside every level

noncomputable def TauCeti.ContCohomology.evalLevel (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (m : ℕ) : ↑((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX m) →L[R] ↑((TopRep.of (ContRepresentation.trivial R G A)).resolutionX m)

Evaluation at 1 inside every level of the coinduced resolution of Coind_1^G A: evalLevel 0 f = f 1 and evalLevel (m + 1) F x = evalLevel m (F x). It lands in the coinduced resolution of A with the trivial action, and it is not G-equivariant.

Equations

• TauCeti.ContCohomology.evalLevel R G A 0 = { toLinearMap := TauCeti.DiscreteCoind.evalLinear G ⊥ A R, cont := ⋯ }
• TauCeti.ContCohomology.evalLevel R G A m.succ = ContinuousLinearMap.compLeftContinuous R G (TauCeti.ContCohomology.evalLevel R G A m)

@[simp]

theorem TauCeti.ContCohomology.evalLevel_zero_apply (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (f : DiscreteCoind G ⊥ A) : (evalLevel R G A 0) f = f 1

@[simp]

theorem TauCeti.ContCohomology.evalLevel_succ_apply (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (m : ℕ) (F : ↑((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX (m + 1))) (x : G) : ((evalLevel R G A (m + 1)) F) x = (evalLevel R G A m) (F x)

@[simp]

theorem TauCeti.ContCohomology.evalLevel_d (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (m : ℕ) (F : ↑((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX m)) : (evalLevel R G A (m + 1)) ((TopRep.Hom.hom ((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).d m)) F) = (TopRep.Hom.hom ((TopRep.of (ContRepresentation.trivial R G A)).d m)) ((evalLevel R G A m) F)

Evaluation at 1 is a chain map from the coinduced resolution of Coind_1^G A to the coinduced resolution of A.

Spreading a level of the resolution of A over G

noncomputable def TauCeti.ContCohomology.coindLevel (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (m : ℕ) : C(G, ↑((TopRep.of (ContRepresentation.trivial R G A)).resolutionX m)) → ↑((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX m)

Spreading a level over G. For Ψ : C(G, C(G, …, C(G, A))) with m inner factors, coindLevel m Ψ is the element x₁ ↦ ⋯ ↦ xₘ ↦ (y ↦ Ψ y (y x₁) ⋯ (y xₘ)) of level m of the coinduced resolution of Coind_1^G A: coindLevel 0 Ψ is Ψ read as a locally constant map, and coindLevel (m + 1) Ψ x = coindLevel m (y ↦ Ψ y (y x)). On a constant family Ψ = Φ it inverts evalLevel on the invariant elements (eq_coindLevel_const_evalLevel).

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.ContCohomology.coindLevel R G A 0 = TauCeti.DiscreteCoind.ofContinuousMap G A

@[simp]

theorem TauCeti.ContCohomology.coindLevel_zero (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (Ψ : C(G, A)) : coindLevel R G A 0 Ψ = DiscreteCoind.ofContinuousMap G A Ψ

@[simp]

theorem TauCeti.ContCohomology.coindLevel_succ_apply (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (m : ℕ) (Ψ : C(G, ↑((TopRep.of (ContRepresentation.trivial R G A)).resolutionX (m + 1)))) (x : G) : (coindLevel R G A (m + 1) Ψ) x = coindLevel R G A m (Ψ.compSwapShearMulRight x)

@[simp]

theorem TauCeti.ContCohomology.evalLevel_coindLevel (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (m : ℕ) (Ψ : C(G, ↑((TopRep.of (ContRepresentation.trivial R G A)).resolutionX m))) : (evalLevel R G A m) (coindLevel R G A m Ψ) = Ψ 1

Evaluation at 1 recovers the parameter of coindLevel at 1.

@[simp]

theorem TauCeti.ContCohomology.ρ_coindLevel (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (m : ℕ) (g : G) (Ψ : C(G, ↑((TopRep.of (ContRepresentation.trivial R G A)).resolutionX m))) : (((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX m).ρ g) (coindLevel R G A m Ψ) = coindLevel R G A m (Ψ.comp (ContinuousMap.mulRight g))

The action of G on the coinduced resolution translates the parameter of coindLevel: g • coindLevel m Ψ = coindLevel m (y ↦ Ψ (y * g)).

theorem TauCeti.ContCohomology.eq_coindLevel_of_forall_evalLevel_ρ (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (m : ℕ) (F : ↑((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX m)) (Ψ : C(G, ↑((TopRep.of (ContRepresentation.trivial R G A)).resolutionX m))) : (∀ (y : G), (evalLevel R G A m) ((((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX m).ρ y) F) = Ψ y) → F = coindLevel R G A m Ψ

Reconstruction of a level from its translates. An element F of level m of the coinduced resolution of Coind_1^G A whose translates g • F evaluate at 1 to Ψ g is coindLevel m Ψ.

theorem TauCeti.ContCohomology.eq_coindLevel_const_evalLevel (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (m : ℕ) (F : ↑((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX m)) (hF : ∀ (g : G), (((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX m).ρ g) F = F) : F = coindLevel R G A m (ContinuousMap.const G ((evalLevel R G A m) F))

An invariant level is recovered from its evaluation at 1: an invariant F is coindLevel m of the constant family at evalLevel m F.

theorem TauCeti.ContCohomology.eq_of_evalLevel_eq (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (m : ℕ) {F F' : ↑((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX m)} (hF : ∀ (g : G), (((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX m).ρ g) F = F) (hF' : ∀ (g : G), (((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX m).ρ g) F' = F') (h : (evalLevel R G A m) F = (evalLevel R G A m) F') : F = F'

Evaluation at 1 is injective on the invariant elements of every level.

theorem TauCeti.ContCohomology.ρ_coindLevel_const (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (m : ℕ) (g : G) (Φ : ↑((TopRep.of (ContRepresentation.trivial R G A)).resolutionX m)) : (((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).resolutionX m).ρ g) (coindLevel R G A m (ContinuousMap.const G Φ)) = coindLevel R G A m (ContinuousMap.const G Φ)

The constant family at a level of the resolution of A spreads to an invariant element.

@[simp]

theorem TauCeti.ContCohomology.d_coindLevel_const (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (m : ℕ) (Φ : ↑((TopRep.of (ContRepresentation.trivial R G A)).resolutionX m)) : (TopRep.Hom.hom ((ofDiscreteModule R G (DiscreteCoind G ⊥ A)).d m)) (coindLevel R G A m (ContinuousMap.const G Φ)) = coindLevel R G A (m + 1) (ContinuousMap.const G ((TopRep.Hom.hom ((TopRep.of (ContRepresentation.trivial R G A)).d m)) Φ))

Spreading a constant family commutes with the differentials: the differential of the coinduced resolution of Coind_1^G A carries coindLevel m of the constant family at Φ to coindLevel (m + 1) of the constant family at d m Φ. With evalLevel_d, this makes coindLevel on constant families a chain map, inverse to evalLevel on the invariant elements.

Acyclicity

instance TauCeti.ContCohomology.subsingleton_continuousCohomology_discreteCoind_bot (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul R A] [DistribMulAction (↥⊥) A] [SMulCommClass (↥⊥) R A] (n : ℕ) : Subsingleton ↑(continuousCohomology (n + 1) (ofDiscreteModule R G (DiscreteCoind G ⊥ A))).toModuleCat

Coind_1^G A is acyclic in every positive degree. For a compact group G and a discrete module A over a topological ring R, the continuous cohomology Hⁿ⁺¹(G, Coind_1^G A) of the locally constant maps G → A under right translation vanishes for every n. The action of the trivial subgroup ⊥ on A carried by Coind_1^G A is arbitrary, for instance the restriction of an action of G on A: the equivariance condition it imposes is vacuous, so it does not change the underlying module of locally constant maps.

The integral module structure

instance TauCeti.ContCohomology.subsingleton_continuousCohomology_discreteCoind_bot_int (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : Type u) [AddCommGroup A] [DistribMulAction (↥⊥) A] (n : ℕ) : Subsingleton ↑(continuousCohomology (n + 1) (ofDiscreteModule ℤ G (DiscreteCoind G ⊥ A))).toModuleCat

Coind_1^G A is acyclic in every positive degree, for the integral module structure AddCommGroup.toIntModule on Coind_1^G A and an abelian group A carrying no topology. This is subsingleton_continuousCohomology_discreteCoind_bot at R = ℤ, restated for the module structure that instance search produces for Coind_1^G A, which is the one the long exact sequence of TauCeti.ContCohomology.DiscreteShortExact uses: it is transported from the scalar module structure of TauCeti.DiscreteCoind along the equality of the two ℤ-module structures.

The bundled statement

theorem TauCeti.ContCohomology.coindAcyclic (R : Type v) [Ring R] [TopologicalSpace R] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : SmoothDiscreteTopRep R ↥⊥) (n : ℕ) (hn : 0 < n) : CategoryTheory.Limits.IsZero (continuousCohomology n ((smoothDiscreteι R G).obj (coindTopRep R G ⊥ A)))

Coind_1^G A is acyclic in every positive degree, in the bundled language: for a smooth discrete representation A of the trivial subgroup, the continuous cohomology Hⁿ(G, Coind_1^G A) of Coind_1^G A = TauCeti.coindTopRep R G ⊥ A is a zero object of TopModuleCat R for every n > 0. This is subsingleton_continuousCohomology_discreteCoind_bot for the underlying module of A, with the action of the trivial subgroup read off from A.