The de Rham complex and its cohomology

The exterior derivative on smooth real-valued forms defines the nonnegative de Rham cochain complex. Its cohomology is Mathlib's categorical homology, with a concrete linear class map from closed forms, HomologicalComplex.moduleCatHomologyClass of their inclusion. This map is surjective and its kernel consists exactly of exact forms; exact forms in degree zero are zero, and exact one-forms are differentials of smooth real functions. On a manifold modelled on a finite-dimensional space every alternating form of degree above the dimension is zero, so de Rham cohomology vanishes there.

The construction applies to manifolds of class C² with corners and does not require finite dimensionality, separation, or completeness of the model space.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 17.
• Mathlib's CochainComplex.of provides the complex.

noncomputable def TauCeti.deRhamComplex {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] : CochainComplex (ModuleCat ℝ) ℕ

The nonnegative cochain complex of smooth real-valued differential forms.

noncomputable def TauCeti.deRhamComplexXIso {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : (deRhamComplex I M).X k ≅ ↧(SmoothForm I M ℝ k)

The canonical identification of the degree-k object with smooth k-forms. This isomorphism makes the form carrier available without unfolding the complex.

theorem TauCeti.deRhamComplex_d {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : CategoryTheory.CategoryStruct.comp ((deRhamComplex I M).d k (k + 1)) (deRhamComplexXIso I (k + 1)).hom = CategoryTheory.CategoryStruct.comp (deRhamComplexXIso I k).hom (ModuleCat.ofHom (mextDerivₗ I k))

Under the canonical identifications of the objects, the differential is the exterior derivative.

theorem TauCeti.deRhamComplex_d_assoc {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) {Z : ModuleCat ℝ} (h : ↧(SmoothForm I M ℝ (k + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((deRhamComplex I M).d k (k + 1)) (CategoryTheory.CategoryStruct.comp (deRhamComplexXIso I (k + 1)).hom h) = CategoryTheory.CategoryStruct.comp (deRhamComplexXIso I k).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (mextDerivₗ I k)) h)

Under the canonical identifications of the objects, the differential is the exterior derivative.

theorem TauCeti.deRhamComplex_d_apply {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) (x : ↑((deRhamComplex I M).X k)) : (CategoryTheory.ConcreteCategory.hom ((deRhamComplex I M).d k (k + 1))) x = (CategoryTheory.ConcreteCategory.hom (deRhamComplexXIso I (k + 1)).inv) ((mextDerivₗ I k) ((CategoryTheory.ConcreteCategory.hom (deRhamComplexXIso I k).hom) x))

The differential of the de Rham complex, evaluated on an element.

noncomputable def TauCeti.closedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : Submodule ℝ (SmoothForm I M ℝ k)

The submodule of smooth forms whose exterior derivative vanishes.

@[simp]

theorem TauCeti.mem_closedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {k : ℕ} (φ : SmoothForm I M ℝ k) : φ ∈ closedForms I M k ↔ mextDeriv ↑φ = 0

A smooth form is closed precisely when its exterior derivative vanishes.

theorem TauCeti.mem_closedForms_iff_mextDerivₗ_eq_zero {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {k : ℕ} (φ : SmoothForm I M ℝ k) : φ ∈ closedForms I M k ↔ (mextDerivₗ I k) φ = 0

A smooth form is closed precisely when its exterior derivative, as a smooth form, vanishes.

noncomputable def TauCeti.exactForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : Submodule ℝ (SmoothForm I M ℝ k)

Exact forms are exterior derivatives of smooth forms in positive degree, and zero in degree zero.

@[simp]

theorem TauCeti.exactForms_zero {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] : exactForms I M 0 = ⊥

There are no nonzero exact forms in degree zero.

@[simp]

theorem TauCeti.exactForms_succ {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : exactForms I M (k + 1) = (mextDerivₗ I k).range

In positive degree, exact forms are the range of the exterior derivative.

theorem TauCeti.exists_contMDiff_mextDeriv_eq_of_mem_exactForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {φ : SmoothForm I M ℝ 1} (hφ : φ ∈ exactForms I M 1) : ∃ (f : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f ∧ mextDeriv (RoughForm.ofFunction I f) = ↑φ

An exact smooth real one-form is the differential of a smooth real function. This identifies its smooth zero-form primitive with a function and requires no finite dimensionality, separation, connectedness, or completeness assumptions.

theorem TauCeti.exactForms_le_closedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : exactForms I M k ≤ closedForms I M k

An exact smooth form is closed.

theorem TauCeti.mextDerivₗ_mem_closedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) (φ : SmoothForm I M ℝ k) : (mextDerivₗ I k) φ ∈ closedForms I M (k + 1)

The exterior derivative of a smooth form is closed.

theorem TauCeti.mem_closedForms_of_finrank_le {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [FiniteDimensional ℝ E] {k : ℕ} (h : Module.finrank ℝ E ≤ k) (φ : SmoothForm I M ℝ k) : φ ∈ closedForms I M k

On a manifold of finite dimension at most k, every smooth k-form is closed.

@[reducible, inline]

abbrev TauCeti.deRhamCohomology {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : Type (max u_1 u_3)

De Rham cohomology is the categorical homology of the de Rham complex.

theorem TauCeti.deRhamComplex_d_eq_zero_of_mem_closedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) {φ : SmoothForm I M ℝ k} (hφ : φ ∈ closedForms I M k) : (CategoryTheory.ConcreteCategory.hom ((deRhamComplex I M).d k (k + 1))) ((CategoryTheory.ConcreteCategory.hom (deRhamComplexXIso I k).inv) φ) = 0

A closed form, viewed in the de Rham complex, is killed by the differential.

noncomputable def TauCeti.deRhamCohomology.mk {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : ↥(closedForms I M k) →ₗ[ℝ] deRhamCohomology I M k

The cohomology class of a closed smooth form, the homology class of the corresponding cycle of the de Rham complex.

theorem TauCeti.deRhamCohomology.mk_eq_moduleCatHomologyClass {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : mk I k = HomologicalComplex.moduleCatHomologyClass (deRhamComplex I M) ⋯ (ModuleCat.Hom.hom (deRhamComplexXIso I k).inv ∘ₗ (closedForms I M k).subtype) ⋯

The class map is the homology class map of the inclusion of closed forms into the de Rham complex.

theorem TauCeti.deRhamCohomology.mk_surjective {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : Function.Surjective ⇑(mk I k)

Every de Rham cohomology class is represented by a closed smooth form.

@[simp]

theorem TauCeti.deRhamCohomology.mk_eq_zero_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) (φ : ↥(closedForms I M k)) : (mk I k) φ = 0 ↔ ↑φ ∈ exactForms I M k

A closed form represents zero precisely when it is exact.

theorem TauCeti.deRhamCohomology.ker_mk {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : (mk I k).ker = Submodule.comap (closedForms I M k).subtype (exactForms I M k)

The kernel of the cycle-class map is exactly the submodule of exact forms inside closed forms.

theorem TauCeti.subsingleton_deRhamCohomology_of_finrank_lt {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [FiniteDimensional ℝ E] {k : ℕ} (hk : Module.finrank ℝ E < k) : Subsingleton (deRhamCohomology I M k)

De Rham cohomology vanishes in degrees above the dimension of the model, where every alternating form is zero.