De Rham cohomology in degree zero

A 0-form is a function, and its exterior derivative is the differential of that function. A differentiable function has zero differential exactly when it is locally constant, so the closed smooth 0-forms are the locally constant real functions. Since there are no exact forms in degree zero, this identifies H⁰_dR(M) with LocallyConstant M ℝ; on a connected manifold it is one-dimensional.

On a preconnected noncompact manifold a locally constant function is constant, and a nonzero constant does not have compact support, so compactly supported cohomology H⁰_c(M) vanishes.

Everything holds on C² manifolds with boundary or corners, without finite dimensionality, separation or completeness hypotheses on the model.

Main declarations

• TauCeti.mem_closedForms_zero_iff: a smooth 0-form is closed exactly when its function is locally constant.
• TauCeti.closedFormsZeroEquiv: closed smooth 0-forms are locally constant functions.
• TauCeti.deRhamCohomologyZeroEquiv: H⁰_dR(M) ≃ₗ[ℝ] LocallyConstant M ℝ.
• TauCeti.deRhamCohomology.const: the degree-zero class of a constant real function.
• TauCeti.deRhamCohomology.exists_eq_const: on a preconnected manifold, every degree-zero class is constant.
• TauCeti.deRhamCohomology.const_injective: on a nonempty manifold, distinct constants have distinct degree-zero classes.
• TauCeti.finrank_deRhamCohomology_zero: H⁰_dR(M) has dimension one when M is connected.
• TauCeti.finrank_deRhamCohomology_zero_of_discreteTopology: on a discrete manifold, finrank ℝ H⁰_dR(M) = Nat.card M, so H⁰_dR(M) has dimension the number of points when M is finite (both sides are 0 when M is infinite).
• TauCeti.subsingleton_compactlySupportedDeRhamCohomology_zero: H⁰_c(M) = 0 when M is preconnected and noncompact.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 17, cohomology in degree zero, and section Cohomology with Compact Support.

theorem TauCeti.mem_closedForms_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] (φ : SmoothForm I M ℝ 0) : φ ∈ closedForms I M 0 ↔ IsLocallyConstant fun (x : M) => (↑φ x) 0

A smooth real 0-form is closed exactly when its function is locally constant.

noncomputable def TauCeti.closedFormsZeroEquiv {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] : ↥(closedForms I M 0) ≃ₗ[ℝ] LocallyConstant M ℝ

Closed smooth real 0-forms are exactly the locally constant real functions.

@[simp]

theorem TauCeti.closedFormsZeroEquiv_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] (φ : ↥(closedForms I M 0)) (x : M) : ((closedFormsZeroEquiv I M) φ) x = (↑↑φ x) 0

The locally constant function of a closed 0-form is its value on the empty tuple.

@[simp]

theorem TauCeti.coe_closedFormsZeroEquiv_symm_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] (f : LocallyConstant M ℝ) : ↑↑((closedFormsZeroEquiv I M).symm f) = RoughForm.ofFunction I ⇑f

The closed 0-form of a locally constant function is its 0-form.

theorem TauCeti.deRhamCohomology.mk_zero_injective {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] : Function.Injective ⇑(mk I 0)

In degree zero the cycle-class map is injective, since there are no exact 0-forms.

noncomputable def TauCeti.deRhamCohomologyZeroEquiv {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] : deRhamCohomology I M 0 ≃ₗ[ℝ] LocallyConstant M ℝ

Degree-zero de Rham cohomology. H⁰_dR(M) is the space of locally constant real functions on M, for any C² manifold with boundary or corners.

@[simp]

theorem TauCeti.deRhamCohomologyZeroEquiv_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] (φ : ↥(closedForms I M 0)) (x : M) : ((deRhamCohomologyZeroEquiv I M) ((deRhamCohomology.mk I 0) φ)) x = (↑↑φ x) 0

The class of a closed 0-form corresponds to its locally constant function.

@[simp]

theorem TauCeti.deRhamCohomologyZeroEquiv_symm_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] (f : LocallyConstant M ℝ) : (deRhamCohomologyZeroEquiv I M).symm f = (deRhamCohomology.mk I 0) ((closedFormsZeroEquiv I M).symm f)

A locally constant function corresponds to the class of its 0-form.

noncomputable def TauCeti.deRhamCohomology.const {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] : ℝ →ₗ[ℝ] deRhamCohomology I M 0

The degree-zero de Rham class of a constant real function, as a linear map.

theorem TauCeti.deRhamCohomology.const_eq_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] (r : ℝ) : (const I M) r = (mk I 0) ((closedFormsZeroEquiv I M).symm (LocallyConstant.const M r))

A constant cohomology class is represented by the corresponding constant closed zero-form.

@[simp]

theorem TauCeti.deRhamCohomology.deRhamCohomologyZeroEquiv_const {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] (r : ℝ) : (deRhamCohomologyZeroEquiv I M) ((const I M) r) = LocallyConstant.const M r

The degree-zero identification takes a constant class to its constant function.

theorem TauCeti.deRhamCohomology.const_injective {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] [Nonempty M] : Function.Injective ⇑(const I M)

On a nonempty manifold, distinct real constants have distinct degree-zero classes.

theorem TauCeti.deRhamCohomology.exists_eq_const {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] [PreconnectedSpace M] (c : deRhamCohomology I M 0) : ∃ (r : ℝ), c = (const I M) r

On a preconnected manifold, every degree-zero de Rham class is the class of a constant function.

theorem TauCeti.finrank_deRhamCohomology_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] [ConnectedSpace M] : Module.finrank ℝ (deRhamCohomology I M 0) = 1

On a connected manifold, degree-zero de Rham cohomology is one-dimensional.

theorem TauCeti.finrank_deRhamCohomology_zero_of_discreteTopology {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] [DiscreteTopology M] : Module.finrank ℝ (deRhamCohomology I M 0) = Nat.card M

On a discrete manifold, degree-zero de Rham cohomology has dimension the number of points, since every real function is locally constant. For an infinite manifold both sides are 0 by convention.

theorem TauCeti.eq_zero_of_mem_compactlySupportedClosedForms_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] [PreconnectedSpace M] [NoncompactSpace M] {φ : SmoothForm I M ℝ 0} (hφ : φ ∈ compactlySupportedClosedForms I M 0) : φ = 0

On a preconnected noncompact manifold, the only compactly supported closed 0-form is zero: its function is locally constant, hence constant, and a nonzero constant function on a noncompact space does not have compact support.

theorem TauCeti.subsingleton_compactlySupportedDeRhamCohomology_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] [PreconnectedSpace M] [NoncompactSpace M] : Subsingleton (compactlySupportedDeRhamCohomology I M 0)

Compactly supported cohomology in degree zero. On a preconnected noncompact manifold, H⁰_c(M) vanishes.