Continuous low-degree Lie algebra cohomology with discrete coefficients

Let L be a Lie algebra carrying a topology and M a module of coefficients, regarded as a discrete space. A cochain with values in M is continuous exactly when it is locally constant, and since it is additive in each variable this is a condition at zero only:

• a one-cochain f is continuous when f vanishes near zero;
• an alternating two-cochain c is continuous when it is separately continuous, that is y ↦ c x y vanishes near zero for every x, and moreover c vanishes on a neighbourhood of (0, 0) in L × L.

These conditions define submodules continuousOneCochain and continuousTwoCochain of Mathlib's low-degree Chevalley–Eilenberg cochains, without putting a topology on M. When L is a topological additive group, they are precisely the cochains which are continuous for any discrete topology on M (mem_continuousOneCochain_iff_continuous, mem_continuousTwoCochain_iff_continuous). For a basis of neighbourhoods of zero, such as the order filtration of formal currents, the condition on two-cochains becomes the familiar criterion: separate continuity, together with one basic neighbourhood on which the cochain vanishes identically (mem_continuousTwoCochain_iff_of_hasBasis).

If the bracket of L is continuous and every element of M is annihilated by a neighbourhood of zero (for instance if M is a trivial module), then the differential d₁₂ sends continuous one-cochains to continuous two-cocycles (d₁₂_mem_continuousTwoCocycle). The continuous second cohomology continuousSecondCohomology is the quotient of continuous two-cocycles by those coboundaries of continuous one-cochains which are themselves continuous; under the hypotheses of d₁₂_mem_continuousTwoCocycle these are all coboundaries of continuous one-cochains. With trivial coefficients it is the receptacle for the classes of continuously split central extensions of a topological Lie algebra, such as the formal loop algebra, by a discrete trivial module.

Main definitions

• TauCeti.LieModule.Cohomology.continuousOneCochain: one-cochains vanishing near zero.
• TauCeti.LieModule.Cohomology.continuousTwoCochain: continuous alternating two-cochains.
• TauCeti.LieModule.Cohomology.continuousTwoCocycle: continuous two-cocycles.
• TauCeti.LieModule.Cohomology.continuousTwoCoboundary: the coboundaries of continuous one-cochains which are continuous two-cocycles.
• TauCeti.LieModule.Cohomology.continuousSecondCohomology: their quotient.

Continuous two-cochains pull back along continuous Lie algebra morphisms and push forward along linear maps of coefficients (twoCochainMap_mem_continuousTwoCochain), and with trivial coefficients so do continuous two-cocycles (twoCochainMap_mem_continuousTwoCocycle, and twoCochainMap_id_mem_continuousTwoCocycle for coefficient maps alone). Continuous one-cochains push forward along linear maps of coefficients (comp_mem_continuousOneCochain).

Main results

• TauCeti.LieModule.Cohomology.mem_continuousTwoCochain_iff_continuous: the defining condition is joint continuity for a discrete topology on the coefficients.
• TauCeti.LieModule.Cohomology.mem_continuousTwoCochain_iff_of_hasBasis: the criterion in terms of a basis of neighbourhoods of zero.
• TauCeti.LieModule.Cohomology.continuousTwoCochain_ext_on: continuous two-cochains agreeing on a dense subset are equal.
• TauCeti.LieModule.Cohomology.d₁₂_mem_continuousTwoCocycle: coboundaries of continuous one-cochains are continuous two-cocycles.

References

• E. Frenkel, Langlands Correspondence for Loop Groups, §1.3, for continuous cohomology of the formal loop algebra with trivial coefficients.

def TauCeti.LieModule.Cohomology.continuousOneCochain (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] : Submodule R (LieModule.Cohomology.oneCochain R L M)

Continuous one-cochains with discrete coefficients: the linear maps L → M vanishing on a neighbourhood of zero.

def TauCeti.LieModule.Cohomology.continuousTwoCochain (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] : Submodule R ↥(LieModule.Cohomology.twoCochain R L M)

Continuous alternating two-cochains with discrete coefficients: the alternating bilinear maps c such that every partial map c x vanishes near zero, and c vanishes on a neighbourhood of (0, 0).

theorem TauCeti.LieModule.Cohomology.mem_continuousOneCochain_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] {f : LieModule.Cohomology.oneCochain R L M} : f ∈ continuousOneCochain R L M ↔ ∀ᶠ (x : L) in nhds 0, f x = 0

theorem TauCeti.LieModule.Cohomology.mem_continuousTwoCochain_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] {c : ↥(LieModule.Cohomology.twoCochain R L M)} : c ∈ continuousTwoCochain R L M ↔ (∀ (x : L), ∀ᶠ (y : L) in nhds 0, (c x) y = 0) ∧ ∀ᶠ (p : L × L) in nhds 0, (c p.1) p.2 = 0

theorem TauCeti.LieModule.Cohomology.apply_mem_continuousOneCochain {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] {c : ↥(LieModule.Cohomology.twoCochain R L M)} (hc : c ∈ continuousTwoCochain R L M) (x : L) : c x ∈ continuousOneCochain R L M

The partial maps of a continuous two-cochain are continuous one-cochains.

theorem TauCeti.LieModule.Cohomology.mem_continuousTwoCochain_iff_of_hasBasis {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] {ι : Type u_4} {p : ι → Prop} {s : ι → Set L} (h : (nhds 0).HasBasis p s) {c : ↥(LieModule.Cohomology.twoCochain R L M)} : c ∈ continuousTwoCochain R L M ↔ (∀ (x : L), ∃ (i : ι), p i ∧ ∀ y ∈ s i, (c x) y = 0) ∧ ∃ (i : ι), p i ∧ ∀ u ∈ s i, ∀ v ∈ s i, (c u) v = 0

The joint-continuity criterion. Given a basis s of neighbourhoods of zero, a two-cochain is continuous exactly when each partial map vanishes on some basic neighbourhood, and the cochain vanishes on s i × s i for some basic neighbourhood s i.

theorem TauCeti.LieModule.Cohomology.mem_continuousOneCochain_iff_continuous {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup L] [TopologicalSpace M] [DiscreteTopology M] {f : LieModule.Cohomology.oneCochain R L M} : f ∈ continuousOneCochain R L M ↔ Continuous ⇑f

A one-cochain vanishes near zero exactly when it is continuous for a discrete topology on the coefficients.

theorem TauCeti.LieModule.Cohomology.mem_continuousTwoCochain_iff_continuous {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup L] [TopologicalSpace M] [DiscreteTopology M] {c : ↥(LieModule.Cohomology.twoCochain R L M)} : c ∈ continuousTwoCochain R L M ↔ Continuous fun (p : L × L) => (c p.1) p.2

Continuity of two-cochains. The defining condition of continuousTwoCochain is joint continuity on L × L for a discrete topology on the coefficients.

theorem TauCeti.LieModule.Cohomology.continuousTwoCochain_ext_on {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup L] {c d : ↥(LieModule.Cohomology.twoCochain R L M)} (hc : c ∈ continuousTwoCochain R L M) (hd : d ∈ continuousTwoCochain R L M) {s : Set L} (hs : Dense s) (h : ∀ x ∈ s, ∀ y ∈ s, (c x) y = (d x) y) : c = d

Continuous two-cochains are determined on a dense set. Two continuous two-cochains on a topological Lie algebra which agree on all pairs of elements of a dense subset are equal.

theorem TauCeti.LieModule.Cohomology.twoCochainMap_mem_continuousTwoCochain {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] {L' : Type u_4} {M' : Type u_5} [LieRing L'] [LieAlgebra R L'] [TopologicalSpace L'] [AddCommGroup M'] [Module R M'] (e : M →ₗ[R] M') {φ : L' →ₗ⁅R⁆ L} (hφ : Continuous ⇑φ) {c : ↥(LieModule.Cohomology.twoCochain R L M)} (hc : c ∈ continuousTwoCochain R L M) : (LieModule.Cohomology.twoCochainMap e φ) c ∈ continuousTwoCochain R L' M'

Continuous two-cochains pull back along continuous morphisms. Pulling a continuous two-cochain back along a continuous Lie algebra morphism φ and pushing it forward along a linear map e of coefficients gives a continuous two-cochain.

theorem TauCeti.LieModule.Cohomology.comp_lieHom_mem_continuousOneCochain {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] {L' : Type u_4} [LieRing L'] [LieAlgebra R L'] [TopologicalSpace L'] {φ : L' →ₗ⁅R⁆ L} (hφ : Continuous ⇑φ) {f : LieModule.Cohomology.oneCochain R L M} (hf : f ∈ continuousOneCochain R L M) : f ∘ₗ ↑φ ∈ continuousOneCochain R L' M

Pulling a continuous one-cochain back along a continuous Lie algebra morphism preserves continuity with discrete coefficients.

theorem TauCeti.LieModule.Cohomology.comp_mem_continuousOneCochain {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] {M' : Type u_5} [AddCommGroup M'] [Module R M'] (e : M →ₗ[R] M') {f : LieModule.Cohomology.oneCochain R L M} (hf : f ∈ continuousOneCochain R L M) : e ∘ₗ f ∈ continuousOneCochain R L M'

Pushing a continuous one-cochain forward along a linear map e of coefficients gives a continuous one-cochain.

def TauCeti.LieModule.Cohomology.continuousTwoCocycle (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Submodule R ↥(LieModule.Cohomology.twoCochain R L M)

Continuous two-cocycles: continuous two-cochains annihilated by the differential d₂₃.

def TauCeti.LieModule.Cohomology.continuousTwoCoboundary (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Submodule R ↥(continuousTwoCocycle R L M)

The coboundaries of continuous one-cochains which are themselves continuous, as a submodule of the continuous two-cocycles. By d₁₂_mem_continuousTwoCocycle, this is every coboundary of a continuous one-cochain when the bracket of L is continuous and every element of M is annihilated by a neighbourhood of zero.

@[reducible, inline]

abbrev TauCeti.LieModule.Cohomology.continuousSecondCohomology (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Type (max u_2 u_3)

Continuous second Lie algebra cohomology with discrete coefficients: continuous two-cocycles modulo the continuous coboundaries of continuous one-cochains.

def TauCeti.LieModule.Cohomology.continuousSecondCohomologyMk (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : ↥(continuousTwoCocycle R L M) →ₗ[R] continuousSecondCohomology R L M

The quotient map from continuous two-cocycles to continuous second cohomology.

theorem TauCeti.LieModule.Cohomology.continuousSecondCohomologyMk_eq_mkQ (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : continuousSecondCohomologyMk R L M = (continuousTwoCoboundary R L M).mkQ

The cohomology quotient map is the submodule quotient map.

theorem TauCeti.LieModule.Cohomology.mem_continuousTwoCocycle_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {c : ↥(LieModule.Cohomology.twoCochain R L M)} : c ∈ continuousTwoCocycle R L M ↔ c ∈ continuousTwoCochain R L M ∧ c ∈ LieModule.Cohomology.twoCocycle R L M

theorem TauCeti.LieModule.Cohomology.mem_continuousTwoCoboundary_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {c : ↥(continuousTwoCocycle R L M)} : c ∈ continuousTwoCoboundary R L M ↔ ∃ f ∈ continuousOneCochain R L M, (LieModule.Cohomology.d₁₂ R L M) f = ↑c

theorem TauCeti.LieModule.Cohomology.d₁₂_mem_continuousTwoCocycle {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (hL : Continuous fun (p : L × L) => ⁅p.1, p.2⁆) (hM : ∀ (m : M), ∀ᶠ (x : L) in nhds 0, ⁅x, m⁆ = 0) {f : LieModule.Cohomology.oneCochain R L M} (hf : f ∈ continuousOneCochain R L M) : (LieModule.Cohomology.d₁₂ R L M) f ∈ continuousTwoCocycle R L M

Coboundaries of continuous cochains are continuous cocycles. If the bracket of L is continuous and every element of M is annihilated by a neighbourhood of zero, the differential of a continuous one-cochain is a continuous two-cocycle.

theorem TauCeti.LieModule.Cohomology.twoCochainMap_mem_continuousTwoCocycle {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {L' : Type u_4} {M' : Type u_5} [LieRing L'] [LieAlgebra R L'] [TopologicalSpace L'] [AddCommGroup M'] [Module R M'] [LieRingModule L' M'] [LieModule R L' M'] [LieModule.IsTrivial L M] [LieModule.IsTrivial L' M'] (e : M →ₗ[R] M') {φ : L' →ₗ⁅R⁆ L} (hφ : Continuous ⇑φ) {c : ↥(LieModule.Cohomology.twoCochain R L M)} (hc : c ∈ continuousTwoCocycle R L M) : (LieModule.Cohomology.twoCochainMap e φ) c ∈ continuousTwoCocycle R L' M'

With trivial coefficients, pulling a continuous two-cocycle back along a continuous Lie algebra morphism and pushing it forward along a linear map of coefficients gives a continuous two-cocycle.

theorem TauCeti.LieModule.Cohomology.twoCochainMap_id_mem_continuousTwoCocycle {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M' : Type u_4} [AddCommGroup M'] [Module R M'] [LieRingModule L M'] [LieModule R L M'] [LieModule.IsTrivial L M] [LieModule.IsTrivial L M'] (e : M →ₗ[R] M') {c : ↥(LieModule.Cohomology.twoCochain R L M)} (hc : c ∈ continuousTwoCocycle R L M) : (LieModule.Cohomology.twoCochainMap e LieHom.id) c ∈ continuousTwoCocycle R L M'

With trivial coefficients, pushing a continuous two-cocycle forward along a linear map e of coefficients gives a continuous two-cocycle.

def TauCeti.LieModule.Cohomology.continuousSecondCohomologyLift {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : Type u_4} [AddCommGroup N] [Module R N] (g : ↥(continuousTwoCocycle R L M) →ₗ[R] N) (h : ∀ c ∈ continuousTwoCoboundary R L M, g c = 0) : continuousSecondCohomology R L M →ₗ[R] N

Descend a linear map on continuous two-cocycles that vanishes on coboundaries of continuous one-cochains to continuous second cohomology.

@[simp]

theorem TauCeti.LieModule.Cohomology.continuousSecondCohomologyLift_mk {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : Type u_4} [AddCommGroup N] [Module R N] (g : ↥(continuousTwoCocycle R L M) →ₗ[R] N) (h : ∀ c ∈ continuousTwoCoboundary R L M, g c = 0) (c : ↥(continuousTwoCocycle R L M)) : (continuousSecondCohomologyLift g h) ((continuousSecondCohomologyMk R L M) c) = g c

theorem TauCeti.LieModule.Cohomology.continuousSecondCohomologyLift_unique {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : Type u_4} [AddCommGroup N] [Module R N] (g : ↥(continuousTwoCocycle R L M) →ₗ[R] N) (h : ∀ c ∈ continuousTwoCoboundary R L M, g c = 0) (φ : continuousSecondCohomology R L M →ₗ[R] N) (hφ : φ ∘ₗ continuousSecondCohomologyMk R L M = g) : φ = continuousSecondCohomologyLift g h

A linear map from continuous second cohomology is determined by its values on cocycle representatives.

theorem TauCeti.LieModule.Cohomology.continuousSecondCohomology_hom_ext {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : Type u_4} [AddCommGroup N] [Module R N] {g₁ g₂ : continuousSecondCohomology R L M →ₗ[R] N} (h : g₁ ∘ₗ continuousSecondCohomologyMk R L M = g₂ ∘ₗ continuousSecondCohomologyMk R L M) : g₁ = g₂

Two linear maps out of continuous second cohomology agree once they agree on cocycle representatives.

theorem TauCeti.LieModule.Cohomology.continuousSecondCohomology_hom_ext_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : Type u_4} [AddCommGroup N] [Module R N] {g₁ g₂ : continuousSecondCohomology R L M →ₗ[R] N} : g₁ = g₂ ↔ g₁ ∘ₗ continuousSecondCohomologyMk R L M = g₂ ∘ₗ continuousSecondCohomologyMk R L M

@[simp]

theorem TauCeti.LieModule.Cohomology.continuousSecondCohomologyMk_eq_zero_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(continuousTwoCocycle R L M)) : (continuousSecondCohomologyMk R L M) c = 0 ↔ ∃ f ∈ continuousOneCochain R L M, (LieModule.Cohomology.d₁₂ R L M) f = ↑c

theorem TauCeti.LieModule.Cohomology.continuousSecondCohomologyMk_eq_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c d : ↥(continuousTwoCocycle R L M)) : (continuousSecondCohomologyMk R L M) c = (continuousSecondCohomologyMk R L M) d ↔ ∃ f ∈ continuousOneCochain R L M, (LieModule.Cohomology.d₁₂ R L M) f = ↑(c - d)

Two continuous cocycles represent the same class exactly when their difference is the coboundary of a continuous one-cochain.

theorem TauCeti.LieModule.Cohomology.continuousSecondCohomologyMk_surjective {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Function.Surjective ⇑(continuousSecondCohomologyMk R L M)

Every continuous second cohomology class has a continuous cocycle representative.