De Rham cohomology of a normed space

A real normed space E, viewed as a manifold over its own model 𝓘(ℝ, E), is star-convex about the origin. The Poincaré lemma (StarConvex.exists_contDiffOn_forall_extDeriv_eq) therefore provides a smooth primitive for every closed smooth form of positive degree, so the de Rham cohomology of E vanishes in every positive degree. Together with the degree-zero computation TauCeti.finrank_deRhamCohomology_zero, this computes H^•_dR(E) completely.

No finite dimensionality or completeness of E is needed: the coefficients are real, and the primitive is an integral of real-valued alternating maps.

Main declarations

• TauCeti.exactForms_succ_eq_closedForms_normedSpace: every closed smooth form of positive degree on E is exact.
• TauCeti.subsingleton_deRhamCohomology_normedSpace: H^(k+1)_dR(E) = 0.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 17, the Poincaré lemma.

theorem TauCeti.exactForms_succ_eq_closedForms_normedSpace (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (k : ℕ) : exactForms (modelWithCornersSelf ℝ E) E (k + 1) = closedForms (modelWithCornersSelf ℝ E) E (k + 1)

The Poincaré lemma on a normed space. Every closed smooth real form of positive degree on E is the exterior derivative of a smooth form.

theorem TauCeti.subsingleton_deRhamCohomology_normedSpace (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (k : ℕ) : Subsingleton (deRhamCohomology (modelWithCornersSelf ℝ E) E (k + 1))

The de Rham cohomology of a normed space vanishes in positive degrees.