Naturality of the low-degree connecting maps, and their compatibility with corestriction #
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).
Corestriction along a finite-index open subgroup U ≤ G is not a compatible-pair map, so it is
not a specialization of the two squares. It commutes with the connecting maps nonetheless: for the
sequence over G and its restriction to U,
H⁰(U, C) --δ⁰--> H¹(U, A) H¹(U, C) --δ¹--> H²(U, A)
| | | |
cor⁰ cor¹ cor¹ cor²
v v v v
H⁰(G, C) --δ⁰--> H¹(G, A) H¹(G, C) --δ¹--> H²(G, A)
commute. The upper row is the connecting map of the restricted sequence S.restrict U, so both
rows are taken for the same two coefficient maps, and U is open of finite index, as
corestriction requires.
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 compatible-pair 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.TauCeti.ContCohomology.DiscreteShortExact.explicitCor_delta0andexplicitCor_delta1: corestriction commutes with the connecting maps,cor ∘ δ = δ ∘ cor.
Implementation notes #
The two general squares are stated for arbitrary compatible pairs. The named maps
explicitRes1, explicitRes2, explicitCoeff1, and explicitCoeff2 are rewritten into that
form using the public explicitRes1_eq_explicitMap1, explicitRes2_eq_explicitMap2,
explicitCoeff1_eq_explicitMap1, and explicitCoeff2_eq_explicitMap2 lemmas from
TauCeti/RepresentationTheory/Homological/ContCohomology/ExplicitFunctoriality.lean.
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.
Corestriction commutes with δ⁰: cor¹ ∘ δ⁰ = δ⁰ ∘ cor⁰ (Neukirch–Schmidt–Wingberg
(1.5.2)). The connecting map on the left is that of the sequence restricted to U, so both sides
name the same two coefficient maps.
Corestriction commutes with δ¹: cor² ∘ δ¹ = δ¹ ∘ cor¹, the degree-one counterpart of
TauCeti.ContCohomology.DiscreteShortExact.explicitCor_delta0. The connecting map on the left is
that of S.restrict U, where U is open and has finite index.