Rays in modules

This file defines rays in modules.

Main definitions

• SameRay: 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 SameRay (R : Type u_1) [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (v₁ : M) (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

• SameRay R v₁ v₂ = (v₁ = 0 ∨ v₂ = 0 ∨ ∃ (r₁ : R) (r₂ : R), 0 < r₁ ∧ 0 < r₂ ∧ r₁ • v₁ = r₂ • v₂)

@[simp]

theorem SameRay.zero_left {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (y : M) : SameRay R 0 y

@[simp]

theorem SameRay.zero_right {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (x : M) : SameRay R x 0

theorem SameRay.of_subsingleton {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [Subsingleton M] (x : M) (y : M) : SameRay R x y

theorem SameRay.of_subsingleton' {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [Subsingleton R] (x : M) (y : M) : SameRay R x y

theorem SameRay.refl {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (x : M) : SameRay R x x

SameRay is reflexive.

theorem SameRay.rfl {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {x : M} : SameRay R x x

theorem SameRay.symm {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {x : M} {y : M} (h : SameRay R x y) : SameRay R y x

SameRay is symmetric.

theorem SameRay.exists_pos {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {x : M} {y : M} (h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (r₁ : 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 SameRay.sameRay_comm {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {x : M} {y : M} : SameRay R x y ↔ SameRay R y x

theorem SameRay.trans {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {x : M} {y : M} {z : M} (hxy : SameRay R x y) (hyz : SameRay R y z) (hy : y = 0 → x = 0 ∨ z = 0) : SameRay R x z

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

theorem SameRay.sameRay_nonneg_smul_right {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {S : Type u_5} [OrderedCommSemiring S] [Algebra S R] [Module S M] [SMulPosMono S R] [IsScalarTower S R M] {a : S} (v : M) (h : 0 ≤ a) : SameRay R v (a • v)

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

theorem SameRay.sameRay_nonneg_smul_left {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {S : Type u_5} [OrderedCommSemiring S] [Algebra S R] [Module S M] [SMulPosMono S R] [IsScalarTower S R M] {a : S} (v : M) (ha : 0 ≤ a) : SameRay R (a • v) v

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

theorem SameRay.sameRay_pos_smul_right {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {S : Type u_5} [OrderedCommSemiring S] [Algebra S R] [Module S M] [SMulPosMono S R] [IsScalarTower S R M] {a : S} (v : M) (ha : 0 < a) : SameRay R v (a • v)

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

theorem SameRay.sameRay_pos_smul_left {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {S : Type u_5} [OrderedCommSemiring S] [Algebra S R] [Module S M] [SMulPosMono S R] [IsScalarTower S R M] {a : S} (v : M) (ha : 0 < a) : SameRay R (a • v) v

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

theorem SameRay.nonneg_smul_right {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {x : M} {y : M} {S : Type u_5} [OrderedCommSemiring S] [Algebra S R] [Module S M] [SMulPosMono S R] [IsScalarTower S R M] {a : S} (h : SameRay R x y) (ha : 0 ≤ a) : SameRay R x (a • y)

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

theorem SameRay.nonneg_smul_left {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {x : M} {y : M} {S : Type u_5} [OrderedCommSemiring S] [Algebra S R] [Module S M] [SMulPosMono S R] [IsScalarTower S R M] {a : S} (h : SameRay R x y) (ha : 0 ≤ a) : SameRay R (a • x) y

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

theorem SameRay.pos_smul_right {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {x : M} {y : M} {S : Type u_5} [OrderedCommSemiring S] [Algebra S R] [Module S M] [SMulPosMono S R] [IsScalarTower S R M] {a : S} (h : SameRay R x y) (ha : 0 < a) : SameRay R x (a • y)

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

theorem SameRay.pos_smul_left {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {x : M} {y : M} {S : Type u_5} [OrderedCommSemiring S] [Algebra S R] [Module S M] [SMulPosMono S R] [IsScalarTower S R M] {a : S} (h : SameRay R x y) (hr : 0 < a) : SameRay R (a • x) y

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

theorem SameRay.map {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {x : M} {y : M} (f : M →ₗ[R] N) (h : SameRay R x y) : SameRay R (f x) (f y)

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

theorem Function.Injective.sameRay_map_iff {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {x : M} {y : M} {F : Type u_6} [FunLike F M N] [LinearMapClass F R M N] {f : F} (hf : Function.Injective ⇑f) : SameRay R (f x) (f y) ↔ SameRay R 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 SameRay.sameRay_map_iff {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {x : M} {y : M} (e : M ≃ₗ[R] N) : SameRay R (e x) (e y) ↔ SameRay 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 SameRay.smul {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {x : M} {y : M} {S : Type u_6} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] (h : SameRay R x y) (s : S) : SameRay 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 SameRay.add_left {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {x : M} {y : M} {z : M} (hx : SameRay R x z) (hy : SameRay R y z) : SameRay R (x + y) z

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

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

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

def RayVector (R : Type u_5) (M : Type u_6) [Zero M] : Type u_6

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

Equations

• RayVector R M = { v : M // v ≠ 0 }

instance RayVector.coe {R : Type u_1} {M : Type u_2} [Zero M] : CoeOut (RayVector R M) M

Equations

• RayVector.coe = { coe := Subtype.val }

instance instNonemptyRayVector {R : Type u_5} {M : Type u_6} [Zero M] [Nontrivial M] : Nonempty (RayVector R M)

Equations

• ⋯ = ⋯

instance RayVector.Setoid (R : Type u_1) [StrictOrderedCommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] : Setoid (RayVector R M)

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

Equations

• RayVector.Setoid R M = { r := fun (x y : RayVector R M) => SameRay R ↑x ↑y, iseqv := ⋯ }

def Module.Ray (R : Type u_1) [StrictOrderedCommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] : Type u_2

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

Equations

• Module.Ray R M = Quotient (RayVector.Setoid R M)

theorem equiv_iff_sameRay {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {v₁ : RayVector R M} {v₂ : RayVector R M} : v₁ ≈ v₂ ↔ SameRay R ↑v₁ ↑v₂

Equivalence of nonzero vectors, in terms of SameRay.

def rayOfNeZero (R : Type u_1) [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (v : M) (h : v ≠ 0) : Module.Ray R M

The ray given by a nonzero vector.

Equations

• rayOfNeZero R v h = ⟦{ val := v, property := h }⟧

theorem Module.Ray.ind (R : Type u_1) [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {C : Module.Ray R M → Prop} (h : ∀ (v : M) (hv : v ≠ 0), C (rayOfNeZero R v hv)) (x : Module.Ray R M) : C x

An induction principle for Module.Ray, used as induction x using Module.Ray.ind.

instance instNonemptyRay {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [Nontrivial M] : Nonempty (Module.Ray R M)

Equations

• ⋯ = ⋯

theorem ray_eq_iff {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {v₁ : M} {v₂ : M} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) : rayOfNeZero R v₁ hv₁ = rayOfNeZero R v₂ hv₂ ↔ SameRay R v₁ v₂

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

@[simp]

theorem ray_pos_smul {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {v : M} (h : v ≠ 0) {r : R} (hr : 0 < r) (hrv : r • v ≠ 0) : rayOfNeZero R (r • v) hrv = rayOfNeZero R v h

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

def RayVector.mapLinearEquiv {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) : RayVector R M ≃ RayVector R N

An equivalence between modules implies an equivalence between ray vectors.

Equations

• RayVector.mapLinearEquiv e = Equiv.subtypeEquiv (LinearEquiv.toEquiv e) ⋯

def Module.Ray.map {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) : Module.Ray R M ≃ Module.Ray R N

An equivalence between modules implies an equivalence between rays.

Equations

• Module.Ray.map e = Quotient.congr (RayVector.mapLinearEquiv e) ⋯

@[simp]

theorem Module.Ray.map_apply {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (v : M) (hv : v ≠ 0) : (Module.Ray.map e) (rayOfNeZero R v hv) = rayOfNeZero R (e v) ⋯

@[simp]

theorem Module.Ray.map_refl {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] : Module.Ray.map (LinearEquiv.refl R M) = Equiv.refl (Module.Ray R M)

@[simp]

theorem Module.Ray.map_symm {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) : (Module.Ray.map e).symm = Module.Ray.map (LinearEquiv.symm e)

instance instMulActionRayVectorToZeroToAddMonoidToMonoidToDivInvMonoid {M : Type u_2} [AddCommMonoid M] {G : Type u_5} [Group G] [DistribMulAction G M] {R : Type u_6} : MulAction G (RayVector R M)

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

Equations

• instMulActionRayVectorToZeroToAddMonoidToMonoidToDivInvMonoid = MulAction.mk ⋯ ⋯

instance instMulActionRayToMonoidToDivInvMonoid {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {G : Type u_5} [Group G] [DistribMulAction G M] [SMulCommClass R G M] : MulAction G (Module.Ray R M)

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

Equations

• instMulActionRayToMonoidToDivInvMonoid = MulAction.mk ⋯ ⋯

@[simp]

theorem Module.Ray.linearEquiv_smul_eq_map {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) (v : Module.Ray R M) : e • v = (Module.Ray.map e) v

The action via LinearEquiv.apply_distribMulAction corresponds to Module.Ray.map.

@[simp]

theorem smul_rayOfNeZero {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {G : Type u_5} [Group G] [DistribMulAction G M] [SMulCommClass R G M] (g : G) (v : M) (hv : v ≠ 0) : g • rayOfNeZero R v hv = rayOfNeZero R (g • v) ⋯

theorem Module.Ray.units_smul_of_pos {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid 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.

def Module.Ray.someRayVector {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (x : Module.Ray R M) : RayVector R M

An arbitrary RayVector giving a ray.

Equations

• Module.Ray.someRayVector x = Quotient.out x

@[simp]

theorem Module.Ray.someRayVector_ray {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (x : Module.Ray R M) : ⟦Module.Ray.someRayVector x⟧ = x

The ray of someRayVector.

def Module.Ray.someVector {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (x : Module.Ray R M) : M

An arbitrary nonzero vector giving a ray.

Equations

• Module.Ray.someVector x = ↑(Module.Ray.someRayVector x)

@[simp]

theorem Module.Ray.someVector_ne_zero {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (x : Module.Ray R M) : Module.Ray.someVector x ≠ 0

someVector is nonzero.

@[simp]

theorem Module.Ray.someVector_ray {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (x : Module.Ray R M) : rayOfNeZero R (Module.Ray.someVector x) ⋯ = x

The ray of someVector.

@[simp]

theorem sameRay_neg_iff {R : Type u_1} [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} : SameRay R (-x) (-y) ↔ SameRay R x y

SameRay.neg as an iff.

theorem SameRay.of_neg {R : Type u_1} [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} : SameRay R (-x) (-y) → SameRay R x y

Alias of the forward direction of sameRay_neg_iff.

---

SameRay.neg as an iff.

theorem SameRay.neg {R : Type u_1} [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} : SameRay R x y → SameRay R (-x) (-y)

Alias of the reverse direction of sameRay_neg_iff.

---

SameRay.neg as an iff.

theorem sameRay_neg_swap {R : Type u_1} [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} : SameRay R (-x) y ↔ SameRay R x (-y)

theorem eq_zero_of_sameRay_neg_smul_right {R : Type u_1} [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} [NoZeroSMulDivisors R M] {r : R} (hr : r < 0) (h : SameRay R x (r • x)) : x = 0

theorem eq_zero_of_sameRay_self_neg {R : Type u_1} [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} [NoZeroSMulDivisors R M] (h : SameRay R x (-x)) : x = 0

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

instance RayVector.instNegRayVectorToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoid {M : Type u_2} [AddCommGroup M] {R : Type u_4} : Neg (RayVector R M)

Negating a nonzero vector.

Equations

• RayVector.instNegRayVectorToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoid = { neg := fun (v : RayVector R M) => { val := -↑v, property := ⋯ } }

@[simp]

theorem RayVector.coe_neg {M : Type u_2} [AddCommGroup M] {R : Type u_4} (v : RayVector R M) : ↑(-v) = -↑v

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

instance RayVector.instInvolutiveNegRayVectorToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoid {M : Type u_2} [AddCommGroup M] {R : Type u_4} : InvolutiveNeg (RayVector R M)

Negating a nonzero vector twice produces the original vector.

Equations

• RayVector.instInvolutiveNegRayVectorToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoid = InvolutiveNeg.mk ⋯

@[simp]

theorem RayVector.equiv_neg_iff {R : Type u_1} [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {v₁ : RayVector R M} {v₂ : RayVector R M} : -v₁ ≈ -v₂ ↔ v₁ ≈ v₂

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

instance instNegRayToStrictOrderedCommSemiringToAddCommMonoid (R : Type u_1) [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] : Neg (Module.Ray R M)

Negating a ray.

Equations

• instNegRayToStrictOrderedCommSemiringToAddCommMonoid R = { neg := Quotient.map (fun (v : RayVector R M) => -v) ⋯ }

@[simp]

theorem neg_rayOfNeZero (R : Type u_1) [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (v : M) (h : v ≠ 0) : -rayOfNeZero R v h = rayOfNeZero R (-v) ⋯

The ray given by the negation of a nonzero vector.

instance Module.Ray.instInvolutiveNegRayToStrictOrderedCommSemiringToAddCommMonoid {R : Type u_1} [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] : InvolutiveNeg (Module.Ray R M)

Negating a ray twice produces the original ray.

Equations

• Module.Ray.instInvolutiveNegRayToStrictOrderedCommSemiringToAddCommMonoid = InvolutiveNeg.mk ⋯

theorem Module.Ray.ne_neg_self {R : Type u_1} [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors 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} [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup 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} [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (u : Rˣ) (hu : ↑u < 0) (v : Module.Ray R M) : u • v = -v

Scaling by a negative unit is negation.

@[simp]

theorem Module.Ray.map_neg {R : Type u_1} [StrictOrderedCommRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M ≃ₗ[R] N) (v : Module.Ray R M) : (Module.Ray.map f) (-v) = -(Module.Ray.map f) v

theorem sameRay_of_mem_orbit {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {v₁ : M} {v₂ : M} (h : v₁ ∈ MulAction.orbit (↥(Units.posSubgroup R)) v₂) : SameRay R v₁ v₂

SameRay follows from membership of MulAction.orbit for the Units.posSubgroup.

@[simp]

theorem units_inv_smul {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup 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 sameRay_smul_right_iff {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} {r : R} : SameRay R v (r • v) ↔ 0 ≤ r ∨ v = 0

theorem sameRay_smul_right_iff_of_ne {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} (hv : v ≠ 0) {r : R} (hr : r ≠ 0) : SameRay 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 sameRay_smul_left_iff {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} {r : R} : SameRay R (r • v) v ↔ 0 ≤ r ∨ v = 0

theorem sameRay_smul_left_iff_of_ne {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} (hv : v ≠ 0) {r : R} (hr : r ≠ 0) : SameRay 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 sameRay_neg_smul_right_iff {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} {r : R} : SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0

theorem sameRay_neg_smul_right_iff_of_ne {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} {r : R} (hv : v ≠ 0) (hr : r ≠ 0) : SameRay R (-v) (r • v) ↔ r < 0

@[simp]

theorem sameRay_neg_smul_left_iff {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} {r : R} : SameRay R (r • v) (-v) ↔ r ≤ 0 ∨ v = 0

theorem sameRay_neg_smul_left_iff_of_ne {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} {r : R} (hv : v ≠ 0) (hr : r ≠ 0) : SameRay R (r • v) (-v) ↔ r < 0

@[simp]

theorem units_smul_eq_self_iff {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors 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} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {u : Rˣ} {v : Module.Ray R M} : u • v = -v ↔ ↑u < 0

theorem sameRay_or_sameRay_neg_iff_not_linearIndependent {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : M} {y : M} : SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![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 sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent {R : Type u_1} [LinearOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : M} {y : M} : SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![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 SameRay.exists_pos_left {R : Type u_1} [LinearOrderedField R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} (h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (r : R), 0 < r ∧ r • x = y

theorem SameRay.exists_pos_right {R : Type u_1} [LinearOrderedField R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} (h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (r : R), 0 < r ∧ x = r • y

theorem SameRay.exists_nonneg_left {R : Type u_1} [LinearOrderedField R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} (h : SameRay 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 SameRay.exists_nonneg_right {R : Type u_1} [LinearOrderedField R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} (h : SameRay 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 SameRay.exists_eq_smul_add {R : Type u_1} [LinearOrderedField R] {M : Type u_2} [AddCommGroup M] [Module R M] {v₁ : M} {v₂ : M} (h : SameRay R v₁ v₂) : ∃ (a : R) (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 SameRay.exists_eq_smul {R : Type u_1} [LinearOrderedField R] {M : Type u_2} [AddCommGroup M] [Module R M] {v₁ : M} {v₂ : M} (h : SameRay R v₁ v₂) : ∃ (u : M) (a : R) (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 SameRay.exists_eq_smul_add.

theorem exists_pos_left_iff_sameRay {R : Type u_1} [LinearOrderedField R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} (hx : x ≠ 0) (hy : y ≠ 0) : (∃ (r : R), 0 < r ∧ r • x = y) ↔ SameRay R x y

theorem exists_pos_left_iff_sameRay_and_ne_zero {R : Type u_1} [LinearOrderedField R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} (hx : x ≠ 0) : (∃ (r : R), 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0

theorem exists_nonneg_left_iff_sameRay {R : Type u_1} [LinearOrderedField R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} (hx : x ≠ 0) : (∃ (r : R), 0 ≤ r ∧ r • x = y) ↔ SameRay R x y

theorem exists_pos_right_iff_sameRay {R : Type u_1} [LinearOrderedField R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} (hx : x ≠ 0) (hy : y ≠ 0) : (∃ (r : R), 0 < r ∧ x = r • y) ↔ SameRay R x y

theorem exists_pos_right_iff_sameRay_and_ne_zero {R : Type u_1} [LinearOrderedField R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} (hy : y ≠ 0) : (∃ (r : R), 0 < r ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0

theorem exists_nonneg_right_iff_sameRay {R : Type u_1} [LinearOrderedField R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : M} {y : M} (hy : y ≠ 0) : (∃ (r : R), 0 ≤ r ∧ x = r • y) ↔ SameRay R x y