English
For a linear equivalence f: M1 ≃ M2, the induced dual map is a linear equivalence f^*: Dual M2 ≃ Dual M1, given by the forward dual map and its inverse by the dual of f.
Русский
Для линейного эквивалента f: M1 ≃ M2 дуальное отображение образует линейное эквивалентное отображение f^*: M2^* ≃ M1^*, задаваемое соответствующими формулами через f и f^{-1}.
LaTeX
$$$$ f^* : M_2^* \\to M_1^* \\quad \\text{is a linear equivalence, with} \\quad (f^*)^{-1} = (f^{-1})^*. $$$$
Lean4
/-- The `Linear_equiv` version of `LinearMap.dualMap`. -/
def dualMap (f : M₁ ≃ₗ[R] M₂) : Dual R M₂ ≃ₗ[R] Dual R M₁
where
__ := f.toLinearMap.dualMap
invFun := f.symm.toLinearMap.dualMap
left_inv φ := LinearMap.ext fun x ↦ congr_arg φ (f.right_inv x)
right_inv φ := LinearMap.ext fun x ↦ congr_arg φ (f.left_inv x)
