Shapiro's lemma in every degree #
For a closed subgroup U of a profinite group G and a discrete U-module A, the canonical
Shapiro map TauCeti.ContinuousCohomology.shapiroMap,
Hⁿ(G, Coind_U^G A) ⟶ Hⁿ(U, A),
is an isomorphism in every degree n. This is Shapiro's lemma for Mathlib's canonical
continuous cohomology; the isomorphism is TauCeti.ContinuousCohomology.shapiroIso. On the level
of complexes, it says that the Shapiro cochain map TauCeti.ContinuousCohomology.shapiroCochainMap,
of which shapiroMap is the map on homology, is a quasi-isomorphism. In general the two complexes
are not isomorphic at all (already their degree-0 terms differ in size for the discrete group
G of order 2, U = ⊥ and A = ZMod 2); only the maps induced on cohomology are isomorphisms.
The degrees 0 and 1 are the base cases, where the canonical map agrees with the explicit
low-degree Shapiro isomorphisms (TauCeti.ContinuousCohomology.bijective_shapiroMap_of_le_two).
The step from degree n + 1 to degree n + 2 is dimension shifting. The short exact sequence
0 → A → Coind_1^U A → Q → 0 of TauCeti.ContCohomology.coindShortExact U ⊥ A, with
Q = Coind_1^U A ⧸ A, and its coinduction to G fit into the commuting square
Hⁿ⁺¹(G, Coind_U^G Q) ---δ---> Hⁿ⁺²(G, Coind_U^G A)
| |
shapiroMap shapiroMap
v v
Hⁿ⁺¹(U, Q) ----------δ--------> Hⁿ⁺²(U, A)
of TauCeti.ContCohomology.DiscreteShortExact.delta_shapiroMap. Both connecting maps are
isomorphisms, because both middle terms are acyclic in positive degrees: Coind_1^U A by
TauCeti.ContCohomology.subsingleton_continuousCohomology_discreteCoind_bot_int, and
Coind_U^G (Coind_1^U A) because transitivity of coinduction identifies it with Coind_1^G A
(TauCeti.DiscreteCoind.transIsoBot). The left vertical map is an isomorphism by induction, applied
to the module Q, so the right one is too.
Closedness of U enters through the base cases, which use the explicit Shapiro isomorphisms for a
closed subgroup, and through the coinduction of a short exact sequence, whose surjectivity on the
right needs a closed subgroup.
The last section transfers the result to a smooth discrete A : TopRep R U over an arbitrary ring
R. The generic Shapiro map TauCeti.ContinuousCohomology.shapiroMapTopRep is restriction to U
together with the coinduction counit TauCeti.coindCounit. Forgetting the scalars
(TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntIso) turns it into the canonical
Shapiro map of the underlying discrete U-module, by naturality of scalar restriction under
simultaneous change of group and coefficients
(TauCeti.ContCohomology.map_comp_restrictScalarsIntIso_hom_of_hom). Since the canonical map is
bijective, so is the generic one, and a bijective map between discrete topological modules is an
isomorphism.
Main definitions #
TauCeti.ContinuousCohomology.shapiroIso: Shapiro's lemma in every degree,Hⁿ(G, Coind_U^G A) ≅ Hⁿ(U, A)for a closed subgroupUof a profinite groupG, with forward map the canonical Shapiro map (shapiroIso_hom).TauCeti.ContinuousCohomology.shapiroCochainMapTopRep,TauCeti.ContinuousCohomology.shapiroMapTopRep,TauCeti.ContinuousCohomology.shapiroIsoTopRep: the Shapiro cochain map, the Shapiro map and Shapiro's isomorphism for a smooth discrete representation over an arbitrary ring.
Main results #
TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_discreteCoind_discreteCoind_bot:Coind_U^G (Coind_1^U A)is acyclic in every positive degree.TauCeti.ContinuousCohomology.isIso_shapiroMap,TauCeti.ContinuousCohomology.bijective_shapiroMap: the canonical Shapiro map is an isomorphism, resp. bijective, in every degree.TauCeti.ContinuousCohomology.quasiIso_shapiroCochainMap: equivalently, the Shapiro cochain map is a quasi-isomorphism of homogeneous cochain complexes.TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_discreteCoind_iff:Hⁿ(U, A)vanishes exactly whenHⁿ(G, Coind_U^G A)does.TauCeti.ContinuousCohomology.coeffMap_unit_comp_shapiroMap,TauCeti.ContinuousCohomology.res_comp_shapiroIso_inv: for a discreteG-moduleM, restriction toUis the coefficient map of the unitM → Coind_U^G Mof coinduction followed by the Shapiro map, so restriction followed by the inverse of Shapiro's isomorphism is the coefficient map of the unit.TauCeti.ContinuousCohomology.isIso_shapiroMapTopRep,TauCeti.ContinuousCohomology.quasiIso_shapiroCochainMapTopRep: the generic Shapiro map is an isomorphism in every degree, and the generic Shapiro cochain map a quasi-isomorphism, for a closed subgroup of a profinite group and an arbitrary coefficient ring.
References #
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008),
(1.6.4), with the footnote on p. 61 recording that NSW write
Indfor the coinduced module, and (1.3.7) for the dimension-shifting argument. - L. Ribes, P. Zalesskii, Profinite Groups, Thm. 6.10.5.
- J.-P. Serre, Galois Cohomology, Ch. I, §2.5.
Acyclicity of Coind_U^G (Coind_1^U A) #
Coind_U^G (Coind_1^U A) is acyclic in every positive degree, for a compact group G and
any subgroup U: transitivity of coinduction identifies it with Coind_1^G A, whose
positive-degree cohomology vanishes.
Restriction through the unit of coinduction #
Restriction factors through the unit of coinduction and the Shapiro map: the coefficient
map Hⁿ(G, M) ⟶ Hⁿ(G, Coind_U^G M) of the unit m ↦ (g ↦ g • m), followed by the Shapiro map
Hⁿ(G, Coind_U^G M) ⟶ Hⁿ(U, M), is restriction to U. Evaluation at 1 retracts the unit, and
the Shapiro map is restriction followed by evaluation at 1. This holds for every subgroup U of
every topological group G.
Restriction factors through the unit of coinduction and the Shapiro map: the coefficient
map Hⁿ(G, M) ⟶ Hⁿ(G, Coind_U^G M) of the unit m ↦ (g ↦ g • m), followed by the Shapiro map
Hⁿ(G, Coind_U^G M) ⟶ Hⁿ(U, M), is restriction to U. Evaluation at 1 retracts the unit, and
the Shapiro map is restriction followed by evaluation at 1. This holds for every subgroup U of
every topological group G.
Shapiro's lemma #
Shapiro's lemma in every degree, as an isomorphism of TopModuleCat ℤ: for a closed
subgroup U of a profinite group G and a discrete U-module A, the canonical Shapiro map
Hⁿ(G, Coind_U^G A) ⟶ Hⁿ(U, A) is an isomorphism.
Shapiro's lemma in every degree: for a closed subgroup U of a profinite group G and a
discrete U-module A, the canonical Shapiro map Hⁿ(G, Coind_U^G A) ⟶ Hⁿ(U, A) is bijective.
Shapiro's lemma in every degree, on cochains: for a closed subgroup U of a profinite group
G and a discrete U-module A, the Shapiro cochain map σ ↦ ev₁ ∘ σ ∘ ι from the homogeneous
cochains of G with coefficients Coind_U^G A to those of U with coefficients A is a
quasi-isomorphism.
The Shapiro isomorphism Hⁿ(G, Coind_U^G A) ≅ Hⁿ(U, A) in every degree, for a closed
subgroup U of a profinite group G and a discrete U-module A. Its forward map is the
canonical Shapiro map, restriction to U followed by evaluation at 1 on the coefficients
(shapiroIso_hom, TauCeti.ContinuousCohomology.shapiroMap_eq_res_comp_coeffMap).
Equations
Instances For
The forward map of the Shapiro isomorphism is the canonical Shapiro map.
The inverse of the Shapiro isomorphism followed by the canonical Shapiro map is the identity.
The canonical Shapiro map followed by the inverse of the Shapiro isomorphism is the identity.
Vanishing transfers along Shapiro's lemma: Hⁿ(U, A) vanishes exactly when
Hⁿ(G, Coind_U^G A) does.
Restriction of a discrete G-module M to a closed subgroup U of a profinite group,
followed by the inverse of Shapiro's isomorphism, is the coefficient map of the unit
M → Coind_U^G M of coinduction.
The Shapiro cochain map for a smooth discrete topological representation over any ring: the
cochain map σ ↦ ev₁ ∘ σ ∘ ι of the compatible pair of the inclusion ι : U ↪ G and the
coinduction counit ev₁ (evaluation at 1).
Equations
Instances For
The defining equation of shapiroCochainMapTopRep: Mathlib's cochain map of the inclusion
U → G and the coinduction counit.
The canonical Shapiro map for a smooth discrete topological representation over any ring:
restriction from G to U together with the coinduction counit (evaluation at 1), that is, the
map shapiroCochainMapTopRep induces on homology.
Equations
Instances For
The generic Shapiro map is the map induced on homology by the generic Shapiro cochain map.
The defining equation of shapiroMapTopRep: the compatible-pair map of the inclusion
U → G and the coinduction counit.
The generic Shapiro map is an isomorphism for a closed subgroup of a profinite group.
Shapiro's lemma on cochains for smooth discrete representations over any ring: for a closed
subgroup U of a profinite group G, the generic Shapiro cochain map is a quasi-isomorphism.
Shapiro's lemma for smooth discrete topological representations over any ring.
Equations
Instances For
Applying Shapiro after its inverse returns the original cohomology class.