Acyclicity of Coind_1^G and dimension shifting #
For a profinite group G, the coinduced module Coind_1^G A of the trivial subgroup, which is the
group of all locally constant maps G → A (TauCeti.mem_coind_bot_iff), has vanishing
explicit continuous cohomology in degrees one and two. This is Shapiro's lemma at U = ⊥: the
trivial subgroup of a totally disconnected group is closed, and a trivial group has no cohomology
in positive degrees. In every positive degree, and for any compact G, the canonical continuous
cohomology of Coind_1^G A vanishes by
TauCeti.ContCohomology.subsingleton_continuousCohomology_discreteCoind_bot.
Every discrete G-module M embeds into this acyclic module by its orbit maps, the unit of
coinduction TauCeti.DiscreteCoind.unit G ⊥ M,
M ↪ Coind_1^G M, m ↦ (x ↦ x • m),
and the long exact sequence of 0 → M → Coind_1^G M → Coind_1^G M ⧸ M → 0
(TauCeti.ContCohomology.coindShortExact G ⊥ M, built for an arbitrary subgroup in
TauCeti/RepresentationTheory/Homological/ContCohomology/Coinduced/Quotient.lean) then shifts
degrees:
H²(G, M) ≅ H¹(G, Coind_1^G M ⧸ M),
H¹(G, M) ≅ H⁰(G, Coind_1^G M ⧸ M) ⧸ image of H⁰(G, Coind_1^G M).
These are the two instances of Hⁱ⁺¹(G, M) ≅ Hⁱ(G, Coind_1^G M ⧸ M) in which both sides live in
the explicit low-degree complex; in degree zero the source H⁰(G, Coind_1^G M) need not vanish,
and the statement is the cokernel form. The shift itself is proved for an arbitrary short exact
sequence of discrete modules whose middle term has vanishing H¹ and H²
(TauCeti.ContCohomology.DiscreteShortExact.explicitDelta1_bijective_of_subsingleton, in
TauCeti/RepresentationTheory/Homological/ContCohomology/LongExact.lean).
In every positive degree the same short exact sequence, fed to the long exact sequence of Mathlib's
canonical continuous cohomology and to the all-degree acyclicity of Coind_1^G M, gives
Hⁱ⁺¹(G, M) ≅ Hⁱ(G, Coind_1^G M ⧸ M) (i ≥ 1)
for every compact group G (TauCeti.ContCohomology.dimensionShiftIso), inverse to the
connecting map, which is an isomorphism (TauCeti.ContCohomology.isIso_coindShortExact_bot_delta).
Main definitions #
TauCeti.ContCohomology.explicitDimensionShift1:H¹(G, Coind_1^G M ⧸ M) ≃+ H²(G, M), the connecting mapδ¹.TauCeti.ContCohomology.explicitDimensionShift0: the cokernel ofH⁰(G, Coind_1^G M) → H⁰(G, Coind_1^G M ⧸ M)isH¹(G, M), throughδ⁰.TauCeti.ContCohomology.dimensionShiftIso: dimension shifting in every positive degree,Hⁱ⁺¹(G, M) ≅ Hⁱ(G, Coind_1^G M ⧸ M)fori ≥ 1and the canonical continuous cohomology, inverse to the connecting map.
Main statements #
TauCeti.ContCohomology.subsingleton_H1_discreteCoind_botandsubsingleton_H2_discreteCoind_bot: acyclicity ofCoind_1^G Ain degrees one and two, for profiniteG.TauCeti.ContCohomology.isIso_coindShortExact_bot_delta: the connecting mapHⁱ(G, Coind_1^G M ⧸ M) ⟶ Hⁱ⁺¹(G, M)is an isomorphism fori ≥ 1, for compactG.
Implementation notes #
Compactness of G makes the actions on Coind_1^G M and on Coind_1^G M ⧸ M continuous. Total
disconnectedness supplies the T1 property making the trivial subgroup closed, as
required by the available Shapiro isomorphisms; the acyclicity and the two shifts use both
profinite hypotheses.
References #
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.3.7) and the
dimension-shifting argument following it; (1.6.4) for Shapiro's lemma, with the footnote on p. 61
recording that NSW writes
Indfor the coinduced module used here. - L. Ribes, P. Zalesskii, Profinite Groups, Thm. 6.10.5 and Cor. 6.10.6.
Acyclicity of Coind_1^G A #
Coind_1^G A has vanishing H¹, for a profinite group G: Shapiro's lemma identifies
H¹(G, Coind_1^G A) with H¹(1, A).
Coind_1^G A has vanishing H², for a profinite group G: Shapiro's lemma identifies
H²(G, Coind_1^G A) with H²(1, A).
Dimension shifting #
Dimension shifting from degree two to degree one, H¹(G, Coind_1^G M ⧸ M) ≅ H²(G, M),
for a profinite group G: the connecting map δ¹ of
TauCeti.ContCohomology.coindShortExact G ⊥ M is bijective because Coind_1^G M is acyclic.
Equations
Instances For
The dimension-shifting isomorphism H¹(G, Coind_1^G M ⧸ M) ≃ H²(G, M) is the connecting map
δ¹.
Dimension shifting from degree one to degree zero, for a profinite group G: H¹(G, M) is
the cokernel of H⁰(G, Coind_1^G M) → H⁰(G, Coind_1^G M ⧸ M), through the connecting map δ⁰,
which is surjective because Coind_1^G M has vanishing H¹.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The dimension-shifting isomorphism onto H¹(G, M) sends the class of x ∈ H⁰(G, Coind_1^G M ⧸ M) to δ⁰ x.
Dimension shifting in every degree #
The connecting map of the dimension-shifting sequence is an isomorphism in every positive
degree: δ : Hⁱ(G, Coind_1^G M ⧸ M) ⟶ Hⁱ⁺¹(G, M) for i ≥ 1 and a compact group G, because
Coind_1^G M is acyclic in degrees i and i + 1.
Dimension shifting in every positive degree, Hⁱ⁺¹(G, M) ≅ Hⁱ(G, Coind_1^G M ⧸ M) for
i ≥ 1 and a compact group G, as an isomorphism of Mathlib's canonical continuous cohomology. Its
inverse is the connecting map of TauCeti.ContCohomology.coindShortExact G ⊥ M
(dimensionShiftIso_inv), an isomorphism by isIso_coindShortExact_bot_delta. The analogous
statement on the explicit low-degree model, for a profinite G and in the direction of the
connecting map, is TauCeti.ContCohomology.explicitDimensionShift1 : H¹(G, Coind_1^G M ⧸ M) ≃+ H²(G, M).
Equations
Instances For
The inverse of the dimension-shifting isomorphism is the connecting map.