Restriction, inflation and coefficient maps in continuous cohomology #
Mathlib's ContinuousCohomology.map is functoriality for a compatible pair: a continuous
homomorphism φ : H →ₜ* G together with a morphism f : TopRep.res φ X ⟶ Y induces
Hⁿ(G, X) ⟶ Hⁿ(H, Y). This file names the three instances of that construction which the rest of
the continuous-cohomology theory uses, each with its composition law:
- coefficient maps, at
φ = id, which package the carrier as a functorcontinuousCohomologyFunctor; - restriction along the inclusion of an arbitrary subgroup, carrying the subspace topology;
- inflation along a quotient map
G → G ⧸ Nfor a normal subgroupN, with the invariantsXᴺofTopRep.quotientToInvariantsas coefficients.
Each of the three carries its defining equation — coeffMap_def, res_def and infl_def — which
identifies it with the compatible pair it specialises ContinuousCohomology.map at.
Restriction and inflation are natural in the coefficients, and this is recorded by the two natural
transformations resNatTrans and inflNatTrans, matching the shape of Mathlib's discrete
groupCohomology.resNatTrans and groupCohomology.infNatTrans.
Main definitions #
TauCeti.ContinuousCohomology.coeffMap,TauCeti.ContinuousCohomology.res,TauCeti.ContinuousCohomology.infl: the three named instances ofContinuousCohomology.map.TauCeti.ContinuousCohomology.resLE: restriction along the inclusion of a subgroup into a larger subgroup.TauCeti.ContinuousCohomology.continuousCohomologyFunctor:Hⁿ(G, -)as a functor.TauCeti.ContinuousCohomology.resNatTrans,TauCeti.ContinuousCohomology.inflNatTrans.
Main results #
TauCeti.ContinuousCohomology.resolutionMap_injectiveandTauCeti.ContinuousCohomology.cochainsMap_f_injective: a surjective group map paired with an injective coefficient map induces injective maps on resolutions and homogeneous cochains.TauCeti.ContinuousCohomology.resolutionMap_id_apply_of_comp_eqandTauCeti.ContinuousCohomology.cochainsMap_id_apply_of_comp_eq: elementwise composition of coefficient maps on resolutions and homogeneous cochains.TauCeti.ContinuousCohomology.coeffMap_comp,TauCeti.ContinuousCohomology.res_comp_res,TauCeti.ContinuousCohomology.res_comp_resLE,TauCeti.ContinuousCohomology.resLE_comp_resLEandTauCeti.ContinuousCohomology.infl_comp_infl: the composition laws of the named maps;TauCeti.ContinuousCohomology.resLE_refl: restriction along the identity inclusion is the identity.TauCeti.ContinuousCohomology.coeffMap_comp_res,TauCeti.ContinuousCohomology.coeffMap_comp_resLEandTauCeti.ContinuousCohomology.coeffMap_comp_infl: naturality of restriction and of inflation in the coefficients.TauCeti.ContinuousCohomology.map_comp_coeffMap: the map of a compatible pair is natural in the coefficients, under simultaneous change of group and coefficients.TauCeti.ContinuousCohomology.map_congr: two compatible pairs that agree induce the same map.TauCeti.ContinuousCohomology.iCycles_cocyclesMap_one_applyandTauCeti.ContinuousCohomology.iCycles_cocyclesMap_two_apply: evaluation of mapped homogeneous cocycles in degrees one and two.
A surjective group map and an injective coefficient pair induce injective maps on every term of the coinduced resolutions.
The map on homogeneous cochains induced by a surjective group map and an injective coefficient pair is injective in every degree.
On the coinduced resolutions, the maps induced by two composable coefficient morphisms compose
to the map induced by their composite e, elementwise. This is Mathlib's
ContinuousCohomology.resolutionMap_comp at the identity of G, read on elements; the composite is
passed as e with the equation h because the coefficient morphism of resolutionMap is typed on
TopRep.res id X, where an equation between composites in TopRep k G cannot be rewritten.
On homogeneous cochains, the maps induced by two composable coefficient morphisms compose to
the map induced by their composite e, elementwise: Mathlib's
ContinuousCohomology.cochainsMap_comp at the identity of G, stated as
resolutionMap_id_apply_of_comp_eq is.
Two compatible pairs with equal homomorphisms and equal coefficient maps induce the same map on
continuous cohomology; the continuous counterpart of groupCohomology.map_congr.
A coefficient map: the map on continuous cohomology induced by a morphism of topological
G-representations. It is the instance of ContinuousCohomology.map at φ = id.
Equations
Instances For
The defining equation of coeffMap: it is ContinuousCohomology.map at φ = id.
Coefficient maps preserve identities.
Coefficient maps preserve composition.
Coefficient maps preserve composition.
Naturality of compatible-pair maps in the coefficients: for compatible pairs (φ, f) and
(φ, f') and coefficient morphisms a, b forming a commutative square
res φ a ≫ f' = f ≫ b, the induced maps satisfy map φ f ≫ coeffMap b = coeffMap a ≫ map φ f'.
Naturality of compatible-pair maps in the coefficients: for compatible pairs (φ, f) and
(φ, f') and coefficient morphisms a, b forming a commutative square
res φ a ≫ f' = f ≫ b, the induced maps satisfy map φ f ≫ coeffMap b = coeffMap a ≫ map φ f'.
The n-th continuous cohomology of a topological group G as a functor in the coefficients.
Its action on morphisms is coeffMap; the continuous counterpart of groupCohomology.functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Restriction to a subgroup, the first named instance of ContinuousCohomology.map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defining equation of res: it is ContinuousCohomology.map for the compatible pair
consisting of the inclusion S ↪ G and the identity of the coefficients.
Restriction is natural in the coefficients.
Restriction is natural in the coefficients.
Restriction to a subgroup, as a natural transformation of functors on TopRep R G; the
continuous counterpart of groupCohomology.resNatTrans.
Equations
- TauCeti.ContinuousCohomology.resNatTrans R S n = { app := fun (X : TopRep R G) => TauCeti.ContinuousCohomology.res S X n, naturality := ⋯ }
Instances For
The component at X of the restriction natural transformation is restriction res S X n.
Restricting to S and then to a subgroup T of S is restriction along the composite
inclusion.
Restricting to S and then to a subgroup T of S is restriction along the composite
inclusion.
Restriction along the inclusion of a subgroup H into a larger subgroup S, from the
cohomology of S to that of H; the instance of ContinuousCohomology.map at the inclusion
H ↪ S and the identity of the coefficients, both subgroups carrying the subspace topology.
Equations
Instances For
The defining equation of resLE: it is ContinuousCohomology.map for the compatible pair
consisting of the inclusion H ↪ S and the identity of the coefficients.
Restriction along the inclusion H ↪ S is natural in the coefficients.
Restriction along the inclusion H ↪ S is natural in the coefficients.
Restricting to S and then to a subgroup H ≤ S is restriction to H.
Restricting to S and then to a subgroup H ≤ S is restriction to H.
Restriction along the inclusion of a subgroup into itself is the identity.
Restricting from T to S and then to H, for subgroups H ≤ S ≤ T, is restricting from
T to H: the transition maps of the system of the Hⁿ(S, X) over the subgroups containing H
compose.
Restricting from T to S and then to H, for subgroups H ≤ S ≤ T, is restricting from
T to H: the transition maps of the system of the Hⁿ(S, X) over the subgroups containing H
compose.
Inflation along G → G ⧸ N, the second named instance of ContinuousCohomology.map: the
coefficients on the quotient are the N-invariants Xᴺ, and the compatible pair is the quotient
homomorphism together with the inclusion Xᴺ ↪ X.
Equations
Instances For
The defining equation of infl: it is ContinuousCohomology.map for the compatible pair
consisting of the quotient homomorphism G → G ⧸ N and the inclusion Xᴺ ↪ X.
Inflation is natural in the coefficients.
Inflation is natural in the coefficients.
Inflation, as a natural transformation of functors on TopRep R G; the continuous counterpart
of groupCohomology.infNatTrans.
Equations
- TauCeti.ContinuousCohomology.inflNatTrans R N n = { app := fun (X : TopRep R G) => TauCeti.ContinuousCohomology.infl N X n, naturality := ⋯ }
Instances For
The component at X of the inflation natural transformation is inflation infl N X n.
Inflating from (G ⧸ N) ⧸ P to G ⧸ N and then from G ⧸ N to G is the map induced by the
composite quotient homomorphism together with the composite inclusion (Xᴺ)ᴾ ↪ Xᴺ ↪ X of
coefficients.
Inflating from (G ⧸ N) ⧸ P to G ⧸ N and then from G ⧸ N to G is the map induced by the
composite quotient homomorphism together with the composite inclusion (Xᴺ)ᴾ ↪ Xᴺ ↪ X of
coefficients.
The map induced by a compatible pair on the (i + 1)-st term of the coinduced resolution,
evaluated at a point of H: it is the map induced on the i-th term, applied to the value at the
image point, (F ↦ f ∘ F ∘ φ) read one level down.
The underlying resolution element of the image of a homogeneous cochain under the cochain map of a compatible pair is the image of its underlying element under the resolution map.
The map on continuous cohomology induced by a compatible pair, on the class of a cocycle: it is the class of the image of the cocycle.
The underlying cochain of the image of a cocycle under the cocycle map of a compatible pair is the image of its underlying cochain under the cochain map.
A mapped homogeneous one-cocycle is evaluated by applying the underlying additive coefficient map after precomposing both arguments with the group homomorphism.
A mapped homogeneous two-cocycle is evaluated by applying the underlying additive coefficient map after precomposing all three arguments with the group homomorphism.
A coefficient map along an equality of coefficient objects is the transport along the induced equality of cohomology groups.