The canonical Shapiro map in every degree #
For a compact group G, a subgroup U and a discrete U-module A, the coinduced module
Coind_U^G A of TauCeti.DiscreteCoind comes with the compatible pair consisting of the inclusion
U ↪ G and the counit Coind_U^G A → A, evaluation at 1. Mathlib's functoriality of continuous
cohomology in compatible pairs turns it into a cochain map
TauCeti.ContinuousCohomology.shapiroCochainMap of homogeneous cochain complexes, and so into a
map in every degree,
Hⁿ(G, Coind_U^G A) ⟶ Hⁿ(U, A),
the canonical Shapiro map TauCeti.ContinuousCohomology.shapiroMap. It is restriction to U
followed by the coefficient map of the counit, and Shapiro's lemma is the statement that it is
bijective. This file defines the map on the canonical carrier and proves three things about it:
- in degrees
0,1and2it is carried by the comparison isomorphisms of the explicit low-degree model to the explicit Shapiro mapsTauCeti.ContCohomology.explicitShapiro0,explicitShapiroMap1andexplicitShapiroMap2, so it is bijective there for a closed subgroup of a profinite group; - it is natural in the coefficient module: for a
U-equivariant homomorphismA → Bof discreteU-modules, the coefficient maps of the homomorphism and of its coinduction toGcommute with the Shapiro maps ofAandB; - it commutes with the connecting maps of the long exact sequence: for a short exact sequence of
discrete
U-modules and its coinduction toG, the square of Shapiro maps and connecting maps commutes in every degree.
Shapiro's lemma in every degree follows from the low-degree bijectivity and the commuting square
with the connecting maps by induction on the degree, given
the acyclicity of Coind_1^G A in every positive degree: for n ≥ 1 the connecting maps
Hⁿ(-, Q) → Hⁿ⁺¹(-, A) of 0 → A → Coind_1^U A → Q → 0 and of its coinduction to G are then
bijective (in degree 0 they are only surjective, since H⁰ of the middle term need not vanish),
transitivity of coinduction identifies Coind_U^G (Coind_1^U A) with Coind_1^G A, and the
commuting square carries bijectivity of the Shapiro map in degree n ≥ 1 to bijectivity in degree
n + 1. The degrees 0 and 1 proved here directly are the base cases of this induction, which is
carried out in TauCeti.RepresentationTheory.Homological.ContCohomology.Shapiro.AllDegrees.
Main definitions #
TauCeti.ContinuousCohomology.shapiroCochainMap: the cochain mapσ ↦ ev₁ ∘ σ ∘ ιfrom the homogeneous cochains ofGwith coefficientsCoind_U^G Ato those ofUwith coefficientsA.TauCeti.ContinuousCohomology.shapiroMap: the canonical Shapiro mapHⁿ(G, Coind_U^G A) ⟶ Hⁿ(U, A)inTopModuleCat ℤ, the mapshapiroCochainMapinduces on homology.
Main results #
TauCeti.ContinuousCohomology.shapiroMap_eq_res_comp_coeffMap: the Shapiro map is restriction followed by the coefficient map of the counit.TauCeti.ContinuousCohomology.shapiroMap_naturality: the Shapiro map is natural in the coefficient module.TauCeti.ContinuousCohomology.explicitH0Iso_shapiroMap,TauCeti.ContinuousCohomology.explicitH1AddEquivContinuousCohomology_shapiroMap,TauCeti.ContinuousCohomology.explicitH2AddEquivContinuousCohomology_shapiroMap: agreement with the explicit Shapiro maps in degrees0,1and2under the comparison isomorphisms.TauCeti.ContinuousCohomology.bijective_shapiroMap_zero,TauCeti.ContinuousCohomology.bijective_shapiroMap_one,TauCeti.ContinuousCohomology.bijective_shapiroMap_two: Shapiro's lemma on the canonical carrier in degrees0,1and2, for a closed subgroup of a profinite group.TauCeti.ContCohomology.DiscreteShortExact.delta_shapiroMap: the Shapiro maps commute with the connecting maps.
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. - L. Ribes, P. Zalesskii, Profinite Groups, Thm. 6.10.5.
The Shapiro cochain map: the map of homogeneous cochain complexes induced by the
compatible pair of the inclusion ι : U ↪ G and the counit ev₁ : Coind_U^G A → A, evaluation at
1, sending a homogeneous cochain σ of G with coefficients Coind_U^G A to the homogeneous
cochain ev₁ ∘ σ ∘ ι of U with coefficients A. Its map on homology is the canonical Shapiro
map (homologyMap_shapiroCochainMap). For a closed subgroup of a profinite group it is a
quasi-isomorphism (TauCeti.ContinuousCohomology.quasiIso_shapiroCochainMap), but in general
not an isomorphism of complexes: a degree-0 homogeneous cochain is determined by its value at
1, so for the discrete group G of order 2, U = ⊥ and A = ZMod 2 the degree-0 terms
have orders 4 and 2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Shapiro cochain map is Mathlib's cochain map of the compatible pair of the inclusion and the counit.
The canonical Shapiro map Hⁿ(G, Coind_U^G A) ⟶ Hⁿ(U, A) in every degree: the map on
continuous cohomology induced by the compatible pair of the inclusion U ↪ G and the counit
Coind_U^G A → A, evaluation at 1, that is, the map shapiroCochainMap induces on homology.
It is defined for any topological group G and any subgroup U; Shapiro's lemma is the
statement that it is bijective, proved here in degree 0 in this generality
(bijective_shapiroMap_zero) and in degrees at most 2 for a closed subgroup of a profinite
group (bijective_shapiroMap_of_le_two).
Equations
Instances For
The canonical Shapiro map is the map induced on homology by the Shapiro cochain map.
The canonical Shapiro map is the compatible-pair map of the inclusion and the counit.
The Shapiro map is restriction followed by the counit: restrict from G to U, then apply
the coefficient map induced by evaluation at 1. The two sides compose because the restriction of
the canonical object of a discrete G-module to U is the canonical object of the same module
over U (TauCeti.res_ofDiscreteModule).
The Shapiro map is natural in the coefficient module: for a U-equivariant homomorphism
f : A → B of discrete U-modules, the coefficient map of its coinduction
Coind_U^G A → Coind_U^G B followed by the Shapiro map of B is the Shapiro map of A followed by
the coefficient map of f. The coinduced homomorphism is the one
TauCeti.ContCohomology.DiscreteShortExact.coind applies to the maps of a short exact sequence.
The Shapiro map is natural in the coefficient module: for a U-equivariant homomorphism
f : A → B of discrete U-modules, the coefficient map of its coinduction
Coind_U^G A → Coind_U^G B followed by the Shapiro map of B is the Shapiro map of A followed by
the coefficient map of f. The coinduced homomorphism is the one
TauCeti.ContCohomology.DiscreteShortExact.coind applies to the maps of a short exact sequence.
Degree zero #
In degree zero the canonical Shapiro map is the explicit one, H⁰(G, Coind_U^G A) ≃+ H⁰(U, A)
by evaluation at 1, under the comparisons with the canonical carrier.
Shapiro's lemma in degree zero on the canonical carrier: the canonical Shapiro map
H⁰(G, Coind_U^G A) ⟶ H⁰(U, A) is bijective. No closedness of U is needed in this degree.
Degrees one and two #
In degree one the canonical Shapiro map is the explicit forward Shapiro map
TauCeti.ContCohomology.explicitShapiroMap1 under the comparisons with the canonical carrier.
In degree two the canonical Shapiro map is the explicit forward Shapiro map
TauCeti.ContCohomology.explicitShapiroMap2 under the comparisons with the canonical carrier.
Shapiro's lemma in degree one on the canonical carrier: for a closed subgroup U of a
profinite group G, the canonical Shapiro map H¹(G, Coind_U^G A) ⟶ H¹(U, A) is bijective.
Shapiro's lemma in degree two on the canonical carrier: for a closed subgroup U of a
profinite group G, the canonical Shapiro map H²(G, Coind_U^G A) ⟶ H²(U, A) is bijective.
Shapiro's lemma in degrees at most two on the canonical carrier, in one statement: for a
closed subgroup U of a profinite group G and n ≤ 2, the canonical Shapiro map
Hⁿ(G, Coind_U^G A) ⟶ Hⁿ(U, A) is bijective.
Compatibility with the connecting maps #
The Shapiro maps commute with the connecting maps. For a short exact sequence
0 → A → B → C → 0 of discrete U-modules and its coinduction
0 → Coind A → Coind B → Coind C → 0 to G, the square
Hⁿ(G, Coind_U^G C) ---δ---> Hⁿ⁺¹(G, Coind_U^G A)
| |
shapiroMap shapiroMap
v v
Hⁿ(U, C) ----------δ--------> Hⁿ⁺¹(U, A)
commutes in every degree. This is the naturality of the connecting map in the compatible pair of
the inclusion and the counit; once the middle terms are acyclic in every positive degree, it is
the step that carries bijectivity of the Shapiro map from degree n ≥ 1 to degree n + 1 (both
connecting maps are then bijective; in degree 0 they are only surjective, so the degrees 0 and
1 are separate base cases). The connecting map of U needs U compact, which follows from its
closedness in the compact group G.
The Shapiro maps commute with the connecting maps. For a short exact sequence
0 → A → B → C → 0 of discrete U-modules and its coinduction
0 → Coind A → Coind B → Coind C → 0 to G, the square
Hⁿ(G, Coind_U^G C) ---δ---> Hⁿ⁺¹(G, Coind_U^G A)
| |
shapiroMap shapiroMap
v v
Hⁿ(U, C) ----------δ--------> Hⁿ⁺¹(U, A)
commutes in every degree. This is the naturality of the connecting map in the compatible pair of
the inclusion and the counit; once the middle terms are acyclic in every positive degree, it is
the step that carries bijectivity of the Shapiro map from degree n ≥ 1 to degree n + 1 (both
connecting maps are then bijective; in degree 0 they are only surjective, so the degrees 0 and
1 are separate base cases). The connecting map of U needs U compact, which follows from its
closedness in the compact group G.