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 incontinuousCohomology n Xof a homogeneousn-cochain whose differential vanishes.
Main results #
TopRep.resolutionX_succ_ρ_apply_applyandTopRep.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.resolutionX_add_self_eq_zero: the resolution of coefficients that are their own additive inverses has the same property.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 satisfiesa 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 thecastof 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_add,TopRep.cochainClass_zeroandTopRep.cochainClass_smul: the class map is linear.TopRep.cochainClass_eq_cochainClass_iff: two homogeneous cocycles of positive degree have the same class exactly when their difference is a coboundary, andTopRep.cochainClass_eq_of_sub_eq_dis the direction that compares two explicit representatives.TauCeti.ContinuousCohomology.map_cochainClass: the map of a compatible pair on the class of a homogeneous cocycle.
The action on a successor level of the coinduced resolution, at a point:
(g • F) x = g • F (g⁻¹ * x).
The successor differential of the coinduced resolution, at a point:
(d (n + 1) F) x = F - d n (F x).
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.
If every coefficient is its own additive inverse, then so is every element of every term of the coinduced resolution, the terms being iterated spaces of continuous functions into the coefficients.
A homogeneous zero-cocycle is the constant resolution element at its value at 1.
The homogeneous differential of a one-cochain, evaluated:
(d a) 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₂.
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 #
The class in continuous cohomology of a homogeneous n-cochain a whose differential
vanishes: the class of the cocycle that a determines.
Instances For
cochainClass is the class map ContinuousCohomology.π applied to the cocycle determined by
the cochain.
The class of the underlying cochain of a cocycle is the class of the cocycle.
The class map is additive: the class of a sum of homogeneous cocycles is the sum of their classes.
The class of the zero cochain is zero.
The class map is linear: the class of a scalar multiple of a homogeneous cocycle is the scalar multiple of its class.
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).
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.
Every continuous cohomology class is the class of a homogeneous cocycle.
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.
Homogeneous cocycles whose difference is a coboundary have the same class.
The map of a compatible pair carries the class of a homogeneous cocycle a to the class of
its image under Mathlib's cochain map ContinuousCohomology.cochainsMap φ f.