The coinduced module of a subgroup #
For a topological group G, a subgroup U and a U-module A, the coinduced module
Coind_U^G A = {f : G → A | f locally constant, f (u * g) = u • f g for all u ∈ U, g ∈ G}
carries the right-translation action (g • f) x = f (x * g) of G. It is Milne's M_*
(Arithmetic Duality Theorems, Remark 0.11) and Ribes-Zalesskii's Coind_U^G
(Profinite Groups, Thm. 6.10.5), and it is the coefficient module Shapiro's lemma is stated
against.
This file builds TauCeti.coind, as an additive subgroup of G → A, and the properties Shapiro's
lemma and the dimension-shifting argument consume. The coinduced module is carried as a
discrete G-module by TauCeti.DiscreteCoind in
TauCeti.RepresentationTheory.Homological.ContCohomology.Coinduced.Discrete. It is packaged as a
functor between categories of smooth discrete representations, and compared with Mathlib's
Representation.coind, in
TauCeti.RepresentationTheory.Homological.ContCohomology.Coinduced.Functor.
Main definitions #
TauCeti.coind: the coinduced moduleCoind_U^G A, aG-module under right translation (TauCeti.instDistribMulActionCoind);TauCeti.coindEval: evaluation at1, the counit of coinduction;TauCeti.coindMap: the functoriality of coinduction inAalongU-equivariant additive maps;TauCeti.coindTrace: for finite-indexU, the tracef ↦ ∑ x : G ⧸ U, x • f x⁻¹.
Main results #
TauCeti.isOpen_stabilizer_coind: the right-translation stabilizers are open for compactG, which is exactly what makes the coinduced module a discreteG-module in the sense of a continuous action on a discrete module;TauCeti.coindMap_injective,TauCeti.coindMap_surjectiveandTauCeti.coindMap_range_eq_ker: coinduction is exact inA, sending a short exact sequence of discreteU-modules to a short exact sequence;TauCeti.coindTrace_smulandTauCeti.coindTrace_coindMap: the trace isG-equivariant and natural in the coefficients;TauCeti.mem_coind_bot_iff: membership inCoind_1^G Ais local constancy, so it is the group of all locally constant mapsG → A, the acyclic module of the dimension-shifting argument;TauCeti.coindEvalTopEquiv:Coind_G^G AisA.
Surjectivity is where the topology does real work. Lifting a locally constant U-equivariant map
G → B through a surjection A ↠ B means choosing preimages coherently along the right cosets
U \ G, and the choice has to stay locally constant. The continuous section of G → G ⧸ U
(TauCeti.exists_continuous_section, Ribes-Zalesskii Prop. 2.2.2) supplies it: inverting turns a
continuous section of the left coset space into a continuous choice s' of representatives of
the right cosets, and g ↦ g * (s' g)⁻¹ is then a continuous U-valued cocycle by which the
lift is transported. Discreteness of A and continuity of the U-action are what make the
transported lift locally constant again.
Implementation notes #
Mathlib's ContRepresentation.coindV is an analogous construction in the bundled continuous-
representation language: in this file's notation, a Submodule R C(G, V) attached to a
ContRepresentation R U V and the inclusion U → G. It is not used here because the
ContRepresentation carrier imposes no continuity of the action in the group variable, which is
needed by TauCeti.coindMap_surjective; TauCeti.coindEvalTopEquiv similarly requires continuity
of each orbit map. The discrete coefficient modules here are also given by the unbundled classes
[DistribMulAction U A], [DiscreteTopology A], [ContinuousSMul U A], and local constancy is a
predicate on plain functions rather than a bundled C(G, A).
For finite-index subgroups, Mathlib's algebraic Rep.coindResAdjunction has the trace as its
counit. Its coinduced object consists of all equivariant functions in Rep k G, whereas this file
uses locally constant functions and only identifies the two for an open subgroup of a compact
group (TauCeti.topologicalCoindIsoAlgebraic). Mathlib's element formula is recorded in
Subgroup.coindResAdjunction_counit_app_hom_apply, and
TauCeti.groupCohomology.corestriction builds the corresponding algebraic all-degree
corestriction. Those use the right-coset convention ∑ g, g⁻¹ • f g; the continuous trace here
uses the equivalent left-coset convention ∑ x, x • f x⁻¹. They cannot be reused directly
because their coefficients live in the purely algebraic category Rep k G, while continuous
cohomology uses this file's locally constant coinduction on discrete modules.
The trace construction follows Brown, Cohomology of Groups, III §9.
The coinduced module Coind_U^G A of a subgroup U ≤ G and a U-module A: the locally
constant maps f : G → A with f (u * g) = u • f g for every u : U and g : G. The
G-action is right translation, (g • f) x = f (x * g).
Equations
Instances For
Membership in the coinduced module: local constancy and U-equivariance.
A member of the coinduced module is locally constant.
A member of the coinduced module is U-equivariant.
The equivariance of a bundled element of the coinduced module, in the form simp can use
without a separate membership hypothesis.
Equivariance at an element of U, in simp-normal form.
Pointwise scalar multiplication by a ring commuting with the U-action.
Equations
- TauCeti.instSMulCoindScalar = { smul := fun (r : R) (f : ↥(TauCeti.coind G U A)) => ⟨fun (g : G) => r • ↑f g, ⋯⟩ }
Equations
The coinduced module is closed under right translation.
The right-translation action (g • f) x = f (x * g).
Equations
- TauCeti.instSMulCoind = { smul := fun (g : G) (f : ↥(TauCeti.coind G U A)) => ⟨fun (x : G) => ↑f (x * g), ⋯⟩ }
Equations
- TauCeti.instDistribMulActionCoind = { toSMul := TauCeti.instSMulCoind, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }
The G-stabilizer of a coinduced element is its right-translation stabilizer.
The coinduced module of a compact group is a discrete G-module: every stabilizer of the
right-translation action is open. This is what lets the coinduced module serve as coefficients for
continuous cohomology.
Evaluation at 1, the counit of coinduction: Coind_U^G A →+ A. It is U-equivariant
(TauCeti.coindEval_smul) and natural in A (TauCeti.coindEval_coindMap).
Equations
- TauCeti.coindEval G U = { toFun := fun (f : ↥(TauCeti.coind G U A)) => ↑f 1, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The counit is U-equivariant for the restriction of the right-translation action.
Coinduction is functorial in the coefficients: a U-equivariant additive map φ : A →+ B
induces Coind_U^G A →+ Coind_U^G B by postcomposition.
Equations
- TauCeti.coindMap G U φ hφ = { toFun := fun (f : ↥(TauCeti.coind G U A)) => ⟨fun (g : G) => φ (↑f g), ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Coinduction of the identity is the identity.
The composite of two coinductions is the coinduction of the composite.
The counit is natural in the coefficients.
coindMap is G-equivariant.
The summand x • f x⁻¹ of the trace of a coinduced element, as a function of the coset
x U rather than of x.
Equations
- TauCeti.coindTraceTerm U f x = Quotient.liftOn x (fun (g : G) => g • ↑f g⁻¹) ⋯
Instances For
The summand of the trace, computed at the canonical representative of a coset.
The effect of right translation on a summand of the trace: translating the coinduced element
by g translates the coset index by g⁻¹ and multiplies the summand by g.
The trace of the coinduced module, f ↦ ∑ x : G ⧸ U, x • f x⁻¹. This is the coefficient
map used after Shapiro's isomorphism in the coinduction construction of corestriction.
Equations
- TauCeti.coindTrace G U = { toFun := fun (f : ↥(TauCeti.coind G U M)) => ∑ x : G ⧸ U, TauCeti.coindTraceTerm U f x, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The trace computed along an arbitrary transversal t : G ⧸ U → G.
The trace is G-equivariant for the right-translation action on the coinduced module.
The trace is natural in the coefficient module: a G-equivariant map of coefficients
commutes with it.
The trace of the whole group is evaluation at 1: the only coset is U itself.
Coinduction preserves injectivity. No topological hypothesis is needed.
Coinduction is exact in the middle. If A →+ B →+ C is exact at B with φ injective,
then the coinduced sequence is exact at Coind_U^G B. No topological hypothesis is needed.
Coinduction preserves surjectivity for a closed subgroup U of a profinite group G
and a discrete U-module A with continuous action.
Together with TauCeti.coindMap_injective and TauCeti.coindMap_range_eq_ker this says that
coinduction along a closed subgroup of a profinite group sends a short exact sequence of discrete
U-modules to a short exact sequence of discrete G-modules.
Coind_1^G A is the group of all locally constant maps G → A: for the trivial subgroup
the equivariance condition is vacuous. This is the module the dimension-shifting argument
embeds a discrete module into.
For U = ⊤ and discrete A, a continuous orbit map g ↦ g • a is a member of the coinduced
module.
Coind_G^G A is A for discrete A with continuous orbit maps: evaluation at 1 is an
isomorphism, with inverse a ↦ (g ↦ g • a).
Equations
- One or more equations did not get rendered due to their size.