Shapiro's lemma for inflated induced representations #
Let G be a profinite group, V an open normal subgroup, C a subgroup of the finite quotient
G ⧸ V and U = π⁻¹(C) its preimage in G, an open subgroup. A representation B of C inflates
to a smooth discrete representation of U (comapInflation), and the representation
Ind_C^{G ⧸ V} B of the finite quotient inflates to one of G. This file proves that
Hⁿ(G, Inf Ind_C^{G ⧸ V} B) ≅ Hⁿ(U, Inf B)
in every degree (indInflationShapiroIso): the finite-index comparison identifies induction with
coinduction, inflation commutes with coinduction (coindInflationIso:
precomposition with G → G ⧸ V identifies the C-equivariant functions G ⧸ V → B with the
locally constant U-equivariant functions G → B), and continuous Shapiro's lemma
shapiroIsoTopRep computes the cohomology of the coinduced module. The comparison of induction
with coinduction is Amelia Livingston's Rep.indCoindIso in Mathlib.
For a local field K and a finite Galois extension L/K cut out by V, this is the step of the
dévissage of the local Euler characteristic that replaces an induced module Ind_C^{Gal(L/K)} B by
the module B over the fixed field of C.
Main definitions #
comapInflation: the inflation of a representation ofC ≤ G ⧸ Vto the preimage ofC.comapInflationLinearEquiv: the inflation has the underlying module of the representation.coindInflationIso:Inf Coind_C^{G ⧸ V} B ≅ Coind_U^G Inf B.indInflationIso:Inf Ind_C^{G ⧸ V} B ≅ Coind_U^G Inf B.indInflationShapiroIso:Hⁿ(G, Inf Ind_C^{G ⧸ V} B) ≅ Hⁿ(U, Inf B).
Implementation notes #
Mathlib's Rep.indCoindIso requires the coefficient universe to contain that of the ring, and
shapiroIsoTopRep requires it to be the universe of the group, so for a ring R : Type v the
Shapiro isomorphism takes G : Type (max u v) and coefficients in Type (max u v). In this file
the universe levels of indInflationIso and indInflationShapiroIso are given explicitly:
elaborating max ?u ?v =?= max u v otherwise times out. The inflation comapInflation only
needs R to be a ring; the comparison of inflation with coinduction needs it to be commutative,
as Mathlib's Rep.coind does.
References #
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.6.4), and the proof of (7.3.1).
- J. S. Milne, Arithmetic Duality Theorems, 2nd ed., I, proof of Theorem 2.8.
The inflation of a representation B of a subgroup C of the quotient G ⧸ V to the
preimage of C in G, with the discrete topology. It is smooth because V is open. Its
underlying module is identified with that of B by comapInflationLinearEquiv.
Instances For
The inflation is the discrete representation of C restricted along π⁻¹(C) → C.
Inflation does not change the underlying module: the identification of the underlying module
of the inflation with that of B.
Instances For
An element of the preimage of C acts on the inflation through its image in C.
An element of the preimage of C acts on the inflation through its image in C, transported
along the inverse identification.
Inflation commutes with coinduction: precomposition with the quotient map G → G ⧸ V
identifies Coind_C^{G ⧸ V} B with the locally constant functions G → B equivariant for the
preimage of C.
Instances For
The comparison precomposes a coinduced function with the quotient map.
The inverse comparison descends a coinduced function along the quotient map.
The inflation of a discrete representation of G ⧸ V is discrete.
The inflation of Coind_C^{G ⧸ V} B to G is the coinduction to G of the inflation of B
to the preimage of C.
Instances For
The comparison acts on underlying functions as coindInflationEquiv, by precomposition with
the quotient map.
The inverse comparison acts on underlying functions as the inverse of coindInflationEquiv,
by descent along the quotient map.
The inflation of Ind_C^{G ⧸ V} B to G is the coinduction to G of the inflation of B to
the preimage of C: Mathlib's finite-index comparison Rep.indCoindIso followed by
coindInflationIso.
Instances For
The comparison indInflationIso is Mathlib's finite-index comparison, inflated, followed by
coindInflationIso.
Shapiro's lemma for inflated induced representations. For an open normal subgroup V of
a profinite group G, a subgroup C of G ⧸ V and a representation B of C, the cohomology of
G with coefficients in the inflation of Ind_C^{G ⧸ V} B is the cohomology of the preimage of
C with coefficients in the inflation of B.
Instances For
The Shapiro isomorphism for inflated induced representations is the coefficient map of
indInflationIso followed by the canonical Shapiro map: restriction to the preimage of C and
evaluation at 1.
The inflation of Ind_C^{G ⧸ V} B to G and the inflation of B to the preimage of C have
cohomology groups of the same cardinality.