Currying continuous alternating maps without domain norms

This file provides the pointwise interior product for continuous alternating maps on topological modules. It keeps the domain norm-free while retaining the algebraic linearity in the inserted vector from AlternatingMap.curryLeft.

Main declarations

• ContinuousAlternatingMap.map_insertNth': the alternating insertion-sign formula.
• ContinuousAlternatingMap.curryLeftTopological: the norm-free interior product.
• ContinuousAlternatingMap.curryLeftTopologicalLinear: the interior product with a fixed vector, as a linear map of alternating maps over any scalars acting on the codomain.
• ContinuousAlternatingMap.curryLeftTopological_curryLeftTopological: inserting the same vector twice gives zero.

The construction follows Mathlib's AlternatingMap.curryLeft and map_insertNth.

References

• Yury Kudryashov's DeRhamCohomology project, whose alternating-map design informs the surrounding differential-form API.

theorem ContinuousAlternatingMap.map_insertNth' {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→L[R] N) (p : Fin (n + 1)) (x : M) (v : Fin n → M) : f (p.insertNth x v) = (-1) ^ ↑p • f (Matrix.vecCons x v)

Inserting a vector into a continuous alternating map gives the usual alternating sign.

noncomputable def ContinuousAlternatingMap.curryLeftTopological {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→L[R] N) : M →ₗ[R] M [⋀^Fin n]→L[R] N

The pointwise interior product obtained by fixing the first vector argument.

This is the norm-free companion to Mathlib's normed ContinuousAlternatingMap.curryLeft: it is linear in the inserted vector because it is bundled as a linear map, while continuity is required only in the remaining alternating arguments.

@[simp]

theorem ContinuousAlternatingMap.curryLeftTopological_apply_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→L[R] N) (x : M) (v : Fin n → M) : (f.curryLeftTopological x) v = f (Matrix.vecCons x v)

@[simp]

theorem ContinuousAlternatingMap.toAlternatingMap_curryLeftTopological {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→L[R] N) (x : M) : (f.curryLeftTopological x).toAlternatingMap = f.toAlternatingMap.curryLeft x

@[simp]

theorem ContinuousAlternatingMap.curryLeftTopological_zero {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] {n : ℕ} : curryLeftTopological 0 = 0

@[simp]

theorem ContinuousAlternatingMap.curryLeftTopological_add {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] {n : ℕ} (f g : M [⋀^Fin (n + 1)]→L[R] N) : (f + g).curryLeftTopological = f.curryLeftTopological + g.curryLeftTopological

@[simp]

theorem ContinuousAlternatingMap.curryLeftTopological_smul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] {n : ℕ} (c : R) (f : M [⋀^Fin (n + 1)]→L[R] N) : (c • f).curryLeftTopological = c • f.curryLeftTopological

@[simp]

theorem ContinuousAlternatingMap.curryLeftTopological_curryLeftTopological {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] {n : ℕ} (f : M [⋀^Fin (n + 2)]→L[R] N) (x : M) : (f.curryLeftTopological x).curryLeftTopological x = 0

Inserting the same vector twice into an alternating map gives zero.

noncomputable def ContinuousAlternatingMap.curryLeftTopologicalLinear {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] (S : Type u_4) [Semiring S] [Module S N] [ContinuousConstSMul S N] [SMulCommClass R S N] {n : ℕ} (x : M) : M [⋀^Fin (n + 1)]→L[R] N →ₗ[S] M [⋀^Fin n]→L[R] N

The interior product with a fixed vector x, as a linear map of alternating maps over any scalars acting on the codomain.

@[simp]

theorem ContinuousAlternatingMap.curryLeftTopologicalLinear_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] (S : Type u_4) [Semiring S] [Module S N] [ContinuousConstSMul S N] [SMulCommClass R S N] {n : ℕ} (x : M) (f : M [⋀^Fin (n + 1)]→L[R] N) : (curryLeftTopologicalLinear S x) f = f.curryLeftTopological x

theorem ContinuousAlternatingMap.curryLeftTopologicalLinear_add {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] (S : Type u_4) [Semiring S] [Module S N] [ContinuousConstSMul S N] [SMulCommClass R S N] {n : ℕ} (x y : M) : curryLeftTopologicalLinear S (x + y) = curryLeftTopologicalLinear S x + curryLeftTopologicalLinear S y

The interior product is additive in the inserted vector.

theorem ContinuousAlternatingMap.curryLeftTopologicalLinear_neg {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [IsTopologicalAddGroup N] [ContinuousConstSMul R N] (S : Type u_4) [Semiring S] [Module S N] [ContinuousConstSMul S N] [SMulCommClass R S N] {n : ℕ} (x : M) : curryLeftTopologicalLinear S (-x) = -curryLeftTopologicalLinear S x

The interior product with -x is the negative of the interior product with x.