Home

Welcome to the DeRhamCohomology wiki!

Design choices

• Use ContinuousAlternatingMap for differential forms.

Roadmap (TODO: turn into a blueprint)

• ContinuousAlternatingMaps on NormedSpaces

• Exterior derivative of E -> ContinuousAlternatingMap (Fin n) E F.

  • Inserting a vector field in a form.

• Exterior derivative is a functor (ext. deriv of the pullback).

• Ext. deriv ^ 2 = 0.

• Vector bundle of continuous alternating maps (there is a draft in HM-alternating-bundle)

• Rephrase everything for manifolds.

• Poincaré lemma (H^k(disk) = 0).

• Wedge product

• d(ω ∧ η) = ...

• Cup product of cohomologies.

• Graded ring structure on cohomologies.

• Link to category theory library (?).

• (optional): pairing with k vector fields

  • the result depends on the wedge product of these vector fields only (?).

• Coordinate approach (f dx₁ ∧ dx₃ + g dx₃ ∧ dx₂).