Abstract data for the Hodge-theoretic setting near degree $k+1$: three inner-product spaces $\Omega^k, \Omega^{k+1}, \Omega^{k+2}$ with exterior derivatives $d_k, d_{k+1}$ satisfying $d^2 = 0$ and their formal adjoints $d^*$.
- Ωk : Type u_1
- Ωk1 : Type u_2
- Ωk2 : Type u_3
- nacg_k : NormedAddCommGroup self.Ωk
- ips_k : InnerProductSpace ℝ self.Ωk
- nacg_k1 : NormedAddCommGroup self.Ωk1
- ips_k1 : InnerProductSpace ℝ self.Ωk1
- nacg_k2 : NormedAddCommGroup self.Ωk2
- ips_k2 : InnerProductSpace ℝ self.Ωk2
Instances For
The Hodge Laplacian $\Delta = d\,d^* + d^*\,d$ on $\Omega^{k+1}$.
Instances For
A form $\alpha$ is harmonic iff $\Delta \alpha = 0$.
Instances For
Existence data for the Hodge decomposition: a Green operator $G$ and harmonic projection $H$ such that $\alpha = H\alpha + d\,d^* G\alpha + d^* d\, G\alpha$, with $H\alpha$ harmonic, closed, and co-closed.
- H_harmonic (α : hd.Ωk1) : hd.IsHarmonic (self.H α)
Instances For
A harmonic form that is also exact ($h = d\beta$) must be zero, by the orthogonality $\langle d\beta, h\rangle = \langle \beta, d^* h\rangle = 0$.
The space of harmonic forms is closed under subtraction.
Uniqueness helper: if $h_1 + d\beta_1 = h_2 + d\beta_2$ with both $h_i$ harmonic, then $h_1 = h_2$ (since their difference is harmonic and exact).
Existence and uniqueness of the harmonic representative: every closed form $\alpha$ decomposes uniquely as $\alpha = h + d\beta$ with $h$ harmonic.