continuousAlternatingMapCongrRightEquiv

English

If e : N ≃L[R] N' is a continuous linear equivalence, postcomposition with e defines a natural equivalence between spaces of continuous alternating maps M [⋀^ι]→L[R] N and M [⋀^ι]→L[R] N'.

Русский

Если e : N ≃L[R] N' — непрерывное линейное взаимно однозначное отображение, то вычисление через e делает естественное эквивалентство между пространствами непрерывных чередующихся отображений с кодоменами N и N'.

LaTeX

$$$ (M [⋀^ι]→L[R] N) \cong (M [⋀^ι]→L[R] N') $$$

Lean4

/-- A continuous linear equivalence of codomains
defines an equivalence between continuous alternating maps. -/
@[simps -fullyApplied apply]
def _root_.ContinuousLinearEquiv.continuousAlternatingMapCongrRightEquiv (e : N ≃L[R] N') :
    M [⋀^ι]→L[R] N ≃ M [⋀^ι]→L[R] N'
    where
  toFun := (e : N →L[R] N').compContinuousAlternatingMap
  invFun := (e.symm : N' →L[R] N).compContinuousAlternatingMap
  left_inv f := by ext; simp [(· ∘ ·)]
  right_inv f := by ext; simp [(· ∘ ·)]

Похожие утверждения