English
Orientation.map sends x to -x exactly when the determinant is negative.
Русский
Ориентация отображается в −x тогда, когда детерминант отрицателен.
LaTeX
$$$$ Orientation.map ι f x = -x \\iff det f < 0 $$$$
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 negation of that orientation if and
only if the determinant is negative. -/
theorem map_eq_neg_iff_det_neg (x : Orientation R M ι) (f : M ≃ₗ[R] M) (h : Fintype.card ι = finrank R M) :
Orientation.map ι f x = -x ↔ LinearMap.det (f : M →ₗ[R] M) < 0 :=
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, Module.Ray.ne_neg_self x]
have H : 0 < finrank R M := by
rw [← h]
exact Fintype.card_pos
haveI : FiniteDimensional R M := of_finrank_pos H
rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_neg_iff, LinearEquiv.coe_det]
