Continuous linear alternatization

Mathlib's ContinuousMultilinearMap.alternatization is the signed permutation sum. Here it is bundled as a continuous linear map, with its factorial norm bound. Its value on alternating maps is given by the factorial identity in TauCeti.Topology.Algebra.Module.Alternating.Basic. Dividing by the factorial gives a retraction onto alternating maps when the factorial is nonzero in the scalar field, useful for transporting smoothness from multilinear maps.

The construction uses Yury Kudryashov's alternatization in Mathlib.Topology.Algebra.Module.Alternating.Basic.

theorem ContinuousMultilinearMap.norm_alternatization_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap 𝕜 (fun (x : ι) => E) F) : ‖alternatization f‖ ≤ ↑(Fintype.card ι).factorial * ‖f‖

The norm of the signed permutation sum is at most the arity factorial times ‖f‖.

noncomputable def ContinuousMultilinearMap.alternatizationCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [DecidableEq ι] : ContinuousMultilinearMap 𝕜 (fun (x : ι) => E) F →L[𝕜] E [⋀^ι]→L[𝕜] F

Alternatization, the signed sum over permutations, as a continuous linear map.

@[simp]

theorem ContinuousMultilinearMap.alternatizationCLM_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap 𝕜 (fun (x : ι) => E) F) : alternatizationCLM f = alternatization f

The continuous linear alternatization evaluates to Mathlib's signed permutation sum.

theorem ContinuousAlternatingMap.inv_factorial_smul_alternatizationCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [DecidableEq ι] [NeZero ↑(Fintype.card ι).factorial] (φ : E [⋀^ι]→L[𝕜] F) : (↑(Fintype.card ι).factorial)⁻¹ • ContinuousMultilinearMap.alternatizationCLM φ.toContinuousMultilinearMap = φ

Normalized alternatization recovers an alternating map when the arity factorial is nonzero in the scalar field.