The coinduced module as a discrete G-module #
For a topological group G, a subgroup U and a U-module A, the coinduced module
Coind_U^G A of TauCeti.coind is an additive subgroup of G → A. This file carries it as a
discrete G-module, TauCeti.DiscreteCoind G U A: the same additive group with the discrete
topology imposed. It is the coefficient object of the explicit low-degree continuous cohomology,
and the one Shapiro's lemma is stated against.
Main definitions #
TauCeti.DiscreteCoind:Coind_U^G Awith the discrete topology, identified withTauCeti.coindbyTauCeti.DiscreteCoind.toCoind;TauCeti.DiscreteCoind.mkbuilds an element from a locally constantU-equivariant function;TauCeti.DiscreteCoind.evalandTauCeti.DiscreteCoind.evalLinear: evaluation at1, the counit of coinduction;TauCeti.DiscreteCoind.map: the linear map induced by aU-equivariant linear map of coefficients;TauCeti.DiscreteCoind.traceandTauCeti.DiscreteCoind.traceLinear: for finite-indexU, the traceTauCeti.coindTraceon the discrete carrier, as aG-equivariant additive map and as a linear map;TauCeti.DiscreteCoind.unit: for a discreteG-moduleM, the unitM → Coind_U^G Mof coinduction,m ↦ (g ↦ g • m), as aG-equivariant additive map;TauCeti.DiscreteCoind.single: for an open subgroupU, the coinduced functionsingle hU g asupported on the right cosetU * gwith valueaatg, additive ina; its values aresingle_apply_mulandsingle_apply_of_notMem, andsingle_mulandsmul_singlemove its base point alongUand under the right-translation action ofG;TauCeti.DiscreteCoind.conj: forg : GandV ≤ gUg⁻¹, theG-equivariant conjugation mapCoind_U^G M → Coind_V^G M,f ↦ (x ↦ g • f (g⁻¹ x)).
Main results #
TauCeti.DiscreteCoind.instContinuousSMul: for compactGthe right-translation action on the discrete carrier is continuous, soCoind_U^G Ais a discreteG-module;TauCeti.DiscreteCoind.smul_eq_self_of_forall_smul_eq_self: a normal subgroupUacting trivially onAacts trivially onCoind_U^G A;TauCeti.DiscreteCoind.instContinuousSMulScalar: for compactGand discrete coefficients, scalar multiplication is continuous;TauCeti.DiscreteCoind.unit_injectiveandTauCeti.DiscreteCoind.map_unit: the unit is injective (a section of the counit) and natural in the coefficients;TauCeti.DiscreteCoind.trace_apply,TauCeti.DiscreteCoind.trace_eq_sum_transversalandTauCeti.DiscreteCoind.trace_map: the trace formula, along any transversal, and its naturality in the coefficients;TauCeti.DiscreteCoind.eval_unitandTauCeti.DiscreteCoind.trace_unit: evaluation at1retracts the unit, and the trace of the unit is multiplication by the index[G : U];TauCeti.DiscreteCoind.trace_map_single: the trace of the coinduction of an equivariant mapf : A → Mapplied tosingle hU g aisg⁻¹ • f a;TauCeti.DiscreteCoind.trace_conj: forV = gUg⁻¹, conjugation commutes with the traces;TauCeti.DiscreteCoind.ofContinuousMapandTauCeti.DiscreteCoind.toContinuousMap: a continuous map into a discrete group as an element ofCoind_1^G A, and conversely, packaged as the additive equivalenceTauCeti.DiscreteCoind.addEquivContinuousMap : Coind_1^G A ≃+ C(G, A), withTauCeti.DiscreteCoind.smul_ofContinuousMapcomputing the translation action.
Coind_U^G A as a discrete G-module: the additive group TauCeti.coind carrying the
discrete topology.
The topology is imposed, not inherited. Viewed as an AddSubgroup of G → A the coinduced module
inherits the pointwise topology, in which a basic neighbourhood constrains only finitely many
values and therefore does not isolate a locally constant function; that is the same trap
TauCeti.ContCohomology.DiscreteH1 records for the low-degree cohomology quotients. The
coefficients of continuous cohomology are discrete modules, and
TauCeti.isOpen_stabilizer_coind is exactly the statement that the right-translation action is
continuous for the discrete topology once G is compact
(TauCeti.DiscreteCoind.instContinuousSMul). TauCeti.DiscreteCoind.toCoind keeps the
computations on representatives available.
The body is @[expose]d because every carrier instance below transports one from
TauCeti.coind along it, and an exposed instance may only be built from exposed definitions.
Equations
- TauCeti.DiscreteCoind G U A = ↥(TauCeti.coind G U A)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
The additive equivalence between the discrete carrier and the coinduced subgroup: the identity
on elements, so that a computation performed on the underlying function transfers unchanged. The
body is @[expose]d because the coercion to a function below is defined through it.
Equations
- TauCeti.DiscreteCoind.toCoind G U A = AddEquiv.refl (TauCeti.DiscreteCoind G U A)
Instances For
Equations
- TauCeti.DiscreteCoind.instFunLike = { coe := fun (f : TauCeti.DiscreteCoind G U A) => ↑((TauCeti.DiscreteCoind.toCoind G U A) f), coe_injective := ⋯ }
The underlying function of an element of Coind_U^G A lies in TauCeti.coind.
An element of Coind_U^G A is locally constant.
The defining equivariance f (u * g) = u • f g.
Equivariance at an element of U, in simp-normal form.
An element of Coind_U^G A from a locally constant U-equivariant function. The body is
@[expose]d so that TauCeti.DiscreteCoind.coe_mk recovers the function it was built from.
Equations
- TauCeti.DiscreteCoind.mk G U A f hlc heq = (TauCeti.DiscreteCoind.toCoind G U A).symm ⟨f, ⋯⟩
Instances For
The zero is pointwise, so that Mathlib's sum_apply applies.
The addition is pointwise, so that Mathlib's sum_apply applies.
The ℕ-action is pointwise, so that Mathlib's FunLike.coe_smul and smul_apply apply.
A natural number killing A kills Coind_U^G A.
Equations
The scalar module structure on the discrete carrier. Its scalar action is instSMulScalar
itself, so that instances stated for that action, such as instSMulCommClass, apply to the module
structure at instance transparency.
Equations
- TauCeti.DiscreteCoind.instModuleScalar = { toSMul := TauCeti.DiscreteCoind.instSMulScalar, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }
Evaluation at 1 on the discrete carrier, the counit of coinduction.
Equations
- TauCeti.DiscreteCoind.eval G U A = (TauCeti.coindEval G U).comp (TauCeti.DiscreteCoind.toCoind G U A).toAddMonoidHom
Instances For
Evaluation at 1 is continuous, the source being discrete.
Evaluation at a point is continuous, the source being discrete.
Equations
- TauCeti.DiscreteCoind.instDistribMulAction = { smul := TauCeti.DiscreteCoind.instDistribMulAction._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }
A G-invariant element of Coind_U^G A is a constant function: its value at x is its value
at 1, because x • f = f evaluated at 1 reads f x = f 1.
The counit is U-equivariant for the restriction of the right-translation action. This is the
compatible-pair hypothesis Shapiro's lemma is an instance of.
The G-stabilizer of an element of Coind_U^G A is its right-translation stabilizer.
A normal subgroup acting trivially on A acts trivially on Coind_U^G A: for u ∈ U and
x : G, (u • f) x = f ((x u x⁻¹) x) = (x u x⁻¹) • f x = f x, since x u x⁻¹ ∈ U.
The scalar orbit map r ↦ r • f of a discrete coinduced element is continuous when the group
G is compact and the coefficient module is discrete. Together these orbit maps give the
ContinuousSMul R (DiscreteCoind G U A) instance below.
Coinduction of a U-equivariant linear map, acting pointwise on locally constant functions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Coinduction of a coefficient map commutes with the right-translation action.
Composing the maps of coinduced functions induced by two equivariant linear maps gives the map induced by their composite.
Evaluation at 1 as a linear map, the counit of linear coinduction.
Equations
- TauCeti.DiscreteCoind.evalLinear G U A R = { toAddHom := ↑(TauCeti.DiscreteCoind.eval G U A), map_smul' := ⋯ }
Instances For
The G-equivariant additive trace DiscreteCoind G U M →+[G] M.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The discrete-carrier trace is the unbundled trace after forgetting the discrete topology.
The discrete-carrier trace computed along an arbitrary transversal.
The discrete-carrier trace is natural in G-equivariant linear coefficient maps.
The trace is continuous, the source being discrete.
The trace on the discrete carrier as an R-linear map.
Equations
- TauCeti.DiscreteCoind.traceLinear G U M R = { toAddHom := ↑(TauCeti.DiscreteCoind.trace G U M).toAddMonoidHom, map_smul' := ⋯ }
Instances For
The unit M → Coind_U^G M of coinduction, sending m to its orbit map g ↦ g • m, which
is locally constant because the action is continuous and M is discrete. It is G-equivariant for
the right-translation action on Coind_U^G M, and evaluation at 1 retracts it
(TauCeti.DiscreteCoind.eval_unit); it is the unit of the adjunction between restriction to U
and coinduction, whose counit is TauCeti.DiscreteCoind.eval.
Equations
- TauCeti.DiscreteCoind.unit G U M = { toFun := fun (m : M) => TauCeti.DiscreteCoind.mk G U M (fun (g : G) => g • m) ⋯ ⋯, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The unit sends m to its orbit map: unit m g = g • m.
Evaluation at 1 retracts the unit.
The unit is injective, being retracted by evaluation at 1.
The unit is natural in the coefficient module: for a G-equivariant linear map
f : M → N of discrete G-modules, coinducing f carries the orbit map of m to the orbit map
of f m. The U-equivariance TauCeti.DiscreteCoind.map asks for is the restriction of the
G-equivariance hf.
The trace of the unit is multiplication by the index: ∑_{gU} g • g⁻¹ • m = [G : U] • m.
The coinduced function supported on one right coset. For an open subgroup U, g : G and
a : A, single hU g a is the element of Coind_U^G A that is u • a at u * g for u : U
and 0 off the right coset U * g (single_apply_mul, single_apply_of_notMem). It is
additive in a, and for a subgroup of finite index every coinduced function is the sum of its
singles over a right transversal (TauCeti.DiscreteCoind.sum_single): these are the functions
through which Coind_U^G A is a direct sum of [G : U] copies of A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
single hU g a takes the value u • a at u * g. Not a simp lemma: simp already proves
it from TauCeti.DiscreteCoind.apply_mul and TauCeti.DiscreteCoind.single_apply_self.
single hU g a takes the value a at g.
single hU g a vanishes off the right coset U * g.
Moving the base point of a single along U twists its value: single (u * g) a is
single g (u⁻¹ • a).
Right translation moves the support of a single: g' • single g a = single (g * g'⁻¹) a.
The trace of a coinduced single: for a U-equivariant linear map f : A → M into a
G-module, the trace of the coinduction of f applied to single hU g a is g⁻¹ • f a. Only the
coset of g⁻¹ contributes to the trace.
Coind_U^G A is a discrete G-module over a compact group: the right-translation action
on the discrete carrier is continuous, because a locally constant function on a compact group is
uniformly locally constant.
Conjugation of coinduced modules #
Conjugation of coinduced modules. For g : G and a subgroup V ≤ gUg⁻¹, the map
Coind_U^G M → Coind_V^G M sending f to x ↦ g • f (g⁻¹ x). It is G-equivariant for the
right-translation actions, and for V = gUg⁻¹ it commutes with the traces (trace_conj).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conjugation map sends f to x ↦ g • f (g⁻¹ x).
Conjugation of coinduced modules commutes with the traces: for V = gUg⁻¹, the trace of
Coind_V^G M after conjugation by g is the trace of Coind_U^G M. Right multiplication by
g⁻¹ carries the cosets of U to those of V, and carries the term of the coset xU in one sum
to the term of the coset x g⁻¹ V in the other.
The coinduced module of the trivial subgroup #
A continuous map from G to a discrete group A, as an element of Coind_1^G A: it is
locally constant, and the equivariance condition for the trivial subgroup is empty.
Equations
- TauCeti.DiscreteCoind.ofContinuousMap G A f = TauCeti.DiscreteCoind.mk G ⊥ A ⇑f ⋯ ⋯
Instances For
An element of Coind_1^G A, as a continuous map G → A: it is locally constant, and A is
discrete.
Equations
- TauCeti.DiscreteCoind.toContinuousMap G A f = { toFun := ⇑f, continuous_toFun := ⋯ }
Instances For
Coind_1^G A is the group of continuous maps G → A: the locally constant maps into the
discrete group A are the continuous ones, and the equivariance condition for the trivial
subgroup is empty.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Right translation on Coind_1^G A is precomposition with right multiplication.