leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.48k stars 324 forks source link

Define the Hodge star operator #17722

Open ocfnash opened 1 week ago

ocfnash commented 1 week ago

I think a fun project would be for someone to define the Hodge star operator.

The classical construction is that if $V$ is a finite-dimensional vector space of dimension $n$, then a choice of orientation together with a choice of non-degenerate symmetric bilinear form determines natural isomorphisms: $$\wedge^r V \simeq \wedge^{n-r} V$$ for $0 \le r \le n$.

Note that it is also possible to define a Hodge star operator when the bilinear form is skew-symmetric instead of symmetric. This case comes up less often but is still important (e.g., it means symplectic manifolds carry such operators, though the associated Laplacian vanishes). So we should certainly make a definition that is general enough to cover both of these cases.

Useful first results about the definition would be:

ocfnash commented 1 week ago

Corresponding thread on Zulip here.