English
Continuous linear equivalences between domains and codomains induce an equivalence between the spaces of continuous alternating maps, i.e., there is a bijection between (M ≃L[R] M') and (N ≃L[R] N')-twisted map spaces via pre- and post-composition.
Русский
Непрерывные линейные эквивалентности между доменами и кодом сопровождают эквивалентность между пространствами непрерывных чередующих карт: биекция между соответствующими пространствами отображений по пред- и пост-композициям.
LaTeX
$$$\text{Given } e: M \simeq_L[R] M',\ e': N \simeq_L[R] N',\text{ we have } (M [⋀^ι]→L[R] N) \cong (M' [⋀^ι]→L[R] N').$$$
Lean4
/-- Continuous linear equivalences between domains and codomains
define an equivalence between the spaces of continuous alternating maps. -/
def _root_.ContinuousLinearEquiv.continuousAlternatingMapCongrEquiv (e : M ≃L[R] M') (e' : N ≃L[R] N') :
M [⋀^ι]→L[R] N ≃ M' [⋀^ι]→L[R] N' :=
e.continuousAlternatingMapCongrLeftEquiv.trans e'.continuousAlternatingMapCongrRightEquiv
