English
Given a continuous linear equivalence between F and G, the induced map on spaces of continuous alternating maps is itself a continuous linear equivalence.
Русский
Дано непрерывное линейное эквивалентство между F и G, индуцированное отображение на пространствах непрерывных чередующихся отображений тоже является непрерывным линейным эквивалентом.
LaTeX
$$$\mathrm{continuousAlternatingMapCongrRight} : (F \simeq_L G) \to (ContinuousAlternatingMap 𝕜 E F ι) \simeq_L (ContinuousAlternatingMap 𝕜 E G ι)$$$
Lean4
/-- Flip arguments in `f : F →L[𝕜] E [⋀^ι]→L[𝕜] G` to get `⋀^ι⟮𝕜; E; F →L[𝕜] G⟯` -/
@[simps! apply_apply]
def flipAlternating (f : F →L[𝕜] (E [⋀^ι]→L[𝕜] G)) : E [⋀^ι]→L[𝕜] (F →L[𝕜] G)
where
toContinuousMultilinearMap := ((ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜).comp f).flipMultilinear
map_eq_zero_of_eq' v i j hv hne := by ext x; simp [(f x).map_eq_zero_of_eq v hv hne]
