English
If e: M ≃L[R] M' is a continuous linear equivalence, then precomposing continuous alternating maps by e gives a bijection between the spaces of such maps: f ↦ f ∘ e^{-1} with inverse g ↦ g ∘ e.
Русский
Если e: M ≃L[R] M' является непрерывным линейным эквивалентом, то предкомпозиция чередующих карт по e задаёт биекцию между множествами таких отображений: f ↦ f ∘ e^{-1}, обратная карта g ↦ g ∘ e.
LaTeX
$$$\text{For a continuous linear equivalence } e: M \simeq_L[R] M',\text{ the map } f \mapsto f \circ e^{-1} \text{ induces an equivalence } (M [⋀^ι]\toL[R] N) \\cong (M' [⋀^ι]\toL[R] N).$$$
Lean4
/-- A continuous linear equivalence of domains
defines an equivalence between continuous alternating maps.
This is available as a continuous linear isomorphism at
`ContinuousLinearEquiv.continuousAlternatingMapCongrLeft`.
This is `ContinuousAlternatingMap.compContinuousLinearMap` as an equivalence. -/
@[simps -fullyApplied apply]
def _root_.ContinuousLinearEquiv.continuousAlternatingMapCongrLeftEquiv (e : M ≃L[R] M') :
M [⋀^ι]→L[R] N ≃ M' [⋀^ι]→L[R] N
where
toFun f := f.compContinuousLinearMap ↑e.symm
invFun f := f.compContinuousLinearMap ↑e
left_inv f := by ext; simp [Function.comp_def]
right_inv f := by ext; simp [Function.comp_def]
