Shapiro's lemma in degrees zero, one and two #
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),
H²(G, Coind_U^G A) ≅ H²(U, A).
All three isomorphisms are evaluation at 1 composed with restriction to U, so in degrees one
and two the forward map is the compatible-pair pullback TauCeti.ContCohomology.explicitMap1,
respectively explicitMap2, 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 a 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.
Degree two is the same argument written in the homogeneous form of
TauCeti/RepresentationTheory/Homological/ContCohomology/Homogeneous.lean, which is what makes it
manageable: TauCeti.ContCohomology.coindCochain2 sends a continuous 2-cocycle c of U to
(a (g, h)) y = homogeneous2 c (w y) (w (y * g)) (w (y * g * h)),
the homogeneous form of c read at the three points y, y g, y g h of G pushed into U by
w. Its cocycle identity is the four-term homogeneous relation
TauCeti.ContCohomology.homogeneous2_add_eq_add, and the comparison of a cocycle with the cochain
rebuilt from its Shapiro image is the pointwise prism identity
TauCeti.ContCohomology.homogeneous2_sub_comp applied along w. Here the factorization is
required to be
normalized, w 1 = 1, which TauCeti.exists_continuous_rightCosetFactorization supplies: the
Shapiro image of the rebuilt cochain is then c on the nose
(TauCeti.ContCohomology.shapiroCocycles2_coindCocycle2), where a factorization with w 1 = s
would return the conjugate of c by s instead. Local constancy of both cochains in their group
arguments is uniform local constancy of the underlying function on the compact groups G × G and
G × G × G (TauCeti.exists_isOpen_forall_mul_right_eq).
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).TauCeti.ContCohomology.shapiroCocycles2andTauCeti.ContCohomology.explicitShapiroMap2: the forward Shapiro map on continuous2-cocycles and onH².TauCeti.ContCohomology.coindCochain2andTauCeti.ContCohomology.coindCocycle2: the inverse cochain in degree two, built from a normalized continuous right-coset factorization.TauCeti.ContCohomology.explicitShapiro2: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. Degrees one and two are 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.
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
The coinduced function constCoind G a is constant with value a.
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 degree-zero Shapiro map evaluates a G-invariant coinduced function at 1.
The inverse degree-zero Shapiro map sends a ∈ A^U to the constant function with value a.
The degree-zero Shapiro isomorphism is the compatible-pair pullback along the inclusion
U ↪ G and evaluation at 1, like the forward Shapiro maps in degrees one and two.
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 lift shapiroLift w c is y ↦ c (w y).
The lift of a continuous cochain along a continuous factorization is continuous.
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 Shapiro map on 1-cocycles restricts a cocycle f to U and evaluates at 1: u ↦ f u 1.
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 sends g to the function x ↦ c (w (x * g)) - c (w x).
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 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 underlying cochain of the inverse Shapiro 1-cocycle is coindCochain1.
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 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 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
explicitShapiro1 is the forward Shapiro map explicitShapiroMap1 on H¹.
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.
The homogeneous form of a 2-cochain with coinduced coefficients, evaluated at 1, recovers
the cochain along the three points y, y g, y g h.
At a point of U the homogeneous form of a 2-cochain with coinduced coefficients is
evaluated at 1 by the defining equivariance. This is the shape in which its continuity is
read off.
The forward Shapiro map on continuous 2-cocycles: restrict a continuous 2-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 Shapiro map on 2-cocycles restricts a cocycle f to U × U and evaluates at 1: (u, v) ↦ f (u, v) 1.
The Shapiro image has the restricted homogeneous form. Read at points of U and evaluated
at 1, the homogeneous form of a continuous 2-cocycle of G with coinduced coefficients is the
homogeneous form of its Shapiro image.
The inverse Shapiro cochain in degree two. From a continuous 2-cochain c of U and a
continuous factorization w of G over the right cosets of U, the 2-cochain of G with
coefficients in Coind_U^G A whose value at (g, h) is the function
y ↦ homogeneous2 c (w y) (w (y * g)) (w (y * g * h)): the homogeneous form of c read at the
three points y, y g, y g h of G pushed into U by w.
Equations
- TauCeti.ContCohomology.coindCochain2 w c hw hwmul hccont q = TauCeti.DiscreteCoind.mk G U A (fun (y : G) => TauCeti.ContCohomology.homogeneous2 c (w y) (w (y * q.1)) (w (y * q.1 * q.2))) ⋯ ⋯
Instances For
The inverse Shapiro 2-cochain sends (g, h) to the function y ↦ homogeneous2 c (w y) (w (y * g)) (w (y * g * h)).
The inverse Shapiro cochain satisfies the 2-cocycle identity: at each y it is the
four-term homogeneous relation for c at the four points w y, w (y g), w (y g h),
w (y g h j).
The inverse Shapiro cochain is a continuous 2-cocycle: local constancy in (g, h) is
uniform local constancy of the homogeneous form of c read through w, on the compact group
G × G × G.
The inverse Shapiro cochain, as a continuous 2-cocycle.
Equations
- TauCeti.ContCohomology.coindCocycle2 w c hw hwmul hccont hccoc = ⟨TauCeti.ContCohomology.coindCochain2 w c hw hwmul hccont, ⋯⟩
Instances For
The underlying cochain of the inverse Shapiro 2-cocycle is coindCochain2.
The Shapiro image of the inverse cochain is the cocycle it was built from. Unlike degree
one there is no correction term: a normalized factorization is the identity on U, so the three
points read by the inverse cochain at y = 1 are 1, u₁ and u₁ u₂.
The inverse Shapiro cochain of a 2-coboundary of U is a 2-coboundary of G, with the
primitive y ↦ homogeneous1 α (w y) (w (y * g)) built from a primitive α of c. This is what
makes the inverse construction descend to cohomology.
Every continuous 2-cocycle of G is rebuilt from its Shapiro image, up to the explicit
coboundary whose primitive is the comparison function of
TauCeti.ContCohomology.homogeneous2_sub_comp along w, evaluated at 1. With
TauCeti.ContCohomology.shapiroCocycles2_coindCocycle2 this is what makes the Shapiro map
bijective.
The forward Shapiro map on H², the compatible-pair pullback along the inclusion U ↪ G
and evaluation at 1. TauCeti.ContCohomology.explicitShapiro2 upgrades it to an
isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward Shapiro map on H² is the compatible-pair pullback along the inclusion U ↪ G and
the counit Coind_U^G A → A; this is how it is compared with the canonical map.
The characteristic property of the forward Shapiro map on H²: it sends the class of a
continuous 2-cocycle to the class of its Shapiro image. Together with
TauCeti.ContCohomology.shapiroCocycles2_apply this determines the map, so consumers never need
to unfold it.
The forward Shapiro map in degree two is bijective, which is Shapiro's lemma. Surjectivity
is TauCeti.ContCohomology.shapiroCocycles2_coindCocycle2 and injectivity combines
TauCeti.ContCohomology.sub_coindCochain2_mem_B2 with
TauCeti.ContCohomology.coindCochain2_mem_B2_of_mem_B2; 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 two, 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
explicitShapiro2 is the forward Shapiro map explicitShapiroMap2 on H².
The inverse of the degree-two Shapiro isomorphism is the section formula, for every continuous
right-coset factorization of G over U. For a normalized factorization the formula is exact on
cocycles; an arbitrary factorization gives the same cohomology class by
TauCeti.ContCohomology.sub_coindCochain2_mem_B2.