The sign of a basis relative to an orientation

The relative sign takes values in the integer units and compensates the sign of a change of basis. It is unchanged when the orientation and the basis are transported along the same linear equivalence (Orientation.signBasis_map). Empty index types are included, so both zero-dimensional orientations retain their sign. Two orientations are equal exactly when they agree on whether they are the orientation of a fixed basis (Module.Basis.eq_iff_eq_orientation_iff).

theorem Module.Basis.orientation_eq_neg_iff_det_neg {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] (b c : Basis ι R E) : b.orientation = -c.orientation ↔ b.det ⇑c < 0

Two bases have opposite orientations exactly when their change-of-basis determinant is negative.

theorem Module.Basis.eq_iff_eq_orientation_iff {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] (e : Basis ι R E) (x y : Orientation R E ι) : x = y ↔ (x = e.orientation ↔ y = e.orientation)

Two orientations are equal exactly when they agree on whether they are the orientation of a fixed basis e, since every orientation is that of e or its opposite.

noncomputable def Orientation.signBasis {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] (o : Orientation R E ι) (b : Module.Basis ι R E) : ℤˣ

The sign of a basis relative to a model orientation, including empty index types.

@[simp]

theorem Orientation.signBasis_orientation {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R E) : b.orientation.signBasis b = 1

A basis giving the chosen orientation has positive relative sign.

@[simp]

theorem Orientation.signBasis_map {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] {F : Type u_4} [AddCommGroup F] [Module R F] (o : Orientation R E ι) (b : Module.Basis ι R E) (e : E ≃ₗ[R] F) : ((map ι e) o).signBasis (b.map e) = o.signBasis b

Transporting both the orientation and the basis along a linear equivalence preserves their relative sign.

@[simp]

theorem Orientation.signBasis_neg {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] (o : Orientation R E ι) (b : Module.Basis ι R E) : (-o).signBasis b = -o.signBasis b

Reversing the orientation reverses the relative basis sign.

theorem Orientation.signBasis_cast_mul_self {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] (o : Orientation R E ι) (b : Module.Basis ι R E) : ↑↑(o.signBasis b) * ↑↑(o.signBasis b) = 1

The relative basis sign squares to one in the scalar ring.

theorem Orientation.signBasis_eq_neg_of_orientation_eq_neg {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] (o : Orientation R E ι) (b b' : Module.Basis ι R E) (h : b'.orientation = -b.orientation) : o.signBasis b' = -o.signBasis b

Reversing the basis orientation reverses its relative sign.

@[simp]

theorem Orientation.signBasis_reindex {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] {ι' : Type u_4} [Fintype ι'] [DecidableEq ι'] (o : Orientation R E ι) (b : Module.Basis ι R E) (e : ι ≃ ι') : ((reindex R E e) o).signBasis (b.reindex e) = o.signBasis b

Reindexing an orientation and a basis along the same equivalence preserves their relative sign.

theorem Orientation.signBasis_mul_det_mul_pos {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] (o : Orientation R E ι) (b b' : Module.Basis ι R E) : 0 < ↑↑(o.signBasis b) * b.det ⇑b' * ↑↑(o.signBasis b')

The basis signs compensate the change-of-basis determinant to give a positive product.

theorem AlternatingMap.signBasis_mul_apply_eq_abs_det_mul {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] (f : E [⋀^ι]→ₗ[R] R) (b₀ b : Module.Basis ι R E) : ↑↑(b₀.orientation.signBasis b) * f ⇑b = |b₀.det ⇑b| * f ⇑b₀

A top-degree alternating form evaluated on a basis and weighted by that basis's sign relative to the orientation of a reference basis is its value on the reference basis times the absolute change-of-basis determinant. In particular, a form that is nonnegative (positive) on the bases of one orientation has nonnegative (positive) signed value on every basis.

theorem AlternatingMap.apply_pos_of_orientation_eq {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] (f : E [⋀^ι]→ₗ[R] R) {b₀ b : Module.Basis ι R E} (hb : b.orientation = b₀.orientation) (h : 0 < f ⇑b₀) : 0 < f ⇑b

A top-degree alternating form positive on a basis b₀ is positive on every basis with the orientation of b₀: the two values differ by the positive change-of-basis determinant.

theorem Orientation.signBasis_mul_det_div_abs {R : Type u_1} {E : Type u_2} {ι : Type u_3} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] (o : Orientation R E ι) (b b' : Module.Basis ι R E) : ↑↑(o.signBasis b') * (b.det ⇑b' / |b.det ⇑b'|) = ↑↑(o.signBasis b)

The relative basis sign compensates exactly for the signed determinant ratio.

theorem Orientation.signBasis_mul_units_mul_det_pos {R : Type u_1} {E : Type u_2} {ι : Type u_3} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Fintype ι] [DecidableEq ι] (o : Orientation R E ι) (b : Module.Basis ι R E) (A : E ≃ₗ[R] E) (u : ℤˣ) (h : (map ι A) ((Units.map ↑(Int.castRingHom R)) u • o) = b.orientation) : 0 < ↑↑(o.signBasis b) * ↑↑u * LinearMap.det ↑A

If a linear equivalence sends a signed model orientation to a basis orientation, its Jacobian multiplied by the two relative signs is positive.