# mathlib3documentation

linear_algebra.ray

# Rays in modules #

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

This file defines rays in modules.

## Main definitions #

• same_ray: two vectors belong to the same ray if they are proportional with a nonnegative coefficient.

• module.ray is a type for the equivalence class of nonzero vectors in a module with some common positive multiple.

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

Two vectors are in the same ray if either one of them is zero or some positive multiples of them are equal (in the typical case over a field, this means one of them is a nonnegative multiple of the other).

Equations
@[simp]
theorem same_ray.zero_left {R : Type u_1} {M : Type u_2} [ M] (y : M) :
0 y
@[simp]
theorem same_ray.zero_right {R : Type u_1} {M : Type u_2} [ M] (x : M) :
x 0
theorem same_ray.of_subsingleton {R : Type u_1} {M : Type u_2} [ M] [subsingleton M] (x y : M) :
x y
theorem same_ray.of_subsingleton' {R : Type u_1} {M : Type u_2} [ M] [subsingleton R] (x y : M) :
x y
@[refl]
theorem same_ray.refl {R : Type u_1} {M : Type u_2} [ M] (x : M) :
x x

same_ray is reflexive.

@[protected]
theorem same_ray.rfl {R : Type u_1} {M : Type u_2} [ M] {x : M} :
x x
@[symm]
theorem same_ray.symm {R : Type u_1} {M : Type u_2} [ M] {x y : M} (h : x y) :
y x

same_ray is symmetric.

theorem same_ray.exists_pos {R : Type u_1} {M : Type u_2} [ M] {x y : M} (h : x y) (hx : x 0) (hy : y 0) :
(r₁ r₂ : R), 0 < r₁ 0 < r₂ r₁ x = r₂ y

If x and y are nonzero vectors on the same ray, then there exist positive numbers r₁ r₂ such that r₁ • x = r₂ • y.

theorem same_ray_comm {R : Type u_1} {M : Type u_2} [ M] {x y : M} :
x y y x
theorem same_ray.trans {R : Type u_1} {M : Type u_2} [ M] {x y z : M} (hxy : x y) (hyz : y z) (hy : y = 0 x = 0 z = 0) :
x z

same_ray is transitive unless the vector in the middle is zero and both other vectors are nonzero.

theorem same_ray_nonneg_smul_right {R : Type u_1} {M : Type u_2} [ M] (v : M) {r : R} (h : 0 r) :
v (r v)

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

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

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

theorem same_ray.nonneg_smul_right {R : Type u_1} {M : Type u_2} [ M] {x y : M} {r : R} (h : x y) (hr : 0 r) :
x (r y)

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

theorem same_ray.pos_smul_right {R : Type u_1} {M : Type u_2} [ M] {x y : M} {r : R} (h : x y) (hr : 0 < r) :
x (r y)

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

theorem same_ray_nonneg_smul_left {R : Type u_1} {M : Type u_2} [ M] (v : M) {r : R} (h : 0 r) :
(r v) v

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

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

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

theorem same_ray.nonneg_smul_left {R : Type u_1} {M : Type u_2} [ M] {x y : M} {r : R} (h : x y) (hr : 0 r) :
(r x) y

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

theorem same_ray.pos_smul_left {R : Type u_1} {M : Type u_2} [ M] {x y : M} {r : R} (h : x y) (hr : 0 < r) :
(r x) y

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} {M : Type u_2} [ M] {N : Type u_3} [ N] {x y : M} (f : M →ₗ[R] N) (h : x y) :
(f x) (f y)

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

theorem function.injective.same_ray_map_iff {R : Type u_1} {M : Type u_2} [ M] {N : Type u_3} [ N] {x y : M} {F : Type u_4} [ M N] {f : F} (hf : function.injective f) :
(f x) (f y) x y

The images of two vectors under an injective linear map are on the same ray if and only if the original vectors are on the same ray.

@[simp]
theorem same_ray_map_iff {R : Type u_1} {M : Type u_2} [ M] {N : Type u_3} [ N] {x y : M} (e : M ≃ₗ[R] N) :
(e x) (e y) x y

The images of two vectors under a linear equivalence are on the same ray if and only if the original vectors are on the same ray.

theorem same_ray.smul {R : Type u_1} {M : Type u_2} [ M] {x y : M} {S : Type u_3} [monoid S] [ M] [ M] (h : x y) (s : S) :
(s x) (s y)

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

theorem same_ray.add_left {R : Type u_1} {M : Type u_2} [ M] {x y z : M} (hx : x z) (hy : y z) :
(x + y) z

If x and y are on the same ray as z, then so is x + y.

theorem same_ray.add_right {R : Type u_1} {M : Type u_2} [ M] {x y z : M} (hy : x y) (hz : x z) :
x (y + z)

If y and z are on the same ray as x, then so is y + z.

@[nolint]
def ray_vector (R : Type u_1) (M : Type u_2) [has_zero M] :
Type u_2

Nonzero vectors, as used to define rays. This type depends on an unused argument R so that ray_vector.setoid can be an instance.

Equations
• M = {v // v 0}
Instances for ray_vector
@[protected, instance]
def ray_vector.has_coe {R : Type u_1} {M : Type u_2} [has_zero M] :
has_coe M) M
Equations
@[protected, instance]
def ray_vector.nonempty {R : Type u_1} {M : Type u_2} [has_zero M] [nontrivial M] :
@[protected, instance]
def ray_vector.setoid (R : Type u_1) (M : Type u_2) [ M] :

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

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

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

Equations
• M =
Instances for module.ray
theorem equiv_iff_same_ray {R : Type u_1} {M : Type u_2} [ M] {v₁ v₂ : M} :
v₁ v₂ v₁ v₂

Equivalence of nonzero vectors, in terms of same_ray.

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

The ray given by a nonzero vector.

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

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

@[protected, instance]
def module.ray.nonempty {R : Type u_1} {M : Type u_2} [ M] [nontrivial M] :
theorem ray_eq_iff {R : Type u_1} {M : Type u_2} [ M] {v₁ v₂ : M} (hv₁ : v₁ 0) (hv₂ : v₂ 0) :
v₁ hv₁ = v₂ hv₂ 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} {M : Type u_2} [ M] {v : M} (h : v 0) {r : R} (hr : 0 < r) (hrv : r v 0) :
(r v) hrv = h

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

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

An equivalence between modules implies an equivalence between ray vectors.

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

An equivalence between modules implies an equivalence between rays.

Equations
@[simp]
theorem module.ray.map_apply {R : Type u_1} {M : Type u_2} [ M] {N : Type u_3} [ N] (e : M ≃ₗ[R] N) (v : M) (hv : v 0) :
v hv) = (e v) _
@[simp]
theorem module.ray.map_refl {R : Type u_1} {M : Type u_2} [ M] :
@[simp]
theorem module.ray.map_symm {R : Type u_1} {M : Type u_2} [ M] {N : Type u_3} [ N] (e : M ≃ₗ[R] N) :
@[protected, instance]
def ray_vector.mul_action {M : Type u_2} {G : Type u_5} [group G] [ M] {R : Type u_1} :
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} {M : Type u_2} [ M] {G : Type u_5} [group G] [ M] [ M] :
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} {M : Type u_2} [ M] (e : M ≃ₗ[R] M) (v : M) :
e v = v

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} {M : Type u_2} [ M] {G : Type u_5} [group G] [ M] [ M] (g : G) (v : M) (hv : v 0) :
g hv = (g v) _
theorem module.ray.units_smul_of_pos {R : Type u_1} {M : Type u_2} [ M] (u : Rˣ) (hu : 0 < u) (v : M) :
u v = v

Scaling by a positive unit is a no-op.

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

An arbitrary ray_vector giving a ray.

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

The ray of some_ray_vector.

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

An arbitrary nonzero vector giving a ray.

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

some_vector is nonzero.

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

The ray of some_vector.

@[simp]
theorem same_ray_neg_iff {R : Type u_1} {M : Type u_2} [ M] {x y : M} :
(-x) (-y) x y

same_ray.neg as an iff.

theorem same_ray.of_neg {R : Type u_1} {M : Type u_2} [ M] {x y : M} :
(-x) (-y) x y

Alias of the forward direction of same_ray_neg_iff.

theorem same_ray.neg {R : Type u_1} {M : Type u_2} [ M] {x y : M} :
x y (-x) (-y)

Alias of the reverse direction of same_ray_neg_iff.

theorem same_ray_neg_swap {R : Type u_1} {M : Type u_2} [ M] {x y : M} :
(-x) y x (-y)
theorem eq_zero_of_same_ray_neg_smul_right {R : Type u_1} {M : Type u_2} [ M] {x : M} {r : R} (hr : r < 0) (h : x (r x)) :
x = 0
theorem eq_zero_of_same_ray_self_neg {R : Type u_1} {M : Type u_2} [ M] {x : M} (h : x (-x)) :
x = 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} {R : Type u_1} :

Negating a nonzero vector.

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

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

@[protected, instance]
def ray_vector.has_involutive_neg {M : Type u_2} {R : Type u_1} :

Negating a nonzero vector twice produces the original vector.

Equations
@[simp]
theorem ray_vector.equiv_neg_iff {R : Type u_1} {M : Type u_2} [ M] {v₁ v₂ : 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) {M : Type u_2} [ M] :

Negating a ray.

Equations
@[simp]
theorem neg_ray_of_ne_zero (R : Type u_1) {M : Type u_2} [ M] (v : M) (h : v 0) :
- h = (-v) _

The ray given by the negation of a nonzero vector.

@[protected, instance]
def module.ray.has_involutive_neg {R : Type u_1} {M : Type u_2} [ M] :

Negating a ray twice produces the original ray.

Equations
theorem module.ray.ne_neg_self {R : Type u_1} {M : Type u_2} [ M] (x : M) :
x -x

A ray does not equal its own negation.

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

Scaling by a negative unit is negation.

@[protected, simp]
theorem module.ray.map_neg {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] (f : M ≃ₗ[R] N) (v : M) :
(-v) = - v
theorem same_ray_of_mem_orbit {R : Type u_1} {M : Type u_2} [ M] {v₁ v₂ : M} (h : v₁ ) :
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} {M : Type u_2} [ M] (u : Rˣ) (v : 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} {M : Type u_2} [ M] {v : M} {r : R} :
v (r v) 0 r v = 0
theorem same_ray_smul_right_iff_of_ne {R : Type u_1} {M : Type u_2} [ M] {v : M} (hv : v 0) {r : R} (hr : r 0) :
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} {M : Type u_2} [ M] {v : M} {r : R} :
(r v) v 0 r v = 0
theorem same_ray_smul_left_iff_of_ne {R : Type u_1} {M : Type u_2} [ M] {v : M} (hv : v 0) {r : R} (hr : r 0) :
(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} {M : Type u_2} [ M] {v : M} {r : R} :
(-v) (r v) r 0 v = 0
theorem same_ray_neg_smul_right_iff_of_ne {R : Type u_1} {M : Type u_2} [ M] {v : M} {r : R} (hv : v 0) (hr : r 0) :
(-v) (r v) r < 0
@[simp]
theorem same_ray_neg_smul_left_iff {R : Type u_1} {M : Type u_2} [ M] {v : M} {r : R} :
(r v) (-v) r 0 v = 0
theorem same_ray_neg_smul_left_iff_of_ne {R : Type u_1} {M : Type u_2} [ M] {v : M} {r : R} (hv : v 0) (hr : r 0) :
(r v) (-v) r < 0
@[simp]
theorem units_smul_eq_self_iff {R : Type u_1} {M : Type u_2} [ M] {u : Rˣ} {v : M} :
u v = v 0 < u
@[simp]
theorem units_smul_eq_neg_iff {R : Type u_1} {M : Type u_2} [ M] {u : Rˣ} {v : M} :
u v = -v u < 0
theorem same_ray_or_same_ray_neg_iff_not_linear_independent {R : Type u_1} {M : Type u_2} [ M] {x y : M} :
x y x (-y) ¬ ![x, y]

Two vectors are in the same ray, or the first is in the same ray as the negation of the second, if and only if they are not linearly independent.

theorem same_ray_or_ne_zero_and_same_ray_neg_iff_not_linear_independent {R : Type u_1} {M : Type u_2} [ M] {x y : M} :
x y x 0 y 0 x (-y) ¬ ![x, y]

Two vectors are in the same ray, or they are nonzero and the first is in the same ray as the negation of the second, if and only if they are not linearly independent.

theorem same_ray.exists_pos_left {R : Type u_1} {M : Type u_2} [ M] {x y : M} (h : x y) (hx : x 0) (hy : y 0) :
(r : R), 0 < r r x = y
theorem same_ray.exists_pos_right {R : Type u_1} {M : Type u_2} [ M] {x y : M} (h : x y) (hx : x 0) (hy : y 0) :
(r : R), 0 < r x = r y
theorem same_ray.exists_nonneg_left {R : Type u_1} {M : Type u_2} [ M] {x y : M} (h : x y) (hx : x 0) :
(r : R), 0 r r x = y

If a vector v₂ is on the same ray as a nonzero vector v₁, then it is equal to c • v₁ for some nonnegative c.

theorem same_ray.exists_nonneg_right {R : Type u_1} {M : Type u_2} [ M] {x y : M} (h : x y) (hy : y 0) :
(r : R), 0 r x = r y

If a vector v₁ is on the same ray as a nonzero vector v₂, then it is equal to c • v₂ for some nonnegative c.

theorem same_ray.exists_eq_smul_add {R : Type u_1} {M : Type u_2} [ M] {v₁ v₂ : M} (h : v₁ v₂) :
(a b : R), 0 a 0 b a + b = 1 v₁ = a (v₁ + v₂) v₂ = b (v₁ + v₂)

If vectors v₁ and v₂ are on the same ray, then for some nonnegative a b, a + b = 1, we have v₁ = a • (v₁ + v₂) and v₂ = b • (v₁ + v₂).

theorem same_ray.exists_eq_smul {R : Type u_1} {M : Type u_2} [ M] {v₁ v₂ : M} (h : v₁ v₂) :
(u : M) (a b : R), 0 a 0 b a + b = 1 v₁ = a u v₂ = b u

If vectors v₁ and v₂ are on the same ray, then they are nonnegative multiples of the same vector. Actually, this vector can be assumed to be v₁ + v₂, see same_ray.exists_eq_smul_add.

theorem exists_pos_left_iff_same_ray {R : Type u_1} {M : Type u_2} [ M] {x y : M} (hx : x 0) (hy : y 0) :
( (r : R), 0 < r r x = y) x y
theorem exists_pos_left_iff_same_ray_and_ne_zero {R : Type u_1} {M : Type u_2} [ M] {x y : M} (hx : x 0) :
( (r : R), 0 < r r x = y) x y y 0
theorem exists_nonneg_left_iff_same_ray {R : Type u_1} {M : Type u_2} [ M] {x y : M} (hx : x 0) :
( (r : R), 0 r r x = y) x y
theorem exists_pos_right_iff_same_ray {R : Type u_1} {M : Type u_2} [ M] {x y : M} (hx : x 0) (hy : y 0) :
( (r : R), 0 < r x = r y) x y
theorem exists_pos_right_iff_same_ray_and_ne_zero {R : Type u_1} {M : Type u_2} [ M] {x y : M} (hy : y 0) :
( (r : R), 0 < r x = r y) x y x 0
theorem exists_nonneg_right_iff_same_ray {R : Type u_1} {M : Type u_2} [ M] {x y : M} (hy : y 0) :
( (r : R), 0 r x = r y) x y