WikiLeanRecent changes · Flags · Stats · About

Diff — Hodge star operator

Revision #1297 → #2033 · back to history

modifiedHodge star operator5e07b2cd8fc9
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Hodge star operator is defined anywhere in Mathlib4 (no `hodgeStar`/`Hodge` results in `Mathlib/`).
status—not_formalized
modifiedHodge dual in 3D Euclidean spacea9994afb7209
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has `crossProduct` and `Orientation.volumeForm`, but no Hodge-dual interpretation linking bivectors to vectors in 3D.
status—not_formalized
modifiedInduced inner product on k-vectorsc7e46dcc6439
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has `ExteriorPower` and inner product spaces but no induced inner product on the exterior power of an inner product space.
status—not_formalized
modifiedUnit n-vectorb521f60c091e
FieldFrom #1297To #2033
mathlib.decl—Orientation.volumeForm
mathlib.match_kind——
mathlib.module—Mathlib.Analysis.InnerProductSpace.Orientation
note—The dual notion of the unit top-form is captured by `Orientation.volumeForm`, but the unit n-vector itself in the exterior algebra is not defined.
status—partial
modifiedRight complement of a basis element3a9880fc404f
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No notion of right complement on basis elements of an exterior algebra appears in Mathlib.
status—not_formalized
modifiedHodge star operator (constructive formula)97169a4a4071
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Hodge star is defined on the exterior algebra in Mathlib.
status—not_formalized
modifiedDefining property of Hodge star9cac4b3f3826
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The defining identity α∧⋆β = ⟨α,β⟩ω is absent from Mathlib since the Hodge star itself is not formalized.
status—not_formalized
modifiedVolume form dual to unit n-vector3c70350d831c
FieldFrom #1297To #2033
mathlib.decl—Orientation.volumeForm
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.InnerProductSpace.Orientation
note—`Orientation.volumeForm` is the canonical top-dimensional alternating form on an oriented real inner product space.
status—formalized
modifiedDual property of Hodge star3cc8b830ab7a
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Without a Hodge star in Mathlib, the dual property ⟨⋆α,β⟩ω = α∧β is also absent.
status—not_formalized
modifiedHodge dual on orthonormal basis k-vectors4c5cfa3b2171
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formula for the Hodge star on orthonormal k-vectors in Mathlib.
status—not_formalized
modifiedHodge dual via geometric product5806fa8fbbcb
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has `CliffordAlgebra` but no Hodge dual expressed via geometric product.
status—not_formalized
modifiedLeft Hodge dual6f6954d85225
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No left Hodge dual in Mathlib.
status—not_formalized
modifiedHodge star is an isometrye9c1cd9cb50e
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Hodge star, hence no isometry property in Mathlib.
status—not_formalized
modifiedGeometric correspondence of Hodge star8de35b93697b
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The geometric (orthogonal-complement) characterization of the Hodge star is not in Mathlib.
status—not_formalized
modifiedHodge star in two dimensionscdbafd0ba7f3
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Hodge star in Mathlib; the 2D rotation-by-90° comes from `Orientation.rightAngleRotation` but is not framed as a Hodge dual.
status—not_formalized
modifiedHodge star in three dimensionsd481fb3d090f
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has the 3D `crossProduct` but no Hodge star tying it to bivectors.
status—not_formalized
modifiedHodge star and cross product57ed69aa8615
FieldFrom #1297To #2033
mathlib.decl—crossProduct
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.CrossProduct
note—`crossProduct` exists in Mathlib but is not identified with the Hodge dual of an exterior product.
status—partial
modifiedAxial vector–bivector isomorphism1e1c73e2c312
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formal Hodge-star isomorphism between vectors and bivectors in 3D appears in Mathlib.
status—not_formalized
modifiedCross product corresponds to commutator2a822a4e549f
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib defines `crossProduct` and Lie brackets but does not identify the cross product with the commutator of associated linear operators.
status—not_formalized
modifiedHodge star as involution on 2-forms in 4D Riemannian caseb0f330ea2eaf
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Hodge star and no associated involution on 2-forms in Mathlib.
status—not_formalized
modifiedHodge star on one-forms in Minkowski space925f37b27fd6
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Minkowski-signature Hodge star is not formalized in Mathlib.
status—not_formalized
modifiedSelf-dual and anti-self-dual two-forms5c630e7375cf
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Self-dual/anti-self-dual two-forms are not defined in Mathlib.
status—not_formalized
modifiedConformal invariance of Hodge star70f83b87466e
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Hodge star and no statement of conformal invariance on middle-degree forms in Mathlib.
status—not_formalized
modifiedGradient via d and Hodge stara1cd77268bb4
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Gradient is in Mathlib but not expressed via Hodge star and exterior derivative.
status—not_formalized
modifiedCurl via Hodge star0438df9b652d
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Curl is not expressed via Hodge star and exterior derivative in Mathlib.
status—not_formalized
modifiedDivergence via Hodge star6d05ada4e118
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Divergence in Mathlib is not expressed using Hodge star and exterior derivative.
status—not_formalized
modifiedSpecial cases of d² = 099782f82fd9b
FieldFrom #1297To #2033
anchor.sectionExample: Derivatives in three dimensionsExample: Derivatives in three cases
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The vector-calculus identities curl∘grad=0 and div∘curl=0 are not stated as consequences of d² = 0 in Mathlib.
status—not_formalized
modifiedLaplacian via Hodge star5ab69df23dbf
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Laplacian is defined in Mathlib but not via the Hodge star / codifferential construction.
status—not_formalized
modifiedDouble Hodge star identityaf9c6ae9d8b3
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No ⋆⋆ = ±id identity since Mathlib has no Hodge star.
status—not_formalized
modifiedInverse of the Hodge star85a5351e9da8
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized; the Hodge star itself is absent.
status—not_formalized
modifiedHodge dual on a pseudo-Riemannian manifold5dd7ead79929
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Pseudo-Riemannian Hodge dual on differential forms is not in Mathlib.
status—not_formalized
modifiedHodge star for non-orientable manifolds8530a73905bc
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Hodge star with values in pseudo-forms / densities is formalized in Mathlib.
status—not_formalized
modifiedHodge dual in index notation45488045ad0f
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The index-notation formula for the Hodge dual is not in Mathlib.
status—not_formalized
modifiedUnit volume form9ea47d847c7c
FieldFrom #1297To #2033
mathlib.decl—Orientation.volumeForm
mathlib.match_kind——
mathlib.module—Mathlib.Analysis.InnerProductSpace.Orientation
note—`Orientation.volumeForm` provides the volume form on an oriented real inner product space; the coordinate formula √|det g| ε is not stated.
status—partial
modifiedCodifferentialb76368e83fbd
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The codifferential δ is not defined in Mathlib.
status—not_formalized
modifiedCodifferential as adjoint of exterior derivative137138966b5f
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib (no codifferential and no L²-adjoint statement for d).
status—not_formalized
modifiedCodifferential squares to zero970b98cd95cc
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—δ² = 0 is not in Mathlib because δ is not defined.
status—not_formalized
modifiedLaplace–deRham operator851b6e634b04
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Hodge Laplacian Δ = dδ + δd is not formalized in Mathlib.
status—not_formalized
modifiedHodge star preserves harmonic formsa6dabe89baa5
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Harmonic forms and the Hodge star are absent from Mathlib.
status—not_formalized
modifiedCodifferential in coordinatesb99b977eb936
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No coordinate formula for the codifferential in Mathlib.
status—not_formalized
modifiedPoincaré lemma for codifferentialdbb57c120161
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib; even the standard Poincaré lemma for d is not present at this generality.
status—not_formalized
modifiedCohomotopy operator981a0bea9ef7
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No cohomotopy operator on differential forms in Mathlib.
status—not_formalized
modifiedCohomotopy invariance formula05a764e7e185
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedAnticoexact forms67767be5a20e
FieldFrom #1297To #2033
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Anticoexact forms are not formalized in Mathlib.
status—not_formalized
addedHodge star induces isomorphism of cohomology groupsb5fe00c99be3
addedLaplace–deRham operator is symmetric and non-negative2ff527d02d13
addedHomotopy operatorf10ab14eb772
addedDirect sum decomposition into exact and anticoexact formsb2f5c8d66737