English
Given a basis, its orientation is the ray spanned by its determinant; orientation provides a canonical choice of orientation.
Русский
Для базы ориентирование задается лучом, порожденным детерминантом базы.
LaTeX
$$$\text{Module.Basis.orientation}: \text{orientation}(e) := rayOfNeZero R _ e.det_ne_zero$$$
Lean4
/-- The value of `Orientation.map` when the index type has the cardinality of a basis, in terms
of `f.det`. -/
theorem map_orientation_eq_det_inv_smul [Finite ι] (e : Basis ι R M) (x : Orientation R M ι) (f : M ≃ₗ[R] M) :
Orientation.map ι f x = (LinearEquiv.det f)⁻¹ • x :=
by
cases nonempty_fintype ι
letI := Classical.decEq ι
induction x using Module.Ray.ind with
| h g hg =>
rw [Orientation.map_apply, smul_rayOfNeZero, ray_eq_iff, Units.smul_def,
(g.compLinearMap f.symm).eq_smul_basis_det e, g.eq_smul_basis_det e, AlternatingMap.compLinearMap_apply,
AlternatingMap.smul_apply,
show (fun i ↦ (LinearEquiv.symm f).toLinearMap (e i)) = (LinearEquiv.symm f).toLinearMap ∘ e by rfl,
Basis.det_comp, Basis.det_self, mul_one, smul_eq_mul, mul_comm, mul_smul, LinearEquiv.coe_inv_det]
