Change of group in positive Tate degrees #
Let φ : G →* Q be a homomorphism of finite groups, M a representation of Q, N a
representation of G and f : Res_φ M ⟶ N a morphism of G-representations. Ordinary group
cohomology has the change-of-group map groupCohomology.map φ f n : Hⁿ(Q, M) ⟶ Hⁿ(G, N). In
positive degrees Mathlib identifies Tate cohomology with ordinary cohomology, and this file
transports the change-of-group map across that identification as TauCeti.TateCohomology.posMap.
Positive-degree restriction to a subgroup (TauCeti.TateCohomology.posRes: φ the inclusion,
f the identity) and inflation from a quotient (TauCeti.TateCohomology.infl: φ the quotient
map, f the inclusion of invariants) are both of this form. In degree zero there is no such map
in general: for a surjective φ the norm of G on Res_φ M is |ker φ| times the norm of Q,
so a norm of Q need not be a norm of G, and the quotient of invariants by norms does not map
along the identity of invariants.
The change-of-group map is natural in both coefficient representations (posMap_comp_map,
map_comp_posMap), and it commutes with the connecting maps of short exact sequences
(δ_comp_posMap). The degree-zero source of a connecting map is a quotient of the ordinary
invariants, so the compatibility is stated on ordinary cohomology classes through the comparison
Rep.fromGroupCohomology, which also covers the connecting map from degree zero to degree one
(fromGroupCohomology_δ_comp_posMap). This is what allows a statement about change of group to
be moved across degrees by dimension shifting, as in the compatibility of the Tate cup product
with inflation.
For integral coefficients, change of group along the identity of ℤ carries the connecting class
δχ ∈ H²(Q, ℤ) of a character χ of Q to the connecting class of its pullback χ ∘ φ to G
(posMap_characterConnectingClass). For φ a quotient map this is the compatibility of δχ
with inflation.
Main definitions #
TauCeti.TateCohomology.posMap: the change-of-group map in a positive Tate degree.
Main results #
TauCeti.TateCohomology.fromGroupCohomology_comp_posMap: through the comparison with ordinary cohomology,posMapisgroupCohomology.map.TauCeti.TateCohomology.posMap_comp_map,TauCeti.TateCohomology.map_comp_posMap: naturality in the two coefficient representations.TauCeti.TateCohomology.posMap_id,TauCeti.TateCohomology.posMap_comp: functoriality in the group homomorphism.TauCeti.TateCohomology.fromGroupCohomology_δ_comp_posMap,TauCeti.TateCohomology.δ_comp_posMap: compatibility with connecting maps.TauCeti.TateCohomology.posMap_characterConnectingClass: change of group carries the connecting class of a character to the connecting class of its pullback.
References #
- K. S. Brown, Cohomology of Groups, Chapter III, §8 and Chapter VI, §5.
- E. Artin and J. Tate, Class Field Theory, Chapter XIV, §4.
Change of group in a positive Tate degree. For φ : G →* Q and a morphism
f : Res_φ M ⟶ N, this is the ordinary change-of-group map groupCohomology.map φ f n read
through Mathlib's identification TateCohomology.isoGroupCohomology of Tate cohomology with
ordinary cohomology in degree n ≠ 0. On a cochain it is c ↦ (g₁, …, gₙ) ↦ f (c (φ g₁, …, φ gₙ)).
Instances For
Positive-degree change of group is ordinary change of group between Mathlib's comparisons of Tate with ordinary cohomology.
Positive-degree change of group, read through the comparison with ordinary cohomology, is the ordinary change-of-group map.
Positive-degree change of group, read through the comparison with ordinary cohomology, is the ordinary change-of-group map.
Through the comparison Rep.fromGroupCohomology of ordinary with Tate cohomology,
positive-degree change of group is the ordinary change-of-group map.
Through the comparison Rep.fromGroupCohomology of ordinary with Tate cohomology,
positive-degree change of group is the ordinary change-of-group map.
Positive-degree change of group followed by a map of G-representations is change of group
along the composite coefficient map.
Positive-degree change of group followed by a map of G-representations is change of group
along the composite coefficient map.
A map of Q-representations followed by positive-degree change of group is change of group
along the composite coefficient map.
A map of Q-representations followed by positive-degree change of group is change of group
along the composite coefficient map.
Change of group along the identity homomorphism with the identity coefficient map is the identity.
Change of group is transitive. For ψ : H →* G and φ : G →* Q, changing the group
along φ with f : Res_φ M ⟶ N and then along ψ with g : Res_ψ N ⟶ L is change of group
along φ.comp ψ with the composite coefficient map Res_ψ f ≫ g.
Change of group is transitive. For ψ : H →* G and φ : G →* Q, changing the group
along φ with f : Res_φ M ⟶ N and then along ψ with g : Res_ψ N ⟶ L is change of group
along φ.comp ψ with the composite coefficient map Res_ψ f ≫ g.
Change of group commutes with connecting maps, from degree zero on. Let S be a short
exact sequence of Q-representations, S' one of G-representations and Φ : Res_φ S ⟶ S'.
On an ordinary cohomology class z of S.X₃ in degree n, changing the group of the Tate
connecting image of z gives the Tate connecting image of the changed class. In degree zero the
class z is an invariant of S.X₃, and its Tate class is its image in the norm quotient.
Change of group commutes with connecting maps, from degree zero on. Let S be a short
exact sequence of Q-representations, S' one of G-representations and Φ : Res_φ S ⟶ S'.
On an ordinary cohomology class z of S.X₃ in degree n, changing the group of the Tate
connecting image of z gives the Tate connecting image of the changed class. In degree zero the
class z is an invariant of S.X₃, and its Tate class is its image in the norm quotient.
Change of group commutes with connecting maps in positive degrees. For short exact
sequences S of Q-representations and S' of G-representations and a morphism
Φ : Res_φ S ⟶ S', the connecting maps Hⁿ(Q, S.X₃) ⟶ Hⁿ⁺¹(Q, S.X₁) and
Hⁿ(G, S'.X₃) ⟶ Hⁿ⁺¹(G, S'.X₁) commute with change of group along Φ, for n ≠ 0.
Change of group commutes with connecting maps in positive degrees. For short exact
sequences S of Q-representations and S' of G-representations and a morphism
Φ : Res_φ S ⟶ S', the connecting maps Hⁿ(Q, S.X₃) ⟶ Hⁿ⁺¹(Q, S.X₁) and
Hⁿ(G, S'.X₃) ⟶ Hⁿ⁺¹(G, S'.X₁) commute with change of group along Φ, for n ≠ 0.
The connecting class of a character #
Change of group of the connecting class of a character. Let φ : G →* Q and let
f : Res_φ ℤ ⟶ ℤ be the identity of the integers. Changing the group along φ and f carries
the connecting class δχ ∈ H²(Q, ℤ) of a character χ : Qᵃᵇ → ℚ/ℤ to the connecting class of
the pulled-back character χ ∘ φᵃᵇ : Gᵃᵇ → ℚ/ℤ. For a quotient map φ this says that inflation
of δχ is δ of the inflated character.