15class HasCoboundary (α : Type) where 16 d : ∀ {k : Nat}, DForm α k → DForm α (k+1) 17 d_zero : ∀ {k}, d (fun (_ : Simplex α k) => 0) = (fun _ => 0) 18 19/-- Hodge star interface (metric/constitutive). 20 We expose linearity and a signature-correct involution law `⋆⋆ = σ(k) · id`. 21 The `σ` function captures the metric signature effect; for example in 4D 22 Riemannian one may take `σ k = (-1)^(k*(4-k))`, while in Lorentzian (−,+,+,+) 23 one would use `σ k = (-1)^(k*(4-k)+1)`. We keep this abstract so concrete 24 meshes can choose either. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.