Transitivity of low-degree corestriction #
For finite-index open subgroups V ≤ U ≤ G, corestriction is transitive in degrees zero, one,
and two: cor_V^G = cor_U^G ∘ cor_V^U. Degree one requires separately continuous
multiplication, and degree two requires continuous multiplication; neither requires continuous
inversion. Relative corestriction only requires continuity of multiplication and the coefficient
action on the subgroups involved. The tower of coset spaces is organised by Mathlib's
equivalence Subgroup.quotientEquivProdOfLE', which splits G ⧸ V as (G ⧸ U) × (U ⧸ V).
Transitivity is what makes a corestriction computable one step at a time: it may be evaluated
through any chain of intermediate finite-index open subgroups instead of in a single jump from V
to G, and conversely a corestriction from V may be recognised as one from an intermediate U.
Main declarations #
explicitCor0Le,explicitCor1Le,explicitCor2Le: corestriction along a subgroup inclusionV ≤ U, evaluated bycoe_explicitCor0Le,explicitCor1Le_mk, andexplicitCor2Le_mk.explicitCor2Le_explicitMap2_subgroupInclusion: relative corestriction after restriction is multiplication by the relative index[U : V]in degree two.explicitCor0Le_trans: transitivity of relative degree-zero corestriction in a subgroup tower.explicitCor0_trans,explicitCor1_trans,explicitCor2_trans: transitivity from a subgroup to the ambient group in degrees zero, one, and two.
Relative corestriction #
Relative degree-zero corestriction for V ≤ U: identify V with its copy inside U,
then apply degree-zero corestriction there.
Instances For
The underlying coefficient of relative degree-zero corestriction is the norm over the cosets
of V in U, taken along the canonical transversal.
Relative degree-one corestriction for an inclusion V ≤ U with V open in U; the
ambient group U need not be open in G. The source is the cohomology of V itself, transported
to the definitionally different subgroup V.subgroupOf U along Mathlib's topological
identification Subgroup.subgroupOfContinuousMulEquivOfLe, which leaves ambient values -- and
hence the action on M -- unchanged.
Instances For
Relative degree-one corestriction sends the class of a continuous 1-cocycle on V to the
class of the degree-one corestriction cochain of its transport to V.subgroupOf U, taken over the
canonical transversal.
Relative degree-two corestriction for an inclusion V ≤ U with V open in U; the
ambient group U need not be open in G. The source is transported along Mathlib's canonical
topological group isomorphism V.subgroupOf U ≃ₜ* V.
Instances For
Relative degree-two corestriction sends the class of a continuous 2-cocycle on V to the
class of the degree-two corestriction cochain of its transport to V.subgroupOf U, taken over the
canonical transversal.
cor²_V^U ∘ res²_U^V = [U : V] • id on H²(U, M): restricting along the inclusion
V ≤ U and corestricting back multiplies by the relative index.
Transitivity #
Transitivity of degree-zero corestriction. For subgroups V ≤ U ≤ G with V of finite
index in U and U of finite index in G, cor⁰_V^G = cor⁰_U^G ∘ cor⁰_V^U.
Transitivity of relative degree-zero corestriction. For subgroups V ≤ U ≤ W, the
relative corestriction from V to W is the composite of the relative corestrictions through
U.
Transitivity of degree-one corestriction. For open subgroups V ≤ U ≤ G with V of
finite index in U and U of finite index in G, cor¹_V^G = cor¹_U^G ∘ cor¹_V^U.
Transitivity of degree-two corestriction. For open subgroups V ≤ U ≤ G with V of
finite index in U and U of finite index in G, cor²_V^G = cor²_U^G ∘ cor²_V^U.