The exterior derivative on a manifold #

TERM-SCOPE(Kahler) — this module names the "Kahler / symplectic manifold API" row of the Mathlib-gaps register; the source repository's terms register records what is backed and what is not.

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Geometry.Manifold, the ## TODO of Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean).

A differential form on a manifold (DifferentialForm.lean) is a smooth section of the alternating bundle on the tangent bundle. Its exterior derivative is defined chart by chart and glued by the flat naturality lemma extDeriv_pullback:

DifferentialForm.localRep s x₀ — the local representative of a family s of alternating maps in the chart at x₀: an unbundled flat form on the model space; Naming. mextDerivFamily acts on families s : ∀ x, TₓM [⋀^k]→L ℝ; DifferentialForm.mextDeriv is the bundled operator on C^∞ forms. (Until 2026-09-16 the family operator was a root mextDeriv, which the bundled name shadowed inside namespace DifferentialForm; external review asked for distinct names.)
mextDerivFamily s x — the exterior derivative of a family s : ∀ x, TₓM [⋀^k]→L ℝ: the flat extDeriv of the local representative in the chart at x, read at x (the tangent space at x is the model space definitionally, so no transport is needed at the base point);
★ DifferentialForm.trivializationAt_snd — the trivialisation of a section value is the pullback along the derivative of the chart transition (VectorBundleCore.trivializationAt_symmL and tangentBundleCore_coordChange_achart, read on the model);
★ DifferentialForm.localRep_transition — local representatives in two charts differ by the pullback along the transition (the tangent-bundle cocycle VectorBundleCore.coordChange_comp);
★★ DifferentialForm.localRep_mextDerivFamily — the local representative of d s is the flat d of the local representative of s, in every chart, at every point of the chart. This is where extDeriv_pullback is spent, and it is the whole content of chart-independence;
★★ contMDiff_mextDerivFamily — d of a C^∞ section is a C^∞ section, so d iterates: DifferentialForm.mextDeriv is the bundled operator DifferentialForm 𝓘(ℝ, E) M ∞ (Fin k) G → DifferentialForm 𝓘(ℝ, E) M ∞ (Fin (k+1)) G;
★★ mextDerivFamily_mextDerivFamily, DifferentialForm.mextDeriv_mextDeriv — d ∘ d = 0, transported from extDeriv_extDeriv_apply;
0-forms: zeroFormFamily f (a function f : M → G as a 0-form family), localRep_zeroFormFamily, contMDiff_zeroFormFamily (the section is C^∞ when f is), the bundled zeroForm f hf, and ★ toFlat_mextDerivFamily_zeroFormFamily / toFlat_mextDeriv_zeroForm — the exterior derivative of a 0-form is its differential, (df)_x = ofSubsingleton 0 (mfderiv f x), transported from extDeriv_constOfIsEmpty.

The design decisions the scoping note's §4 asked for, all taken the cheap way:

real, boundaryless model 𝓘(ℝ, E) — every finite-dimensional real manifold this tree uses, ℂℙⁿ included; range 𝓘 = univ, so fderivWithin is fderiv and no UniqueDiffOn is ever supplied; minSmoothness ℝ 2 = 2;
smoothness ∞ only — d of C^∞ is C^∞, and no n - 1 arithmetic leaks anywhere;
degrees Fin k — the flat extDeriv is Fin k → Fin (k + 1);
toFlat, a definitional cast from the fibre TₓM [⋀^k]→L G to the model fibre, so that every identity is stated on the model space and rewriting never has to cross the TangentSpace-vs-model instance path (that crossing, done pointwise, is what trivializationAt_snd is for).

Honest scope #

⚠️ ∞ and 𝓘(ℝ, E) only. No C^n bookkeeping, no boundary, no other field. A consumer needing d on a C^n manifold or on a manifold with corners needs a generalisation, and the smoothness arithmetic that this file deliberately avoids would come with it.

⚠️ What is not here: the Palais formula, naturality d(f^*ω) = f^*(dω) for maps of manifolds, linearity, and the Leibniz rule (which needs the wedge of sections).

⚠️ The chart at x is chartAt E x, the atlas's own choice. mextDerivFamily is defined through it; localRep_mextDerivFamily is what shows the value is the same in every chart.

Provenance and references. The exterior-derivative plan (the plan, and its §3a on why the "walls" recorded before this file were not walls); Geometry/Manifold/DifferentialForm.lean (step (2a)); Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean (extDeriv, extDeriv_pullback, extDeriv_extDeriv_apply); the Mathlib-gaps register (Kahler / symplectic manifold API); the backlog (XL, "Manifold exterior calculus"); the completed-work ledger. Consumers: Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudyForm.lean (fsForm_mextDeriv); Geometry/Manifold/HamiltonianVectorField.lean (IsHamiltonianVectorField.isLocallyHamiltonian, the 0-form API).

The exterior derivative on a manifold #

Honest scope #

0-forms: the exterior derivative is the differential #

`0`-forms: the exterior derivative is the differential #