Rational dimension shifting for integral continuous cohomology

For a compact group with trivial discrete coefficients, the connecting map of 0 → ℤ → ℚ → ℚ/ℤ → 0 identifies Hⁿ(G, ℚ/ℤ) with Hⁿ⁺¹(G, ℤ) for n > 0. In degree one this describes integral second cohomology by continuous rational characters. It is the connecting-map half of the computation of second integral cohomology of the profinite integers.

The integers and rationals are lifted to the universe of the group. The rational module must carry a discrete topology. The quotient coefficient module is supplied through an additive equivalence with AddCircle (1 : ℚ), allowing any discrete model of the rational circle. All caller-supplied actions are retained and assumed trivial. No new cohomology carrier is used.

The algebraic exactness is reused from ModuleCat.ratAddCircleShortComplex_shortExact; the isomorphism uses the canonical connecting map and vanishing of positive-degree continuous cohomology of discrete rational vector spaces.

References

• J.-P. Serre, Local Fields, Chapter XIII, §1, Propositions 1–2.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.3.2) and (1.6.1).

def TauCeti.ContCohomology.rationalIntegralShortExact (G : Type u) [Group G] [DistribMulAction G (ULift.{u, 0} ℤ)] [DistribMulAction G (ULift.{u, 0} ℚ)] [TopologicalSpace (ULift.{u, 0} ℚ)] [DiscreteTopology (ULift.{u, 0} ℚ)] (C : Type u) [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (e : C ≃+ AddCircle 1) (hℤ : ∀ (g : G) (x : ULift.{u, 0} ℤ), g • x = x) (hℚ : ∀ (g : G) (x : ULift.{u, 0} ℚ), g • x = x) (hC : ∀ (g : G) (x : C), g • x = x) : DiscreteShortExact G (ULift.{u, 0} ℤ) (ULift.{u, 0} ℚ) C

The discrete trivial coefficient sequence 0 → ℤ → ℚ → ℚ/ℤ → 0, with a supplied model of the rational circle. The two small coefficient groups are universe-lifted.

@[simp]

theorem TauCeti.ContCohomology.rationalIntegralShortExact_incl_apply (G : Type u) [Group G] [DistribMulAction G (ULift.{u, 0} ℤ)] [DistribMulAction G (ULift.{u, 0} ℚ)] [TopologicalSpace (ULift.{u, 0} ℚ)] [DiscreteTopology (ULift.{u, 0} ℚ)] (C : Type u) [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (e : C ≃+ AddCircle 1) (hℤ : ∀ (g : G) (x : ULift.{u, 0} ℤ), g • x = x) (hℚ : ∀ (g : G) (x : ULift.{u, 0} ℚ), g • x = x) (hC : ∀ (g : G) (x : C), g • x = x) (x : ULift.{u, 0} ℤ) : (rationalIntegralShortExact G C e hℤ hℚ hC).incl x = { down := ↑x.down }

The inclusion sends a lifted integer to the same rational number.

@[simp]

theorem TauCeti.ContCohomology.rationalIntegralShortExact_proj_apply (G : Type u) [Group G] [DistribMulAction G (ULift.{u, 0} ℤ)] [DistribMulAction G (ULift.{u, 0} ℚ)] [TopologicalSpace (ULift.{u, 0} ℚ)] [DiscreteTopology (ULift.{u, 0} ℚ)] (C : Type u) [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (e : C ≃+ AddCircle 1) (hℤ : ∀ (g : G) (x : ULift.{u, 0} ℤ), g • x = x) (hℚ : ∀ (g : G) (x : ULift.{u, 0} ℚ), g • x = x) (hC : ∀ (g : G) (x : C), g • x = x) (x : ULift.{u, 0} ℚ) : (rationalIntegralShortExact G C e hℤ hℚ hC).proj x = e.symm ↑x.down

The projection is reduction of the rational value modulo 1, read in the supplied model.

@[simp]

theorem TauCeti.ContCohomology.rationalIntegralShortExact_restrict (G : Type u) [Group G] [DistribMulAction G (ULift.{u, 0} ℤ)] [DistribMulAction G (ULift.{u, 0} ℚ)] [TopologicalSpace (ULift.{u, 0} ℚ)] [DiscreteTopology (ULift.{u, 0} ℚ)] (C : Type u) [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (e : C ≃+ AddCircle 1) (hℤ : ∀ (g : G) (x : ULift.{u, 0} ℤ), g • x = x) (hℚ : ∀ (g : G) (x : ULift.{u, 0} ℚ), g • x = x) (hC : ∀ (g : G) (x : C), g • x = x) (T : Subgroup G) : (rationalIntegralShortExact G C e hℤ hℚ hC).restrict T = rationalIntegralShortExact (↥T) C e ⋯ ⋯ ⋯

Restricting the rational coefficient sequence retains the same inclusion and projection.

noncomputable def TauCeti.ContCohomology.rationalIntegralDeltaIso (G : Type u) [Group G] [DistribMulAction G (ULift.{u, 0} ℤ)] [DistribMulAction G (ULift.{u, 0} ℚ)] [TopologicalSpace (ULift.{u, 0} ℚ)] [DiscreteTopology (ULift.{u, 0} ℚ)] (C : Type u) [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (e : C ≃+ AddCircle 1) (hℤ : ∀ (g : G) (x : ULift.{u, 0} ℤ), g • x = x) (hℚ : ∀ (g : G) (x : ULift.{u, 0} ℚ), g • x = x) (hC : ∀ (g : G) (x : C), g • x = x) [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [ContinuousSMul G (ULift.{u, 0} ℚ)] (n : ℕ) : continuousCohomology (n + 1) (ofDiscreteModule ℤ G C) ≅ continuousCohomology (n + 1 + 1) (ofDiscreteModule ℤ G (ULift.{u, 0} ℤ))

Rational dimension shifting in every positive degree: the canonical connecting map Hⁿ⁺¹(G, ℚ/ℤ) → Hⁿ⁺²(G, ℤ) is an isomorphism of topological integer modules.

@[simp]

theorem TauCeti.ContCohomology.rationalIntegralDeltaIso_hom (G : Type u) [Group G] [DistribMulAction G (ULift.{u, 0} ℤ)] [DistribMulAction G (ULift.{u, 0} ℚ)] [TopologicalSpace (ULift.{u, 0} ℚ)] [DiscreteTopology (ULift.{u, 0} ℚ)] (C : Type u) [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (e : C ≃+ AddCircle 1) (hℤ : ∀ (g : G) (x : ULift.{u, 0} ℤ), g • x = x) (hℚ : ∀ (g : G) (x : ULift.{u, 0} ℚ), g • x = x) (hC : ∀ (g : G) (x : C), g • x = x) [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [ContinuousSMul G (ULift.{u, 0} ℚ)] (n : ℕ) : (rationalIntegralDeltaIso G C e hℤ hℚ hC n).hom = (rationalIntegralShortExact G C e hℤ hℚ hC).delta (n + 1)

The forward map of rational dimension shifting is the canonical connecting map of the named coefficient sequence.

theorem TauCeti.ContCohomology.rationalIntegralDeltaIso_hom_res (G : Type u) [Group G] [DistribMulAction G (ULift.{u, 0} ℤ)] [DistribMulAction G (ULift.{u, 0} ℚ)] [TopologicalSpace (ULift.{u, 0} ℚ)] [DiscreteTopology (ULift.{u, 0} ℚ)] (C : Type u) [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (e : C ≃+ AddCircle 1) (hℤ : ∀ (g : G) (x : ULift.{u, 0} ℤ), g • x = x) (hℚ : ∀ (g : G) (x : ULift.{u, 0} ℚ), g • x = x) (hC : ∀ (g : G) (x : C), g • x = x) [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [ContinuousSMul G (ULift.{u, 0} ℚ)] (T : Subgroup G) [CompactSpace ↥T] (n : ℕ) : CategoryTheory.CategoryStruct.comp (rationalIntegralDeltaIso G C e hℤ hℚ hC n).hom (ContinuousCohomology.res T (ofDiscreteModule ℤ G (ULift.{u, 0} ℤ)) (n + 1 + 1)) = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.res T (ofDiscreteModule ℤ G C) (n + 1)) (rationalIntegralDeltaIso (↥T) C e ⋯ ⋯ ⋯ n).hom

Rational dimension shifting commutes with restriction to a compact subgroup.

theorem TauCeti.ContCohomology.rationalIntegralDeltaIso_hom_res_assoc (G : Type u) [Group G] [DistribMulAction G (ULift.{u, 0} ℤ)] [DistribMulAction G (ULift.{u, 0} ℚ)] [TopologicalSpace (ULift.{u, 0} ℚ)] [DiscreteTopology (ULift.{u, 0} ℚ)] (C : Type u) [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (e : C ≃+ AddCircle 1) (hℤ : ∀ (g : G) (x : ULift.{u, 0} ℤ), g • x = x) (hℚ : ∀ (g : G) (x : ULift.{u, 0} ℚ), g • x = x) (hC : ∀ (g : G) (x : C), g • x = x) [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [ContinuousSMul G (ULift.{u, 0} ℚ)] (T : Subgroup G) [CompactSpace ↥T] (n : ℕ) {Z : TopModuleCat ℤ} (h : continuousCohomology (n + 1 + 1) (TopRep.res T.subtype (ofDiscreteModule ℤ G (ULift.{u, 0} ℤ))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (rationalIntegralDeltaIso G C e hℤ hℚ hC n).hom (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.res T (ofDiscreteModule ℤ G (ULift.{u, 0} ℤ)) (n + 1 + 1)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.res T (ofDiscreteModule ℤ G C) (n + 1)) (rationalIntegralDeltaIso (↥T) C e ⋯ ⋯ ⋯ n).hom) h

Rational dimension shifting commutes with restriction to a compact subgroup.

noncomputable def TauCeti.ContCohomology.continuousCohomologyTwoIntEquivContinuousMonoidHom (G : Type u) [Group G] [DistribMulAction G (ULift.{u, 0} ℤ)] [DistribMulAction G (ULift.{u, 0} ℚ)] [TopologicalSpace (ULift.{u, 0} ℚ)] [DiscreteTopology (ULift.{u, 0} ℚ)] (C : Type u) [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (e : C ≃+ AddCircle 1) (hℤ : ∀ (g : G) (x : ULift.{u, 0} ℤ), g • x = x) (hℚ : ∀ (g : G) (x : ULift.{u, 0} ℚ), g • x = x) (hC : ∀ (g : G) (x : C), g • x = x) [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [ContinuousSMul G (ULift.{u, 0} ℚ)] [ContinuousSMul G C] : ↑(continuousCohomology 2 (ofDiscreteModule ℤ G (ULift.{u, 0} ℤ))).toModuleCat ≃+ Additive (G →ₜ* Multiplicative C)

Integral second continuous cohomology of a compact group is the additive group of continuous rational-circle characters.

@[simp]

theorem TauCeti.ContCohomology.continuousCohomologyTwoIntEquivContinuousMonoidHom_symm_apply (G : Type u) [Group G] [DistribMulAction G (ULift.{u, 0} ℤ)] [DistribMulAction G (ULift.{u, 0} ℚ)] [TopologicalSpace (ULift.{u, 0} ℚ)] [DiscreteTopology (ULift.{u, 0} ℚ)] (C : Type u) [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (e : C ≃+ AddCircle 1) (hℤ : ∀ (g : G) (x : ULift.{u, 0} ℤ), g • x = x) (hℚ : ∀ (g : G) (x : ULift.{u, 0} ℚ), g • x = x) (hC : ∀ (g : G) (x : C), g • x = x) [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [ContinuousSMul G (ULift.{u, 0} ℚ)] [ContinuousSMul G C] (χ : Additive (G →ₜ* Multiplicative C)) : (continuousCohomologyTwoIntEquivContinuousMonoidHom G C e hℤ hℚ hC).symm χ = (CategoryTheory.ConcreteCategory.hom ((rationalIntegralShortExact G C e hℤ hℚ hC).delta 1)) ((explicitH1AddEquivContinuousCohomology G C) ((H1EquivOfSmulEqSelf hC).symm χ))

The inverse character identification takes the explicit class of the character to canonical cohomology and then applies the connecting map.