Pointwise formulas for the coinduced resolution, and classes of homogeneous cocycles

Mathlib computes the continuous cohomology of a topological representation X from the coinduced resolution TopRep.resolutionX X n, the iterated function space C(G, C(G, …, C(G, X))), whose differential TopRep.d is defined recursively by d (n + 1) F x = F - d n (F x). This file records the pointwise formulas that the recursion gives for the action and for the differential on a successor level, and their consequence that evaluation at any point x : G contracts the resolution: d n (F x) + (d (n + 1) F) x = F, summed over finitely many points. Evaluation at a point is not G-equivariant, so the contraction does not descend to the invariants, which are the homogeneous cochains; it is nevertheless what drives the acyclicity of coinduced modules, and a sum of such contractions over suitably chosen points can descend.

In degree zero, the cocycle equation says that a homogeneous cochain is constant. The formula TopRep.homogeneousCochains.eq_d_zero_apply_of_d_eq_zero records that the cochain is the constant resolution element at its value at 1.

A homogeneous cochain killed by the differential has a class in continuous cohomology, TopRep.cochainClass. Constructions given by a cochain formula reach continuous cohomology through it, and two such cocycles have the same class exactly when they differ by a homogeneous coboundary.

Main definitions

• TopRep.cochainClass: the class in continuousCohomology n X of a homogeneous n-cochain whose differential vanishes.

Main results

• TopRep.resolutionX_succ_ρ_apply_apply and TopRep.hom_d_succ_apply_apply: the action and the differential on a successor level of the resolution, at a point.
• TopRep.d_sum_apply_add_sum_d_apply: evaluation at finitely many points, summed, contracts the coinduced resolution up to the number of points.
• TopRep.homogeneousCochains.eq_d_zero_apply_of_d_eq_zero: a homogeneous zero-cocycle is constant.
• TopRep.homogeneousCochains.d_one_apply: the differential of a homogeneous one-cochain, evaluated, is (d a) g₀ g₁ g₂ = a g₁ g₂ - (a g₀ g₂ - a g₀ g₁); so a one-cocycle satisfies a g₀ g₂ = a g₀ g₁ + a g₁ g₂ (TopRep.homogeneousCochains.apply_eq_add_of_d_eq_zero).
• TopRep.homogeneousCochains.d_two_apply: the differential of a homogeneous two-cochain, evaluated, is (d a) g₀ g₁ g₂ g₃ = a g₁ g₂ g₃ - (a g₀ g₂ g₃ - (a g₀ g₁ g₃ - a g₀ g₁ g₂)).
• TopRep.eval_iCycles_eqToHom: reading a cocycle transported along an equality of coefficient objects is the cast of reading the untransported cocycle.
• TopRep.eqToHom_π_eq_cochainClass: the transport of a class along an equality of coefficient objects is the class of the transported cocycle.
• TopRep.cochainClass_eq_cochainClass_iff: two homogeneous cocycles of positive degree have the same class exactly when their difference is a coboundary, and TopRep.cochainClass_eq_of_sub_eq_d is the direction that compares two explicit representatives.

@[simp]

theorem TopRep.resolutionX_succ_ρ_apply_apply {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) (g : G) (F : ↑(X.resolutionX (n + 1))) (x : G) : (((X.resolutionX (n + 1)).ρ g) F) x = ((X.resolutionX n).ρ g) (F (g⁻¹ * x))

The action on a successor level of the coinduced resolution, at a point: (g • F) x = g • F (g⁻¹ * x).

@[simp]

theorem TopRep.hom_d_succ_apply_apply {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) (F : ↑(X.resolutionX (n + 1))) (x : G) : ((Hom.hom (X.d (n + 1))) F) x = F - (Hom.hom (X.d n)) (F x)

The successor differential of the coinduced resolution, at a point: (d (n + 1) F) x = F - d n (F x).

theorem TopRep.d_sum_apply_add_sum_d_apply {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) {ι : Type u_3} [Fintype ι] (σ : ι → G) (m : ℕ) (F : ↑(X.resolutionX (m + 1))) : (Hom.hom (X.d m)) (∑ i : ι, F (σ i)) + ∑ i : ι, ((Hom.hom (X.d (m + 1))) F) (σ i) = Fintype.card ι • F

Summed evaluations contract the coinduced resolution up to a multiple. For an element F : C(G, Xₘ) of the degree m + 1 term of the coinduced resolution and finitely many points σ i of G, dₘ (∑ᵢ F (σ i)) + ∑ᵢ (dₘ₊₁ F) (σ i) = |ι| • F. Each summand is the identity dₘ (F x) + (dₘ₊₁ F) x = F saying that evaluation at a point contracts the resolution.

theorem TopRep.homogeneousCochains.eq_d_zero_apply_of_d_eq_zero {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {a : ↑(X.homogeneousCochains.X 0).toModuleCat} (ha : (TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1)) a = 0) : ↑a = (Hom.hom (X.d 0)) (↑a 1)

A homogeneous zero-cocycle is the constant resolution element at its value at 1.

theorem TopRep.homogeneousCochains.d_one_apply {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} (a : ↑(X.homogeneousCochains.X 1).toModuleCat) (g₀ g₁ g₂ : G) : ((↑((TopModuleCat.Hom.hom (X.homogeneousCochains.d 1 (1 + 1))) a) g₀) g₁) g₂ = (↑a g₁) g₂ - ((↑a g₀) g₂ - (↑a g₀) g₁)

The homogeneous differential of a one-cochain, evaluated: (d a) g₀ g₁ g₂ = a g₁ g₂ - (a g₀ g₂ - a g₀ g₁).

theorem TopRep.homogeneousCochains.apply_eq_add_of_d_eq_zero {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {a : ↑(X.homogeneousCochains.X 1).toModuleCat} (ha : (TopModuleCat.Hom.hom (X.homogeneousCochains.d 1 (1 + 1))) a = 0) (g₀ g₁ g₂ : G) : (↑a g₀) g₂ = (↑a g₀) g₁ + (↑a g₁) g₂

A homogeneous one-cocycle satisfies a g₀ g₂ = a g₀ g₁ + a g₁ g₂.

theorem TopRep.homogeneousCochains.d_two_apply {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} (a : ↑(X.homogeneousCochains.X 2).toModuleCat) (g₀ g₁ g₂ g₃ : G) : (((↑((TopModuleCat.Hom.hom (X.homogeneousCochains.d 2 (2 + 1))) a) g₀) g₁) g₂) g₃ = ((↑a g₁) g₂) g₃ - (((↑a g₀) g₂) g₃ - (((↑a g₀) g₁) g₃ - ((↑a g₀) g₁) g₂))

The homogeneous differential of a two-cochain, evaluated: (d a) g₀ g₁ g₂ g₃ = a g₁ g₂ g₃ - (a g₀ g₂ g₃ - (a g₀ g₁ g₃ - a g₀ g₁ g₂)).

Classes of homogeneous cocycles

noncomputable def TopRep.cochainClass {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) (a : ↑(X.homogeneousCochains.X n).toModuleCat) (ha : (TopModuleCat.Hom.hom (X.homogeneousCochains.d n (n + 1))) a = 0) : ↑(continuousCohomology n X).toModuleCat

The class in continuous cohomology of a homogeneous n-cochain a whose differential vanishes: the class of the cocycle that a determines.

Equations

• X.cochainClass n a ha = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X n)) (HomologicalComplex.cyclesMkOfEq X.homogeneousCochains a (n + 1) ⋯ ha)

theorem TopRep.cochainClass_def {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) (a : ↑(X.homogeneousCochains.X n).toModuleCat) (ha : (TopModuleCat.Hom.hom (X.homogeneousCochains.d n (n + 1))) a = 0) : X.cochainClass n a ha = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X n)) (HomologicalComplex.cyclesMkOfEq X.homogeneousCochains a (n + 1) ⋯ ha)

cochainClass is the class map ContinuousCohomology.π applied to the cocycle determined by the cochain.

theorem TopRep.cochainClass_iCycles {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {n : ℕ} (z : ↑(ContinuousCohomology.cocycles X n).toModuleCat) : X.cochainClass n ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains n)) z) ⋯ = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X n)) z

The class of the underlying cochain of a cocycle is the class of the cocycle.

theorem TopRep.eval_iCycles_eqToHom {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {n : ℕ} {Y : TopRep k G} (h : X = Y) (z : ↑(ContinuousCohomology.cocycles X n).toModuleCat) {T : TopRep k G → Sort u_3} (ev : (B : TopRep k G) → ↑(B.homogeneousCochains.X n).toModuleCat → T B) : ev Y ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles Y.homogeneousCochains n)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) z)) = cast ⋯ (ev X ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains n)) z))

Any reading ev of homogeneous cochains, applied to a cocycle transported along an equality X = Y of coefficient objects, is the cast of its reading of the untransported cocycle. Once the reading lands in a type that does not depend on the coefficient object up to definitional equality, the cast is the identity (cast_eq).

theorem TopRep.eqToHom_π_eq_cochainClass {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {n : ℕ} {Y : TopRep k G} (h : X = Y) (z : ↑(ContinuousCohomology.cocycles X n).toModuleCat) (a : ↑(Y.homogeneousCochains.X n).toModuleCat) (ha : (TopModuleCat.Hom.hom (Y.homogeneousCochains.d n (n + 1))) a = 0) (hza : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles Y.homogeneousCochains n)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) z) = a) : (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X n)) z) = Y.cochainClass n a ha

Transporting the class of a cocycle z along an equality X = Y of coefficient objects gives the class of any homogeneous cochain of Y that the transported cocycle presents.

theorem TopRep.exists_cochainClass_eq {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {n : ℕ} (x : ↑(continuousCohomology n X).toModuleCat) : ∃ (a : ↑(X.homogeneousCochains.X n).toModuleCat) (ha : (TopModuleCat.Hom.hom (X.homogeneousCochains.d n (n + 1))) a = 0), X.cochainClass n a ha = x

Every continuous cohomology class is the class of a homogeneous cocycle.

theorem TopRep.cochainClass_eq_cochainClass_iff {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {n j : ℕ} (hj : j + 1 = n) {a b : ↑(X.homogeneousCochains.X n).toModuleCat} (ha : (TopModuleCat.Hom.hom (X.homogeneousCochains.d n (n + 1))) a = 0) (hb : (TopModuleCat.Hom.hom (X.homogeneousCochains.d n (n + 1))) b = 0) : X.cochainClass n a ha = X.cochainClass n b hb ↔ ∃ (c : ↑(X.homogeneousCochains.X j).toModuleCat), a - b = (TopModuleCat.Hom.hom (X.homogeneousCochains.d j n)) c

Cohomologous cocycles, and only they, have the same class. In degree n = j + 1, two homogeneous cocycles have the same class exactly when their difference is the differential of a homogeneous j-cochain.

theorem TopRep.cochainClass_eq_of_sub_eq_d {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {n j : ℕ} (hj : j + 1 = n) {a b : ↑(X.homogeneousCochains.X n).toModuleCat} (ha : (TopModuleCat.Hom.hom (X.homogeneousCochains.d n (n + 1))) a = 0) (hb : (TopModuleCat.Hom.hom (X.homogeneousCochains.d n (n + 1))) b = 0) (c : ↑(X.homogeneousCochains.X j).toModuleCat) (hc : a - b = (TopModuleCat.Hom.hom (X.homogeneousCochains.d j n)) c) : X.cochainClass n a ha = X.cochainClass n b hb

Homogeneous cocycles whose difference is a coboundary have the same class.