Naturality of the low-degree connecting maps #
The connecting maps δ⁰ : H⁰(G, C) → H¹(G, A) and δ¹ : H¹(G, C) → H²(G, A) of a short exact
sequence 0 → A → B → C → 0 of discrete G-modules are natural in the sequence and in the group.
Both statements are instances of a single square: a continuous homomorphism φ : H →ₜ* G together
with coefficient maps fA, fB, fC that are equivariant along φ and commute with the two
maps of the sequences carries δ for the sequence over G to δ for a sequence over H.
H⁰(G, C) --δ⁰--> H¹(G, A) H¹(G, C) --δ¹--> H²(G, A)
| | | |
fC fA fC fA
v v v v
H⁰(H, C') -δ⁰-> H¹(H, A') H¹(H, C') -δ¹-> H²(H, A')
Taking φ to be the inclusion of a subgroup and the three coefficient maps to be the identity
gives naturality of δ under restriction, and taking φ to be the identity of G gives its
naturality in a morphism of short exact sequences. Inflation is the same square at the quotient
homomorphism G → G ⧸ N, but this file exports no inflation theorem: the invariants of a short
exact sequence need not be exact, so the sequence over G ⧸ N is data a caller supplies rather
than something constructible here, and inflation is left as a direct specialization of the two
general squares.
There is no compatible-pair map in degree zero to state the left-hand leg against: the
degree-zero carrier H⁰(G, C) = C^G has the two named maps explicitRes0 and explicitCoeff0
and no general one. Only explicitDelta0_naturality is affected: it takes the image c' of the
invariant c as an argument, together with the hypothesis (c' : C') = fC c identifying it, and
so does not assume fC equivariant at all; each named degree-zero instance discharges that
hypothesis by the coe_ lemma of its own degree-zero map. In degree one both legs are
compatible-pair maps, so explicitDelta1_naturality takes only the class x : H¹(G, C).
Continuity of a coefficient map is never a hypothesis here: every module in sight is discrete.
Mathlib's discrete groupCohomology.δ_naturality is the corresponding statement for Rep k G; it
keeps the group fixed and varies only the short complex, so it covers the explicitDelta0_coeffMap
and explicitDelta1_coeffMap half and not the change of group.
Main statements #
TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0_naturalityandexplicitDelta1_naturality: the two squares above.TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0_resandexplicitDelta1_res: restriction to a subgroup commutes with the connecting maps.TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0_coeffMapandexplicitDelta1_coeffMap: a morphism of short exact sequences commutes with the connecting maps.
Implementation notes #
The named instances explicitRes1, explicitRes2, explicitCoeff1 and explicitCoeff2 are
definitions of TauCeti/RepresentationTheory/Homological/ContCohomology/ExplicitFunctoriality.lean
whose bodies are not exposed, so they are not definitionally the compatible-pair pullbacks the two
general squares are stated against. The four private lemmas at the head of this file identify them,
each by evaluating both sides on a cocycle class with the _mk lemmas that file exports.
This implements the naturality half of the long exact sequence milestone of Layer 5 of the
human-authored roadmap at TauCetiRoadmap/ProfiniteCohomology/README.md, whose Suggested.lean
fixes the names explicitDelta0_res and explicitDelta1_res.
References #
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.3.2) and (1.5.2): the low-degree long exact sequence and the naturality of its connecting maps.
δ⁰ is natural in compatible pairs. For a continuous homomorphism φ : H →ₜ* G and
coefficient maps fA and fB equivariant along it and commuting with the two maps of the
sequences, the square
H⁰(G, C) --δ⁰--> H¹(G, A)
| |
c ↦ c' fA
v v
H⁰(H, C') -δ⁰-> H¹(H, A')
commutes. Degree zero carries no general compatible-pair map, so the left-hand leg is not fC but
an invariant c' of C' supplied together with the relation (c' : C') = fC c. Only fA and
fB are assumed equivariant; fC enters through that relation alone.
δ¹ is natural in compatible pairs, the degree-one counterpart of
TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0_naturality. Both legs are
compatible-pair pullbacks here, explicitMap1 on the source and explicitMap2 on the target.
Restriction commutes with δ⁰. The compatible pair is the inclusion of T together with
the identity on the coefficients, and the sequence over T is
TauCeti.ContCohomology.DiscreteShortExact.restrict.
Restriction commutes with δ¹, the degree-one counterpart of
TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0_res.
A morphism of short exact sequences commutes with δ⁰. This is
TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0_naturality at the identity
homomorphism of G, where the two legs of the square are the named coefficient maps.
A morphism of short exact sequences commutes with δ¹, the degree-one counterpart of
TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0_coeffMap.