Top-degree continuous alternating forms

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Analysis.Normed.Module.Alternating).

A continuous alternating form on E whose degree is a basis index type of E is a scalar multiple of that basis's determinant, and pulling it back along an endomorphism scales the scalar by the endomorphism's determinant. Both are upstream facts about AlternatingMap (AlternatingMap.eq_smul_basis_det, Module.Basis.det_comp); this module states them for ContinuousAlternatingMap, which is the type differential forms are made of, in the form the measure of a top form consumes:

• apply_eq_mul_basis_det — α v = α e * e.det v;
• ext_basis — two top-degree forms agreeing on a basis are equal;
• ★ compContinuousLinearMap_apply_basis — (α.compContinuousLinearMap L) e = L.det * α e, the Jacobian rule for the coefficient of a top form: this is the exact factor the change of variables formula carries (MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul), so the density of a top form transforms as a density should.

Honest scope

⚠️ Real scalars only, and the degree is an arbitrary finite type ι with a basis indexed by it; no finrank bookkeeping is done here. Nothing about manifolds.

Provenance and references. The top-power plan (M1); Mathlib/LinearAlgebra/Determinant.lean (AlternatingMap.eq_smul_basis_det, Module.Basis.det_comp, Module.Basis.det_self); the completed-work ledger.

theorem ContinuousAlternatingMap.apply_eq_mul_basis_det {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℝ E) (α : E [⋀^ι]→L[ℝ] ℝ) (v : ι → E) : α v = α ⇑e * e.det v

A top-degree continuous alternating form is its value on a basis times that basis's determinant.

theorem ContinuousAlternatingMap.ext_basis {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℝ E) {α β : E [⋀^ι]→L[ℝ] ℝ} (h : α ⇑e = β ⇑e) : α = β

Two top-degree forms that agree on a basis are equal.

theorem ContinuousAlternatingMap.compContinuousLinearMap_apply_basis {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℝ E) (α : E [⋀^ι]→L[ℝ] ℝ) (L : E →L[ℝ] E) : (α.compContinuousLinearMap L) ⇑e = L.det * α ⇑e

★ The Jacobian rule. Pulling a top-degree form back along an endomorphism multiplies its coefficient on a basis by the determinant of the endomorphism.