Tate cohomology along an isomorphism of finite groups #
Mathlib's Tate cohomology of a finite group is functorial in the coefficient representation, but
the group is fixed throughout. This file supplies the missing variance in the group for the case
of an isomorphism. A compatible pair consists of a group isomorphism e : G ≃* H and a
linear map φ between the coefficient modules of M : Rep R G and N : Rep R H satisfying
φ ∘ ρ g = σ (e g) ∘ φ,
which is Mathlib's Representation.IsIntertwiningMap M.ρ (N.ρ.comp e) φ; the general
representation-theoretic API of such a map lives in
TauCeti.RepresentationTheory.Rep.ChangeOfGroup.
Such a pair induces a map of Tate complexes, hence a map
tateCohomology M n ⟶ tateCohomology N n in every integer degree, and that map is an
isomorphism as soon as φ is.
The construction connects the two halves of the Tate complex: on the chain half it is Mathlib's
groupHomology.chainsMap along e, on the cochain half it is groupCohomology.cochainsMap
along e.symm, and the two agree on the Tate norm because e permutes the group, so the norm
∑ g, ρ g is carried to ∑ h, σ h. In the degrees where Mathlib identifies Tate cohomology
with ordinary group cohomology or homology, the construction is the ordinary change-of-group map
of that theory.
The main application is conjugation: for an element of a group acting on a normal layer of a class formation, conjugation is an isomorphism of finite Galois groups covered by an isomorphism of coefficient modules, and the class-formation axioms compare the invariants of a layer with the invariants of its conjugate through the resulting map in degree two.
Main definitions #
TauCeti.TateCohomology.complexMap: the induced map of Tate complexes.TauCeti.TateCohomology.map: the induced map in a single integer degree.TauCeti.TateCohomology.mapIso: the induced isomorphism, forφa linear equivalence.TauCeti.TateCohomology.negSuccIso: Mathlib's identification of Tate cohomology in degree-(n+1)with group homology in degreen, as an isomorphism of the two modules.TauCeti.TateCohomology.resIso: the packaged natural isomorphismRes(e) ⋙ tateCohomologyFunctor n ≅ tateCohomologyFunctor n.
Main results #
TauCeti.TateCohomology.complexMap_refl: along the identity isomorphism the construction is Mathlib's coefficient functoriality.TauCeti.TateCohomology.map_idandTauCeti.TateCohomology.map_comp: functoriality in the compatible pair.TauCeti.TateCohomology.map_comp_isoGroupCohomology_hom: in positive degrees the construction isgroupCohomology.mapalonge.symm.TauCeti.TateCohomology.map_comp_isoGroupHomology_hom: in degrees at most-2it isgroupHomology.mapalonge;TauCeti.TateCohomology.map_comp_negSuccIso_homrestates this throughTauCeti.TateCohomology.negSuccIso, whichTauCeti.TateCohomology.negSuccIso_homidentifies with Mathlib's comparison.TauCeti.TateCohomology.map_comp_H0IsoNormQuotient_hom: in degree zero the construction is the map induced on the quotient of invariants by the norm image.TauCeti.TateCohomology.HNegOneπ_comp_map: in degree-1the construction sends the class of a norm-zero element to the class of its image (TauCeti.TateCohomology.mapKerNorm).TauCeti.TateCohomology.H0π_comp_tateCohomologyFunctor_map: in degree zero, Mathlib's coefficient functoriality sends the class of an invariant to the class of its image.TauCeti.TateCohomology.tateCohomologyFunctor_map_comp_mapandTauCeti.TateCohomology.δ_comp_map: the construction is natural in the coefficients and commutes with the connecting maps of short exact sequences.TauCeti.TateCohomology.tateCohomologyFunctor_map_comp_map_res: every compatible pair factors as a morphism into the restriction of its target followed by the pairRes(e)(N) → N.
References #
- E. Artin and J. Tate, Class Field Theory, Chapter XIV, §4.
- J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, Chapter I, §5.
The square joining the chain half of the Tate complex to its cochain half commutes for a
compatible pair: this is IsIntertwiningMap.comp_norm in degree zero.
The map of Tate complexes attached to a compatible pair. On the chain half it is
groupHomology.chainsMap along e, on the cochain half groupCohomology.cochainsMap along
e.symm.
Equations
- TauCeti.TateCohomology.complexMap hφ = (tateComplexConnectData M).map (tateComplexConnectData N) (groupHomology.chainsMap (↑e) hφ.toRes) (groupCohomology.cochainsMap (↑e.symm) hφ.ofRes) ⋯
Instances For
In degree zero, the map of Tate complexes is the degree-zero component of
groupCohomology.cochainsMap along e.symm.
In degree -1, the map of Tate complexes is the degree-zero component of
groupHomology.chainsMap along e.
Under the identification groupCohomology.cochainsIso₀ of the degree-zero term of the Tate
complex with the coefficient module, the degree-zero component of the map of Tate complexes becomes
φ.
Under the identification groupCohomology.cochainsIso₀ of the degree-zero term of the Tate
complex with the coefficient module, the degree-zero component of the map of Tate complexes becomes
φ.
Under the identification groupHomology.chainsIso₀ of the degree -1 term of the Tate complex
with the coefficient module, the degree -1 component of the map of Tate complexes becomes φ.
Under the identification groupHomology.chainsIso₀ of the degree -1 term of the Tate complex
with the coefficient module, the degree -1 component of the map of Tate complexes becomes φ.
The map of Tate complexes depends only on the compatible pair, not on the compatibility proof.
Along the identity isomorphism the construction is Mathlib's coefficient functoriality.
The construction is functorial in the compatible pair.
The construction is functorial in the compatible pair.
The isomorphism of Tate complexes attached to a compatible pair whose linear part is an equivalence.
Equations
- TauCeti.TateCohomology.complexMapIso he = { hom := TauCeti.TateCohomology.complexMap he, inv := TauCeti.TateCohomology.complexMap ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Tate cohomology along a compatible pair, in a single integer degree.
Equations
Instances For
TauCeti.TateCohomology.map is the homology map of complexMap. This records the body of
map, whose definition is not exported.
Tate cohomology along a compatible pair whose linear part is an equivalence is an isomorphism in every integer degree.
Equations
Instances For
Degree zero #
A compatible pair carries invariants to invariants.
Equations
Instances For
The map on norm quotients induced by a compatible pair.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map on norm quotients sends the class of an invariant to the class of its image.
Under the identifications H0CyclesIso of the degree-zero cycles of the Tate complexes of M
and N with the invariants, the map that complexMap induces on degree-zero cycles is
mapInvariants, the restriction of φ to the invariants.
Under the identifications H0CyclesIso of the degree-zero cycles of the Tate complexes of M
and N with the invariants, the map that complexMap induces on degree-zero cycles is
mapInvariants, the restriction of φ to the invariants.
The degree-zero Tate map sends the class of an invariant to the class of its image under the compatible coefficient map.
The degree-zero Tate map sends the class of an invariant to the class of its image under the compatible coefficient map.
The degree-zero Tate map sends the class of an invariant to the class of its image under the compatible coefficient map.
In degree zero, the map attached to a compatible pair is the induced map on the quotient of invariants by the norm image.
Degree minus one #
A compatible pair carries norm-zero elements to norm-zero elements.
Equations
- TauCeti.TateCohomology.mapKerNorm hφ = LinearMap.codRestrict (LinearMap.ker N.ρ.norm) (φ ∘ₗ (LinearMap.ker M.ρ.norm).subtype) ⋯
Instances For
Under the identifications HNegOneCyclesIso of the degree -1 cycles of the Tate complexes of
M and N with the kernels of the norms, the map that complexMap induces on degree -1 cycles
is mapKerNorm, the restriction of φ to the elements of norm zero.
Under the identifications HNegOneCyclesIso of the degree -1 cycles of the Tate complexes of
M and N with the kernels of the norms, the map that complexMap induces on degree -1 cycles
is mapKerNorm, the restriction of φ to the elements of norm zero.
The degree -1 Tate map sends the class of a norm-zero element to the class of its image
under the compatible coefficient map.
The degree -1 Tate map sends the class of a norm-zero element to the class of its image
under the compatible coefficient map.
The degree -1 Tate map sends the class of a norm-zero element to the class of its image
under the compatible coefficient map.
Tate cohomology in a fixed degree depends only on the compatible pair.
Along the identity isomorphism, Tate cohomology of a compatible pair is Mathlib's coefficient functoriality.
Tate cohomology is functorial in the compatible pair, in every degree.
Tate cohomology is functorial in the compatible pair, in every degree.
In positive degrees the construction is the ordinary cohomological change-of-group map
along e.symm, read through Mathlib's comparison between Tate and group cohomology.
In degrees at most -2 the construction is the ordinary homological change-of-group map
along e, read through Mathlib's comparison between Tate cohomology and group homology.
Tate cohomology in degree -(n+1), for n > 0, is group homology in degree n: the
component at M of Mathlib's comparison TateCohomology.isoGroupHomology.
Equations
- TauCeti.TateCohomology.negSuccIso M n = (TateCohomology.isoGroupHomology (Int.negSucc n) n ⋯).app M
Instances For
TauCeti.TateCohomology.negSuccIso is the component at M of Mathlib's comparison
TateCohomology.isoGroupHomology.
In degrees -(n+1) with n > 0 the construction is the ordinary homological
change-of-group map along e, read through TauCeti.TateCohomology.negSuccIso.
In degrees -(n+1) with n > 0 the construction is the ordinary homological
change-of-group map along e, read through TauCeti.TateCohomology.negSuccIso.
Naturality in the coefficients and the connecting maps #
The map of Tate complexes of a compatible pair is natural in the coefficients: if
morphisms f : M ⟶ M' and f' : N ⟶ N' commute with the linear parts of compatible pairs
M → N and M' → N', the induced square of Tate complexes commutes.
Tate cohomology of a compatible pair is natural in the coefficients, in every degree.
Tate cohomology of a compatible pair is natural in the coefficients, in every degree.
Restricting the coefficients along an isomorphism of finite groups does not change Tate cohomology, naturally in the coefficients.
Equations
- TauCeti.TateCohomology.resIso e n = CategoryTheory.NatIso.ofComponents (fun (N : Rep R H) => TauCeti.TateCohomology.mapIso ⋯ n) ⋯
Instances For
Tate cohomology groups matched by a compatible pair whose linear part is an equivalence have the same cardinality.
In degree zero, the map induced by a morphism of representations of one finite group sends the class of an invariant to the class of its image.
In degree zero, the map induced by a morphism of representations of one finite group sends the class of an invariant to the class of its image.
In degree zero, the map induced by a morphism of representations of one finite group sends the class of an invariant to the class of its image.
Connecting maps #
Tate cohomology of compatible pairs commutes with the connecting maps. Compatible pairs
between the terms of a short exact sequence S of G-representations and those of a short exact
sequence S' of H-representations, whose linear parts commute with the maps of the two
sequences, intertwine the connecting maps of S and S' in every degree.
A compatible pair factors through the restriction of its target: Tate cohomology of the
pair (e, φ) is the coefficient map induced by a morphism f : M ⟶ Res(e)(N) with linear part φ,
followed by Tate cohomology of the pair Res(e)(N) → N.