Orientations of real inner product spaces.

This file provides definitions and proves lemmas about orientations of real inner product spaces.

Main definitions

• OrthonormalBasis.adjustToOrientation takes an orthonormal basis and an orientation, and returns an orthonormal basis with that orientation: either the original orthonormal basis, or one constructed by negating a single (arbitrary) basis vector.
• Orientation.finOrthonormalBasis is an orthonormal basis, indexed by Fin n, with the given orientation.
• Orientation.volumeForm is a nonvanishing top-dimensional alternating form on an oriented real inner product space, uniquely defined by compatibility with the orientation and inner product structure.

Main theorems

• Orientation.volumeForm_apply_le states that the result of applying the volume form to a set of n vectors, where n is the dimension the inner product space, is bounded by the product of the lengths of the vectors.
• Orientation.abs_volumeForm_apply_of_pairwise_orthogonal states that the result of applying the volume form to a set of n orthogonal vectors, where n is the dimension the inner product space, is equal up to sign to the product of the lengths of the vectors.

theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e f : OrthonormalBasis ι Real E) (h : Eq e.toBasis.orientation f.toBasis.orientation) : Eq (DFunLike.coe e.toBasis.det (DFunLike.coe f)) 1

The change-of-basis matrix between two orthonormal bases with the same orientation has determinant 1.

theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e f : OrthonormalBasis ι Real E) (h : Ne e.toBasis.orientation f.toBasis.orientation) : Eq (DFunLike.coe e.toBasis.det (DFunLike.coe f)) (-1)

The change-of-basis matrix between two orthonormal bases with the opposite orientations has determinant -1.

theorem OrthonormalBasis.same_orientation_iff_det_eq_det {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {e f : OrthonormalBasis ι Real E} : Iff (Eq e.toBasis.det f.toBasis.det) (Eq e.toBasis.orientation f.toBasis.orientation)

Two orthonormal bases with the same orientation determine the same "determinant" top-dimensional form on E, and conversely.

theorem OrthonormalBasis.det_eq_neg_det_of_opposite_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e f : OrthonormalBasis ι Real E) (h : Ne e.toBasis.orientation f.toBasis.orientation) : Eq e.toBasis.det (Neg.neg f.toBasis.det)

Two orthonormal bases with opposite orientations determine opposite "determinant" top-dimensional forms on E.

theorem OrthonormalBasis.orthonormal_adjustToOrientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι Real E) (x : Orientation Real E ι) [Nonempty ι] : Orthonormal Real (DFunLike.coe (e.toBasis.adjustToOrientation x))

OrthonormalBasis.adjustToOrientation, applied to an orthonormal basis, preserves the property of orthonormality.

def OrthonormalBasis.adjustToOrientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι Real E) (x : Orientation Real E ι) [Nonempty ι] : OrthonormalBasis ι Real E

Given an orthonormal basis and an orientation, return an orthonormal basis giving that orientation: either the original basis, or one constructed by negating a single (arbitrary) basis vector.

Equations

• Eq (e.adjustToOrientation x) ((e.toBasis.adjustToOrientation x).toOrthonormalBasis ⋯)

theorem OrthonormalBasis.toBasis_adjustToOrientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι Real E) (x : Orientation Real E ι) [Nonempty ι] : Eq (e.adjustToOrientation x).toBasis (e.toBasis.adjustToOrientation x)

theorem OrthonormalBasis.orientation_adjustToOrientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι Real E) (x : Orientation Real E ι) [Nonempty ι] : Eq (e.adjustToOrientation x).toBasis.orientation x

adjustToOrientation gives an orthonormal basis with the required orientation.

theorem OrthonormalBasis.adjustToOrientation_apply_eq_or_eq_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι Real E) (x : Orientation Real E ι) [Nonempty ι] (i : ι) : Or (Eq (DFunLike.coe (e.adjustToOrientation x) i) (DFunLike.coe e i)) (Eq (DFunLike.coe (e.adjustToOrientation x) i) (Neg.neg (DFunLike.coe e i)))

Every basis vector from adjustToOrientation is either that from the original basis or its negation.

theorem OrthonormalBasis.det_adjustToOrientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι Real E) (x : Orientation Real E ι) [Nonempty ι] : Or (Eq (e.adjustToOrientation x).toBasis.det e.toBasis.det) (Eq (e.adjustToOrientation x).toBasis.det (Neg.neg e.toBasis.det))

theorem OrthonormalBasis.abs_det_adjustToOrientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι Real E) (x : Orientation Real E ι) [Nonempty ι] (v : ι → E) : Eq (abs (DFunLike.coe (e.adjustToOrientation x).toBasis.det v)) (abs (DFunLike.coe e.toBasis.det v))

def Orientation.finOrthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} (hn : LT.lt 0 n) (h : Eq (Module.finrank Real E) n) (x : Orientation Real E (Fin n)) : OrthonormalBasis (Fin n) Real E

An orthonormal basis, indexed by Fin n, with the given orientation.

Equations

• Eq (Orientation.finOrthonormalBasis hn h x) (((stdOrthonormalBasis Real E).reindex (finCongr h)).adjustToOrientation x)

theorem Orientation.finOrthonormalBasis_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} (hn : LT.lt 0 n) (h : Eq (Module.finrank Real E) n) (x : Orientation Real E (Fin n)) : Eq (Orientation.finOrthonormalBasis hn h x).toBasis.orientation x

Orientation.finOrthonormalBasis gives a basis with the required orientation.

theorem Orientation.volumeForm_def {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} [_i : Fact (Eq (Module.finrank Real E) n)] (o : Orientation Real E (Fin n)) : Eq o.volumeForm (Nat.casesAuxOn (motive := fun (a : Nat) => Eq n a → AlternatingMap Real E Real (Fin n)) n (fun (h : Eq n 0) => Eq.ndrec (motive := fun {n : Nat} => [_i : Fact (Eq (Module.finrank Real E) n)] → Orientation Real E (Fin n) → AlternatingMap Real E Real (Fin n)) (fun [Fact (Eq (Module.finrank Real E) 0)] (o : Orientation Real E (Fin 0)) => let opos := AlternatingMap.constOfIsEmpty Real E (Fin 0) 1; ⋯.by_cases (fun (x : Eq o Module.Oriented.positiveOrientation) => opos) fun (x : Eq o (Neg.neg Module.Oriented.positiveOrientation)) => Neg.neg opos) ⋯ o) (fun (n_1 : Nat) (h : Eq n (HAdd.hAdd n_1 1)) => Eq.ndrec (motive := fun {n : Nat} => [_i : Fact (Eq (Module.finrank Real E) n)] → Orientation Real E (Fin n) → AlternatingMap Real E Real (Fin n)) (fun [Fact (Eq (Module.finrank Real E) (HAdd.hAdd n_1 1))] (o : Orientation Real E (Fin (HAdd.hAdd n_1 1))) => (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ o) ⋯)

@[irreducible]

def Orientation.volumeForm {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} [_i : Fact (Eq (Module.finrank Real E) n)] (o : Orientation Real E (Fin n)) : AlternatingMap Real E Real (Fin n)

The volume form on an oriented real inner product space, a nonvanishing top-dimensional alternating form uniquely defined by compatibility with the orientation and inner product structure.

Equations

• Eq (@Orientation.volumeForm) Orientation.wrapped✝.1

theorem Orientation.volumeForm_zero_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] [_i : Fact (Eq (Module.finrank Real E) 0)] : Eq Module.Oriented.positiveOrientation.volumeForm (DFunLike.coe AlternatingMap.constLinearEquivOfIsEmpty 1)

theorem Orientation.volumeForm_zero_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] [_i : Fact (Eq (Module.finrank Real E) 0)] : Eq (Neg.neg Module.Oriented.positiveOrientation).volumeForm (Neg.neg (DFunLike.coe AlternatingMap.constLinearEquivOfIsEmpty 1))

theorem Orientation.volumeForm_robust {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} [_i : Fact (Eq (Module.finrank Real E) n)] (o : Orientation Real E (Fin n)) (b : OrthonormalBasis (Fin n) Real E) (hb : Eq b.toBasis.orientation o) : Eq o.volumeForm b.toBasis.det

The volume form on an oriented real inner product space can be evaluated as the determinant with respect to any orthonormal basis of the space compatible with the orientation.

theorem Orientation.volumeForm_robust_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} [_i : Fact (Eq (Module.finrank Real E) n)] (o : Orientation Real E (Fin n)) (b : OrthonormalBasis (Fin n) Real E) (hb : Ne b.toBasis.orientation o) : Eq o.volumeForm (Neg.neg b.toBasis.det)

The volume form on an oriented real inner product space can be evaluated as the determinant with respect to any orthonormal basis of the space compatible with the orientation.

theorem Orientation.volumeForm_neg_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} [_i : Fact (Eq (Module.finrank Real E) n)] (o : Orientation Real E (Fin n)) : Eq (Neg.neg o).volumeForm (Neg.neg o.volumeForm)

theorem Orientation.volumeForm_robust' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} [_i : Fact (Eq (Module.finrank Real E) n)] (o : Orientation Real E (Fin n)) (b : OrthonormalBasis (Fin n) Real E) (v : Fin n → E) : Eq (abs (DFunLike.coe o.volumeForm v)) (abs (DFunLike.coe b.toBasis.det v))

theorem Orientation.abs_volumeForm_apply_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} [_i : Fact (Eq (Module.finrank Real E) n)] (o : Orientation Real E (Fin n)) (v : Fin n → E) : LE.le (abs (DFunLike.coe o.volumeForm v)) (Finset.univ.prod fun (i : Fin n) => Norm.norm (v i))

Let v be an indexed family of n vectors in an oriented n-dimensional real inner product space E. The output of the volume form of E when evaluated on v is bounded in absolute value by the product of the norms of the vectors v i.

theorem Orientation.volumeForm_apply_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} [_i : Fact (Eq (Module.finrank Real E) n)] (o : Orientation Real E (Fin n)) (v : Fin n → E) : LE.le (DFunLike.coe o.volumeForm v) (Finset.univ.prod fun (i : Fin n) => Norm.norm (v i))

theorem Orientation.abs_volumeForm_apply_of_pairwise_orthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} [_i : Fact (Eq (Module.finrank Real E) n)] (o : Orientation Real E (Fin n)) {v : Fin n → E} (hv : Pairwise fun (i j : Fin n) => Eq (Inner.inner (v i) (v j)) 0) : Eq (abs (DFunLike.coe o.volumeForm v)) (Finset.univ.prod fun (i : Fin n) => Norm.norm (v i))

Let v be an indexed family of n orthogonal vectors in an oriented n-dimensional real inner product space E. The output of the volume form of E when evaluated on v is, up to sign, the product of the norms of the vectors v i.

theorem Orientation.abs_volumeForm_apply_of_orthonormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} [_i : Fact (Eq (Module.finrank Real E) n)] (o : Orientation Real E (Fin n)) (v : OrthonormalBasis (Fin n) Real E) : Eq (abs (DFunLike.coe o.volumeForm (DFunLike.coe v))) 1

The output of the volume form of an oriented real inner product space E when evaluated on an orthonormal basis is ±1.

theorem Orientation.volumeForm_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} [_i : Fact (Eq (Module.finrank Real E) n)] (o : Orientation Real E (Fin n)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace Real F] [Fact (Eq (Module.finrank Real F) n)] (φ : LinearIsometryEquiv (RingHom.id Real) E F) (x : Fin n → F) : Eq (DFunLike.coe (DFunLike.coe (map (Fin n) φ.toLinearEquiv) o).volumeForm x) (DFunLike.coe o.volumeForm (Function.comp (DFunLike.coe φ.symm) x))

theorem Orientation.volumeForm_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace Real E] {n : Nat} [_i : Fact (Eq (Module.finrank Real E) n)] (o : Orientation Real E (Fin n)) (φ : LinearIsometryEquiv (RingHom.id Real) E E) (hφ : LT.lt 0 (DFunLike.coe LinearMap.det φ.toLinearMap)) (x : Fin n → E) : Eq (DFunLike.coe o.volumeForm (Function.comp (DFunLike.coe φ) x)) (DFunLike.coe o.volumeForm x)

The volume form is invariant under pullback by a positively-oriented isometric automorphism.