Explicit low-degree classes of cocycles on contracted complexes

Let X be a discrete topological representation of G and let J be a complex of topological representations with a contraction c : TopRep.ResolutionContraction X J, whose retraction proj : J⁰ → X and homotopies hom n : Jⁿ⁺¹ → Jⁿ need not be equivariant. An invariant cocycle z of J has a class c.cohomologyClass z in Mathlib's continuous cohomology, the class of the homogeneous cocycle into which the comparison with the coinduced resolution carries z. In degrees one and two this file writes that class as the class of an explicit continuous inhomogeneous cocycle:

H¹:  g ↦ g • proj (g⁻¹ • hom₀ z),
H²:  (g, h) ↦ (g h) • proj (h⁻¹ • hom₀ (g⁻¹ • hom₁ z)).

This is how a class defined through a contraction, such as the class of the tensor power of a cocycle on a tensor-induced resolution in Evens' multiplicative transfer, is compared with a class given by an explicit cocycle formula. For a contraction built by TopRep.ResolutionContraction.ofGraded from maps π and h on a total module, simp rewrites these formulas in terms of π and h through ofGraded_proj_apply, ofGraded_hom_apply and gradedCochainComplex_ρ_apply.

The first step does not involve contractions: a homogeneous 1- or 2-cocycle a of a discrete X has the inhomogeneous form TopRep.inhomogeneousCocycle1, respectively TopRep.inhomogeneousCocycle2, and the explicit comparisons carry its class to the class of a (TopRep.explicitH1AddEquivContinuousCohomologyOfDiscrete_eq_cochainClass and its degree-two companion, in CohomologyComparison.lean). This file applies that to the homogeneous cocycle obtained from z through the comparison with the coinduced resolution.

Main definitions

• TopRep.ResolutionContraction.explicitCocycle1, TopRep.ResolutionContraction.explicitCocycle2: the explicit inhomogeneous cocycles of an invariant 1- or 2-cocycle of a contracted complex.

Main results

• TopRep.ResolutionContraction.explicitCocycle1_apply and TopRep.ResolutionContraction.explicitCocycle2_apply: the formulas above.
• TopRep.ResolutionContraction.explicitH1AddEquivContinuousCohomologyOfDiscrete_explicitCocycle1 and its degree-two companion TopRep.ResolutionContraction.explicitH2AddEquivContinuousCohomologyOfDiscrete_explicitCocycle2: the explicit cocycles represent the classes of the invariant cocycles.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I, §2: the passage between homogeneous and inhomogeneous cochains.
• C. A. Weibel, An Introduction to Homological Algebra, Comparison Theorem 2.3.7.
• L. Evens, A generalization of the transfer map in the cohomology of groups, Trans. Amer. Math. Soc. 108 (1963), §§2–5.

Cocycles on contracted complexes

noncomputable def TopRep.ResolutionContraction.explicitCocycle1 {k : Type v} [Ring k] [TopologicalSpace k] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} [DiscreteTopology ↑X] [ContinuousSMul G ↑X] {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) (z : ↥(J.X 1).ρ.invariants) (hz : (Hom.hom (J.d 1 2)) ↑z = 0) : ↥(TauCeti.ContCohomology.Z1 G ↑X)

The explicit inhomogeneous 1-cocycle of an invariant 1-cocycle z of a complex contracted onto a discrete X: g ↦ g • proj (g⁻¹ • hom₀ z) (explicitCocycle1_apply). Its class is the class of z (explicitH1AddEquivContinuousCohomologyOfDiscrete_explicitCocycle1).

@[simp]

theorem TopRep.ResolutionContraction.explicitCocycle1_apply {k : Type v} [Ring k] [TopologicalSpace k] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} [DiscreteTopology ↑X] [ContinuousSMul G ↑X] {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) (z : ↥(J.X 1).ρ.invariants) (hz : (Hom.hom (J.d 1 2)) ↑z = 0) (g : G) : ↑(c.explicitCocycle1 z hz) g = (X.ρ g) (c.proj (((J.X 0).ρ g⁻¹) ((c.hom 0) ↑z)))

The explicit cocycle of an invariant 1-cocycle z is g ↦ g • proj (g⁻¹ • hom₀ z).

theorem TopRep.ResolutionContraction.explicitH1AddEquivContinuousCohomologyOfDiscrete_explicitCocycle1 {k : Type v} [Ring k] [TopologicalSpace k] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} [DiscreteTopology ↑X] [ContinuousSMul G ↑X] {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) (z : ↥(J.X 1).ρ.invariants) (hz : (Hom.hom (J.d 1 2)) ↑z = 0) : X.explicitH1AddEquivContinuousCohomologyOfDiscrete ↑(c.explicitCocycle1 z hz) = c.cohomologyClass z hz

The class of an invariant 1-cocycle in explicit coordinates. The degree-one comparison carries the class of the explicit cocycle g ↦ g • proj (g⁻¹ • hom₀ z) to the class of z in H¹(G, X).

noncomputable def TopRep.ResolutionContraction.explicitCocycle2 {k : Type v} [Ring k] [TopologicalSpace k] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} [DiscreteTopology ↑X] [ContinuousSMul G ↑X] {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [LocallyCompactSpace G] (z : ↥(J.X 2).ρ.invariants) (hz : (Hom.hom (J.d 2 3)) ↑z = 0) : ↥(TauCeti.ContCohomology.Z2 G ↑X)

The explicit inhomogeneous 2-cocycle of an invariant 2-cocycle z of a complex contracted onto a discrete X: (g, h) ↦ (g h) • proj (h⁻¹ • hom₀ (g⁻¹ • hom₁ z)) (explicitCocycle2_apply). Its class is the class of z (explicitH2AddEquivContinuousCohomologyOfDiscrete_explicitCocycle2).

@[simp]

theorem TopRep.ResolutionContraction.explicitCocycle2_apply {k : Type v} [Ring k] [TopologicalSpace k] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} [DiscreteTopology ↑X] [ContinuousSMul G ↑X] {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [LocallyCompactSpace G] (z : ↥(J.X 2).ρ.invariants) (hz : (Hom.hom (J.d 2 3)) ↑z = 0) (g h : G) : ↑(c.explicitCocycle2 z hz) (g, h) = (X.ρ (g * h)) (c.proj (((J.X 0).ρ h⁻¹) ((c.hom 0) (((J.X 1).ρ g⁻¹) ((c.hom 1) ↑z)))))

The explicit cocycle of an invariant 2-cocycle z is (g, h) ↦ (g h) • proj (h⁻¹ • hom₀ (g⁻¹ • hom₁ z)).

theorem TopRep.ResolutionContraction.explicitH2AddEquivContinuousCohomologyOfDiscrete_explicitCocycle2 {k : Type v} [Ring k] [TopologicalSpace k] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} [DiscreteTopology ↑X] [ContinuousSMul G ↑X] {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [LocallyCompactSpace G] (z : ↥(J.X 2).ρ.invariants) (hz : (Hom.hom (J.d 2 3)) ↑z = 0) : X.explicitH2AddEquivContinuousCohomologyOfDiscrete ↑(c.explicitCocycle2 z hz) = c.cohomologyClass z hz

The class of an invariant 2-cocycle in explicit coordinates. The degree-two comparison carries the class of the explicit cocycle (g, h) ↦ (g h) • proj (h⁻¹ • hom₀ (g⁻¹ • hom₁ z)) to the class of z in H²(G, X).