The homogeneous form of a low-degree cochain

An inhomogeneous n-cochain f of G with values in M has a homogeneous partner, the G-equivariant function of n + 1 group elements

homogeneous1 f h₀ h₁ = h₀ • f (h₀⁻¹ h₁),
homogeneous2 f h₀ h₁ h₂ = h₀ • f (h₀⁻¹ h₁, h₁⁻¹ h₂),

which this file builds in degrees one and two. Equivariance (TauCeti.ContCohomology.homogeneous2_smul) is definitional bookkeeping; the point of the homogeneous form is that the cocycle and coboundary conditions become symmetric in the arguments. A 2-cocycle becomes the four-term relation TauCeti.ContCohomology.homogeneous2_add_eq_add, which says that the alternating sum over dropping one of four points vanishes, and the coboundary of a 1-cochain becomes the alternating sum TauCeti.ContCohomology.homogeneous2_d1 of its own homogeneous form.

The reason to have the symmetric form is TauCeti.ContCohomology.homogeneous2_sub_comp: for an arbitrary map v : G → G, the values of a homogeneous 2-cocycle at three points and at their images under v differ by the alternating sum of the explicit two-variable comparison function TauCeti.ContCohomology.homogeneousHomotopy2. This pointwise prism identity, applied to a retraction of G onto a subgroup, is the comparison used in Shapiro's lemma. The comparison function is itself a homogeneous (that is, equivariant) 1-cochain only for those g with which v commutes (TauCeti.ContCohomology.homogeneousHomotopy2_smul).

Mathlib's Rep.diagonalHomEquiv is the bundled k-linear version of the same correspondence, for Rep k G and the diagonal resolution, and ContinuousCohomology.homogeneousCochains is the all-degree homogeneous complex computing the canonical carrier. Neither applies to the unbundled DistribMulAction-valued continuous cochains of TauCeti/RepresentationTheory/Homological/ContCohomology/LowDegree.lean, which is what the declarations below are stated for; nothing here builds a competing cohomology theory, only a change of coordinates on the cochains of that file.

Main definitions

• TauCeti.ContCohomology.homogeneous1 and TauCeti.ContCohomology.homogeneous2: the homogeneous forms of a 1- and a 2-cochain.
• TauCeti.ContCohomology.homogeneousHomotopy2: the two-variable comparison function between the values of a homogeneous 2-cocycle at points and at their images under a self-map of G.

Main statements

• TauCeti.ContCohomology.homogeneous2_add_eq_add: the homogeneous four-term form of the 2-cocycle identity.
• TauCeti.ContCohomology.homogeneous2_d1: the homogeneous form of a 2-coboundary is the alternating sum of the homogeneous form of its primitive.
• TauCeti.ContCohomology.homogeneous2_sub_comp: the values of a homogeneous 2-cocycle at points and at their images under an arbitrary self-map of G differ by an alternating sum.
• TauCeti.ContCohomology.continuous_homogeneous1 and TauCeti.ContCohomology.continuous_homogeneous2: continuity of the homogeneous forms read along continuous families of group elements.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I §2, where the homogeneous and inhomogeneous descriptions of the standard complex are compared.

def TauCeti.ContCohomology.homogeneous1 {G : Type u} [Group G] {M : Type v} [MulAction G M] (f : G → M) (h₀ h₁ : G) : M

The homogeneous form h₀ • f (h₀⁻¹ h₁) of a 1-cochain f.

Equations

• TauCeti.ContCohomology.homogeneous1 f h₀ h₁ = h₀ • f (h₀⁻¹ * h₁)

def TauCeti.ContCohomology.homogeneous2 {G : Type u} [Group G] {M : Type v} [MulAction G M] (f : G × G → M) (h₀ h₁ h₂ : G) : M

The homogeneous form h₀ • f (h₀⁻¹ h₁, h₁⁻¹ h₂) of a 2-cochain f.

Equations

• TauCeti.ContCohomology.homogeneous2 f h₀ h₁ h₂ = h₀ • f (h₀⁻¹ * h₁, h₁⁻¹ * h₂)

@[simp]

theorem TauCeti.ContCohomology.homogeneous1_apply {G : Type u} [Group G] {M : Type v} [MulAction G M] (f : G → M) (h₀ h₁ : G) : homogeneous1 f h₀ h₁ = h₀ • f (h₀⁻¹ * h₁)

The defining formula for the homogeneous form of a 1-cochain.

@[simp]

theorem TauCeti.ContCohomology.homogeneous2_apply {G : Type u} [Group G] {M : Type v} [MulAction G M] (f : G × G → M) (h₀ h₁ h₂ : G) : homogeneous2 f h₀ h₁ h₂ = h₀ • f (h₀⁻¹ * h₁, h₁⁻¹ * h₂)

The defining formula for the homogeneous form of a 2-cochain.

theorem TauCeti.ContCohomology.homogeneous1_one_left {G : Type u} [Group G] {M : Type v} [MulAction G M] (f : G → M) (h : G) : homogeneous1 f 1 h = f h

At the identity the homogeneous form of a 1-cochain is the cochain itself. Not a simp lemma: TauCeti.ContCohomology.homogeneous1_apply already rewrites the left-hand side.

theorem TauCeti.ContCohomology.homogeneous2_one_left {G : Type u} [Group G] {M : Type v} [MulAction G M] (f : G × G → M) (h₁ h₂ : G) : homogeneous2 f 1 h₁ h₂ = f (h₁, h₁⁻¹ * h₂)

At the identity the homogeneous form of a 2-cochain is the cochain itself, read at the second point and the difference of the two. Not a simp lemma: TauCeti.ContCohomology.homogeneous2_apply already rewrites the left-hand side.

theorem TauCeti.ContCohomology.homogeneous1_smul {G : Type u} [Group G] {M : Type v} [MulAction G M] (f : G → M) (g h₀ h₁ : G) : homogeneous1 f (g * h₀) (g * h₁) = g • homogeneous1 f h₀ h₁

The homogeneous form of a 1-cochain is equivariant.

theorem TauCeti.ContCohomology.homogeneous2_smul {G : Type u} [Group G] {M : Type v} [MulAction G M] (f : G × G → M) (g h₀ h₁ h₂ : G) : homogeneous2 f (g * h₀) (g * h₁) (g * h₂) = g • homogeneous2 f h₀ h₁ h₂

The homogeneous form of a 2-cochain is equivariant.

def TauCeti.ContCohomology.homogeneousHomotopy2 {G : Type u} [Group G] {M : Type v} [AddGroup M] [DistribMulAction G M] (f : G × G → M) (v : G → G) (h₀ h₁ : G) : M

The two-variable comparison function in the pointwise prism identity relating a homogeneous 2-cocycle at points to its values at their images under a self-map v of G; see TauCeti.ContCohomology.homogeneous2_sub_comp. For arbitrary v it is not equivariant, so not a homogeneous cochain; TauCeti.ContCohomology.homogeneousHomotopy2_smul gives equivariance under those g with which v commutes.

Equations

• TauCeti.ContCohomology.homogeneousHomotopy2 f v h₀ h₁ = TauCeti.ContCohomology.homogeneous2 f (v h₀) h₀ h₁ - TauCeti.ContCohomology.homogeneous2 f (v h₀) (v h₁) h₁

theorem TauCeti.ContCohomology.homogeneousHomotopy2_apply {G : Type u} [Group G] {M : Type v} [AddGroup M] [DistribMulAction G M] (f : G × G → M) (v : G → G) (h₀ h₁ : G) : homogeneousHomotopy2 f v h₀ h₁ = homogeneous2 f (v h₀) h₀ h₁ - homogeneous2 f (v h₀) (v h₁) h₁

The defining formula for the comparison function. It is not a simp lemma: its right-hand side is rewritten further by TauCeti.ContCohomology.homogeneous2_apply.

theorem TauCeti.ContCohomology.homogeneousHomotopy2_smul {G : Type u} [Group G] {M : Type v} [AddGroup M] [DistribMulAction G M] (f : G × G → M) (v : G → G) {g : G} (hv : ∀ (x : G), v (g * x) = g * v x) (h₀ h₁ : G) : homogeneousHomotopy2 f v (g * h₀) (g * h₁) = g • homogeneousHomotopy2 f v h₀ h₁

The comparison function is equivariant for any g that v commutes with.

theorem TauCeti.ContCohomology.homogeneous2_add_eq_add {G : Type u} [Group G] {M : Type v} [AddCommGroup M] [DistribMulAction G M] {f : G × G → M} (hf : groupCohomology.IsCocycle₂ f) (h₀ h₁ h₂ h₃ : G) : homogeneous2 f h₁ h₂ h₃ + homogeneous2 f h₀ h₁ h₃ = homogeneous2 f h₀ h₂ h₃ + homogeneous2 f h₀ h₁ h₂

The homogeneous 2-cocycle identity. For a 2-cocycle the alternating sum of the four values obtained by dropping one of four group elements vanishes, here written as the equality of the two positive halves.

theorem TauCeti.ContCohomology.homogeneous2_d1 {G : Type u} [Group G] {M : Type v} [AddCommGroup M] [DistribMulAction G M] (f : G → M) (h₀ h₁ h₂ : G) : homogeneous2 ((d1 G M) f) h₀ h₁ h₂ = homogeneous1 f h₁ h₂ - homogeneous1 f h₀ h₂ + homogeneous1 f h₀ h₁

The homogeneous form of a 2-coboundary is the alternating sum of the homogeneous form of its primitive.

theorem TauCeti.ContCohomology.homogeneous2_sub_comp {G : Type u} [Group G] {M : Type v} [AddCommGroup M] [DistribMulAction G M] {f : G × G → M} (hf : groupCohomology.IsCocycle₂ f) (v : G → G) (h₀ h₁ h₂ : G) : homogeneous2 f h₀ h₁ h₂ - homogeneous2 f (v h₀) (v h₁) (v h₂) = homogeneousHomotopy2 f v h₁ h₂ - homogeneousHomotopy2 f v h₀ h₂ + homogeneousHomotopy2 f v h₀ h₁

Pointwise prism identity for a homogeneous 2-cocycle. Its values at three points and at their images under any self-map v differ by the displayed alternating sum. No equivariance is assumed of v, so this is a pointwise identity rather than an induced map of resolutions.

theorem TauCeti.ContCohomology.continuous_homogeneous1 {G : Type u} [Group G] {M : Type v} [MulAction G M] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [ContinuousSMul G M] {X : Type u_1} [TopologicalSpace X] {f : G → M} (hf : Continuous f) {a b : X → G} (ha : Continuous a) (hb : Continuous b) : Continuous fun (x : X) => homogeneous1 f (a x) (b x)

The homogeneous form of a continuous 1-cochain, read along continuous families of group elements, is continuous.

theorem TauCeti.ContCohomology.continuous_homogeneous2 {G : Type u} [Group G] {M : Type v} [MulAction G M] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [ContinuousSMul G M] {X : Type u_1} [TopologicalSpace X] {f : G × G → M} (hf : Continuous f) {a b d : X → G} (ha : Continuous a) (hb : Continuous b) (hd : Continuous d) : Continuous fun (x : X) => homogeneous2 f (a x) (b x) (d x)

The homogeneous form of a continuous 2-cochain, read along continuous families of group elements, is continuous.