The explicit long exact sequence in low degrees

A short exact sequence 0 → A → B → C → 0 of discrete modules over a topological group G induces the exact sequence

0 → H⁰(G, A) → H⁰(G, B) → H⁰(G, C) →δ⁰→ H¹(G, A) → H¹(G, B) → H¹(G, C) →δ¹→ H²(G, A) → H²(G, B)

of the explicit continuous-cochain model. This file proves exactness at each of its eight nodes.

The two leftmost nodes need no topology on G at all; the remaining six carry exactly the hypotheses their maps require, so the three nodes touching H² also ask for a continuous multiplication on G.

The arguments are the ordinary diagram chases, run on continuous cochains. The topological input is entirely in ShortExact.lean: a continuous cochain into the discrete C lifts to a continuous cochain into B, and a continuous cochain into B killed by the projection retracts to a continuous cochain into A. Once a chase has produced a cochain, mem_Z1_of_incl_comp_mem_Z1 and mem_Z2_of_incl_comp_mem_Z2 are what put it back into the continuous cocycles.

Main statements

• TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H0A: the coefficient inclusion is injective on H⁰.
• TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H0B: exactness at H⁰(G, B).
• TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H0C: exactness at H⁰(G, C).
• TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H1A: exactness at H¹(G, A).
• TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H1B: exactness at H¹(G, B).
• TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H1C: exactness at H¹(G, C).
• TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H2A: exactness at H²(G, A).
• TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H2B: exactness at H²(G, B).
• TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0_surjective_of_subsingleton and explicitDelta1_bijective_of_subsingleton: when H¹(G, B) and H²(G, B) vanish, δ⁰ is onto and δ¹ is bijective.
• TauCeti.ContCohomology.DiscreteShortExact.explicitCoeff0_surjective_of_subsingleton: when H¹(G, A) vanishes, H⁰(G, B) → H⁰(G, C) is onto.

The maps and their normalization are those of TauCeti/RepresentationTheory/Homological/ContCohomology/LowDegree.lean, ExplicitFunctoriality.lean and ShortExact.lean. This implements the eight exactness nodes of the long exact sequence milestone of Layer 5 of the human-authored roadmap at TauCetiRoadmap/ProfiniteCohomology/README.md, whose Suggested.lean fixes the eight names above.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.3.2): the low-degree long exact sequence used here.

Coefficient maps on chosen representatives

Every chase below hands a cocycle to a coefficient map and has to recognize the result as the class of a cocycle already in hand. These two lemmas do that recognition once; they are the explicitCoeff counterpart of explicitDelta0_apply and explicitDelta1_apply.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H0A {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : Function.Injective ⇑(explicitCoeff0 G A S.inclDistribMulActionHom)

Exactness at H⁰(G, A): the coefficient inclusion remains injective on invariants.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H0B {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : (explicitCoeff0 G A S.inclDistribMulActionHom).range = (explicitCoeff0 G B S.projDistribMulActionHom).ker

Exactness at H⁰(G, B): the invariant elements killed by the projection are precisely the invariant elements coming from A.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H0C {G : Type u} [Group G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : (explicitCoeff0 G B S.projDistribMulActionHom).range = S.explicitDelta0.ker

Exactness at H⁰(G, C): the image of the projection on invariants is the kernel of the connecting homomorphism δ⁰ : H⁰(G, C) → H¹(G, A).

The degree-one nodes

Exactness at H¹(G, A) and at H¹(G, B). Neither node mentions H², so neither needs a continuous multiplication on G.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H1A {G : Type u} [Group G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : S.explicitDelta0.range = (explicitCoeff1 G A S.inclDistribMulActionHom ⋯).ker

Exactness at H¹(G, A), the node where δ⁰ lands.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H1B {G : Type u} [Group G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] (S : DiscreteShortExact G A B C) : (explicitCoeff1 G A S.inclDistribMulActionHom ⋯).range = (explicitCoeff1 G B S.projDistribMulActionHom ⋯).ker

Exactness at H¹(G, B).

The nodes touching degree two

Exactness at H¹(G, C), where δ¹ leaves, and at H²(G, A) and H²(G, B). All three mention H², hence carry the continuous multiplication on G that makes d¹ preserve continuity.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H1C {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] (S : DiscreteShortExact G A B C) : (explicitCoeff1 G B S.projDistribMulActionHom ⋯).range = S.explicitDelta1.ker

Exactness at H¹(G, C), the node where δ¹ leaves.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H2A {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] (S : DiscreteShortExact G A B C) : S.explicitDelta1.range = (explicitCoeff2 G A S.inclDistribMulActionHom ⋯).ker

Exactness at H²(G, A), the node where δ¹ lands.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitLongExact_H2B {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] (S : DiscreteShortExact G A B C) : (explicitCoeff2 G A S.inclDistribMulActionHom ⋯).range = (explicitCoeff2 G B S.projDistribMulActionHom ⋯).ker

Exactness at H²(G, B), the eighth and last node.

An acyclic middle term

When B has vanishing H¹ and H², the long exact sequence makes the connecting maps shift degree: δ⁰ is onto and δ¹ is an isomorphism. This is the step of the dimension-shifting argument that does not depend on how the acyclic module was built.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0_surjective_of_subsingleton {G : Type u} [Group G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) [Subsingleton (H1 G B)] : Function.Surjective ⇑S.explicitDelta0

If the middle term has vanishing H¹, then δ⁰ : H⁰(G, C) → H¹(G, A) is surjective.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitDelta1_bijective_of_subsingleton {G : Type u} [Group G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) [ContinuousMul G] [ContinuousSMul G C] [Subsingleton (H1 G B)] [Subsingleton (H2 G B)] : Function.Bijective ⇑S.explicitDelta1

If the middle term has vanishing H¹ and H², then δ¹ : H¹(G, C) → H²(G, A) is bijective.

An acyclic first term

When A has vanishing H¹, the connecting map δ⁰ is zero, so taking invariants is exact on the right: every invariant of C is the image of an invariant of B.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitCoeff0_surjective_of_subsingleton {G : Type u} [Group G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) [Subsingleton (H1 G A)] : Function.Surjective ⇑(explicitCoeff0 G B S.projDistribMulActionHom)

If the first term has vanishing H¹, then H⁰(G, B) → H⁰(G, C) is surjective.