Corestriction in degrees zero, one and two

For a finite-index subgroup U of a group G acting on an abelian group M, the corestriction attached to a transversal t : G ⧸ U → G is, in the three lowest degrees,

cor⁰_t(m) = ∑ u : G ⧸ U, t u • m,
(cor¹_t f) γ = ∑ u : G ⧸ U, t u • f (ℓᵗ_u γ),
(cor²_t f) (γ, η) = ∑ u : G ⧸ U, t u • f (ℓᵗ_u γ, ℓᵗ_{γ⁻¹ • u} η),

where ℓᵗ_u(γ) = (t u)⁻¹ * γ * t (γ⁻¹ • u) is the transversal word TauCeti.lWord. In degree zero, if m is fixed by U then the sum is fixed by G; in degrees one and two, if f is a cocycle on U then corⁱ_t f is a cocycle on G, and corⁱ_t carries coboundaries to coboundaries. All three therefore descend to additive maps Hⁱ(U, M) → Hⁱ(G, M). The transversal is kept variable until its independence has been proved, and the public maps explicitCor0, explicitCor1 and explicitCor2 then use Quotient.out.

The factor t u • is essential for nontrivial coefficient actions. It is exactly the identity t u * ℓᵗ_u(γ) = γ * t (γ⁻¹ • u) of TauCeti.transversal_mul_lWord that turns the U-cocycle law for f into the G-cocycle law for cor¹_t f; without the action factor the sums are not cocycles. A trivial-action formula that omits it is correct for trivial coefficients and wrong in general.

Degree one is where the two normalizations start to differ from degree zero. Independence of the transversal is no longer an equality of cochains but an explicit coboundary (cochainsCor1_changeTransversal), and cor¹ ∘ res¹ is not the index on cochains either: it differs from it by the coboundary of ∑ u, c (t u) (cochainsCor1_res). Only after passing to cohomology do the clean statements explicitCor1_changeTransversal and explicitCor1_comp_res1 hold. Degree two repeats that pattern with longer correction terms: the two transversals differ by the coboundary of γ ↦ ∑ u, t u • (f (d_u, ℓᵗ'_u γ) - f (ℓᵗ_u γ, d_{γ⁻¹ • u})) (cochainsCor2_changeTransversal), and cor² ∘ res² differs from the index by the coboundary of γ ↦ ∑ u, (c (t u, ℓᵗ_u γ) - c (γ, t u)) (cochainsCor2_res).

Continuity is needed only for the passage from cochains to H¹ and H², and only through openness of U: TauCeti.continuous_lWord makes γ ↦ ℓᵗ_u(γ) continuous for an open U and any map t, and TauCeti.continuous_lWord_inv_smul does the same for the second transversal word of the degree-two sum, whose coset index moves with the first variable. So no continuity is required of the transversal itself.

This is the degree-zero, degree-one and degree-two part of Layer 6 of the Profinite Cohomology roadmap. The degree-zero formulas and proof organization are adapted from the earlier, unmerged degree-zero portion of Tau Ceti PR #4061, which was removed there because the canonical H0 carrier had not yet landed.

Main declarations

• TauCeti.ContCohomology.explicitCor0Transversal: the norm for a variable transversal.
• TauCeti.ContCohomology.explicitCor0_changeTransversal: independence of that transversal.
• TauCeti.ContCohomology.explicitCor0: the canonical degree-zero corestriction.
• TauCeti.ContCohomology.explicitCor0_comp_res0: the normalization cor⁰ ∘ res⁰ = (G : U) • id.
• TauCeti.ContCohomology.cochainsCor1: the degree-one corestriction cochain for a variable transversal, with cochainsCor1_isCocycle₁ and cochainsCor1_mem_B1.
• TauCeti.ContCohomology.cochainsCor1_changeTransversal and TauCeti.ContCohomology.cochainsCor1_res: the two cochain-level correction terms.
• TauCeti.ContCohomology.explicitCor1Transversal and TauCeti.ContCohomology.explicitCor1: degree-one corestriction on H¹, for a variable and for the canonical transversal.
• TauCeti.ContCohomology.explicitCor1_comp_res1: the normalization cor¹ ∘ res¹ = (G : U) • id on H¹.
• TauCeti.ContCohomology.explicitCor1_explicitMap1_id: degree-one corestriction is natural in an equivariant coefficient map.
• TauCeti.ContCohomology.cochainsCor2: the degree-two corestriction cochain for a variable transversal, with cochainsCor2_isCocycle₂ and cochainsCor2_mem_B2.
• TauCeti.ContCohomology.cochainsCor2_changeTransversal and TauCeti.ContCohomology.cochainsCor2_res: the two degree-two cochain-level correction terms.
• TauCeti.ContCohomology.explicitCor2Transversal and TauCeti.ContCohomology.explicitCor2: degree-two corestriction on H², for a variable and for the canonical transversal.
• TauCeti.ContCohomology.explicitCor2_comp_res2: the normalization cor² ∘ res² = (G : U) • id on H².

References

The normalization is Neukirch--Schmidt--Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.7), and Serre, Local Fields, VII §7 Proposition 6. In positive degrees it is an identity of cohomology classes; in degree zero, a cocycle is already an invariant element.

theorem TauCeti.ContCohomology.sum_transversal_smul_mem_H0 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) {m : M} (hm : m ∈ H0 (↥U) M) : ∑ u : G ⧸ U, t u • m ∈ H0 G M

The transversal norm of a U-invariant element is G-invariant.

noncomputable def TauCeti.ContCohomology.explicitCor0Transversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) : ↥(H0 (↥U) M) →+ ↥(H0 G M)

Corestriction in degree zero for a variable transversal, the norm m ↦ ∑ u, t u • m : H⁰(U, M) → H⁰(G, M).

Equations

• TauCeti.ContCohomology.explicitCor0Transversal G M U t ht = { toFun := fun (m : ↥(TauCeti.ContCohomology.H0 (↥U) M)) => ⟨∑ u : G ⧸ U, t u • ↑m, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.ContCohomology.coe_explicitCor0Transversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (m : ↥(H0 (↥U) M)) : ↑((explicitCor0Transversal G M U t ht) m) = ∑ u : G ⧸ U, t u • ↑m

The underlying coefficient of the transversal corestriction is its defining norm sum.

theorem TauCeti.ContCohomology.coe_explicitCor0Transversal_of_smul_eq_self (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (htriv : ∀ (g : G) (m : M), g • m = m) (m : ↥(H0 (↥U) M)) : ↑((explicitCor0Transversal G M U t ht) m) = U.index • ↑m

For a trivial coefficient action, the transversal norm is multiplication by the index.

theorem TauCeti.ContCohomology.map_explicitCor0Transversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) {N : Type w} [AddCommGroup N] [DistribMulAction G N] (f : M →+[G] N) (m : ↥(H0 (↥U) M)) : (explicitCoeff0 G M f) ((explicitCor0Transversal G M U t ht) m) = (explicitCor0Transversal G N U t ht) ((fixedPointsMap f U) m)

Naturality of the transversal norm in an equivariant coefficient homomorphism.

theorem TauCeti.ContCohomology.explicitCor0Transversal_comp_res0 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (m : ↥(H0 G M)) : (explicitCor0Transversal G M U t ht) ((explicitRes0 G M U) m) = U.index • m

cor⁰_t ∘ res⁰ = (G : U) • id for a variable transversal.

theorem TauCeti.ContCohomology.explicitCor0_changeTransversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t t' : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (ht' : ∀ (u : G ⧸ U), ↑(t' u) = u) : explicitCor0Transversal G M U t ht = explicitCor0Transversal G M U t' ht'

Independence of the transversal in degree zero. Two transversals differ by a U-valued factor, which acts trivially on H⁰(U, M), so their norms agree on the nose.

noncomputable def TauCeti.ContCohomology.explicitCor0 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] : ↥(H0 (↥U) M) →+ ↥(H0 G M)

Corestriction in degree zero, the canonical norm m ↦ ∑ u, Quotient.out u • m : H⁰(U, M) → H⁰(G, M).

Equations

• TauCeti.ContCohomology.explicitCor0 G M U = TauCeti.ContCohomology.explicitCor0Transversal G M U Quotient.out ⋯

@[simp]

theorem TauCeti.ContCohomology.coe_explicitCor0 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (m : ↥(H0 (↥U) M)) : ↑((explicitCor0 G M U) m) = ∑ u : G ⧸ U, Quotient.out u • ↑m

The underlying coefficient of canonical degree-zero corestriction is the norm over Quotient.out.

theorem TauCeti.ContCohomology.coe_explicitCor0_of_smul_eq_self (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (htriv : ∀ (g : G) (m : M), g • m = m) (m : ↥(H0 (↥U) M)) : ↑((explicitCor0 G M U) m) = U.index • ↑m

For a trivial coefficient action, canonical degree-zero corestriction is multiplication by the subgroup index.

theorem TauCeti.ContCohomology.explicitCor0_eq_transversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) : explicitCor0 G M U = explicitCor0Transversal G M U t ht

The canonical degree-zero corestriction can be computed using any transversal.

theorem TauCeti.ContCohomology.map_explicitCor0 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] {N : Type w} [AddCommGroup N] [DistribMulAction G N] (f : M →+[G] N) (m : ↥(H0 (↥U) M)) : (explicitCoeff0 G M f) ((explicitCor0 G M U) m) = (explicitCor0 G N U) ((fixedPointsMap f U) m)

Naturality of canonical degree-zero corestriction in an equivariant coefficient homomorphism.

theorem TauCeti.ContCohomology.explicitCor0_comp_res0 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (m : ↥(H0 G M)) : (explicitCor0 G M U) ((explicitRes0 G M U) m) = U.index • m

cor⁰ ∘ res⁰ = (G : U) • id on H⁰(G, M).

The degree-one corestriction cochain

No topology is needed to write cor¹_t down, to check that it carries 1-cocycles to 1-cocycles and 1-coboundaries to 1-coboundaries, or to compare two transversals. Continuity enters only in the next section, where the cochain is pushed to H¹.

noncomputable def TauCeti.ContCohomology.cochainsCor1 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) : (↥U → M) →+ G → M

The degree-one corestriction cochain for a transversal t, (cor¹_t f) γ = ∑ u : G ⧸ U, t u • f (ℓᵗ_u γ), where ℓᵗ is the transversal word TauCeti.lWord, which lands in U by TauCeti.lWord_mem.

Equations

• TauCeti.ContCohomology.cochainsCor1 G M U t ht = { toFun := fun (f : ↥U → M) (γ : G) => ∑ u : G ⧸ U, t u • f ⟨TauCeti.lWord U t u γ, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.ContCohomology.cochainsCor1_apply (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (f : ↥U → M) (γ : G) : (cochainsCor1 G M U t ht) f γ = ∑ u : G ⧸ U, t u • f ⟨lWord U t u γ, ⋯⟩

The defining formula for the degree-one corestriction cochain.

theorem TauCeti.ContCohomology.cochainsCor1_apply_of_smul_eq_self (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (htriv : ∀ (g : G) (m : M), g • m = m) (f : ↥U → M) (γ : G) : (cochainsCor1 G M U t ht) f γ = ∑ u : G ⧸ U, f ⟨lWord U t u γ, ⋯⟩

For a trivial coefficient action the representative factor t u • disappears, and the degree-one corestriction is the plain sum of the values of the cochain on the transversal words.

theorem TauCeti.ContCohomology.map_cochainsCor1 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) {N : Type w} [AddCommGroup N] [DistribMulAction G N] (φ : M →+ N) (hφ : ∀ (g : G) (m : M), φ (g • m) = g • φ m) (f : ↥U → M) (γ : G) : φ ((cochainsCor1 G M U t ht) f γ) = (cochainsCor1 G N U t ht) (fun (x : ↥U) => φ (f x)) γ

Naturality of the degree-one corestriction cochain in an equivariant coefficient homomorphism.

theorem TauCeti.ContCohomology.smul_apply_lWord_of_isCocycle₁ (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) (t : G ⧸ U → G) {c : G → M} (hc : groupCohomology.IsCocycle₁ c) (γ : G) (u : G ⧸ U) : t (γ • u) • c (lWord U t (γ • u) γ) = γ • c (t u) - c (t (γ • u)) + c γ

The 1-cocycle law of a cochain c on G at the factorization t (γ • u) * ℓᵗ_{γ • u}(γ) = γ * t u of TauCeti.transversal_smul_mul_lWord: the value of c at the transversal word ℓᵗ_{γ • u}(γ), translated by t (γ • u), is γ • c (t u) - c (t (γ • u)) + c γ.

theorem TauCeti.ContCohomology.smul_apply_lWord_mul_of_isCocycle₁ (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) {f : ↥U → M} (hf : groupCohomology.IsCocycle₁ f) (γ η : G) (u : G ⧸ U) : t u • f ⟨lWord U t u (γ * η), ⋯⟩ = t u • f ⟨lWord U t u γ, ⋯⟩ + (γ * t (γ⁻¹ • u)) • f ⟨lWord U t (γ⁻¹ • u) η, ⋯⟩

The 1-cocycle law of a cochain f on U at the factorization ℓᵗ_u(γ * η) = ℓᵗ_u(γ) * ℓᵗ_{γ⁻¹ • u}(η) of TauCeti.lWord_mul_lWord, translated by t u: the translated value at ℓᵗ_u(γ * η) is the translated value at ℓᵗ_u(γ) plus the value at ℓᵗ_{γ⁻¹ • u}(η) translated by γ * t (γ⁻¹ • u).

theorem TauCeti.ContCohomology.cochainsCor1_isCocycle₁ (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) {f : ↥U → M} (hf : groupCohomology.IsCocycle₁ f) : groupCohomology.IsCocycle₁ ((cochainsCor1 G M U t ht) f)

The corestriction of a 1-cocycle is a 1-cocycle. The factor t u • is what makes this true: the transversal identity t u * ℓᵗ_u(γ) = γ * t (γ⁻¹ • u) of TauCeti.transversal_mul_lWord is what converts the U-cocycle law for f into the G-cocycle law for cor¹_t f, and the reindexed sum is what produces the leading γ •.

theorem TauCeti.ContCohomology.cochainsCor1_d0 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (m : M) : (cochainsCor1 G M U t ht) ((d0 (↥U) M) m) = (d0 G M) (∑ u : G ⧸ U, t u • m)

The degree-one corestriction of a coboundary is the coboundary of the degree-zero corestriction.

theorem TauCeti.ContCohomology.cochainsCor1_mem_B1 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) {f : ↥U → M} (hf : f ∈ B1 (↥U) M) : (cochainsCor1 G M U t ht) f ∈ B1 G M

The degree-one corestriction cochain preserves 1-coboundaries.

theorem TauCeti.ContCohomology.cochainsCor1_changeTransversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (t' : G ⧸ U → G) (ht' : ∀ (u : G ⧸ U), ↑(t' u) = u) {f : ↥U → M} (hf : groupCohomology.IsCocycle₁ f) : (cochainsCor1 G M U t' ht') f = (cochainsCor1 G M U t ht) f + (d0 G M) (∑ v : G ⧸ U, t v • f ⟨transversalDiff U t t' v, ⋯⟩)

Change of transversal in degree one, as an explicit coboundary. Two transversals give corestriction cochains differing by d⁰ of the degree-zero corestriction of the values of f on the transversal difference TauCeti.transversalDiff. Unlike in degree zero, the two cochains are genuinely different; only their classes in H¹(G, M) agree.

theorem TauCeti.ContCohomology.cochainsCor1_res (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) {c : G → M} (hc : groupCohomology.IsCocycle₁ c) : ((cochainsCor1 G M U t ht) fun (x : ↥U) => c ↑x) = U.index • c + (d0 G M) (∑ u : G ⧸ U, c (t u))

cor¹_t ∘ res¹ on cochains, with its correction term: for a 1-cocycle c on G, cor¹_t (res c) = (G : U) • c + d⁰ (∑ u, c (t u)). The correction term is genuinely there — unlike in degree zero, cor ∘ res is not multiplication by the index on cochains — and it is a coboundary, which is what makes TauCeti.ContCohomology.explicitCor1_comp_res1 true on classes.

Corestriction on H¹

Openness of U makes every corestriction cochain continuous, so the cochain layer above descends to H¹ = Z¹/B¹.

theorem TauCeti.ContCohomology.continuous_cochainsCor1 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) {f : ↥U → M} (hf : Continuous f) : Continuous ((cochainsCor1 G M U t ht) f)

The corestriction of a continuous cochain along an open subgroup is continuous. Continuity of the transversal t is not required: TauCeti.continuous_lWord needs only openness of U.

theorem TauCeti.ContCohomology.cochainsCor1_mem_Z1 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) {f : ↥U → M} (hf : f ∈ Z1 (↥U) M) : (cochainsCor1 G M U t ht) f ∈ Z1 G M

The degree-one corestriction cochain preserves continuous 1-cocycles.

noncomputable def TauCeti.ContCohomology.cocyclesCor1 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) : ↥(Z1 (↥U) M) →+ ↥(Z1 G M)

Corestriction in degree one for a variable transversal, on continuous cocycles.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ContCohomology.coe_cocyclesCor1 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) (f : ↥(Z1 (↥U) M)) : ↑((cocyclesCor1 G M U t ht hU) f) = (cochainsCor1 G M U t ht) ↑f

The underlying cochain of the corestriction of a continuous cocycle.

noncomputable def TauCeti.ContCohomology.explicitCor1Transversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) : H1 (↥U) M →+ H1 G M

Corestriction in degree one for a variable transversal.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ContCohomology.explicitCor1Transversal_mk (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) (f : ↥(Z1 (↥U) M)) : (explicitCor1Transversal G M U t ht hU) ↑f = ↑((cocyclesCor1 G M U t ht hU) f)

Degree-one corestriction sends the class of a continuous 1-cocycle to the class of its corestriction cochain.

theorem TauCeti.ContCohomology.explicitCor1_changeTransversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) (t' : G ⧸ U → G) (ht' : ∀ (u : G ⧸ U), ↑(t' u) = u) : explicitCor1Transversal G M U t ht hU = explicitCor1Transversal G M U t' ht' hU

Independence of the transversal in degree one. Two transversals give the same map on H¹(U, M), because by TauCeti.ContCohomology.cochainsCor1_changeTransversal their corestriction cochains differ by a 1-coboundary.

noncomputable def TauCeti.ContCohomology.explicitCor1 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (hU : IsOpen ↑U) : H1 (↥U) M →+ H1 G M

Corestriction in degree one, at the canonical transversal Quotient.out.

Equations

• TauCeti.ContCohomology.explicitCor1 G M U hU = TauCeti.ContCohomology.explicitCor1Transversal G M U Quotient.out ⋯ hU

theorem TauCeti.ContCohomology.explicitCor1_eq_transversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) : explicitCor1 G M U hU = explicitCor1Transversal G M U t ht hU

The canonical degree-one corestriction can be computed using any transversal.

@[simp]

theorem TauCeti.ContCohomology.explicitCor1_mk (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (hU : IsOpen ↑U) (f : ↥(Z1 (↥U) M)) : (explicitCor1 G M U hU) ↑f = ↑((cocyclesCor1 G M U Quotient.out ⋯ hU) f)

Canonical degree-one corestriction sends the class of a continuous 1-cocycle to the class of its corestriction cochain over Quotient.out.

theorem TauCeti.ContCohomology.explicitCor1Transversal_comp_res1 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) (x : H1 G M) : (explicitCor1Transversal G M U t ht hU) ((explicitRes1 G M U) x) = U.index • x

cor¹_t ∘ res¹ = (G : U) • id on H¹(G, M), for a variable transversal. On cochains the two sides differ by the coboundary recorded in TauCeti.ContCohomology.cochainsCor1_res.

theorem TauCeti.ContCohomology.explicitCor1_comp_res1 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (hU : IsOpen ↑U) (x : H1 G M) : (explicitCor1 G M U hU) ((explicitRes1 G M U) x) = U.index • x

cor¹ ∘ res¹ = (G : U) • id on H¹(G, M).

theorem TauCeti.ContCohomology.explicitCor1_explicitMap1_id (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (hU : IsOpen ↑U) {N : Type w} [AddCommGroup N] [DistribMulAction G N] [TopologicalSpace N] [IsTopologicalAddGroup N] [ContinuousSMul G N] (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (g : G) (m : M), f (g • m) = g • f m) (x : H1 (↥U) M) : (explicitCor1 G N U hU) ((explicitMap1 (↥U) M (↥U) N (ContinuousMonoidHom.id ↥U) f hf ⋯) x) = (explicitMap1 G M G N (ContinuousMonoidHom.id G) f hf ⋯) ((explicitCor1 G M U hU) x)

Degree-one corestriction is natural in the coefficients: for a continuous G-equivariant f : M →+ N, applying f on H¹(U, -) and then corestricting agrees with corestricting and then applying f. On cochains this is TauCeti.ContCohomology.map_cochainsCor1.

The degree-two corestriction cochain

As in degree one, nothing in this section needs a topology: the 2-cocycle law for cor²_t, the comparison of two transversals and the correction term of cor² ∘ res² are all identities of plain cochains. Continuity enters only in the next section, where the cochain is pushed to H².

noncomputable def TauCeti.ContCohomology.cochainsCor2 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) : (↥U × ↥U → M) →+ G × G → M

The degree-two corestriction cochain for a transversal t, (cor²_t f) (γ, η) = ∑ u : G ⧸ U, t u • f (ℓᵗ_u γ, ℓᵗ_{γ⁻¹ • u} η).

Both transversal words lie in U by TauCeti.lWord_mem. The coset index of the second one is translated by γ⁻¹, exactly as in the transversal cocycle law TauCeti.lWord_mul_lWord; that translation is what makes the sum a 2-cocycle.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ContCohomology.cochainsCor2_apply (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (f : ↥U × ↥U → M) (γ η : G) : (cochainsCor2 G M U t ht) f (γ, η) = ∑ u : G ⧸ U, t u • f (⟨lWord U t u γ, ⋯⟩, ⟨lWord U t (γ⁻¹ • u) η, ⋯⟩)

The defining formula for the degree-two corestriction cochain.

theorem TauCeti.ContCohomology.cochainsCor2_apply_of_smul_eq_self (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (htriv : ∀ (g : G) (m : M), g • m = m) (f : ↥U × ↥U → M) (γ η : G) : (cochainsCor2 G M U t ht) f (γ, η) = ∑ u : G ⧸ U, f (⟨lWord U t u γ, ⋯⟩, ⟨lWord U t (γ⁻¹ • u) η, ⋯⟩)

For a trivial coefficient action the representative factor t u • disappears, and the degree-two corestriction is the plain sum of the values of the cochain on the transversal words.

theorem TauCeti.ContCohomology.map_cochainsCor2 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) {N : Type w} [AddCommGroup N] [DistribMulAction G N] (φ : M →+ N) (hφ : ∀ (g : G) (m : M), φ (g • m) = g • φ m) (f : ↥U × ↥U → M) (γ η : G) : φ ((cochainsCor2 G M U t ht) f (γ, η)) = (cochainsCor2 G N U t ht) (fun (q : ↥U × ↥U) => φ (f q)) (γ, η)

Naturality of the degree-two corestriction cochain in an equivariant coefficient homomorphism.

theorem TauCeti.ContCohomology.cochainsCor2_isCocycle₂ (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) {f : ↥U × ↥U → M} (hf : groupCohomology.IsCocycle₂ f) : groupCohomology.IsCocycle₂ ((cochainsCor2 G M U t ht) f)

The corestriction of a 2-cocycle is a 2-cocycle. The three arguments to which the U-cocycle law of f is applied are ℓᵗ_u(γ), ℓᵗ_{γ⁻¹ • u}(η) and ℓᵗ_{(γη)⁻¹ • u}(ζ); their two consecutive products are ℓᵗ_u(γη) and ℓᵗ_{γ⁻¹ • u}(ηζ) by TauCeti.lWord_mul_lWord, which is what matches the four terms of the law with the four corestriction sums. The leading γ • comes, as in degree one, from TauCeti.transversal_mul_lWord together with a translation of the summation index.

theorem TauCeti.ContCohomology.cochainsCor2_d1 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (c : ↥U → M) : (cochainsCor2 G M U t ht) ((d1 (↥U) M) c) = (d1 G M) ((cochainsCor1 G M U t ht) c)

The degree-two corestriction is a chain map: it turns the degree-one corestriction of a 1-cochain into the degree-two corestriction of its coboundary. This is the identity that carries 2-coboundaries to 2-coboundaries.

theorem TauCeti.ContCohomology.cochainsCor2_changeTransversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (t' : G ⧸ U → G) (ht' : ∀ (u : G ⧸ U), ↑(t' u) = u) {f : ↥U × ↥U → M} (hf : groupCohomology.IsCocycle₂ f) : (cochainsCor2 G M U t' ht') f = (cochainsCor2 G M U t ht) f + (d1 G M) fun (γ : G) => ∑ u : G ⧸ U, t u • (f (⟨transversalDiff U t t' u, ⋯⟩, ⟨lWord U t' u γ, ⋯⟩) - f (⟨lWord U t u γ, ⋯⟩, ⟨transversalDiff U t t' (γ⁻¹ • u), ⋯⟩))

Change of transversal in degree two, as an explicit coboundary. Two transversals give degree-two corestriction cochains differing by d¹ of the 1-cochain

γ ↦ ∑ u, t u • (f (d_u, ℓᵗ'_u γ) - f (ℓᵗ_u γ, d_{γ⁻¹ • u})),

built from the transversal difference TauCeti.transversalDiff. As in degree one the two cochains are genuinely different; only their classes in H²(G, M) agree.

theorem TauCeti.ContCohomology.cochainsCor2_res (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) {c : G × G → M} (hc : groupCohomology.IsCocycle₂ c) : ((cochainsCor2 G M U t ht) fun (q : ↥U × ↥U) => c (↑q.1, ↑q.2)) = U.index • c + (d1 G M) fun (γ : G) => ∑ u : G ⧸ U, (c (t u, lWord U t u γ) - c (γ, t u))

cor²_t ∘ res² on cochains, with its correction term: for a continuous 2-cocycle c on G, cor²_t (res c) = (G : U) • c + d¹ k with k γ = ∑ u, (c (t u, ℓᵗ_u γ) - c (γ, t u)). The correction term is again genuinely there, and it is a coboundary, which is what makes TauCeti.ContCohomology.explicitCor2_comp_res2 true on classes.

Corestriction on H²

Openness of U makes every degree-two corestriction cochain continuous — through TauCeti.continuous_lWord and TauCeti.continuous_lWord_inv_smul, one for each of the two transversal words — so the cochain layer above descends to H² = Z²/B².

Degree one needs separately continuous multiplication on G. This section uses the stronger bundled IsTopologicalGroup G to obtain IsTopologicalGroup ↥U, which Z²(U, M) needs: B² is the image of the continuous 1-cochains on U.

theorem TauCeti.ContCohomology.continuous_cochainsCor2 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) {f : ↥U × ↥U → M} (hf : Continuous f) : Continuous ((cochainsCor2 G M U t ht) f)

The degree-two corestriction of a continuous cochain along an open subgroup is continuous. As in degree one, no continuity is required of the transversal t.

theorem TauCeti.ContCohomology.cochainsCor2_mem_Z2 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) {f : ↥U × ↥U → M} (hf : f ∈ Z2 (↥U) M) : (cochainsCor2 G M U t ht) f ∈ Z2 G M

The degree-two corestriction cochain preserves continuous 2-cocycles.

theorem TauCeti.ContCohomology.cochainsCor2_mem_B2 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) {f : ↥U × ↥U → M} (hf : f ∈ B2 (↥U) M) : (cochainsCor2 G M U t ht) f ∈ B2 G M

The degree-two corestriction cochain preserves 2-coboundaries: by TauCeti.ContCohomology.cochainsCor2_d1 it sends d¹ c to d¹ of the degree-one corestriction of c, which is continuous because U is open.

noncomputable def TauCeti.ContCohomology.cocyclesCor2 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) : ↥(Z2 (↥U) M) →+ ↥(Z2 G M)

Corestriction in degree two for a variable transversal, on continuous cocycles.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ContCohomology.coe_cocyclesCor2 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) (f : ↥(Z2 (↥U) M)) : ↑((cocyclesCor2 G M U t ht hU) f) = (cochainsCor2 G M U t ht) ↑f

The underlying cochain of the corestriction of a continuous 2-cocycle.

noncomputable def TauCeti.ContCohomology.explicitCor2Transversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) : H2 (↥U) M →+ H2 G M

Corestriction in degree two for a variable transversal.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ContCohomology.explicitCor2Transversal_mk (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) (f : ↥(Z2 (↥U) M)) : (explicitCor2Transversal G M U t ht hU) ↑f = ↑((cocyclesCor2 G M U t ht hU) f)

Degree-two corestriction sends the class of a continuous 2-cocycle to the class of its corestriction cochain.

theorem TauCeti.ContCohomology.explicitCor2_changeTransversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) (t' : G ⧸ U → G) (ht' : ∀ (u : G ⧸ U), ↑(t' u) = u) : explicitCor2Transversal G M U t ht hU = explicitCor2Transversal G M U t' ht' hU

Independence of the transversal in degree two. Two transversals give the same map on H²(U, M), because by TauCeti.ContCohomology.cochainsCor2_changeTransversal their corestriction cochains differ by a 2-coboundary.

noncomputable def TauCeti.ContCohomology.explicitCor2 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (hU : IsOpen ↑U) : H2 (↥U) M →+ H2 G M

Corestriction in degree two, at the canonical transversal Quotient.out.

Equations

• TauCeti.ContCohomology.explicitCor2 G M U hU = TauCeti.ContCohomology.explicitCor2Transversal G M U Quotient.out ⋯ hU

theorem TauCeti.ContCohomology.explicitCor2_eq_transversal (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) : explicitCor2 G M U hU = explicitCor2Transversal G M U t ht hU

The canonical degree-two corestriction can be computed using any transversal.

@[simp]

theorem TauCeti.ContCohomology.explicitCor2_mk (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (hU : IsOpen ↑U) (f : ↥(Z2 (↥U) M)) : (explicitCor2 G M U hU) ↑f = ↑((cocyclesCor2 G M U Quotient.out ⋯ hU) f)

Canonical degree-two corestriction sends the class of a continuous 2-cocycle to the class of its corestriction cochain over Quotient.out.

theorem TauCeti.ContCohomology.explicitCor2Transversal_comp_res2 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) (x : H2 G M) : (explicitCor2Transversal G M U t ht hU) ((explicitRes2 G M U) x) = U.index • x

cor²_t ∘ res² = (G : U) • id on H²(G, M), for a variable transversal. On cochains the two sides differ by the coboundary recorded in TauCeti.ContCohomology.cochainsCor2_res.

theorem TauCeti.ContCohomology.explicitCor2_comp_res2 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) [U.FiniteIndex] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (hU : IsOpen ↑U) (x : H2 G M) : (explicitCor2 G M U hU) ((explicitRes2 G M U) x) = U.index • x

cor² ∘ res² = (G : U) • id on H²(G, M).