English
Orientation.map preserves the orientation (map x = x) if and only if the determinant is positive.
Русский
Ориентация сохраняется после отображения, если детерминант положителен.
LaTeX
$$$$ Orientation.map ι f x = x \\iff 0 < det f $$$$
Lean4
/-- If the index type has cardinality equal to the finite dimension, composing an alternating
map with the same linear equiv on each argument gives the same orientation if and only if the
determinant is positive. -/
theorem map_eq_iff_det_pos [FiniteDimensional R M] (x : Orientation R M ι) (f : M ≃ₗ[R] M)
(h : Fintype.card ι = finrank R M) : Orientation.map ι f x = x ↔ 0 < LinearMap.det (f : M →ₗ[R] M) :=
by
cases isEmpty_or_nonempty ι
· have H : finrank R M = 0 := h.symm.trans Fintype.card_eq_zero
simp [LinearMap.det_eq_one_of_finrank_eq_zero H]
rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_self_iff, LinearEquiv.coe_det]
