English
For an orientation o on a module with empty index type, o is either the positive orientation or its negation.
Русский
Для ориентации o на модуле с пустым индексным множеством, o равна либо положительной ориентации, либо её отрицанию.
LaTeX
$$$$ o = {\\rm positiveOrientation} \\quad\\lor\\quad o = -{\\rm positiveOrientation} $$$$
Lean4
/-- A module `M` over a linearly ordered commutative ring has precisely two "orientations" with
respect to an empty index type. (Note that these are only orientations of `M` of in the conventional
mathematical sense if `M` is zero-dimensional.) -/
theorem eq_or_eq_neg_of_isEmpty [IsEmpty ι] (o : Orientation R M ι) :
o = positiveOrientation ∨ o = -positiveOrientation := by
induction o using Module.Ray.ind with
| h x hx =>
dsimp [positiveOrientation]
simp only [ray_eq_iff]
rw [sameRay_or_sameRay_neg_iff_not_linearIndependent]
intro h
set f : (M [⋀^ι]→ₗ[R] R) ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
have H : LinearIndependent R ![f x, 1] :=
by
convert h.map' f.toLinearMap f.ker
ext i
fin_cases i <;> simp [f]
rw [linearIndependent_iff'] at H
simpa using H Finset.univ ![1, -f x] (by simp [Fin.sum_univ_succ]) 0 (by simp)
