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₂)

Instances For

source

@[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

source

@[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

source

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

source

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

source

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.

source

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

SameRay R x x

source

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.

source

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.

source

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

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

@[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.

source

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.

source

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.

source

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.

source

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 }

Instances For

source

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

CoeOut (RayVector R M) M

Equations

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

source

instance instNonemptyRayVectorOfNontrivial {R : Type u_5} {M : Type u_6} [Zero M] [Nontrivial M] :

Nonempty (RayVector R M)

Equations

⋯ = ⋯

source

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 := ⋯ }

source

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)

Instances For

source

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.

source

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 = ⟦⟨v, h⟩⟧

Instances For

source

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.

source

instance instNonemptyRayOfNontrivial {R : Type u_1} [StrictOrderedCommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [Nontrivial M] :

Nonempty (Module.Ray R M)

Equations

⋯ = ⋯

source

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.

source

@[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.

source

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 = e.toEquiv.subtypeEquiv ⋯

Instances For

source

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) ⋯

Instances For

source

@[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) ⋯

source

@[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)

source

@[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 e.symm

source

instance instMulActionRayVector {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

instMulActionRayVector = MulAction.mk ⋯ ⋯

source

instance instMulActionRay {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

instMulActionRay = MulAction.mk ⋯ ⋯

source

@[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.

source

@[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) ⋯

source

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.

source

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

x.someRayVector = Quotient.out x

Instances For

source

@[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) :

⟦x.someRayVector⟧ = x

The ray of someRayVector.

source

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

An arbitrary nonzero vector giving a ray.

Equations

x.someVector = ↑x.someRayVector

Instances For

source

@[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) :

x.someVector ≠ 0

someVector is nonzero.

source

@[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 x.someVector ⋯ = x

The ray of someVector.

source

@[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.

source

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.

source

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.

source

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)

source

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

source

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.

source

instance RayVector.instNeg {M : Type u_2} [AddCommGroup M] {R : Type u_4} :

Neg (RayVector R M)

Negating a nonzero vector.

Equations

RayVector.instNeg = { neg := fun (v : RayVector R M) => ⟨-↑v, ⋯⟩ }

source

@[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.

source

instance RayVector.instInvolutiveNeg {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.instInvolutiveNeg = InvolutiveNeg.mk ⋯

source

@[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.

source

instance instNegRay (R : Type u_1) [StrictOrderedCommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] :

Neg (Module.Ray R M)

Negating a ray.

Equations

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

source

@[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.

source

instance Module.Ray.instInvolutiveNeg {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.instInvolutiveNeg = InvolutiveNeg.mk ⋯

source

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.

source

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)

source

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.

source

@[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

source

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.

source

@[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.

source

@[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

source

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.

source

@[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

source

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.

source

@[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

source

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

source

@[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

source

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

source

@[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

source

@[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

source

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.

source

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.

source

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

source

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

source

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.

source

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.

source

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₂).

source

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.

source

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

source

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

source

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

source

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

source

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

source

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

Documentation

Mathlib.LinearAlgebra.Ray

Rays in modules #

Main definitions #