mathlib documentation

linear_algebra.ray

Rays in modules #

This file defines rays in modules.

Main definitions #

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 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} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (y : M) :
same_ray R 0 y
@[simp]
theorem same_ray.zero_right {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (x : M) :
same_ray R x 0
theorem same_ray.of_subsingleton {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [subsingleton M] (x y : M) :
same_ray R x y
theorem same_ray.of_subsingleton' {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [subsingleton R] (x y : M) :
same_ray R x y
theorem same_ray.refl {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (x : M) :
same_ray R x x

same_ray is reflexive.

@[protected]
theorem same_ray.rfl {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x : M} :
same_ray R x x
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} (h : same_ray R x y) :
same_ray R y x

same_ray is symmetric.

theorem same_ray.exists_pos {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y : M} (h : same_ray R 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} [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 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} (hxy : same_ray R x y) (hyz : same_ray R y z) (hy : y = 0x = 0 z = 0) :
same_ray R 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} [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 nonnegative 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 : 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.nonneg_smul_right {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y : M} {r : R} (h : same_ray R x y) (hr : 0 r) :
same_ray 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} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y : M} {r : R} (h : same_ray R x y) (hr : 0 < r) :
same_ray 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} [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 nonnegative 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 : 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.nonneg_smul_left {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y : M} {r : R} (h : same_ray R x y) (hr : 0 r) :
same_ray 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} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y : M} {r : R} (h : same_ray R x y) (hr : 0 < r) :
same_ray 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} [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] {x y : M} (f : M →ₗ[R] N) (h : same_ray R x y) :
same_ray R (f x) (f y)

If two vectors are on the same ray then they remain so after applying 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] {x y : M} (e : M ≃ₗ[R] N) :
same_ray R (e x) (e y) same_ray R 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} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y : M} {S : Type u_3} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] (h : same_ray R x y) (s : S) :
same_ray R (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} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y z : M} (hx : same_ray R x z) (hy : same_ray R y z) :
same_ray R (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} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y z : M} (hy : same_ray R x y) (hz : same_ray R x z) :
same_ray R 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
Instances for ray_vector
@[protected, instance]
def ray_vector.has_coe {R : Type u_1} {M : Type u_2} [has_zero 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) [ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] :

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

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

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

Equations
Instances for module.ray
theorem equiv_iff_same_ray {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {v₁ v₂ : ray_vector R M} :
v₁ v₂ same_ray R v₁ v₂

Equivalence of nonzero vectors, in terms of same_ray.

@[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] (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] {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.

@[protected, instance]
def module.ray.nonempty {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial M] :
theorem ray_eq_iff {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {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] {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] (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] (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] :
@[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] (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] {R : Type u_1} :

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] [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] (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] [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] (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] (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] (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] (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] (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] (x : module.ray R M) :

The ray of some_vector.

@[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] {x y : M} :
same_ray R (-x) (-y) same_ray R x y

same_ray.neg as an iff.

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

Alias of the forward direction of same_ray_neg_iff.

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

Alias of the reverse direction of same_ray_neg_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] {x y : M} :
same_ray R (-x) y same_ray R x (-y)
theorem eq_zero_of_same_ray_neg_smul_right {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {x : M} [no_zero_smul_divisors R M] {r : R} (hr : r < 0) (h : same_ray R x (r x)) :
x = 0
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] {x : M} [no_zero_smul_divisors R M] (h : same_ray R 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} [add_comm_group M] {R : Type u_1} :

Negating a nonzero vector.

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

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

@[protected, instance]
def ray_vector.has_involutive_neg {M : Type u_2} [add_comm_group M] {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} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {v₁ v₂ : ray_vector R 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] :

Negating a ray.

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

The ray given by the negation of a nonzero vector.

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

Negating a ray twice produces the original ray.

Equations
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] [no_zero_smul_divisors R M] (x : module.ray R M) :
x -x

A ray does not equal its own negation.

theorem module.ray.neg_units_smul {R : Type u_1} [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)
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] (u : Rˣ) (hu : u < 0) (v : module.ray R M) :
u v = -v

Scaling by a negative unit is negation.

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} {r : R} :
same_ray R v (r v) 0 r v = 0
theorem same_ray_smul_right_iff_of_ne {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} (hr : r 0) :
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} {r : R} :
same_ray R (r v) v 0 r v = 0
theorem same_ray_smul_left_iff_of_ne {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} (hr : r 0) :
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} {r : R} :
same_ray R (-v) (r v) r 0 v = 0
theorem same_ray_neg_smul_right_iff_of_ne {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} {r : R} (hv : v 0) (hr : r 0) :
same_ray R (-v) (r v) r < 0
@[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} {r : R} :
same_ray R (r v) (-v) r 0 v = 0
theorem same_ray_neg_smul_left_iff_of_ne {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} {r : R} (hv : v 0) (hr : r 0) :
same_ray R (r v) (-v) r < 0
@[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
@[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
theorem same_ray.exists_pos_left {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {x y : M} (h : same_ray R 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} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {x y : M} (h : same_ray R 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} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {x y : M} (h : same_ray R 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} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {x y : M} (h : same_ray R 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} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {v₁ v₂ : M} (h : same_ray R 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} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {v₁ v₂ : M} (h : same_ray R 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.