Classes of invariant homogeneous cocycles in continuous cohomology

Definition

MilnorConjecture_HomogeneousCochains

by vatsj · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebracontinuous-cohomologygroup-cohomology

Let $G$ be a locally compact topological group, $k$ a topological ring and $M$ a topological $k$ -module, regarded as a trivial representation of $G$ . Mathlib computes continuous cohomology $H^n_{\mathrm{cts}}(G,M)$ from the complex of $G$ -invariant elements of $C(G, C(G, \cdots C(G, M)))$ ( $n+1$ nested copies of $G$ in degree $n$ ), with an inductively defined differential.

This file translates that model into functions of several variables. For a continuous $F : G^{n+1}\to M$ which is invariant under simultaneous left translation,

F(gx_0,\dots,gx_n) = F(x_0,\dots,x_n)\quad (g\in G),

and satisfies the homogeneous cocycle identity

\sum_{i=0}^{n+1} (-1)^i\, F(y_0,\dots,\widehat{y_i},\dots,y_{n+1}) = 0,

it defines the class $[F] \in H^n_{\mathrm{cts}}(G,M)$ of the corresponding nested cochain $x_0\mapsto x_1\mapsto\cdots\mapsto F(x_0,\dots,x_n)$ . The file proves that Mathlib's differential of this nested cochain is the alternating face sum above, and that the $G$ -action translates all arguments.

This is reusable infrastructure: it gives a concrete way to write down classes in Mathlib's continuous cohomology with trivial coefficients.

Formalization Note curryN, coboundary and classOf are sorry-free; local compactness of $G$ is used only to make iterated currying continuous.

Definition code

import Mathlib

/-!
# Homogeneous cochains with trivial coefficients, as functions of several variables

Mathlib's continuous cohomology `continuousCohomology n A` is the homology of the complex
of `G`-invariant elements of `C(G, C(G, ⋯ C(G, A)))` (`n + 1` nested copies of `G`), with the
inductively defined differential `TopRep.d`. For trivial coefficients `M` and a locally compact
group `G`, this file turns a continuous function `F : Gⁿ⁺¹ → M` that is invariant under
simultaneous left translation and satisfies the homogeneous cocycle identity
`∑ᵢ (-1)ⁱ F(x₀, …, x̂ᵢ, …, xₙ₊₁) = 0` into a class in `continuousCohomology n`.
-/

open CategoryTheory

namespace MilnorConjecture

universe u

variable {k G M : Type u} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [Module k M]
  [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul k M]

variable (k G M) in
/-- `M` as a trivial continuous `k`-linear representation of `G`. -/
abbrev trivialRep : TopRep k G := TopRep.of (ContRepresentation.trivial k G M)

/-- The map `(x, v) ↦ (x, v₀, …, vₙ₋₁)` from `G × Gⁿ` to `Gⁿ⁺¹`. -/
def consMap (n : ℕ) : C(G × (Fin n → G), Fin (n + 1) → G) :=
  ⟨fun p ↦ Fin.cons p.1 p.2, by fun_prop⟩

variable (k G M) in
/-- Currying `n` times: a continuous `F : Gⁿ → M` becomes the element
`x₀ ↦ x₁ ↦ ⋯ ↦ F(x₀, …, xₙ₋₁)` of `C(G, C(G, ⋯ C(G, M)))`, the `n`-th term of Mathlib's
resolution `TopRep.resolutionX`. The assignment is itself continuous. -/
noncomputable def curryN : (n : ℕ) →
    C(C(Fin n → G, M), ((trivialRep k G M).resolutionX n : Type u))
  | 0 => ⟨fun F ↦ F Fin.elim0, continuous_eval_const _⟩
  | n + 1 => ⟨fun F ↦ (curryN n).comp (F.comp (consMap n)).curry,
      (ContinuousMap.continuous_postcomp _).comp
        (ContinuousMap.continuous_curry.comp (ContinuousMap.continuous_precomp _))⟩

@[simp]
lemma curryN_zero_apply (F : C(Fin 0 → G, M)) : curryN k G M 0 F = F Fin.elim0 := rfl

@[simp]
lemma curryN_succ_apply {n : ℕ} (F : C(Fin (n + 1) → G, M)) (x : G) :
    curryN k G M (n + 1) F x = curryN k G M n ⟨fun v ↦ F (Fin.cons x v), by fun_prop⟩ := rfl

lemma curryN_sub {n : ℕ} (F F' : C(Fin n → G, M)) :
    curryN k G M n (F - F') = curryN k G M n F - curryN k G M n F' := by
  induction n with
  | zero => rfl
  | succ n ih =>
    ext1 x
    rw [curryN_succ_apply, ContinuousMap.sub_apply, curryN_succ_apply, curryN_succ_apply, ← ih]
    rfl

/-- The `i`-th face map `Gⁿ⁺¹ → Gⁿ`, deleting the `i`-th coordinate. -/
def faceMap (n : ℕ) (i : Fin (n + 1)) : C(Fin (n + 1) → G, Fin n → G) :=
  ⟨fun y ↦ y ∘ i.succAbove, by fun_prop⟩

/-- The homogeneous coboundary with trivial coefficients:
`(δF)(y₀, …, yₙ) = ∑ᵢ (-1)ⁱ F(y₀, …, ŷᵢ, …, yₙ)`. -/
def coboundary (n : ℕ) (F : C(Fin n → G, M)) : C(Fin (n + 1) → G, M) :=
  ∑ i : Fin (n + 1), ((-1 : ℤ) ^ (i : ℕ)) • F.comp (faceMap n i)

omit [Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] in
lemma coboundary_apply {n : ℕ} (F : C(Fin n → G, M)) (y : Fin (n + 1) → G) :
    coboundary n F y = ∑ i : Fin (n + 1), ((-1 : ℤ) ^ (i : ℕ)) • F (y ∘ i.succAbove) := by
  simp [coboundary, faceMap]

/-- Mathlib's inductively defined differential agrees with the alternating face sum. -/
lemma d_curryN (n : ℕ) (F : C(Fin n → G, M)) :
    ((trivialRep k G M).d n).hom (curryN k G M n F) = curryN k G M (n + 1) (coboundary n F) := by
  induction n with
  | zero =>
    ext x
    show F Fin.elim0 = coboundary 0 F (Fin.cons x Fin.elim0)
    rw [coboundary_apply, Fin.sum_univ_one]
    simp only [Fin.val_zero, pow_zero, one_smul]
    exact congrArg F (funext fun i ↦ i.elim0)
  | succ n ih =>
    ext1 x
    rw [TopRep.hom_d_succ]
    change curryN k G M (n + 1) F - ((trivialRep k G M).d n).hom (curryN k G M (n + 1) F x) = _
    rw [curryN_succ_apply, ih, ← curryN_sub, curryN_succ_apply]
    congr 1
    ext w
    simp only [ContinuousMap.sub_apply, ContinuousMap.coe_mk]
    rw [coboundary_apply, coboundary_apply]
    show F w - ∑ i : Fin (n + 1), ((-1 : ℤ) ^ (i : ℕ)) • F (Fin.cons x (w ∘ i.succAbove)) = _
    conv_rhs => rw [Fin.sum_univ_succ, Fin.val_zero, pow_zero, one_smul, Fin.succAbove_zero,
      Fin.cons_comp_succ]
    rw [sub_eq_add_neg, ← Finset.sum_neg_distrib]
    congr 1
    refine Finset.sum_congr rfl fun j _ ↦ ?_
    rw [Fin.val_succ, pow_succ, mul_neg_one, neg_smul, Fin.cons_comp_succ_succAbove]
    rfl

lemma curryN_zero {n : ℕ} : curryN k G M n 0 = 0 := by
  simpa using curryN_sub (k := k) (0 : C(Fin n → G, M)) 0

/-- Left translation `(v₀, …, vₙ₋₁) ↦ (g v₀, …, g vₙ₋₁)` on `Gⁿ`. -/
def translate (n : ℕ) (g : G) : C(Fin n → G, Fin n → G) :=
  ⟨fun v i ↦ g * v i, by fun_prop⟩

/-- With trivial coefficients, `g` acts on `C(G, ⋯ C(G, M))` by translating every argument
by `g⁻¹`. -/
lemma ρ_curryN (n : ℕ) (g : G) (F : C(Fin n → G, M)) :
    ((trivialRep k G M).resolutionX n).ρ g (curryN k G M n F) =
      curryN k G M n (F.comp (translate n g⁻¹)) := by
  induction n with
  | zero =>
    show F Fin.elim0 = F (fun i ↦ g⁻¹ * Fin.elim0 i)
    exact congrArg F (funext fun i ↦ i.elim0)
  | succ n ih =>
    ext1 x
    rw [ContRepresentation.coind₁_apply_apply, curryN_succ_apply, ih, curryN_succ_apply]
    congr 1
    ext v
    simp only [ContinuousMap.comp_apply, ContinuousMap.coe_mk, translate]
    congr 1
    funext i
    cases i using Fin.cases <;> simp

lemma curryN_mem_invariants {n : ℕ} (F : C(Fin n → G, M))
    (hF : ∀ (g : G) (v : Fin n → G), F (fun i ↦ g * v i) = F v) :
    curryN k G M n F ∈ ((trivialRep k G M).resolutionX n).ρ.invariants := by
  intro g
  rw [ρ_curryN]
  congr 1
  ext v
  exact hF g⁻¹ v

variable [IsTopologicalRing k]

variable (k) in
/-- The class in `continuousCohomology n` of a continuous `F : Gⁿ⁺¹ → M` that is invariant
under simultaneous left translation and is a homogeneous cocycle (`δF = 0`), with `M` a
trivial representation of `G`. -/
noncomputable def classOf (n : ℕ) (F : C(Fin (n + 1) → G, M))
    (hinv : ∀ (g : G) (v : Fin (n + 1) → G), F (fun i ↦ g * v i) = F v)
    (hcoc : coboundary (n + 1) F = 0) :
    continuousCohomology n (trivialRep k G M) :=
  let σ : (trivialRep k G M).homogeneousCochains.X n :=
    ⟨curryN k G M (n + 1) F, curryN_mem_invariants F hinv⟩
  let ι : TopModuleCat.of k k ⟶ (trivialRep k G M).homogeneousCochains.X n :=
    TopModuleCat.ofHom (ContinuousLinearMap.toSpanSingleton k σ)
  have hd : ((trivialRep k G M).homogeneousCochains.d n (n + 1)).hom σ = 0 := by
    apply Subtype.ext
    rw [TopRep.homogeneousCochains.d_apply]
    change ((trivialRep k G M).d (n + 1)).hom (curryN k G M (n + 1) F) = 0
    rw [d_curryN, hcoc, curryN_zero]
  have hσ : ι ≫ (trivialRep k G M).homogeneousCochains.d n (n + 1) = 0 := by
    apply ConcreteCategory.ext
    apply ContinuousLinearMap.ext_ring
    have h1 : ι 1 = σ := one_smul k σ
    rw [ConcreteCategory.comp_apply, h1]
    simpa using hd
  (ContinuousCohomology.π _ n).hom
    (((trivialRep k G M).homogeneousCochains.liftCycles ι (n + 1) (by simp) hσ).hom 1)

end MilnorConjecture

Source

Standard homogeneous-cochain description of continuous group cohomology (cf. Neukirch-Schmidt-Wingberg, Cohomology of Number Fields), specialised to Mathlib's `continuousCohomology` (Mathlib/RepresentationTheory/Homological/ContCohomology/Basic.lean).

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: `Def_MilnorConjecture_HomogeneousCochains.lean`

All declarations live in the namespace MilnorConjecture, and the file imports only Mathlib.

Ambient setting (the `variable` binders)

Three types $k$ , $G$ , $M$ are fixed, all in the same universe $u$ . They come with these assumptions:

$k$ is a (not necessarily commutative) ring with a topology. No compatibility between the ring operations and the topology is assumed, except in classOf (see below).
$G$ is a group with a topology making it a topological group, and $G$ is locally compact. No Hausdorff, profinite, or compactness assumption is made.
$M$ is an additive commutative group and a $k$ -module, with a topology making $(M,+)$ a topological additive group and scalar multiplication $k\times M\to M$ jointly continuous.

Just before classOf, one more assumption is added: $k$ is a topological ring. Only classOf uses it.

Notation used below:

$C(X,Y)$ is the space of continuous maps $X \to Y$ with the compact-open topology.
$G^n$ means the space of functions $\{0,\dots,n-1\}\to G$ (product topology). For $n=0$ this is a one-point space whose only element is the empty tuple $()$ .

`trivialRep`

$\mathrm{triv}_k(G,M)$ is the object of Mathlib's category $\mathrm{TopRep}_k(G)$ built from $M$ with the trivial action: $g\cdot m = m$ for all $g\in G$ , $m\in M$ .

Mathlib's resolution objects $X_n := \mathrm{resolutionX}_n$ of this representation are defined recursively:

$X_0 = M$ ;
$X_{n+1} = C(G, X_n)$ , with the coinduced action $(g\cdot f)(x) = g\cdot\bigl(f(g^{-1}x)\bigr)$ .

So $X_n = C(G, C(G,\dots, C(G,M)))$ with $n$ nested copies of $C(G,\cdot)$ . Because the action on $M$ is trivial, $g$ acts on an element $\varphi\in X_n$ by

(g\cdot\varphi)(x_1)(x_2)\cdots(x_n) = \varphi(g^{-1}x_1)(g^{-1}x_2)\cdots(g^{-1}x_n).

Mathlib's differential $d_n : X_n\to X_{n+1}$ is also defined recursively:

$d_0(m) =$ the constant function $x\mapsto m$ ;
$d_{n+1}(f) = \bigl(x \mapsto f - d_n(f(x))\bigr)$ for $f\in X_{n+1}$ .

The homogeneous cochain complex in Mathlib has degree- $n$ term

\mathcal C^n = X_{n+1}^{G},

the $G$ -invariant elements of $X_{n+1}$ with the subspace topology. Note the shift: degree $n$ uses $X_{n+1}$ . Its differential $\mathcal C^n\to\mathcal C^{n+1}$ is the restriction of $d_{n+1}$ .

continuousCohomology n $= H^n$ is the $n$ -th homology of this complex, taken in the category of topological $k$ -modules. ContinuousCohomology.π is the canonical projection from the $n$ -cocycles onto $H^n$ .

`consMap`

For $n\in\mathbb N$ , $\mathrm{cons}_n : G\times G^n \to G^{n+1}$ is the continuous map

(x, (v_0,\dots,v_{n-1}))\mapsto (x, v_0,\dots,v_{n-1}).

It prepends $x$ as the new coordinate $0$ .

`curryN`

For each $n$ , $\mathrm{curry}_n$ is a continuous map

\mathrm{curry}_n : C(G^n, M)\to X_n.

The continuity is with respect to the compact-open topology on the source and the topology of $X_n$ . It is defined by recursion on $n$ :

$\mathrm{curry}_0(F) = F(())\in M = X_0$ , i.e. $F$ evaluated at the empty tuple.
$\mathrm{curry}_{n+1}(F)$ is the element of $X_{n+1} = C(G, X_n)$ given by

x\;\mapsto\;\mathrm{curry}_n\bigl(v\mapsto F(x, v_0,\dots,v_{n-1})\bigr).

Formally, it is $\mathrm{curry}_n$ composed with the ordinary currying $G\to C(G^n,M)$ of $F\circ \mathrm{cons}_n$ .

Unwinding the recursion, the first (outermost) argument is coordinate $0$ :

\mathrm{curry}_n(F)(x_0)(x_1)\cdots(x_{n-1}) = F(x_0,x_1,\dots,x_{n-1}).

The following lemmas about curryN are proved:

curryN_zero_apply: $\mathrm{curry}_0(F) = F(())$ .
curryN_succ_apply: for $F\in C(G^{n+1},M)$ and $x\in G$ ,

\mathrm{curry}_{n+1}(F)(x) = \mathrm{curry}_n\bigl(v\mapsto F(x,v)\bigr).

curryN_sub: $\mathrm{curry}_n(F-F') = \mathrm{curry}_n(F)-\mathrm{curry}_n(F')$ for all $F,F'\in C(G^n,M)$ .
curryN_zero: $\mathrm{curry}_n(0)=0$ for every $n$ .

`faceMap`

For $n\in\mathbb N$ and $i\in\{0,\dots,n\}$ , $\partial_i : G^{n+1}\to G^n$ deletes coordinate $i$ :

(y_0,\dots,y_n)\mapsto (y_0,\dots,\widehat{y_i},\dots,y_n).

Formally, $y$ is precomposed with the increasing injection $\{0,\dots,n-1\}\to\{0,\dots,n\}$ that skips $i$ .

`coboundary`

For $n\in\mathbb N$ and $F\in C(G^n,M)$ , $\delta_n F\in C(G^{n+1},M)$ is

\delta_n F = \sum_{i=0}^{n}(-1)^i\, F\circ\partial_i .

Here $(-1)^i\in\mathbb Z$ acts on $M$ as an integer multiple.

coboundary_apply states the pointwise formula. It needs only the topologies on $G$ , not the group structure:

(\delta_n F)(y_0,\dots,y_n) = \sum_{i=0}^n (-1)^i F(y_0,\dots,\widehat{y_i},\dots,y_n).

Edge case $n=0$ : $\delta_0 F$ is the constant function $y\mapsto F(())$ .

`d_curryN`

For every $n$ and every $F\in C(G^n,M)$ , Mathlib's differential satisfies

d_n\bigl(\mathrm{curry}_n F\bigr) = \mathrm{curry}_{n+1}\bigl(\delta_n F\bigr)\quad\text{in } X_{n+1}.

Here $d_n: X_n\to X_{n+1}$ is the resolution differential, not the cochain-complex differential in degree $n$ .

`translate`

For $n\in\mathbb N$ and $g\in G$ , $t_g : G^n\to G^n$ is left multiplication by $g$ in every coordinate:

t_g(v_0,\dots,v_{n-1}) = (g v_0,\dots, g v_{n-1}).

For $n=0$ it is the identity of the one-point space.

`ρ_curryN`

For every $n$ , $g\in G$ and $F\in C(G^n,M)$ , the action of $g$ on $X_n$ satisfies

g\cdot \mathrm{curry}_n(F) = \mathrm{curry}_n\bigl(F\circ t_{g^{-1}}\bigr).

The right side is the function $v\mapsto F(g^{-1}v_0,\dots,g^{-1}v_{n-1})$ .

`curryN_mem_invariants`

Suppose $F\in C(G^n,M)$ satisfies

F(gv_0,\dots,gv_{n-1}) = F(v_0,\dots,v_{n-1})\quad\text{for all } g\in G \text{ and } v\in G^n.

Then $\mathrm{curry}_n(F)$ is a $G$ -invariant element of $X_n$ .

For $n=0$ the hypothesis holds automatically, and the conclusion says $F(())\in M$ is invariant, which is automatic for the trivial action.

`classOf`

Inputs:

the ring $k$ , given explicitly;
$G$ and $M$ , given implicitly;
all of the ambient assumptions above, plus: $k$ is a topological ring;
a natural number $n$ ;
a continuous function $F\in C(G^{n+1},M)$ of $n+1$ variables;
a hypothesis $\mathrm{hinv}$ : $F$ is invariant under simultaneous left translation, i.e. $F(gv_0,\dots,gv_n)=F(v_0,\dots,v_n)$ for all $g\in G$ and $v\in G^{n+1}$ ;
a hypothesis $\mathrm{hcoc}$ : $\delta_{n+1}F = 0$ as a function on $G^{n+2}$ , i.e.

\sum_{i=0}^{n+1}(-1)^i F(y_0,\dots,\widehat{y_i},\dots,y_{n+1}) = 0\quad\text{for all } (y_0,\dots,y_{n+1})\in G^{n+2}.

Output: an element of $H^n$ , the $n$ -th continuous cohomology of the trivial representation $\mathrm{triv}_k(G,M)$ (in the Mathlib sense above).

Construction:

Let $\sigma = \mathrm{curry}_{n+1}(F)\in X_{n+1}$ . This is invariant by $\mathrm{hinv}$ , so $\sigma\in\mathcal C^n$ .
Let $\iota : k\to\mathcal C^n$ be the continuous $k$ -linear map $r\mapsto r\cdot\sigma$ .
The file proves that the complex differential kills $\sigma$ , using d_curryN and $\mathrm{hcoc}$ : $d_{n+1}(\sigma)=\mathrm{curry}_{n+2}(\delta_{n+1}F)=0$ . Hence $\iota$ composed with the differential is zero.
$\iota$ therefore lifts to a map from $k$ into the degree- $n$ cycles of the homogeneous cochain complex.
The output is $\pi_n$ applied to the image of $1\in k$ under this lift.

In other words, classOf is the cohomology class in $H^n$ of the cocycle $\sigma = \mathrm{curry}_{n+1}(F)$ , whose value is $\sigma(x_0)\cdots(x_n) = F(x_0,\dots,x_n)$ .

Edge case $n=0$ :

$F$ is a function of one variable, and $\mathrm{hinv}$ says $F(gv)=F(v)$ for all $g,v$ . Taking $g=v^{-1}$ gives $F(v) = F(1)$ , so $F$ must be constant.
$\mathrm{hcoc}$ says $F(y_1)-F(y_0)=0$ for all $y_0,y_1$ , which a constant $F$ satisfies automatically.
The output lies in $H^0$ .

In every degree, both hypotheses can be satisfied, for example by $F=0$ .

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by vatsj · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Classes of invariant homogeneous cocycles in continuous cohomology

Read-back: Def_MilnorConjecture_HomogeneousCochains.lean

Ambient setting (the variable binders)

trivialRep

consMap

curryN

faceMap

coboundary

d_curryN

translate

ρ_curryN

curryN_mem_invariants

classOf