mathlib documentation

linear_algebra.orientation

Orientations of modules and rays in modules #

This file defines rays in modules and orientations of modules.

Main definitions #

Implementation notes #

orientation is defined for an arbitrary index type, but the main intended use case is when that index type is a fintype and there exists a basis of the same cardinality.

References #

def same_ray (R : Type u_1) [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (v₁ v₂ : M) :
Prop

Two vectors are in the same ray if some positive multiples of them are equal (in the typical case over a field, this means each is a positive multiple of the other). Over a field, this is equivalent to mul_action.orbit_rel.

Equations
theorem same_ray.refl {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (x : M) :
same_ray R x x

same_ray is reflexive.

theorem same_ray.symm {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y : M} :
same_ray R x ysame_ray R y x

same_ray is symmetric.

theorem same_ray.trans {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y z : M} :
same_ray R x ysame_ray R y zsame_ray R x z

same_ray is transitive.

theorem same_ray_comm {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y : M} :
same_ray R x y same_ray R y x
theorem equivalence_same_ray (R : Type u_1) [ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] [nontrivial R] :

same_ray is an equivalence relation.

theorem same_ray_pos_smul_right {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (v : M) {r : R} (h : 0 < r) :
same_ray R v (r v)

A vector is in the same ray as a positive multiple of itself.

theorem same_ray.pos_smul_right {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {v₁ v₂ : M} {r : R} (h : same_ray R v₁ v₂) (hr : 0 < r) :
same_ray R v₁ (r v₂)

A vector is in the same ray as a positive multiple of one it is in the same ray as.

theorem same_ray_pos_smul_left {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (v : M) {r : R} (h : 0 < r) :
same_ray R (r v) v

A positive multiple of a vector is in the same ray as that vector.

theorem same_ray.pos_smul_left {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {v₁ v₂ : M} {r : R} (h : same_ray R v₁ v₂) (hr : 0 < r) :
same_ray R (r v₁) v₂

A positive multiple of a vector is in the same ray as one it is in the same ray as.

theorem same_ray.map {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {v₁ v₂ : M} (f : M →ₗ[R] N) (h : same_ray R v₁ v₂) :
same_ray R (f v₁) (f v₂)

If two vectors are on the same ray then they remain so after appling a linear map.

@[simp]
theorem same_ray_map_iff {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {v₁ v₂ : M} (e : M ≃ₗ[R] N) :
same_ray R (e v₁) (e v₂) same_ray R v₁ v₂

If two vectors are on the same ray then they remain so after appling a linear equivalence.

theorem same_ray.smul {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {S : Type u_3} [has_scalar S M] [smul_comm_class R S M] {v₁ v₂ : M} (s : S) (h : same_ray R v₁ v₂) :
same_ray R (s v₁) (s v₂)

If two vectors are on the same ray then both scaled by the same action are also on the same ray.

def same_ray_setoid (R : Type u_1) [ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] [nontrivial R] :

The setoid of the same_ray relation for elements of a module.

Equations
def ray_vector (M : Type u_2) [add_comm_monoid M] :
Type u_2

Nonzero vectors, as used to define rays.

Equations
def ray_vector.same_ray_setoid (R : Type u_1) [ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] [nontrivial R] :

The setoid of the same_ray relation for the subtype of nonzero vectors.

Equations
theorem equiv_iff_same_ray {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (v₁ v₂ : ray_vector M) :
v₁ v₂ same_ray R v₁ v₂

Equivalence of nonzero vectors, in terms of same_ray.

@[nolint]
def module.ray (R : Type u_1) [ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] [nontrivial R] :
Type u_2

A ray (equivalence class of nonzero vectors with common positive multiples) in a module.

Equations
def orientation (R : Type u_1) [ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] (ι : Type u_4) [decidable_eq ι] [nontrivial R] :
Type (max u_2 u_1 u_4)

An orientation of a module, intended to be used when ι is a fintype with the same cardinality as a basis.

@[class]
structure module.oriented (R : Type u_1) [ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] (ι : Type u_4) [decidable_eq ι] [nontrivial R] :
Type (max u_1 u_2 u_4)

A type class fixing an orientation of a module.

@[protected]
def ray_of_ne_zero (R : Type u_1) [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (v : M) (h : v 0) :

The ray given by a nonzero vector.

Equations
theorem module.ray.ind (R : Type u_1) [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] {C : module.ray R M → Prop} (h : ∀ (v : M) (hv : v 0), C (ray_of_ne_zero R v hv)) (x : module.ray R M) :
C x

An induction principle for module.ray, used as induction x using module.ray.ind.

theorem ray_eq_iff (R : Type u_1) [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] {v₁ v₂ : M} (hv₁ : v₁ 0) (hv₂ : v₂ 0) :
ray_of_ne_zero R v₁ hv₁ = ray_of_ne_zero R v₂ hv₂ same_ray R v₁ v₂

The rays given by two nonzero vectors are equal if and only if those vectors satisfy same_ray.

@[simp]
theorem ray_pos_smul {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] {v : M} (h : v 0) {r : R} (hr : 0 < r) (hrv : r v 0) :

The ray given by a positive multiple of a nonzero vector.

def ray_vector.map_linear_equiv {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] (e : M ≃ₗ[R] N) :

An equivalence between modules implies an equivalence between ray vectors.

Equations
def module.ray.map {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] [nontrivial R] (e : M ≃ₗ[R] N) :

An equivalence between modules implies an equivalence between rays.

Equations
@[simp]
theorem module.ray.map_apply {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] [nontrivial R] (e : M ≃ₗ[R] N) (v : M) (hv : v 0) :
@[simp]
theorem module.ray.map_refl {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] :
@[simp]
theorem module.ray.map_symm {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] [nontrivial R] (e : M ≃ₗ[R] N) :
def orientation.map {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] (ι : Type u_4) [decidable_eq ι] [nontrivial R] (e : M ≃ₗ[R] N) :

An equivalence between modules implies an equivalence between orientations.

Equations
@[simp]
theorem orientation.map_apply {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] (ι : Type u_4) [decidable_eq ι] [nontrivial R] (e : M ≃ₗ[R] N) (v : alternating_map R M R ι) (hv : v 0) :
@[simp]
theorem orientation.map_refl {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (ι : Type u_4) [decidable_eq ι] [nontrivial R] :
@[simp]
theorem orientation.map_symm {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] (ι : Type u_4) [decidable_eq ι] [nontrivial R] (e : M ≃ₗ[R] N) :
@[protected, instance]
def ray_vector.mul_action {M : Type u_2} [add_comm_monoid M] {G : Type u_5} [group G] [distrib_mul_action G M] :

Any invertible action preserves the non-zeroness of ray vectors. This is primarily of interest when G = Rˣ

Equations
@[protected, instance]
def module.ray.mul_action {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {G : Type u_5} [group G] [nontrivial R] [distrib_mul_action G M] [smul_comm_class R G M] :

Any invertible action preserves the non-zeroness of rays. This is primarily of interest when G = Rˣ

Equations
@[simp]
theorem module.ray.linear_equiv_smul_eq_map {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (e : M ≃ₗ[R] M) (v : module.ray R M) :

The action via linear_equiv.apply_distrib_mul_action corresponds to module.ray.map.

@[simp]
theorem smul_ray_of_ne_zero {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {G : Type u_5} [group G] [nontrivial R] [distrib_mul_action G M] [smul_comm_class R G M] (g : G) (v : M) (hv : v 0) :
theorem module.ray.units_smul_of_pos {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (u : Rˣ) (hu : 0 < u) (v : module.ray R M) :
u v = v

Scaling by a positive unit is a no-op.

noncomputable def module.ray.some_ray_vector {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (x : module.ray R M) :

An arbitrary ray_vector giving a ray.

Equations
@[simp]
theorem module.ray.some_ray_vector_ray {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (x : module.ray R M) :

The ray of some_ray_vector.

noncomputable def module.ray.some_vector {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (x : module.ray R M) :
M

An arbitrary nonzero vector giving a ray.

Equations
@[simp]
theorem module.ray.some_vector_ne_zero {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (x : module.ray R M) :

some_vector is nonzero.

@[simp]
theorem module.ray.some_vector_ray {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (x : module.ray R M) :

The ray of some_vector.

theorem same_ray.neg {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {v₁ v₂ : M} :
same_ray R v₁ v₂same_ray R (-v₁) (-v₂)

If two vectors are in the same ray, so are their negations.

@[simp]
theorem same_ray_neg_iff {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {v₁ v₂ : M} :
same_ray R (-v₁) (-v₂) same_ray R v₁ v₂

same_ray.neg as an iff.

theorem same_ray_neg_swap {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {v₁ v₂ : M} :
same_ray R (-v₁) v₂ same_ray R v₁ (-v₂)
theorem eq_zero_of_same_ray_self_neg {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {v₁ : M} (h : same_ray R v₁ (-v₁)) :
v₁ = 0

If a vector is in the same ray as its negation, that vector is zero.

@[protected, instance]
def ray_vector.has_neg {M : Type u_2} [add_comm_group M] :

Negating a nonzero vector.

Equations
@[simp, norm_cast]
theorem ray_vector.coe_neg {M : Type u_2} [add_comm_group M] (v : ray_vector M) :

Negating a nonzero vector commutes with coercion to the underlying module.

@[protected, simp]
theorem ray_vector.neg_neg {M : Type u_2} [add_comm_group M] (v : ray_vector M) :
--v = v

Negating a nonzero vector twice produces the original vector.

@[simp]
theorem ray_vector.equiv_neg_iff (R : Type u_1) [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] (v₁ v₂ : ray_vector M) :
-v₁ -v₂ v₁ v₂

If two nonzero vectors are equivalent, so are their negations.

@[protected, instance]
def module.ray.has_neg (R : Type u_1) [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] :

Negating a ray.

Equations
theorem ray_neg (R : Type u_1) [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] (v : M) (h : v 0) :

The ray given by the negation of a nonzero vector.

@[protected, simp]
theorem module.ray.neg_neg {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] (x : module.ray R M) :
--x = x

Negating a ray twice produces the original ray.

theorem module.ray.ne_neg_self {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] [no_zero_smul_divisors R M] (x : module.ray R M) :
x -x

A ray does not equal its own negation.

theorem module.ray.units_smul_of_neg {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] (u : Rˣ) (hu : u < 0) (v : module.ray R M) :
u v = -v

Scaling by a negative unit is negation.

@[protected]
noncomputable def basis.orientation {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [fintype ι] [decidable_eq ι] [nontrivial R] (e : basis ι R M) :

The orientation given by a basis.

Equations
theorem basis.orientation_map {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] {ι : Type u_4} [fintype ι] [decidable_eq ι] [nontrivial R] (e : basis ι R M) (f : M ≃ₗ[R] N) :
theorem basis.map_orientation_eq_det_inv_smul {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [fintype ι] [decidable_eq ι] [nontrivial R] [is_domain R] (e : basis ι R M) (x : orientation R M ι) (f : M ≃ₗ[R] M) :

The value of orientation.map when the index type has the cardinality of a basis, in terms of f.det.

theorem basis.orientation_units_smul {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [fintype ι] [decidable_eq ι] [nontrivial R] (e : basis ι R M) (w : ι → Rˣ) :
(e.units_smul w).orientation = (∏ (i : ι), w i)⁻¹ e.orientation

The orientation given by a basis derived using units_smul, in terms of the product of those units.

theorem same_ray_of_mem_orbit {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {v₁ v₂ : M} (h : v₁ mul_action.orbit (units.pos_subgroup R) v₂) :
same_ray R v₁ v₂

same_ray follows from membership of mul_action.orbit for the units.pos_subgroup.

@[simp]
theorem units_inv_smul {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (u : Rˣ) (v : module.ray R M) :
u⁻¹ v = u v

Scaling by an inverse unit is the same as scaling by itself.

@[simp]
theorem same_ray_smul_right_iff {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {v : M} (hv : v 0) (r : R) :
same_ray R v (r v) 0 < r

A nonzero vector is in the same ray as a multiple of itself if and only if that multiple is positive.

@[simp]
theorem same_ray_smul_left_iff {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {v : M} (hv : v 0) (r : R) :
same_ray R (r v) v 0 < r

A multiple of a nonzero vector is in the same ray as that vector if and only if that multiple is positive.

@[simp]
theorem same_ray_neg_smul_right_iff {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {v : M} (hv : v 0) (r : R) :
same_ray R (-v) (r v) r < 0

The negation of a nonzero vector is in the same ray as a multiple of that vector if and only if that multiple is negative.

@[simp]
theorem same_ray_neg_smul_left_iff {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {v : M} (hv : v 0) (r : R) :
same_ray R (r v) (-v) r < 0

A multiple of a nonzero vector is in the same ray as the negation of that vector if and only if that multiple is negative.

@[simp]
theorem units_smul_eq_self_iff {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {u : Rˣ} {v : module.ray R M} :
u v = v 0 < u

A nonzero vector is in the same ray as a multiple of itself if and only if that multiple is positive.

@[simp]
theorem units_smul_eq_neg_iff {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {u : Rˣ} {v : module.ray R M} :
u v = -v u < 0

A nonzero vector is in the same ray as a multiple of itself if and only if that multiple is positive.

theorem basis.orientation_eq_iff_det_pos {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] (e₁ e₂ : basis ι R M) :
e₁.orientation = e₂.orientation 0 < (e₁.det) e₂

The orientations given by two bases are equal if and only if the determinant of one basis with respect to the other is positive.

theorem basis.orientation_eq_or_eq_neg {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] (e : basis ι R M) (x : orientation R M ι) :

Given a basis, any orientation equals the orientation given by that basis or its negation.

theorem basis.orientation_ne_iff_eq_neg {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] (e : basis ι R M) (x : orientation R M ι) :

Given a basis, an orientation equals the negation of that given by that basis if and only if it does not equal that given by that basis.

theorem basis.orientation_comp_linear_equiv_eq_iff_det_pos {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] (e : basis ι R M) (f : M ≃ₗ[R] M) :

Composing a basis with a linear equiv gives the same orientation if and only if the determinant is positive.

theorem basis.orientation_comp_linear_equiv_eq_neg_iff_det_neg {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] (e : basis ι R M) (f : M ≃ₗ[R] M) :

Composing a basis with a linear equiv gives the negation of that orientation if and only if the determinant is negative.

@[simp]
theorem basis.orientation_neg_single {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [nontrivial R] (e : basis ι R M) (i : ι) :

Negating a single basis vector (represented using units_smul) negates the corresponding orientation.

noncomputable def basis.adjust_to_orientation {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [nontrivial R] [nonempty ι] (e : basis ι R M) (x : orientation R M ι) :
basis ι R M

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

Equations
@[simp]
theorem basis.orientation_adjust_to_orientation {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [nontrivial R] [nonempty ι] (e : basis ι R M) (x : orientation R M ι) :

adjust_to_orientation gives a basis with the required orientation.

theorem basis.adjust_to_orientation_apply_eq_or_eq_neg {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [nontrivial R] [nonempty ι] (e : basis ι R M) (x : orientation R M ι) (i : ι) :

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

theorem same_ray_iff_mem_orbit (R : Type u_1) [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] (v₁ v₂ : M) :

same_ray is equivalent to membership of mul_action.orbit for the units.pos_subgroup.

theorem orientation.eq_or_eq_neg {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] (x₁ x₂ : orientation R M ι) (h : fintype.card ι = finite_dimensional.finrank R M) :
x₁ = x₂ x₁ = -x₂

If the index type has cardinality equal to the finite dimension, any two orientations are equal or negations.

theorem orientation.ne_iff_eq_neg {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] (x₁ x₂ : orientation R M ι) (h : fintype.card ι = finite_dimensional.finrank R M) :
x₁ x₂ x₁ = -x₂

If the index type has cardinality equal to the finite dimension, an orientation equals the negation of another orientation if and only if they are not equal.

theorem orientation.map_eq_det_inv_smul {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] (x : orientation R M ι) (f : M ≃ₗ[R] M) (h : fintype.card ι = finite_dimensional.finrank R M) :

The value of orientation.map when the index type has cardinality equal to the finite dimension, in terms of f.det.

theorem orientation.map_eq_iff_det_pos {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] (x : orientation R M ι) (f : M ≃ₗ[R] M) (h : fintype.card ι = finite_dimensional.finrank R M) :

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 same orientation if and only if the determinant is positive.

theorem orientation.map_eq_neg_iff_det_neg {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] (x : orientation R M ι) (f : M ≃ₗ[R] M) (h : fintype.card ι = finite_dimensional.finrank R M) :

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.

noncomputable def orientation.some_basis {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] [nonempty ι] (x : orientation R M ι) (h : fintype.card ι = finite_dimensional.finrank R M) :
basis ι R M

If the index type has cardinality equal to the finite dimension, a basis with the given orientation.

Equations
@[simp]
theorem orientation.some_basis_orientation {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] [nonempty ι] (x : orientation R M ι) (h : fintype.card ι = finite_dimensional.finrank R M) :

some_basis gives a basis with the required orientation.