Top-degree test forms and scalar tests

A basis of a finite-dimensional real vector space identifies its top-degree test forms with scalar test functions. Both directions are continuous for the native LF topology and preserve the exact support. The coefficient is evaluation on the basis; the inverse multiplies the basis determinant form by the scalar test. The formulas include dimension zero.

The basis-change and linear-pullback formulas record the signed determinant, not its absolute value. These coordinates let a functional on top-degree test forms be tested against scalar tests, as in the local constancy theorem for currents.

The construction uses Mathlib's TestFunction.postcompCLM and AlternatingMap.eq_smul_basis_det. See Federer, Geometric Measure Theory, §4.1.7 for the scalar-test description of top-dimensional currents.

noncomputable def Module.Basis.testTopFormEquiv {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] [DecidableEq ι] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (b : Basis ι ℝ E) : TestFunction Ω (E [⋀^ι]→L[ℝ] ℝ) n ≃L[ℝ] TestFunction Ω ℝ n

A basis identifies top-degree test forms with scalar tests by evaluation on that basis.

@[simp]

theorem Module.Basis.testTopFormEquiv_apply {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] [DecidableEq ι] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (b : Basis ι ℝ E) (φ : TestFunction Ω (E [⋀^ι]→L[ℝ] ℝ) n) (x : E) : (b.testTopFormEquiv φ) x = (φ x) ⇑b

@[simp]

theorem Module.Basis.testTopFormEquiv_symm_apply {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] [DecidableEq ι] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (b : Basis ι ℝ E) (f : TestFunction Ω ℝ n) (x : E) (v : ι → E) : ((b.testTopFormEquiv.symm f) x) v = f x * b.det v

@[simp]

theorem Module.Basis.tsupport_testTopFormEquiv {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] [DecidableEq ι] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (b : Basis ι ℝ E) (φ : TestFunction Ω (E [⋀^ι]→L[ℝ] ℝ) n) : tsupport ⇑(b.testTopFormEquiv φ) = tsupport ⇑φ

Passing from a top-degree test form to its coefficient preserves its support exactly.

@[simp]

theorem Module.Basis.tsupport_testTopFormEquiv_symm {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] [DecidableEq ι] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (b : Basis ι ℝ E) (f : TestFunction Ω ℝ n) : tsupport ⇑(b.testTopFormEquiv.symm f) = tsupport ⇑f

Multiplication by the basis determinant form preserves the support of a scalar test.

theorem Module.Basis.testTopFormEquiv_eq_det_smul {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] [DecidableEq ι] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (b b' : Basis ι ℝ E) (φ : TestFunction Ω (E [⋀^ι]→L[ℝ] ℝ) n) : b'.testTopFormEquiv φ = b.det ⇑b' • b.testTopFormEquiv φ

The scalar coefficient changes by the signed change-of-basis determinant.

theorem Module.Basis.testTopFormEquiv_monoCLM {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] [DecidableEq ι] {Ω Ω' : TopologicalSpace.Opens E} {n : ℕ∞} (b : Basis ι ℝ E) {m : ℕ∞} (φ : TestFunction Ω (E [⋀^ι]→L[ℝ] ℝ) n) : b.testTopFormEquiv ((TestFunction.monoCLM ℝ) φ) = (TestFunction.monoCLM ℝ) (b.testTopFormEquiv φ)

The identification of top-degree tests commutes with extension and lowering regularity.

theorem Module.Basis.testTopFormEquiv_postcomp_compContinuousLinearMap {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] [DecidableEq ι] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (b : Basis ι ℝ E) (A : E →L[ℝ] E) (φ : TestFunction Ω (E [⋀^ι]→L[ℝ] ℝ) n) : b.testTopFormEquiv ((TestFunction.postcompCLM (ContinuousAlternatingMap.compContinuousLinearMapCLM A)) φ) = LinearMap.det ↑A • b.testTopFormEquiv φ

Fibrewise pullback by a linear endomorphism multiplies the top-degree coefficient by its signed determinant. No change of the spatial argument of the test function is made here.