English
Continuous linear equivalences induce a left-congruence on spaces of continuous alternating maps.
Русский
Непрерывные линейные эквивалентности порождают левую конгруэнтность на пространствах непрерывных чередующихся отображений.
LaTeX
$$$\mathrm{continuousAlternatingMapCongrLeft}(f) : E \simeq_L F \to (E [⋀^ι]→L F) \simeq_L (F [⋀^ι]→L G)$$$
Lean4
/-- Given a map `f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G` and an estimate
`H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖`, construct a continuous linear
map from `F` to `E [⋀^ι]→L[𝕜] G`.
In order to lift, e.g., a map `f : (E [⋀^ι]→ₗ[𝕜] F) →ₗ[𝕜] E' [⋀^ι]→ₗ[𝕜] G`
to a map `(E [⋀^ι]→L[𝕜] F) →L[𝕜] E' [⋀^ι]→L[𝕜] G`,
one can apply this construction to `f.comp ContinuousAlternatingMap.toAlternatingMapLinear`
which is a linear map from `E [⋀^ι]→L[𝕜] F` to `E' [⋀^ι]→ₗ[𝕜] G`. -/
def mkContinuousLinear (f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G) (C : ℝ) (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) :
F →L[𝕜] E [⋀^ι]→L[𝕜] G :=
LinearMap.mkContinuous
{ toFun x := (f x).mkContinuous (C * ‖x‖) <| H x
map_add' x y := by ext1; simp
map_smul' c x := by ext1; simp } (max C 0) fun x ↦
by
rw [LinearMap.coe_mk, AddHom.coe_mk]
exact (mkContinuous_norm_le' _ _).trans_eq <| by rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]
