Shapiro's lemma in degrees zero and one #
For a profinite group G, a closed subgroup U and a discrete U-module A, the coinduced
module Coind_U^G A of TauCeti.DiscreteCoind computes the cohomology of U:
H⁰(G, Coind_U^G A) ≅ H⁰(U, A), H¹(G, Coind_U^G A) ≅ H¹(U, A).
Both isomorphisms are evaluation at 1 composed with restriction to U, so in degree one the
forward map is the compatible-pair pullback TauCeti.ContCohomology.explicitMap1 along the pair
consisting of the inclusion U ↪ G and the counit TauCeti.DiscreteCoind.eval; nothing about it
depends on a choice. The choice enters only in proving that this map is bijective, and what it uses
is Layer 0's continuous section of G → G ⧸ U
(TauCeti.exists_continuous_rightCosetFactorization, Ribes-Zalesskii Prop. 2.2.2): writing
g = w g * r g with w : G → U continuous and w (u * g) = u * w g, a continuous 1-cocycle
c of U is spread over G as
(a g) x = c (w (x * g)) - c (w x),
which is TauCeti.ContCohomology.coindCochain1. This is a continuous 1-cocycle of G with
values in Coind_U^G A whose Shapiro image is c up to the explicit coboundary d⁰ (c (w 1))
(TauCeti.ContCohomology.shapiroCocycles1_coindCocycle1), and conversely every continuous
1-cocycle f of G differs from the cochain rebuilt from its Shapiro image by an explicit
coboundary (TauCeti.ContCohomology.sub_coindCochain1_mem_B1). Those two identities make the
forward map bijective, and because the isomorphism is pinned by its forward direction the section
formula for the inverse (TauCeti.ContCohomology.explicitShapiro1_symm_apply) holds for every
such factorization, so there is no separate independence statement to prove.
Main definitions #
TauCeti.ContCohomology.constCoindandTauCeti.ContCohomology.explicitShapiro0: the constant coinduced element at aU-invariant coefficient, andH⁰(G, Coind_U^G A) ≃+ H⁰(U, A).TauCeti.ContCohomology.shapiroCocycles1andTauCeti.ContCohomology.explicitShapiroMap1: the forward Shapiro map on continuous1-cocycles and onH¹.TauCeti.ContCohomology.shapiroLift,TauCeti.ContCohomology.coindCochain1andTauCeti.ContCohomology.coindCocycle1: the inverse cochain built from a continuous right-coset factorization.TauCeti.ContCohomology.explicitShapiro1:H¹(G, Coind_U^G A) ≃+ H¹(U, A).
Implementation notes #
Degree zero needs no topological hypothesis beyond a continuous multiplication on G: a
G-invariant element of the coinduced module is constant, and the constant it takes is
U-invariant. Degree one is where profiniteness and closedness of U are used, through the
continuous factorization; for an open U the finite transversal Quotient.out would already
suffice, but openness is not assumed anywhere here.
This is the degree-0 and degree-1 part of the "Shapiro's lemma" milestone of Layer 7 of the
human-authored roadmap at TauCetiRoadmap/ProfiniteCohomology/README.md, whose Suggested.lean
fixes the names explicitShapiro0 and explicitShapiro1, and whose §5 fixes the direction of the
isomorphism — that of Mathlib's discrete groupCohomology.coindIso — and the forward map.
References #
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.6.4). Note the
terminology trap flagged in the footnote on p. 61: NSW writes
Indfor what is here the coinduced functor. - L. Ribes, P. Zalesskii, Profinite Groups, Thm. 6.10.5, which uses
Coindby that name.
The constant function at a U-invariant coefficient, as an element of Coind_U^G A. It is
the inverse of the degree-zero Shapiro map.
Equations
- TauCeti.ContCohomology.constCoind G a = TauCeti.DiscreteCoind.mk G U A (fun (x : G) => ↑a) ⋯ ⋯
Instances For
A G-invariant element of Coind_U^G A is a constant function: right translation moves 1
to every point of G.
The constant coinduced element is G-invariant.
Shapiro's lemma in degree zero, H⁰(G, Coind_U^G A) ≅ H⁰(U, A), by evaluation at 1.
A G-invariant element of the coinduced module is constant and the constant it takes is
U-invariant; conversely a U-invariant a : A is TauCeti.ContCohomology.constCoind. Only
continuity of the multiplication on G is used: neither compactness of G nor closedness of U
enters in this degree.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The 0-cochain y ↦ c (w y) transporting a 1-cocycle c of U along a factorization w
of G over the right cosets of U. Its failure of U-equivariance is c itself
(TauCeti.ContCohomology.shapiroLift_mul), which is why its right-translation differences carry a
nonzero class.
Equations
- TauCeti.ContCohomology.shapiroLift w c y = c (w y)
Instances For
The failure of U-equivariance of the lift of a 1-cocycle is the cocycle itself.
Evaluation at 1 is a compatible coefficient map for the inclusion U ↪ G: this is the
hypothesis of TauCeti.ContCohomology.explicitMap1 that the Shapiro map is the instance of. It is
a named theorem rather than an inline use of TauCeti.DiscreteCoind.eval_smul because the
inclusion has to be spelled as ContinuousMonoidHom.subgroupSubtype.
The forward Shapiro map on continuous 1-cocycles: restrict a continuous 1-cocycle of
G with coefficients in Coind_U^G A to U, and evaluate its values at 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward Shapiro map on H¹, the compatible-pair pullback along the inclusion U ↪ G
and evaluation at 1. TauCeti.ContCohomology.explicitShapiro1 upgrades it to an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse Shapiro cochain in degree one. From a continuous 1-cocycle c of U and a
continuous factorization w of G over the right cosets of U, the 1-cochain of G with
coefficients in Coind_U^G A whose value at g is the right-translation difference
x ↦ c (w (x * g)) - c (w x) of TauCeti.ContCohomology.shapiroLift.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse Shapiro cochain is a continuous 1-cocycle. It is locally constant because the
lift is uniformly locally constant on the compact group G
(TauCeti.isOpen_rightTranslationStabilizer), and the cocycle identity is the telescoping of its
right-translation differences.
The inverse Shapiro cochain, as a continuous 1-cocycle.
Equations
- TauCeti.ContCohomology.coindCocycle1 w c hw hwmul hccont hccoc = ⟨TauCeti.ContCohomology.coindCochain1 w c hw hwmul hccont hccoc, ⋯⟩
Instances For
The Shapiro image of the inverse cochain is the cocycle it was built from, up to the
explicit coboundary of c (w 1). That correction term is what makes a normalisation w 1 = 1
unnecessary: it is a coboundary whatever the factorization does at 1.
The inverse Shapiro cochain of a 1-coboundary of U is a 1-coboundary of G, with the
primitive x ↦ w x • α in Coind_U^G A. This is what makes the inverse construction descend to
cohomology.
Every continuous 1-cocycle of G is rebuilt from its Shapiro image, up to the explicit
coboundary whose primitive is y ↦ (f y) 1 - c (w y), where c is the Shapiro image of f. With
TauCeti.ContCohomology.shapiroCocycles1_coindCocycle1 this is what makes the Shapiro map
bijective.
The forward Shapiro map in degree one is bijective, which is Shapiro's lemma. Surjectivity
is TauCeti.ContCohomology.shapiroCocycles1_coindCocycle1 and injectivity combines
TauCeti.ContCohomology.sub_coindCochain1_mem_B1 with
TauCeti.ContCohomology.coindCochain1_mem_B1_of_mem_B1; both run on a continuous right-coset
factorization, which is where closedness of U and profiniteness of G are used.
Shapiro's lemma in degree one, H¹(G, Coind_U^G A) ≅ H¹(U, A), for a profinite G and a
closed subgroup U. The forward map is restriction to U followed by evaluation at 1, and it
involves no choice; the continuous section of G → G ⧸ U is used only to prove it bijective.
Equations
Instances For
The inverse of the Shapiro isomorphism is the section formula, for every continuous
right-coset factorization of G over U. Since the equivalence is pinned by its forward
direction, independence of the factorization needs no separate proof.