Short exact sequences of canonical continuous cochains

Mathlib's continuous cohomology is the homology of the homogeneous cochain complex TopRep.homogeneousCochains X, whose degree-n term is the G-invariant submodule of the iterated coinduced representation C(G, C(G, …, C(G, X))) with n + 1 factors of C(G, -). This file shows that a short exact sequence 0 → A → B → C → 0 of discrete G-modules induces, in every degree, a short exact sequence of these cochain modules. This is the input to the snake lemma, hence to the long exact sequence of continuous cohomology in all degrees.

The three exactness statements have different hypotheses, and the statements below carry exactly those:

• Injectivity (resolutionMap_injective, cochainsMap_f_injective): postcomposition with an injective map is injective, so this holds for any injective coefficient map.
• Exactness in the middle (resolutionMap_id_exact, cochainsMap_id_f_exact): a continuous function killed by g factors pointwise through f, and the factorization is continuous when f is inducing. For discrete A and B every injection is an embedding.
• Surjectivity (cochainsMap_id_f_surjective_of_section, DiscreteShortExact.continuousCochainsShortExact_g_surjective) is the substantial one, because an invariant cochain has to be lifted to an invariant cochain. A homogeneous cochain F satisfies F(g x₀, …, g xₙ) = g • F(x₀, …, xₙ), and it is lifted by (x₀, …, xₙ) ↦ x₀ • s (x₀⁻¹ • F(x₀, …, xₙ)) for any set-theoretic section s of B → C. The twisted section (h, c) ↦ h • s (h⁻¹ • c) is jointly continuous because C is discrete and the actions are continuous, and it is equivariant in the sense k • σ(h, c) = σ(k h, k • c), which is what makes the lift invariant. Carrying this through the iterated function spaces uses continuity of evaluation C(G, V) × G → V, which is where local compactness of G enters; profinite groups are locally compact.

The cochain functor is defined in Additive.lean, and the coefficient short complex is defined in ShortExact.lean.

Main definition

• TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact: its image under continuousCochainsFunctor, a short complex of cochain complexes.

Main results

• TauCeti.ContinuousCohomology.cochainsMap_id_f_surjective_of_section: invariant cochains lift along any coefficient map admitting a continuous family of sections σ : G × Z → Y that is equivariant in the sense k • σ(h, z) = σ(k h, k • z), over a locally compact group.
• TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact_f_injective, continuousCochainsShortExact_exact and continuousCochainsShortExact_g_surjective: the degreewise exactness of the cochain sequence.
• TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact_shortExact: after forgetting topologies, the cochain sequence is a short exact sequence of cochain complexes of ℤ-modules. TopModuleCat ℤ is not abelian, so the snake lemma (HomologicalComplex.HomologySequence) applies only after this step.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), Chapter I §2 (homogeneous continuous cochains) and (1.3.2) (the long exact sequence, whose proof starts from the exactness of cochains proved here).

Exactness on the coinduced resolution

@[simp]

theorem TauCeti.ContinuousCohomology.resolutionMap_id_succ_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep R G} (f : X ⟶ Y) (n : ℕ) (F : C(G, ↑(X.resolutionX n))) (x : G) : ((TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.id G) f (n + 1))) F) x = (TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.id G) f n)) (F x)

The level-(n + 1) map of the coinduced resolution is postcomposition with the level-n map.

theorem TauCeti.ContinuousCohomology.isInducing_resolutionMap_id {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep R G} {f : X ⟶ Y} (hf : Topology.IsInducing ⇑(TopRep.Hom.hom f)) (n : ℕ) : Topology.IsInducing ⇑(TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.id G) f n))

The level maps of the coinduced resolution induced by an inducing coefficient map are inducing.

theorem TauCeti.ContinuousCohomology.resolutionMap_id_exact {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Topology.IsInducing ⇑(TopRep.Hom.hom f)) (hfg : Function.Exact ⇑(TopRep.Hom.hom f) ⇑(TopRep.Hom.hom g)) (n : ℕ) : Function.Exact ⇑(TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.id G) f n)) ⇑(TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.id G) g n))

Exactness of the coinduced resolution in the middle. If X → Y → Z is exact and the first map is inducing, then so is every level C(G, …, C(G, X)) → C(G, …, C(G, Y)) → C(G, …, C(G, Z)): a continuous function killed by the second map factors pointwise through the first, and the factorization is continuous because the first map is inducing.

Exactness on homogeneous cochains

theorem TauCeti.ContinuousCohomology.coe_cochainsMap_id_f_hom_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep R G} (f : X ⟶ Y) (n : ℕ) (v : ↥(X.resolutionX (n + 1)).ρ.invariants) : ↑((TopModuleCat.Hom.hom ((ContinuousCohomology.cochainsMap (ContinuousMonoidHom.id G) f).f n)) v) = (TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.id G) f (n + 1))) ↑v

A homogeneous cochain is carried by the cochain map to its image under the level map of the coinduced resolution.

theorem TauCeti.ContinuousCohomology.cochainsMap_id_f_exact {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Topology.IsEmbedding ⇑(TopRep.Hom.hom f)) (hfg : Function.Exact ⇑(TopRep.Hom.hom f) ⇑(TopRep.Hom.hom g)) (n : ℕ) : Function.Exact ⇑(TopModuleCat.Hom.hom ((ContinuousCohomology.cochainsMap (ContinuousMonoidHom.id G) f).f n)) ⇑(TopModuleCat.Hom.hom ((ContinuousCohomology.cochainsMap (ContinuousMonoidHom.id G) g).f n))

Exactness of homogeneous cochains in the middle. If X → Y → Z is exact and the first map is an embedding, the induced sequence of homogeneous n-cochains is exact. Injectivity is what makes the preimage of an invariant cochain invariant.

Lifting invariant cochains along a twisted section

theorem TauCeti.ContinuousCohomology.cochainsMap_id_f_surjective_of_section {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {Y Z : TopRep R G} [LocallyCompactSpace G] (g : Y ⟶ Z) (σ : C(G × ↑Z, ↑Y)) (hσ : ∀ (h : G) (z : ↑Z), (TopRep.Hom.hom g) (σ (h, z)) = z) (hσ' : ∀ (k h : G) (z : ↑Z), (Y.ρ k) (σ (h, z)) = σ (k * h, (Z.ρ k) z)) (n : ℕ) : Function.Surjective ⇑(TopModuleCat.Hom.hom ((ContinuousCohomology.cochainsMap (ContinuousMonoidHom.id G) g).f n))

Invariant cochains lift along a map with an equivariant continuous family of sections. If σ : G × Z → Y is continuous, g (σ (h, z)) = z and k • σ (h, z) = σ (k h, k • z), then every homogeneous n-cochain of Z is the image of one of Y: the lift of F is x ↦ σₙ (x, F x).

noncomputable def TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : CategoryTheory.ShortComplex (CochainComplex (TopModuleCat ℤ) ℕ)

The short complex of canonical homogeneous-cochain complexes attached to a short exact sequence of discrete G-modules: in degree n it is Cⁿ(G, A) → Cⁿ(G, B) → Cⁿ(G, C) on Mathlib's homogeneous continuous cochains.

Equations

• S.continuousCochainsShortExact = S.toShortComplex.map (TauCeti.ContinuousCohomology.continuousCochainsFunctor ℤ G)

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact_X₁ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : S.continuousCochainsShortExact.X₁ = (ContinuousCohomology.continuousCochainsFunctor ℤ G).obj S.toShortComplex.X₁

The first cochain complex is the image of the first coefficient representation.

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact_X₂ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : S.continuousCochainsShortExact.X₂ = (ContinuousCohomology.continuousCochainsFunctor ℤ G).obj S.toShortComplex.X₂

The middle cochain complex is the image of the middle coefficient representation.

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact_X₃ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : S.continuousCochainsShortExact.X₃ = (ContinuousCohomology.continuousCochainsFunctor ℤ G).obj S.toShortComplex.X₃

The last cochain complex is the image of the last coefficient representation.

theorem TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact_f {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : CategoryTheory.CategoryStruct.comp S.continuousCochainsShortExact.f (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((ContinuousCohomology.continuousCochainsFunctor ℤ G).map S.toShortComplex.f)

The first cochain map is the functorial image of the coefficient inclusion, after transporting its source and target along the object identifications.

theorem TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact_g {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : CategoryTheory.CategoryStruct.comp S.continuousCochainsShortExact.g (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((ContinuousCohomology.continuousCochainsFunctor ℤ G).map S.toShortComplex.g)

The second cochain map is the functorial image of the coefficient projection, after transporting its source and target along the object identifications.

theorem TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact_f_injective {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (n : ℕ) : Function.Injective ⇑(TopModuleCat.Hom.hom (S.continuousCochainsShortExact.f.f n))

The cochain map induced by the inclusion A → B is injective in every degree.

theorem TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact_exact {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (n : ℕ) : Function.Exact ⇑(TopModuleCat.Hom.hom (S.continuousCochainsShortExact.f.f n)) ⇑(TopModuleCat.Hom.hom (S.continuousCochainsShortExact.g.f n))

The sequence of homogeneous n-cochains Cⁿ(G, A) → Cⁿ(G, B) → Cⁿ(G, C) is exact in the middle, in every degree.

theorem TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact_g_surjective {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) [LocallyCompactSpace G] [ContinuousSMul G B] (n : ℕ) : Function.Surjective ⇑(TopModuleCat.Hom.hom (S.continuousCochainsShortExact.g.f n))

Continuous cochains lift along B → C in every degree. For a locally compact group G acting continuously on the discrete module B, every homogeneous continuous n-cochain with values in C is the image of one with values in B. Continuity on C follows from the equivariant surjection B → C.

theorem TauCeti.ContCohomology.DiscreteShortExact.continuousCochainsShortExact_shortExact {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) [LocallyCompactSpace G] [ContinuousSMul G B] : (S.continuousCochainsShortExact.map ((CategoryTheory.forget₂ (TopModuleCat ℤ) (ModuleCat ℤ)).mapHomologicalComplex (ComplexShape.up ℕ))).ShortExact

The cochain sequence of a short exact sequence of discrete modules is short exact. After forgetting topologies, 0 → C•(G, A) → C•(G, B) → C•(G, C) → 0 is a short exact sequence of cochain complexes of ℤ-modules, for a locally compact group G acting continuously on B. This is the input to the snake lemma, and hence to the long exact sequence of continuous cohomology in every degree.