Orientations of real inner product spaces. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

orthonormal_basis.adjust_to_orientation 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.fin_orthonormal_basis is an orthonormal basis, indexed by fin n, with the given orientation.
orientation.volume_form 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.volume_form_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_volume_form_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 orthonormal_basis.det_to_matrix_orthonormal_basis_of_same_orientation {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {ι : Type u_2} [fintype ι] [decidable_eq ι] (e f : orthonormal_basis ι ℝ E) (h : e.to_basis.orientation = f.to_basis.orientation) :

⇑(e.to_basis.det) ⇑f = 1

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

source

theorem orthonormal_basis.det_to_matrix_orthonormal_basis_of_opposite_orientation {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {ι : Type u_2} [fintype ι] [decidable_eq ι] (e f : orthonormal_basis ι ℝ E) (h : e.to_basis.orientation ≠ f.to_basis.orientation) :

⇑(e.to_basis.det) ⇑f = -1

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

source

theorem orthonormal_basis.same_orientation_iff_det_eq_det {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {ι : Type u_2} [fintype ι] [decidable_eq ι] {e f : orthonormal_basis ι ℝ E} :

e.to_basis.det = f.to_basis.det ↔ e.to_basis.orientation = f.to_basis.orientation

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

source

theorem orthonormal_basis.det_eq_neg_det_of_opposite_orientation {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {ι : Type u_2} [fintype ι] [decidable_eq ι] (e f : orthonormal_basis ι ℝ E) (h : e.to_basis.orientation ≠ f.to_basis.orientation) :

e.to_basis.det = -f.to_basis.det

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

source

theorem orthonormal_basis.orthonormal_adjust_to_orientation {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {ι : Type u_2} [fintype ι] [decidable_eq ι] [ne : nonempty ι] (e : orthonormal_basis ι ℝ E) (x : orientation ℝ E ι) :

orthonormal ℝ ⇑(e.to_basis.adjust_to_orientation x)

orthonormal_basis.adjust_to_orientation, applied to an orthonormal basis, preserves the property of orthonormality.

source

noncomputable def orthonormal_basis.adjust_to_orientation {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {ι : Type u_2} [fintype ι] [decidable_eq ι] [ne : nonempty ι] (e : orthonormal_basis ι ℝ E) (x : orientation ℝ E ι) :

orthonormal_basis ι ℝ 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

e.adjust_to_orientation x = (e.to_basis.adjust_to_orientation x).to_orthonormal_basis _

source

theorem orthonormal_basis.to_basis_adjust_to_orientation {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {ι : Type u_2} [fintype ι] [decidable_eq ι] [ne : nonempty ι] (e : orthonormal_basis ι ℝ E) (x : orientation ℝ E ι) :

(e.adjust_to_orientation x).to_basis = e.to_basis.adjust_to_orientation x

source

@[simp]

theorem orthonormal_basis.orientation_adjust_to_orientation {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {ι : Type u_2} [fintype ι] [decidable_eq ι] [ne : nonempty ι] (e : orthonormal_basis ι ℝ E) (x : orientation ℝ E ι) :

(e.adjust_to_orientation x).to_basis.orientation = x

adjust_to_orientation gives an orthonormal basis with the required orientation.

source

theorem orthonormal_basis.adjust_to_orientation_apply_eq_or_eq_neg {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {ι : Type u_2} [fintype ι] [decidable_eq ι] [ne : nonempty ι] (e : orthonormal_basis ι ℝ E) (x : orientation ℝ E ι) (i : ι) :

⇑(e.adjust_to_orientation x) i = ⇑e i ∨ ⇑(e.adjust_to_orientation x) i = -⇑e i

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

source

theorem orthonormal_basis.det_adjust_to_orientation {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {ι : Type u_2} [fintype ι] [decidable_eq ι] [ne : nonempty ι] (e : orthonormal_basis ι ℝ E) (x : orientation ℝ E ι) :

(e.adjust_to_orientation x).to_basis.det = e.to_basis.det ∨ (e.adjust_to_orientation x).to_basis.det = -e.to_basis.det

source

theorem orthonormal_basis.abs_det_adjust_to_orientation {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {ι : Type u_2} [fintype ι] [decidable_eq ι] [ne : nonempty ι] (e : orthonormal_basis ι ℝ E) (x : orientation ℝ E ι) (v : ι → E) :

|⇑((e.adjust_to_orientation x).to_basis.det) v| = |⇑(e.to_basis.det) v|

source

@[protected]

noncomputable def orientation.fin_orthonormal_basis {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} (hn : 0 < n) (h : fdim E = n) (x : orientation ℝ E (fin n)) :

orthonormal_basis (fin n) ℝ E

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

Equations

orientation.fin_orthonormal_basis hn h x = ((std_orthonormal_basis ℝ E).reindex (fin_congr h)).adjust_to_orientation x

source

@[simp]

theorem orientation.fin_orthonormal_basis_orientation {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} (hn : 0 < n) (h : fdim E = n) (x : orientation ℝ E (fin n)) :

(orientation.fin_orthonormal_basis hn h x).to_basis.orientation = x

orientation.fin_orthonormal_basis gives a basis with the required orientation.

source

@[irreducible]

noncomputable def orientation.volume_form {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} [fact (fdim E = n)] (o : orientation ℝ E (fin n)) :

alternating_map ℝ E ℝ (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

o.volume_form = n.cases_on (λ [_i : fact (fdim E = 0)] (o : orientation ℝ E (fin 0)), let opos : alternating_map ℝ E ℝ (fin 0) := alternating_map.const_of_is_empty ℝ E (fin 0) 1 in _.by_cases (λ (_x : o = module.oriented.positive_orientation), opos) (λ (_x : o = -module.oriented.positive_orientation), -opos)) (λ (n : ℕ) [_i : fact (fdim E = n.succ)] (o : orientation ℝ E (fin n.succ)), (orientation.fin_orthonormal_basis _ _ o).to_basis.det) o

source

@[simp]

theorem orientation.volume_form_zero_pos {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] [fact (fdim E = 0)] :

module.oriented.positive_orientation.volume_form = ⇑alternating_map.const_linear_equiv_of_is_empty 1

source

theorem orientation.volume_form_zero_neg {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] [fact (fdim E = 0)] :

(-module.oriented.positive_orientation).volume_form = -⇑alternating_map.const_linear_equiv_of_is_empty 1

source

theorem orientation.volume_form_robust {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} [fact (fdim E = n)] (o : orientation ℝ E (fin n)) (b : orthonormal_basis (fin n) ℝ E) (hb : b.to_basis.orientation = o) :

o.volume_form = b.to_basis.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.

source

theorem orientation.volume_form_robust_neg {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} [fact (fdim E = n)] (o : orientation ℝ E (fin n)) (b : orthonormal_basis (fin n) ℝ E) (hb : b.to_basis.orientation ≠ o) :

o.volume_form = -b.to_basis.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.

source

@[simp]

theorem orientation.volume_form_neg_orientation {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} [fact (fdim E = n)] (o : orientation ℝ E (fin n)) :

(-o).volume_form = -o.volume_form

source

theorem orientation.volume_form_robust' {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} [fact (fdim E = n)] (o : orientation ℝ E (fin n)) (b : orthonormal_basis (fin n) ℝ E) (v : fin n → E) :

|⇑(o.volume_form) v| = |⇑(b.to_basis.det) v|

source

theorem orientation.abs_volume_form_apply_le {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} [fact (fdim E = n)] (o : orientation ℝ E (fin n)) (v : fin n → E) :

|⇑(o.volume_form) v| ≤ finset.univ.prod (λ (i : fin n), ‖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.

source

theorem orientation.volume_form_apply_le {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} [fact (fdim E = n)] (o : orientation ℝ E (fin n)) (v : fin n → E) :

⇑(o.volume_form) v ≤ finset.univ.prod (λ (i : fin n), ‖v i‖)

source

theorem orientation.abs_volume_form_apply_of_pairwise_orthogonal {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} [fact (fdim E = n)] (o : orientation ℝ E (fin n)) {v : fin n → E} (hv : pairwise (λ (i j : fin n), has_inner.inner (v i) (v j) = 0)) :

|⇑(o.volume_form) v| = finset.univ.prod (λ (i : fin n), ‖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.

source

theorem orientation.abs_volume_form_apply_of_orthonormal {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} [fact (fdim E = n)] (o : orientation ℝ E (fin n)) (v : orthonormal_basis (fin n) ℝ E) :

|⇑(o.volume_form) ⇑v| = 1

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

source

theorem orientation.volume_form_map {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} [fact (fdim E = n)] (o : orientation ℝ E (fin n)) {F : Type u_2} [normed_add_comm_group F] [inner_product_space ℝ F] [fact (fdim F = n)] (φ : E ≃ₗᵢ[ℝ ] F) (x : fin n → F) :

⇑((⇑(orientation.map (fin n) φ.to_linear_equiv) o).volume_form) x = ⇑(o.volume_form) (⇑(φ.symm) ∘ x)

source

theorem orientation.volume_form_comp_linear_isometry_equiv {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] {n : ℕ} [fact (fdim E = n)] (o : orientation ℝ E (fin n)) (φ : E ≃ₗᵢ[ℝ ] E) (hφ : 0 < ⇑linear_map.det ↑(φ.to_linear_equiv)) (x : fin n → E) :

⇑(o.volume_form) (⇑φ ∘ x) = ⇑(o.volume_form) x

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