English
From a linear map f whose determinant is a unit, one can construct a linear equivalence with the same base structure.
Русский
Из линейного отображения f с детерминантом, являющимся единицей, строится линейное эквивалентное отображение с тем же основанием.
LaTeX
$$$\exists e: M \simeq M',\ \text{det}(toMatrix v v' f) \in R^{\times} \Rightarrow M \simeq M'$$$
Lean4
/-- Builds a linear equivalence from a linear map whose determinant in some bases is a unit. -/
@[simps]
def ofIsUnitDet {f : M →ₗ[R] M'} {v : Basis ι R M} {v' : Basis ι R M'} (h : IsUnit (LinearMap.toMatrix v v' f).det) :
M ≃ₗ[R] M' where
toFun := f
map_add' := f.map_add
map_smul' := f.map_smul
invFun := toLin v' v (toMatrix v v' f)⁻¹
left_inv
x :=
calc
toLin v' v (toMatrix v v' f)⁻¹ (f x)
_ = toLin v v ((toMatrix v v' f)⁻¹ * toMatrix v v' f) x := by
rw [toLin_mul v v' v, toLin_toMatrix, LinearMap.comp_apply]
_ = x := by simp [h]
right_inv
x :=
calc
f (toLin v' v (toMatrix v v' f)⁻¹ x)
_ = toLin v' v' (toMatrix v v' f * (toMatrix v v' f)⁻¹) x := by
rw [toLin_mul v' v v', LinearMap.comp_apply, toLin_toMatrix v v']
_ = x := by simp [h]
