compContinuousAlternatingMap_coe — Mathlib

English

If e: M ≃L[R] M' and e': N ≃L[R] N' are continuous linear equivalences, then there is a natural equivalence between the spaces of continuous alternating maps: f ↦ (e ∘ f ∘ e'^{-1}) giving a bijection between (M [⋀^ι]→L[R] N) and (M' [⋀^ι]→L[R] N').

Русский

Для непрерывных линейных эквивалентностей e: M ≃L[R] M' и e': N ≃L[R] N' существует естественная эквивалентность между пространствами непрерывных чередующих карт: f ↦ e ∘ f ∘ e'^{-1}, образующая биекцию между (M [⋀^ι]→L[R] N) и (M' [⋀^ι]→L[R] N').

LaTeX

$$$\text{If } e: M \simeq_L[R] M'\text{ and } e': N \simeq_L[R] N',\ (M [⋀^ι]→L[R] N) \cong (M' [⋀^ι]→L[R] N'),\ f \mapsto e \circ f \circ e'^{-1}. $$$

Lean4

@[simp]
theorem _root_.ContinuousLinearEquiv.compContinuousAlternatingMap_coe (e : N ≃L[R] N') (f : M [⋀^ι]→L[R] N) :
    ⇑(e.compContinuousAlternatingMap f) = e ∘ f :=
  rfl

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