Mathlib.LinearAlgebra.Ray

SameRay definition

 (R : Type*) [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type*} [AddCommMonoid M] [Module R M]
  (v₁ v₂ : M) : Prop

Full source

/-- 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). -/
@[nolint unusedArguments]
def SameRay (R : Type*) [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R]
    {M : Type*} [AddCommMonoid M] [Module R M] (v₁ v₂ : M) : Prop :=
  v₁ = 0 ∨ v₂ = 0 ∨ ∃ r₁ r₂ : R, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • v₁ = r₂ • v₂

Vectors in the same ray

Informal description

Given a commutative semiring $R$ with a partial order and strict ordered ring structure, and an $R$-module $M$, two vectors $v_1, v_2 \in M$ are said to be in the same ray if either: 1. $v_1 = 0$, or 2. $v_2 = 0$, or 3. There exist positive elements $r_1, r_2 \in R$ such that $r_1 \cdot v_1 = r_2 \cdot v_2$.

SameRay.zero_left theorem

(y : M) : SameRay R 0 y

Full source

@[simp]
theorem zero_left (y : M) : SameRay R 0 y :=
  Or.inl rfl

Zero vector is in the same ray as any vector

Informal description

For any vector $y$ in an $R$-module $M$, the zero vector $0$ is in the same ray as $y$.

SameRay.zero_right theorem

(x : M) : SameRay R x 0

Full source

@[simp]
theorem zero_right (x : M) : SameRay R x 0 :=
  Or.inr <| Or.inl rfl

Zero vector is in the same ray as any vector

Informal description

For any vector $x$ in an $R$-module $M$, $x$ is in the same ray as the zero vector.

SameRay.of_subsingleton theorem

[Subsingleton M] (x y : M) : SameRay R x y

Full source

@[nontriviality]
theorem of_subsingleton [Subsingleton M] (x y : M) : SameRay R x y := by
  rw [Subsingleton.elim x 0]
  exact zero_left _

Same ray relation holds trivially in subsingleton modules

Informal description

For any vectors $x$ and $y$ in an $R$-module $M$, if $M$ is a subsingleton (i.e., all elements of $M$ are equal), then $x$ and $y$ are in the same ray.

SameRay.of_subsingleton' theorem

[Subsingleton R] (x y : M) : SameRay R x y

Full source

@[nontriviality]
theorem of_subsingleton' [Subsingleton R] (x y : M) : SameRay R x y :=
  haveI := Module.subsingleton R M
  of_subsingleton x y

Same Ray Relation Holds Trivially in Modules Over Subsingleton Rings

Informal description

For any vectors $x$ and $y$ in an $R$-module $M$, if the commutative semiring $R$ is a subsingleton (i.e., all elements of $R$ are equal), then $x$ and $y$ are in the same ray.

SameRay.refl theorem

(x : M) : SameRay R x x

Full source

/-- `SameRay` is reflexive. -/
@[refl]
theorem refl (x : M) : SameRay R x x := by
  nontriviality R
  exact Or.inr (Or.inr <| ⟨1, 1, zero_lt_one, zero_lt_one, rfl⟩)

Reflexivity of SameRay Relation

Informal description

For any vector $x$ in an $R$-module $M$, the relation $\text{SameRay}_R(x, x)$ holds. That is, every vector is in the same ray as itself.

SameRay.rfl theorem

: SameRay R x x

Full source

protected theorem rfl : SameRay R x x :=
  refl _

Reflexivity of the SameRay Relation

Informal description

For any vector $x$ in an $R$-module $M$, the relation $\text{SameRay}_R(x, x)$ holds. That is, every vector is in the same ray as itself.

SameRay.symm theorem

(h : SameRay R x y) : SameRay R y x

Full source

/-- `SameRay` is symmetric. -/
@[symm]
theorem symm (h : SameRay R x y) : SameRay R y x :=
  (or_left_comm.1 h).imp_right <| Or.imp_right fun ⟨r₁, r₂, h₁, h₂, h⟩ => ⟨r₂, r₁, h₂, h₁, h.symm⟩

Symmetry of the SameRay Relation

Informal description

Given a commutative semiring $R$ with a partial order and strict ordered ring structure, and an $R$-module $M$, the relation `SameRay` is symmetric. That is, for any vectors $x, y \in M$, if $x$ and $y$ are in the same ray, then $y$ and $x$ are also in the same ray.

SameRay.exists_pos theorem

 (h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) : ∃ r₁ r₂ : R, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y

Full source

/-- 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 exists_pos (h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) :
    ∃ r₁ r₂ : R, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y :=
  (h.resolve_left hx).resolve_left hy

Existence of Positive Scalars for Nonzero Vectors on the Same Ray

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. For any nonzero vectors $x, y \in M$ that lie on the same ray, there exist positive elements $r_1, r_2 \in R$ such that $r_1 \cdot x = r_2 \cdot y$.

SameRay.sameRay_comm theorem

: SameRay R x y ↔ SameRay R y x

Full source

theorem sameRay_comm : SameRaySameRay R x y ↔ SameRay R y x :=
  ⟨SameRay.symm, SameRay.symm⟩

Symmetry of the Same Ray Relation: $\text{SameRay}(x, y) \leftrightarrow \text{SameRay}(y, x)$

Informal description

For any vectors $x, y$ in an $R$-module $M$, where $R$ is a commutative semiring with a partial order and strict ordered ring structure, the relation "same ray" is symmetric. That is, $x$ and $y$ lie on the same ray if and only if $y$ and $x$ lie on the same ray.

SameRay.trans theorem

(hxy : SameRay R x y) (hyz : SameRay R y z) (hy : y = 0 → x = 0 ∨ z = 0) : SameRay R x z

Full source

/-- `SameRay` is transitive unless the vector in the middle is zero and both other vectors are
nonzero. -/
theorem trans (hxy : SameRay R x y) (hyz : SameRay R y z) (hy : y = 0 → x = 0 ∨ z = 0) :
    SameRay R x z := by
  rcases eq_or_ne x 0 with (rfl | hx); · exact zero_left z
  rcases eq_or_ne z 0 with (rfl | hz); · exact zero_right x
  rcases eq_or_ne y 0 with (rfl | hy)
  · exact (hy rfl).elim (fun h => (hx h).elim) fun h => (hz h).elim
  rcases hxy.exists_pos hx hy with ⟨r₁, r₂, hr₁, hr₂, h₁⟩
  rcases hyz.exists_pos hy hz with ⟨r₃, r₄, hr₃, hr₄, h₂⟩
  refine Or.inr (Or.inr <| ⟨r₃ * r₁, r₂ * r₄, mul_pos hr₃ hr₁, mul_pos hr₂ hr₄, ?_⟩)
  rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]

Transitivity of Same Ray Relation with Zero Condition

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. For any vectors $x, y, z \in M$, if $x$ and $y$ lie on the same ray, and $y$ and $z$ lie on the same ray, and either $y \neq 0$ or at least one of $x$ or $z$ is zero, then $x$ and $z$ lie on the same ray.

SameRay.sameRay_nonneg_smul_right theorem

(v : M) (h : 0 ≤ a) : SameRay R v (a • v)

Full source

/-- A vector is in the same ray as a nonnegative multiple of itself. -/
lemma sameRay_nonneg_smul_right (v : M) (h : 0 ≤ a) : SameRay R v (a • v) := by
  obtain h | h := (algebraMap_nonneg R h).eq_or_gt
  · rw [← algebraMap_smul R a v, h, zero_smul]
    exact zero_right _
  · refine Or.inr <| Or.inr ⟨algebraMap S R a, 1, h, by nontriviality R; exact zero_lt_one, ?_⟩
    module

Nonnegative scalar multiple lies in same ray as original vector

Informal description

For any vector $v$ in an $R$-module $M$ and any nonnegative scalar $a \in R$ (i.e., $0 \leq a$), the vector $v$ lies in the same ray as its nonnegative scalar multiple $a \cdot v$.

SameRay.sameRay_nonneg_smul_left theorem

(v : M) (ha : 0 ≤ a) : SameRay R (a • v) v

Full source

/-- A nonnegative multiple of a vector is in the same ray as that vector. -/
lemma sameRay_nonneg_smul_left (v : M) (ha : 0 ≤ a) : SameRay R (a • v) v :=
  (sameRay_nonneg_smul_right v ha).symm

Nonnegative Scalar Multiple Lies in Same Ray as Original Vector (Left Version)

Informal description

For any vector $v$ in an $R$-module $M$ and any nonnegative scalar $a \in R$ (i.e., $0 \leq a$), the nonnegative scalar multiple $a \cdot v$ lies in the same ray as the original vector $v$.

SameRay.sameRay_pos_smul_right theorem

(v : M) (ha : 0 < a) : SameRay R v (a • v)

Full source

/-- A vector is in the same ray as a positive multiple of itself. -/
lemma sameRay_pos_smul_right (v : M) (ha : 0 < a) : SameRay R v (a • v) :=
  sameRay_nonneg_smul_right v ha.le

Positive scalar multiple lies in same ray as original vector

Informal description

For any vector $v$ in an $R$-module $M$ and any positive scalar $a \in R$ (i.e., $0 < a$), the vector $v$ lies in the same ray as its positive scalar multiple $a \cdot v$.

SameRay.sameRay_pos_smul_left theorem

(v : M) (ha : 0 < a) : SameRay R (a • v) v

Full source

/-- A positive multiple of a vector is in the same ray as that vector. -/
lemma sameRay_pos_smul_left (v : M) (ha : 0 < a) : SameRay R (a • v) v :=
  sameRay_nonneg_smul_left v ha.le

Positive Scalar Multiple Lies in Same Ray as Original Vector (Left Version)

Informal description

For any vector $v$ in an $R$-module $M$ and any positive scalar $a \in R$ (i.e., $0 < a$), the positive scalar multiple $a \cdot v$ lies in the same ray as the original vector $v$.

SameRay.nonneg_smul_right theorem

(h : SameRay R x y) (ha : 0 ≤ a) : SameRay R x (a • y)

Full source

/-- A vector is in the same ray as a nonnegative multiple of one it is in the same ray as. -/
lemma nonneg_smul_right (h : SameRay R x y) (ha : 0 ≤ a) : SameRay R x (a • y) :=
  h.trans (sameRay_nonneg_smul_right y ha) fun hy => Or.inr <| by rw [hy, smul_zero]

Nonnegative scalar multiple preserves same-ray relation

Informal description

Given vectors $x$ and $y$ in an $R$-module $M$ that lie on the same ray (i.e., $\text{SameRay}_R\,x\,y$ holds), and a nonnegative scalar $a \in R$ (i.e., $0 \leq a$), the vector $x$ lies on the same ray as the nonnegative scalar multiple $a \cdot y$.

SameRay.nonneg_smul_left theorem

(h : SameRay R x y) (ha : 0 ≤ a) : SameRay R (a • x) y

Full source

/-- A nonnegative multiple of a vector is in the same ray as one it is in the same ray as. -/
lemma nonneg_smul_left (h : SameRay R x y) (ha : 0 ≤ a) : SameRay R (a • x) y :=
  (h.symm.nonneg_smul_right ha).symm

Nonnegative scalar multiple preserves same-ray relation (left version)

Informal description

Given vectors $x$ and $y$ in an $R$-module $M$ that lie on the same ray (i.e., $\text{SameRay}_R\,x\,y$ holds), and a nonnegative scalar $a \in R$ (i.e., $0 \leq a$), the nonnegative scalar multiple $a \cdot x$ lies on the same ray as $y$.

SameRay.pos_smul_right theorem

(h : SameRay R x y) (ha : 0 < a) : SameRay R x (a • y)

Full source

/-- A vector is in the same ray as a positive multiple of one it is in the same ray as. -/
theorem pos_smul_right (h : SameRay R x y) (ha : 0 < a) : SameRay R x (a • y) :=
  h.nonneg_smul_right ha.le

Positive scalar multiple preserves same-ray relation (right version)

Informal description

Given vectors $x$ and $y$ in an $R$-module $M$ that lie on the same ray (i.e., $\text{SameRay}_R\,x\,y$ holds), and a positive scalar $a \in R$ (i.e., $0 < a$), the vector $x$ lies on the same ray as the positive scalar multiple $a \cdot y$.

SameRay.pos_smul_left theorem

(h : SameRay R x y) (hr : 0 < a) : SameRay R (a • x) y

Full source

/-- A positive multiple of a vector is in the same ray as one it is in the same ray as. -/
theorem pos_smul_left (h : SameRay R x y) (hr : 0 < a) : SameRay R (a • x) y :=
  h.nonneg_smul_left hr.le

Positive scalar multiple preserves same-ray relation (left version)

Informal description

Given vectors $x$ and $y$ in an $R$-module $M$ that lie on the same ray (i.e., $\text{SameRay}_R\,x\,y$ holds), and a positive scalar $a \in R$ (i.e., $0 < a$), the positive scalar multiple $a \cdot x$ lies on the same ray as $y$.

SameRay.map theorem

(f : M →ₗ[R] N) (h : SameRay R x y) : SameRay R (f x) (f y)

Full source

/-- If two vectors are on the same ray then they remain so after applying a linear map. -/
theorem map (f : M →ₗ[R] N) (h : SameRay R x y) : SameRay R (f x) (f y) :=
  (h.imp fun hx => by rw [hx, map_zero]) <|
    Or.imp (fun hy => by rw [hy, map_zero]) fun ⟨r₁, r₂, hr₁, hr₂, h⟩ =>
      ⟨r₁, r₂, hr₁, hr₂, by rw [← f.map_smul, ← f.map_smul, h]⟩

Linear Maps Preserve Same-Ray Vectors

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ and $N$ be $R$-modules. Given a linear map $f : M \to N$ and two vectors $x, y \in M$ that lie on the same ray, their images $f(x)$ and $f(y)$ also lie on the same ray in $N$.

Function.Injective.sameRay_map_iff theorem

 {F : Type*} [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

Full source

/-- 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. -/
theorem _root_.Function.Injective.sameRay_map_iff
    {F : Type*} [FunLike F M N] [LinearMapClass F R M N]
    {f : F} (hf : Function.Injective f) :
    SameRaySameRay R (f x) (f y) ↔ SameRay R x y := by
  simp only [SameRay, map_zero, ← hf.eq_iff, map_smul]

Injective Linear Maps Preserve Same-Ray Condition

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ and $N$ be $R$-modules. Given an injective linear map $f : M \to N$ and vectors $x, y \in M$, the images $f(x)$ and $f(y)$ lie on the same ray in $N$ if and only if $x$ and $y$ lie on the same ray in $M$.

SameRay.sameRay_map_iff theorem

(e : M ≃ₗ[R] N) : SameRay R (e x) (e y) ↔ SameRay R x y

Full source

/-- 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. -/
@[simp]
theorem sameRay_map_iff (e : M ≃ₗ[R] N) : SameRaySameRay R (e x) (e y) ↔ SameRay R x y :=
  Function.Injective.sameRay_map_iff (EquivLike.injective e)

Linear Equivalence Preserves Same-Ray Condition if and only if Original Vectors Are on Same Ray

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ and $N$ be $R$-modules. Given a linear equivalence $e : M \simeq N$ and vectors $x, y \in M$, the images $e(x)$ and $e(y)$ lie on the same ray in $N$ if and only if $x$ and $y$ lie on the same ray in $M$.

SameRay.smul theorem

 {S : Type*} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] (h : SameRay R x y) (s : S) :
  SameRay R (s • x) (s • y)

Full source

/-- If two vectors are on the same ray then both scaled by the same action are also on the same
ray. -/
theorem smul {S : Type*} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M]
    (h : SameRay R x y) (s : S) : SameRay R (s • x) (s • y) :=
  h.map (s • (LinearMap.id : M →ₗ[R] M))

Scalar Multiplication Preserves Same-Ray Condition

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. Let $S$ be a monoid with a distributive multiplicative action on $M$ such that the actions of $R$ and $S$ on $M$ commute. For any vectors $x, y \in M$ that lie on the same ray and any scalar $s \in S$, the scaled vectors $s \cdot x$ and $s \cdot y$ also lie on the same ray.

SameRay.add_left theorem

(hx : SameRay R x z) (hy : SameRay R y z) : SameRay R (x + y) z

Full source

/-- If `x` and `y` are on the same ray as `z`, then so is `x + y`. -/
theorem add_left (hx : SameRay R x z) (hy : SameRay R y z) : SameRay R (x + y) z := by
  rcases eq_or_ne x 0 with (rfl | hx₀); · rwa [zero_add]
  rcases eq_or_ne y 0 with (rfl | hy₀); · rwa [add_zero]
  rcases eq_or_ne z 0 with (rfl | hz₀); · apply zero_right
  rcases hx.exists_pos hx₀ hz₀ with ⟨rx, rz₁, hrx, hrz₁, Hx⟩
  rcases hy.exists_pos hy₀ hz₀ with ⟨ry, rz₂, hry, hrz₂, Hy⟩
  refine Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, ?_, ?_⟩)
  · positivity
  · convert congr(ry • $Hx + rx • $Hy) using 1 <;> module

Sum of vectors in same ray as a common vector remains in same ray

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. For any vectors $x, y, z \in M$, if $x$ and $z$ are in the same ray, and $y$ and $z$ are in the same ray, then the sum $x + y$ is in the same ray as $z$.

SameRay.add_right theorem

(hy : SameRay R x y) (hz : SameRay R x z) : SameRay R x (y + z)

Full source

/-- If `y` and `z` are on the same ray as `x`, then so is `y + z`. -/
theorem add_right (hy : SameRay R x y) (hz : SameRay R x z) : SameRay R x (y + z) :=
  (hy.symm.add_left hz.symm).symm

Sum of vectors in same ray as a common vector remains in same ray (right version)

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. For any vectors $x, y, z \in M$, if $x$ and $y$ are in the same ray, and $x$ and $z$ are in the same ray, then $x$ and $y + z$ are also in the same ray.

RayVector definition

(R M : Type*) [Zero M]

Full source

/-- Nonzero vectors, as used to define rays. This type depends on an unused argument `R` so that
`RayVector.Setoid` can be an instance. -/
@[nolint unusedArguments]
def RayVector (R M : Type*) [Zero M] :=
  { v : M // v ≠ 0 }

Nonzero vectors in a module (for defining rays)

Informal description

The type `RayVector R M` consists of nonzero vectors in a module `M` over a ring `R`, where `M` has a zero element. It is defined as the subtype of vectors `v : M` such that `v ≠ 0`. This type is used to define rays in modules, where two vectors are considered to be in the same ray if they are proportional by a nonnegative coefficient.

RayVector.coe instance

[Zero M] : CoeOut (RayVector R M) M

Full source

instance RayVector.coe [Zero M] : CoeOut (RayVector R M) M where
  coe := Subtype.val

Canonical Inclusion of Nonzero Vectors into Module

Informal description

For a module $M$ over a ring $R$ with a zero element, there is a canonical way to view a nonzero vector in $M$ (an element of `RayVector R M`) as an element of $M$.

instNonemptyRayVectorOfNontrivial instance

{R M : Type*} [Zero M] [Nontrivial M] : Nonempty (RayVector R M)

Full source

instance {R M : Type*} [Zero M] [Nontrivial M] : Nonempty (RayVector R M) :=
  let ⟨x, hx⟩ := exists_ne (0 : M)
  ⟨⟨x, hx⟩⟩

Existence of Nonzero Vectors in Nontrivial Modules

Informal description

For any nontrivial module $M$ over a ring $R$ with a zero element, there exists a nonzero vector in $M$.

RayVector.Setoid instance

: Setoid (RayVector R M)

Full source

/-- The setoid of the `SameRay` relation for the subtype of nonzero vectors. -/
instance RayVector.Setoid : Setoid (RayVector R M) where
  r x y := SameRay R (x : M) y
  iseqv :=
    ⟨fun _ => SameRay.refl _, fun h => h.symm, by
      intros x y z hxy hyz
      exact hxy.trans hyz fun hy => (y.2 hy).elim⟩

Setoid Structure on Nonzero Vectors via SameRay Relation

Informal description

For a module $M$ over a commutative semiring $R$ with a partial order and strict ordered ring structure, the equivalence relation `SameRay` on the set of nonzero vectors in $M$ defines a setoid structure on `RayVector R M`. Two nonzero vectors $v_1$ and $v_2$ are equivalent if they lie on the same ray, i.e., if there exist positive elements $r_1, r_2 \in R$ such that $r_1 \cdot v_1 = r_2 \cdot v_2$.

Module.Ray definition

Full source

/-- A ray (equivalence class of nonzero vectors with common positive multiples) in a module. -/
def Module.Ray :=
  Quotient (RayVector.Setoid R M)

Ray in a module

Informal description

The type `Module.Ray R M` represents the equivalence class of nonzero vectors in a module $M$ over a commutative semiring $R$, where two vectors are considered equivalent if they lie on the same ray, i.e., if they are proportional by a nonnegative coefficient. More precisely, given two nonzero vectors $v_1, v_2 \in M$, they belong to the same ray if there exist positive elements $r_1, r_2 \in R$ such that $r_1 \cdot v_1 = r_2 \cdot v_2$.

equiv_iff_sameRay theorem

{v₁ v₂ : RayVector R M} : v₁ ≈ v₂ ↔ SameRay R (v₁ : M) v₂

Full source

/-- Equivalence of nonzero vectors, in terms of `SameRay`. -/
theorem equiv_iff_sameRay {v₁ v₂ : RayVector R M} : v₁ ≈ v₂v₁ ≈ v₂ ↔ SameRay R (v₁ : M) v₂ :=
  Iff.rfl

Equivalence of Nonzero Vectors in Terms of Same Ray Condition

Informal description

For any two nonzero vectors $v_1, v_2$ in a module $M$ over a commutative semiring $R$ with a partial order and strict ordered ring structure, the equivalence relation $v_1 \approx v_2$ holds if and only if $v_1$ and $v_2$ lie on the same ray, i.e., there exist positive elements $r_1, r_2 \in R$ such that $r_1 \cdot v_1 = r_2 \cdot v_2$.

rayOfNeZero definition

(v : M) (h : v ≠ 0) : Module.Ray R M

Full source

/-- The ray given by a nonzero vector. -/
def rayOfNeZero (v : M) (h : v ≠ 0) : Module.Ray R M :=
  ⟦⟨v, h⟩⟧

Ray defined by a nonzero vector

Informal description

Given a nonzero vector $v$ in a module $M$ over a commutative semiring $R$, the function `rayOfNeZero` returns the ray (equivalence class) in $M$ containing $v$. Specifically, it maps $v$ to its equivalence class under the relation that identifies two vectors if they are proportional by a nonnegative coefficient.

Module.Ray.ind theorem

{C : Module.Ray R M → Prop} (h : ∀ (v) (hv : v ≠ 0), C (rayOfNeZero R v hv)) (x : Module.Ray R M) : C x

Full source

/-- An induction principle for `Module.Ray`, used as `induction x using Module.Ray.ind`. -/
theorem Module.Ray.ind {C : Module.Ray R M → Prop} (h : ∀ (v) (hv : v ≠ 0), C (rayOfNeZero R v hv))
    (x : Module.Ray R M) : C x :=
  Quotient.ind (Subtype.rec <| h) x

Induction Principle for Rays in a Module

Informal description

For any predicate $C$ on the rays of a module $M$ over a commutative semiring $R$, if $C$ holds for every ray generated by a nonzero vector $v \in M$, then $C$ holds for every ray $x$ in $M$.

instNonemptyRayOfNontrivial instance

[Nontrivial M] : Nonempty (Module.Ray R M)

Full source

instance [Nontrivial M] : Nonempty (Module.Ray R M) :=
  Nonempty.map Quotient.mk' inferInstance

Existence of Rays in Nontrivial Modules

Informal description

For any nontrivial module $M$ over a commutative semiring $R$, there exists at least one ray in $M$.

ray_eq_iff theorem

 {v₁ v₂ : M} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) : rayOfNeZero R _ hv₁ = rayOfNeZero R _ hv₂ ↔ SameRay R v₁ v₂

Full source

/-- The rays given by two nonzero vectors are equal if and only if those vectors
satisfy `SameRay`. -/
theorem ray_eq_iff {v₁ v₂ : M} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) :
    rayOfNeZerorayOfNeZero R _ hv₁ = rayOfNeZero R _ hv₂ ↔ SameRay R v₁ v₂ :=
  Quotient.eq'

Equality of Rays if and only if Vectors are Proportional by Positive Scalars

Informal description

For any two nonzero vectors $v_1, v_2$ in a module $M$ over a commutative semiring $R$, the rays generated by $v_1$ and $v_2$ are equal if and only if $v_1$ and $v_2$ lie on the same ray, i.e., there exist positive elements $r_1, r_2 \in R$ such that $r_1 \cdot v_1 = r_2 \cdot v_2$.

ray_pos_smul theorem

{v : M} (h : v ≠ 0) {r : R} (hr : 0 < r) (hrv : r • v ≠ 0) : rayOfNeZero R (r • v) hrv = rayOfNeZero R v h

Full source

/-- The ray given by a positive multiple of a nonzero vector. -/
@[simp]
theorem ray_pos_smul {v : M} (h : v ≠ 0) {r : R} (hr : 0 < r) (hrv : r • v ≠ 0) :
    rayOfNeZero R (r • v) hrv = rayOfNeZero R v h :=
  (ray_eq_iff _ _).2 <| SameRay.sameRay_pos_smul_left v hr

Positive Scalar Multiplication Preserves Ray Equality

Informal description

For any nonzero vector $v$ in a module $M$ over a commutative semiring $R$ and any positive scalar $r \in R$ such that $r \cdot v \neq 0$, the ray generated by $r \cdot v$ is equal to the ray generated by $v$.

RayVector.mapLinearEquiv definition

(e : M ≃ₗ[R] N) : RayVector R M ≃ RayVector R N

Full source

/-- An equivalence between modules implies an equivalence between ray vectors. -/
def RayVector.mapLinearEquiv (e : M ≃ₗ[R] N) : RayVectorRayVector R M ≃ RayVector R N :=
  Equiv.subtypeEquiv e.toEquiv fun _ => e.map_ne_zero_iff.symm

Equivalence of nonzero vectors induced by a linear equivalence

Informal description

Given a linear equivalence $e : M \simeq_{R} N$ between modules $M$ and $N$ over a ring $R$, the function maps a nonzero vector in $M$ to its image under $e$ in $N$, which is also nonzero. This defines an equivalence between the types of nonzero vectors in $M$ and $N$.

Module.Ray.map definition

(e : M ≃ₗ[R] N) : Module.Ray R M ≃ Module.Ray R N

Full source

/-- An equivalence between modules implies an equivalence between rays. -/
def Module.Ray.map (e : M ≃ₗ[R] N) : Module.RayModule.Ray R M ≃ Module.Ray R N :=
  Quotient.congr (RayVector.mapLinearEquiv e) fun _ _=> (SameRay.sameRay_map_iff _).symm

Ray equivalence induced by a linear equivalence

Informal description

Given a linear equivalence $e : M \simeq_{R} N$ between modules $M$ and $N$ over a commutative semiring $R$, the function maps a ray in $M$ to its image under $e$ in $N$, preserving the equivalence relation `SameRay`. This defines an equivalence between the types of rays in $M$ and $N$.

Module.Ray.map_apply theorem

 (e : M ≃ₗ[R] N) (v : M) (hv : v ≠ 0) :
  Module.Ray.map e (rayOfNeZero _ v hv) = rayOfNeZero _ (e v) (e.map_ne_zero_iff.2 hv)

Full source

@[simp]
theorem Module.Ray.map_apply (e : M ≃ₗ[R] N) (v : M) (hv : v ≠ 0) :
    Module.Ray.map e (rayOfNeZero _ v hv) = rayOfNeZero _ (e v) (e.map_ne_zero_iff.2 hv) :=
  rfl

Image of a Ray under Linear Equivalence

Informal description

Let $M$ and $N$ be modules over a commutative semiring $R$, and let $e : M \simeq_{R} N$ be a linear equivalence. For any nonzero vector $v \in M$, the image of the ray generated by $v$ under the map induced by $e$ is equal to the ray generated by $e(v)$ in $N$. That is, \[ \text{Module.Ray.map}\, e\, (\text{rayOfNeZero}\, v\, h_v) = \text{rayOfNeZero}\, (e v)\, (e \text{ preserves nonzeroness of } v). \]

Module.Ray.map_refl theorem

: (Module.Ray.map <| LinearEquiv.refl R M) = Equiv.refl _

Full source

@[simp]
theorem Module.Ray.map_refl : (Module.Ray.map <| LinearEquiv.refl R M) = Equiv.refl _ :=
  Equiv.ext <| Module.Ray.ind R fun _ _ => rfl

Identity Ray Equivalence Induces Identity Map

Informal description

The ray equivalence map induced by the identity linear equivalence $\text{id} : M \simeq_R M$ is equal to the identity equivalence on the type of rays $\text{Module.Ray}\, R\, M$.

Module.Ray.map_symm theorem

(e : M ≃ₗ[R] N) : (Module.Ray.map e).symm = Module.Ray.map e.symm

Full source

@[simp]
theorem Module.Ray.map_symm (e : M ≃ₗ[R] N) : (Module.Ray.map e).symm = Module.Ray.map e.symm :=
  rfl

Inverse of Ray Equivalence Induced by Linear Equivalence

Informal description

Given a linear equivalence $e : M \simeq_{R} N$ between modules $M$ and $N$ over a commutative semiring $R$, the inverse of the induced ray equivalence $\text{Module.Ray.map}\, e$ is equal to the ray equivalence induced by the inverse linear equivalence $e^{-1}$, i.e., $(\text{Module.Ray.map}\, e)^{-1} = \text{Module.Ray.map}\, e^{-1}$.

instMulActionRayVector instance

{R : Type*} : MulAction G (RayVector R M)

Full source

/-- Any invertible action preserves the non-zeroness of ray vectors. This is primarily of interest
when `G = Rˣ` -/
instance {R : Type*} : MulAction G (RayVector R M) where
  smul r := Subtype.map (r • ·) fun _ => (smul_ne_zero_iff_ne _).2
  mul_smul a b _ := Subtype.ext <| mul_smul a b _
  one_smul _ := Subtype.ext <| one_smul _ _

Action of a Group on Nonzero Vectors Preserves Non-Zeroness

Informal description

For any group $G$ acting on a module $M$ over a ring $R$, the action preserves the non-zeroness of vectors in the ray vector space $\text{RayVector}\, R\, M$ (the space of nonzero vectors in $M$). In particular, this holds when $G$ is the group of units $R^\times$ of $R$.

instMulActionRay instance

: MulAction G (Module.Ray R M)

Full source

/-- Any invertible action preserves the non-zeroness of rays. This is primarily of interest when
`G = Rˣ` -/
instance : MulAction G (Module.Ray R M) where
  smul r := Quotient.map (r • ·) fun _ _ h => h.smul _
  mul_smul a b := Quotient.ind fun _ => congr_arg Quotient.mk' <| mul_smul a b _
  one_smul := Quotient.ind fun _ => congr_arg Quotient.mk' <| one_smul _ _

Group Action Preserves Ray Structure in Modules

Informal description

For any group $G$ acting on a module $M$ over a commutative semiring $R$, the action of $G$ preserves the ray structure on the set of rays in $M$. That is, the action of $G$ on $M$ induces a natural action on the space of rays $\text{Module.Ray}\, R\, M$, where each ray is an equivalence class of nonzero vectors under the relation of being proportional by a nonnegative coefficient.

Module.Ray.linearEquiv_smul_eq_map theorem

(e : M ≃ₗ[R] M) (v : Module.Ray R M) : e • v = Module.Ray.map e v

Full source

/-- The action via `LinearEquiv.apply_distribMulAction` corresponds to `Module.Ray.map`. -/
@[simp]
theorem Module.Ray.linearEquiv_smul_eq_map (e : M ≃ₗ[R] M) (v : Module.Ray R M) :
    e • v = Module.Ray.map e v :=
  rfl

Action of Linear Equivalence on Ray Equals Ray Map

Informal description

For any linear equivalence $e : M \simeq_{R} M$ and any ray $v$ in the module $M$ over a commutative semiring $R$, the action of $e$ on $v$ is equal to the image of $v$ under the ray map induced by $e$, i.e., $e \cdot v = \text{Module.Ray.map}\, e\, v$.

smul_rayOfNeZero theorem

(g : G) (v : M) (hv) : g • rayOfNeZero R v hv = rayOfNeZero R (g • v) ((smul_ne_zero_iff_ne _).2 hv)

Full source

@[simp]
theorem smul_rayOfNeZero (g : G) (v : M) (hv) :
    g • rayOfNeZero R v hv = rayOfNeZero R (g • v) ((smul_ne_zero_iff_ne _).2 hv) :=
  rfl

Group Action Commutes with Ray Construction

Informal description

For any group element $g \in G$ and any nonzero vector $v \in M$, the action of $g$ on the ray generated by $v$ is equal to the ray generated by the action of $g$ on $v$, i.e., $g \cdot \text{rayOfNeZero}\, R\, v\, hv = \text{rayOfNeZero}\, R\, (g \cdot v)\, (h'v)$, where $h'v$ is the proof that $g \cdot v \neq 0$ derived from $hv$ (the proof that $v \neq 0$).

Module.Ray.units_smul_of_pos theorem

(u : Rˣ) (hu : 0 < (u : R)) (v : Module.Ray R M) : u • v = v

Full source

/-- Scaling by a positive unit is a no-op. -/
theorem units_smul_of_pos (u : Rˣ) (hu : 0 < (u : R)) (v : Module.Ray R M) : u • v = v := by
  induction v using Module.Ray.ind
  rw [smul_rayOfNeZero, ray_eq_iff]
  exact SameRay.sameRay_pos_smul_left _ hu

Positive Unit Action Preserves Ray

Informal description

For any positive unit $u$ in a commutative semiring $R$ (i.e., $0 < u$) and any ray $v$ in an $R$-module $M$, the action of $u$ on $v$ leaves $v$ unchanged, i.e., $u \cdot v = v$.

Module.Ray.someRayVector definition

(x : Module.Ray R M) : RayVector R M

Full source

/-- An arbitrary `RayVector` giving a ray. -/
def someRayVector (x : Module.Ray R M) : RayVector R M :=
  Quotient.out x

Representative vector of a ray

Informal description

Given a ray $x$ in the module $M$ over a commutative semiring $R$, the function selects an arbitrary nonzero vector representative from the equivalence class of vectors that form the ray $x$.

Module.Ray.someRayVector_ray theorem

(x : Module.Ray R M) : (⟦x.someRayVector⟧ : Module.Ray R M) = x

Full source

/-- The ray of `someRayVector`. -/
@[simp]
theorem someRayVector_ray (x : Module.Ray R M) : (⟦x.someRayVector⟧ : Module.Ray R M) = x :=
  Quotient.out_eq _

Representative Vector Generates Original Ray

Informal description

For any ray $x$ in the module $M$ over a commutative semiring $R$, the equivalence class of the representative vector `x.someRayVector` is equal to $x$ itself. In other words, the ray generated by the selected representative vector is identical to the original ray $x$.

Module.Ray.someVector definition

(x : Module.Ray R M) : M

Full source

/-- An arbitrary nonzero vector giving a ray. -/
def someVector (x : Module.Ray R M) : M :=
  x.someRayVector

Representative vector of a ray

Informal description

Given a ray $x$ in the module $M$ over a commutative semiring $R$, the function returns an arbitrary nonzero vector from the equivalence class of vectors that form the ray $x$.

Module.Ray.someVector_ne_zero theorem

(x : Module.Ray R M) : x.someVector ≠ 0

Full source

/-- `someVector` is nonzero. -/
@[simp]
theorem someVector_ne_zero (x : Module.Ray R M) : x.someVector ≠ 0 :=
  x.someRayVector.property

Nonzero Property of Ray Representative Vector

Informal description

For any ray $x$ in the module $M$ over a commutative semiring $R$, the representative vector $v$ chosen by `someVector` is nonzero, i.e., $v \neq 0$.

Module.Ray.someVector_ray theorem

(x : Module.Ray R M) : rayOfNeZero R _ x.someVector_ne_zero = x

Full source

/-- The ray of `someVector`. -/
@[simp]
theorem someVector_ray (x : Module.Ray R M) : rayOfNeZero R _ x.someVector_ne_zero = x :=
  (congr_arg _ (Subtype.coe_eta _ _) :).trans x.out_eq

Representative Vector Generates Original Ray

Informal description

For any ray $x$ in the module $M$ over a commutative semiring $R$, the ray generated by the representative vector $v$ of $x$ (where $v \neq 0$) is equal to $x$ itself. That is, $\text{rayOfNeZero}(v, h_v) = x$, where $h_v$ is the proof that $v \neq 0$.

sameRay_neg_iff theorem

: SameRay R (-x) (-y) ↔ SameRay R x y

Full source

/-- `SameRay.neg` as an `iff`. -/
@[simp]
theorem sameRay_neg_iff : SameRaySameRay R (-x) (-y) ↔ SameRay R x y := by
  simp only [SameRay, neg_eq_zero, smul_neg, neg_inj]

Negation Preserves Same Ray Relation: $\text{SameRay}(-x, -y) \leftrightarrow \text{SameRay}(x, y)$

Informal description

For vectors $x, y$ in an $R$-module $M$, where $R$ is a commutative semiring with a partial order and strict ordered ring structure, the vectors $-x$ and $-y$ lie in the same ray if and only if $x$ and $y$ lie in the same ray.

sameRay_neg_swap theorem

: SameRay R (-x) y ↔ SameRay R x (-y)

Full source

theorem sameRay_neg_swap : SameRaySameRay R (-x) y ↔ SameRay R x (-y) := by rw [← sameRay_neg_iff, neg_neg]

Negation Swap Preserves Same Ray Relation: $\text{SameRay}(-x, y) \leftrightarrow \text{SameRay}(x, -y)$

Informal description

For vectors $x, y$ in an $R$-module $M$, where $R$ is a commutative semiring with a partial order and strict ordered ring structure, the vectors $-x$ and $y$ lie in the same ray if and only if $x$ and $-y$ lie in the same ray.

RayVector.instNeg instance

{R : Type*} : Neg (RayVector R M)

Full source

/-- Negating a nonzero vector. -/
instance {R : Type*} : Neg (RayVector R M) :=
  ⟨fun v => ⟨-v, neg_ne_zero.2 v.prop⟩⟩

Negation of Nonzero Vectors in a Module

Informal description

For any ring $R$ and module $M$ over $R$ with a zero element, the type `RayVector R M` of nonzero vectors in $M$ has a negation operation, where the negation of a nonzero vector remains nonzero.

RayVector.coe_neg theorem

{R : Type*} (v : RayVector R M) : ↑(-v) = -(v : M)

Full source

/-- Negating a nonzero vector commutes with coercion to the underlying module. -/
@[simp, norm_cast]
theorem coe_neg {R : Type*} (v : RayVector R M) : ↑(-v) = -(v : M) :=
  rfl

Negation Commutes with Projection of Nonzero Vectors

Informal description

For any ring $R$ and module $M$ over $R$ with a zero element, and for any nonzero vector $v \in M$, the canonical projection of the negation of $v$ (as a `RayVector`) equals the negation of the canonical projection of $v$. In other words, $(-v) = -v$ under the canonical map from `RayVector R M` to $M$.

RayVector.instInvolutiveNeg instance

{R : Type*} : InvolutiveNeg (RayVector R M)

Full source

/-- Negating a nonzero vector twice produces the original vector. -/
instance {R : Type*} : InvolutiveNeg (RayVector R M) where
  neg := Neg.neg
  neg_neg v := by rw [Subtype.ext_iff, coe_neg, coe_neg, neg_neg]

Involutive Negation of Nonzero Vectors in a Module

Informal description

For any ring $R$ and module $M$ over $R$ with a zero element, the negation operation on the type `RayVector R M` of nonzero vectors in $M$ is involutive. That is, for any nonzero vector $v$ in $M$, we have $-(-v) = v$.

RayVector.equiv_neg_iff theorem

{v₁ v₂ : RayVector R M} : -v₁ ≈ -v₂ ↔ v₁ ≈ v₂

Full source

/-- If two nonzero vectors are equivalent, so are their negations. -/
@[simp]
theorem equiv_neg_iff {v₁ v₂ : RayVector R M} : -v₁ ≈ -v₂-v₁ ≈ -v₂ ↔ v₁ ≈ v₂ :=
  sameRay_neg_iff

Negation Preserves Vector Ray Equivalence: $-v_1 \approx -v_2 \leftrightarrow v_1 \approx v_2$

Informal description

For any two nonzero vectors $v_1, v_2$ in an $R$-module $M$, the negations $-v_1$ and $-v_2$ are equivalent under the `SameRay` relation if and only if $v_1$ and $v_2$ are equivalent under the `SameRay` relation. In other words, $-v_1 \approx -v_2 \leftrightarrow v_1 \approx v_2$.

instNegRay instance

: Neg (Module.Ray R M)

Full source

/-- Negating a ray. -/
instance : Neg (Module.Ray R M) :=
  ⟨Quotient.map (fun v => -v) fun _ _ => RayVector.equiv_neg_iff.2⟩

Negation Operation on Rays in a Module

Informal description

For any commutative semiring $R$ and module $M$ over $R$, the type of rays $\text{Module.Ray}\, R\, M$ has a negation operation. Specifically, for any ray represented by a nonzero vector $v \in M$, its negation $-v$ defines the negation of the ray.

neg_rayOfNeZero theorem

(v : M) (h : v ≠ 0) : -rayOfNeZero R _ h = rayOfNeZero R (-v) (neg_ne_zero.2 h)

Full source

/-- The ray given by the negation of a nonzero vector. -/
@[simp]
theorem neg_rayOfNeZero (v : M) (h : v ≠ 0) :
    -rayOfNeZero R _ h = rayOfNeZero R (-v) (neg_ne_zero.2 h) :=
  rfl

Negation of Ray Equals Ray of Negation: $- [v] = [-v]$

Informal description

For any nonzero vector $v$ in a module $M$ over a commutative semiring $R$, the negation of the ray defined by $v$ is equal to the ray defined by $-v$. That is, $- [v] = [-v]$, where $[v]$ denotes the ray containing $v$.

Module.Ray.instInvolutiveNeg instance

: InvolutiveNeg (Module.Ray R M)

Full source

/-- Negating a ray twice produces the original ray. -/
instance : InvolutiveNeg (Module.Ray R M) where
  neg := Neg.neg
  neg_neg x := by apply ind R (by simp) x

Involutive Negation of Rays in a Module

Informal description

For any commutative semiring $R$ and module $M$ over $R$, the negation operation on the type of rays $\text{Module.Ray}\, R\, M$ is involutive. That is, for any ray $x$, we have $-(-x) = x$.

Module.Ray.ne_neg_self theorem

[NoZeroSMulDivisors R M] (x : Module.Ray R M) : x ≠ -x

Full source

/-- A ray does not equal its own negation. -/
theorem ne_neg_self [NoZeroSMulDivisors R M] (x : Module.Ray R M) : x ≠ -x := by
  induction x using Module.Ray.ind with | h x hx =>
  rw [neg_rayOfNeZero, Ne, ray_eq_iff]
  exact mt eq_zero_of_sameRay_self_neg hx

A ray is distinct from its negation: $x \neq -x$

Informal description

For any commutative semiring $R$ and module $M$ over $R$ with no zero smul divisors, and for any ray $x$ in $\text{Module.Ray}\, R\, M$, the ray $x$ is not equal to its negation $-x$.

Module.Ray.neg_units_smul theorem

(u : Rˣ) (v : Module.Ray R M) : -u • v = -(u • v)

Full source

theorem neg_units_smul (u : Rˣ) (v : Module.Ray R M) : -u • v = -(u • v) := by
  induction v using Module.Ray.ind
  simp only [smul_rayOfNeZero, Units.smul_def, Units.val_neg, neg_smul, neg_rayOfNeZero]

Negation of Scalar Multiplication by Unit in Module Ray

Informal description

For any unit $u$ in a commutative semiring $R$ and any ray $v$ in a module $M$ over $R$, the negation of the scalar multiplication of $u$ with $v$ equals the negation of the ray obtained by scalar multiplying $u$ with $v$. That is, $- (u \cdot v) = - (u \cdot v)$.

Module.Ray.units_smul_of_neg theorem

(u : Rˣ) (hu : (u : R) < 0) (v : Module.Ray R M) : u • v = -v

Full source

/-- Scaling by a negative unit is negation. -/
theorem units_smul_of_neg (u : Rˣ) (hu : (u : R) < 0) (v : Module.Ray R M) : u • v = -v := by
  rw [← neg_inj, neg_neg, ← neg_units_smul, units_smul_of_pos]
  rwa [Units.val_neg, Right.neg_pos_iff]

Negative Unit Scaling Acts as Negation on Rays

Informal description

For any unit $u$ in a commutative semiring $R$ such that $u < 0$, and for any ray $v$ in a module $M$ over $R$, the scalar multiplication of $u$ with $v$ equals the negation of $v$, i.e., $u \cdot v = -v$.

Module.Ray.map_neg theorem

(f : M ≃ₗ[R] N) (v : Module.Ray R M) : map f (-v) = -map f v

Full source

@[simp]
protected theorem map_neg (f : M ≃ₗ[R] N) (v : Module.Ray R M) : map f (-v) = -map f v := by
  induction v using Module.Ray.ind with | h g hg => simp

Negation Commutes with Linear Equivalence of Rays

Informal description

Let $R$ be a commutative semiring and $M, N$ be modules over $R$. For any linear equivalence $f : M \simeq_{R} N$ and any ray $v$ in $M$, the image of the negation of $v$ under $f$ equals the negation of the image of $v$ under $f$, i.e., $f(-v) = -f(v)$.

sameRay_of_mem_orbit theorem

{v₁ v₂ : M} (h : v₁ ∈ MulAction.orbit (Units.posSubgroup R) v₂) : SameRay R v₁ v₂

Full source

/-- `SameRay` follows from membership of `MulAction.orbit` for the `Units.posSubgroup`. -/
theorem sameRay_of_mem_orbit {v₁ v₂ : M} (h : v₁ ∈ MulAction.orbit (Units.posSubgroup R) v₂) :
    SameRay R v₁ v₂ := by
  rcases h with ⟨⟨r, hr : 0 < r.1⟩, rfl : r • v₂ = v₁⟩
  exact SameRay.sameRay_pos_smul_left _ hr

Same Ray Condition via Orbit Membership: $\text{SameRay}(v_1, v_2)$ if $v_1 \in G \cdot v_2$ for positive units $G$

Informal description

Given a commutative semiring $R$ with a partial order and strict ordered ring structure, and an $R$-module $M$, if two vectors $v_1, v_2 \in M$ satisfy $v_1 \in \text{orbit}(G, v_2)$ where $G$ is the subgroup of positive units of $R$, then $v_1$ and $v_2$ lie in the same ray.

units_inv_smul theorem

(u : Rˣ) (v : Module.Ray R M) : u⁻¹ • v = u • v

Full source

/-- Scaling by an inverse unit is the same as scaling by itself. -/
@[simp]
theorem units_inv_smul (u : Rˣ) (v : Module.Ray R M) : u⁻¹ • v = u • v :=
  have := mul_self_pos.2 u.ne_zero
  calc
    u⁻¹ • v = (u * u) • u⁻¹ • v := Eq.symm <| (u⁻¹ • v).units_smul_of_pos _ (by exact this)
    _ = u • v := by rw [mul_smul, smul_inv_smul]

Inverse Unit Action Equals Original on Rays: $u^{-1} \cdot v = u \cdot v$

Informal description

For any unit $u$ in a commutative semiring $R$ and any ray $v$ in an $R$-module $M$, the action of the inverse unit $u^{-1}$ on $v$ equals the action of $u$ on $v$, i.e., $u^{-1} \cdot v = u \cdot v$.

sameRay_smul_right_iff theorem

{v : M} {r : R} : SameRay R v (r • v) ↔ 0 ≤ r ∨ v = 0

Full source

@[simp]
theorem sameRay_smul_right_iff {v : M} {r : R} : SameRaySameRay R v (r • v) ↔ 0 ≤ r ∨ v = 0 :=
  ⟨fun hrv => or_iff_not_imp_left.2 fun hr => eq_zero_of_sameRay_neg_smul_right (not_le.1 hr) hrv,
    or_imp.2 ⟨SameRay.sameRay_nonneg_smul_right v, fun h => h.symm ▸ SameRay.zero_left _⟩⟩

Same Ray Condition for Scalar Multiple: $\text{SameRay}(v, rv) \leftrightarrow r \geq 0 \lor v = 0$

Informal description

For any vector $v$ in an $R$-module $M$ and any scalar $r \in R$, the vector $v$ is in the same ray as its scalar multiple $r \cdot v$ if and only if $r$ is nonnegative or $v$ is the zero vector, i.e., \[ \text{SameRay}(v, r \cdot v) \leftrightarrow r \geq 0 \lor v = 0. \]

sameRay_smul_right_iff_of_ne theorem

{v : M} (hv : v ≠ 0) {r : R} (hr : r ≠ 0) : SameRay R v (r • v) ↔ 0 < r

Full source

/-- A nonzero vector is in the same ray as a multiple of itself if and only if that multiple
is positive. -/
theorem sameRay_smul_right_iff_of_ne {v : M} (hv : v ≠ 0) {r : R} (hr : r ≠ 0) :
    SameRaySameRay R v (r • v) ↔ 0 < r := by
  simp only [sameRay_smul_right_iff, hv, or_false, hr.symm.le_iff_lt]

Same Ray Condition for Nonzero Scalar Multiple: $\text{SameRay}(v, rv) \leftrightarrow r > 0$

Informal description

For a nonzero vector $v$ in an $R$-module $M$ and a nonzero scalar $r \in R$, the vector $v$ is in the same ray as its scalar multiple $r \cdot v$ if and only if $r$ is positive, i.e., \[ \text{SameRay}(v, r \cdot v) \leftrightarrow r > 0. \]

sameRay_smul_left_iff theorem

{v : M} {r : R} : SameRay R (r • v) v ↔ 0 ≤ r ∨ v = 0

Full source

@[simp]
theorem sameRay_smul_left_iff {v : M} {r : R} : SameRaySameRay R (r • v) v ↔ 0 ≤ r ∨ v = 0 :=
  SameRay.sameRay_comm.trans sameRay_smul_right_iff

Same Ray Condition for Scalar Multiple (Left): $\text{SameRay}(rv, v) \leftrightarrow r \geq 0 \lor v = 0$

Informal description

For any vector $v$ in an $R$-module $M$ and any scalar $r \in R$, the scalar multiple $r \cdot v$ is in the same ray as $v$ if and only if $r$ is nonnegative or $v$ is the zero vector, i.e., \[ \text{SameRay}(r \cdot v, v) \leftrightarrow r \geq 0 \lor v = 0. \]

sameRay_smul_left_iff_of_ne theorem

{v : M} (hv : v ≠ 0) {r : R} (hr : r ≠ 0) : SameRay R (r • v) v ↔ 0 < r

Full source

/-- A multiple of a nonzero vector is in the same ray as that vector if and only if that multiple
is positive. -/
theorem sameRay_smul_left_iff_of_ne {v : M} (hv : v ≠ 0) {r : R} (hr : r ≠ 0) :
    SameRaySameRay R (r • v) v ↔ 0 < r :=
  SameRay.sameRay_comm.trans (sameRay_smul_right_iff_of_ne hv hr)

Same Ray Condition for Nonzero Scalar Multiple (Left): $\text{SameRay}(rv, v) \leftrightarrow r > 0$

Informal description

For a nonzero vector $v$ in an $R$-module $M$ and a nonzero scalar $r \in R$, the scalar multiple $r \cdot v$ is in the same ray as $v$ if and only if $r$ is positive, i.e., \[ \text{SameRay}(r \cdot v, v) \leftrightarrow r > 0. \]

sameRay_neg_smul_right_iff theorem

{v : M} {r : R} : SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0

Full source

@[simp]
theorem sameRay_neg_smul_right_iff {v : M} {r : R} : SameRaySameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0 := by
  rw [← sameRay_neg_iff, neg_neg, ← neg_smul, sameRay_smul_right_iff, neg_nonneg]

Same Ray Condition for Negative Vector and Scalar Multiple: $\text{SameRay}(-v, rv) \leftrightarrow r \leq 0 \lor v = 0$

Informal description

For any vector $v$ in an $R$-module $M$ and any scalar $r \in R$, the vector $-v$ and the scalar multiple $r \cdot v$ lie in the same ray if and only if $r$ is nonpositive or $v$ is the zero vector, i.e., \[ \text{SameRay}(-v, r \cdot v) \leftrightarrow r \leq 0 \lor v = 0. \]

sameRay_neg_smul_right_iff_of_ne theorem

{v : M} {r : R} (hv : v ≠ 0) (hr : r ≠ 0) : SameRay R (-v) (r • v) ↔ r < 0

Full source

theorem sameRay_neg_smul_right_iff_of_ne {v : M} {r : R} (hv : v ≠ 0) (hr : r ≠ 0) :
    SameRaySameRay R (-v) (r • v) ↔ r < 0 := by
  simp only [sameRay_neg_smul_right_iff, hv, or_false, hr.le_iff_lt]

Same Ray Condition for Negative Vector and Scalar Multiple: $r < 0$

Informal description

For a nonzero vector $v$ in an $R$-module $M$ and a nonzero scalar $r \in R$, the vector $-v$ and the scalar multiple $r \cdot v$ lie in the same ray if and only if $r$ is negative, i.e., $r < 0$.

sameRay_neg_smul_left_iff theorem

{v : M} {r : R} : SameRay R (r • v) (-v) ↔ r ≤ 0 ∨ v = 0

Full source

@[simp]
theorem sameRay_neg_smul_left_iff {v : M} {r : R} : SameRaySameRay R (r • v) (-v) ↔ r ≤ 0 ∨ v = 0 :=
  SameRay.sameRay_comm.trans sameRay_neg_smul_right_iff

Same Ray Condition for Scalar Multiple and Negative Vector: $\text{SameRay}(r v, -v) \leftrightarrow r \leq 0 \lor v = 0$

Informal description

For any vector $v$ in an $R$-module $M$ and any scalar $r \in R$, the scalar multiple $r \cdot v$ and the vector $-v$ lie in the same ray if and only if $r$ is nonpositive or $v$ is the zero vector, i.e., \[ \text{SameRay}(r \cdot v, -v) \leftrightarrow r \leq 0 \lor v = 0. \]

sameRay_neg_smul_left_iff_of_ne theorem

{v : M} {r : R} (hv : v ≠ 0) (hr : r ≠ 0) : SameRay R (r • v) (-v) ↔ r < 0

Full source

theorem sameRay_neg_smul_left_iff_of_ne {v : M} {r : R} (hv : v ≠ 0) (hr : r ≠ 0) :
    SameRaySameRay R (r • v) (-v) ↔ r < 0 :=
  SameRay.sameRay_comm.trans <| sameRay_neg_smul_right_iff_of_ne hv hr

Same Ray Condition for Scalar Multiple and Negative Vector: $r < 0$

Informal description

For a nonzero vector $v$ in an $R$-module $M$ and a nonzero scalar $r \in R$, the scalar multiple $r \cdot v$ and the vector $-v$ lie in the same ray if and only if $r$ is negative, i.e., $r < 0$.

units_smul_eq_self_iff theorem

{u : Rˣ} {v : Module.Ray R M} : u • v = v ↔ 0 < (u : R)

Full source

@[simp]
theorem units_smul_eq_self_iff {u : Rˣ} {v : Module.Ray R M} : u • v = v ↔ 0 < (u : R) := by
  induction v using Module.Ray.ind with | h v hv =>
  simp only [smul_rayOfNeZero, ray_eq_iff, Units.smul_def, sameRay_smul_left_iff_of_ne hv u.ne_zero]

Unit Scalar Multiplication Preserves Ray if and only if Unit is Positive

Informal description

For any unit $u$ in a commutative semiring $R$ and any ray $v$ in the module $M$ over $R$, the scalar multiplication $u \cdot v$ equals $v$ if and only if the element $u$ is positive, i.e., $0 < u$.

units_smul_eq_neg_iff theorem

{u : Rˣ} {v : Module.Ray R M} : u • v = -v ↔ u.1 < 0

Full source

@[simp]
theorem units_smul_eq_neg_iff {u : Rˣ} {v : Module.Ray R M} : u • v = -v ↔ u.1 < 0 := by
  rw [← neg_inj, neg_neg, ← Module.Ray.neg_units_smul, units_smul_eq_self_iff, Units.val_neg,
    neg_pos]

Unit Scalar Multiplication Yields Negated Ray if and only if Unit is Negative

Informal description

For any unit $u$ in a commutative semiring $R$ and any ray $v$ in the module $M$ over $R$, the scalar multiplication $u \cdot v$ equals the negation of $v$ if and only if the element $u$ is negative, i.e., $u < 0$.

sameRay_or_sameRay_neg_iff_not_linearIndependent theorem

{x y : M} : SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

Full source

/-- 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_sameRay_neg_iff_not_linearIndependent {x y : M} :
    SameRaySameRay R x y ∨ SameRay R x (-y)SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y] := by
  by_cases hx : x = 0; · simpa [hx] using fun h : LinearIndependent R ![0, y] => h.ne_zero 0 rfl
  by_cases hy : y = 0; · simpa [hy] using fun h : LinearIndependent R ![x, 0] => h.ne_zero 1 rfl
  simp_rw [Fintype.not_linearIndependent_iff]
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rcases h with ((hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩) | (hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩))
    · exact False.elim (hx hx0)
    · exact False.elim (hy hy0)
    · refine ⟨![r₁, -r₂], ?_⟩
      rw [Fin.sum_univ_two, Fin.exists_fin_two]
      simp [h, hr₁.ne.symm]
    · exact False.elim (hx hx0)
    · exact False.elim (hy (neg_eq_zero.1 hy0))
    · refine ⟨![r₁, r₂], ?_⟩
      rw [Fin.sum_univ_two, Fin.exists_fin_two]
      simp [h, hr₁.ne.symm]
  · rcases h with ⟨m, hm, hmne⟩
    rw [Fin.sum_univ_two, add_eq_zero_iff_eq_neg] at hm
    dsimp only [Matrix.cons_val] at hm
    rcases lt_trichotomy (m 0) 0 with (hm0 | hm0 | hm0) <;>
      rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
    · refine
        Or.inr (Or.inr (Or.inr ⟨-m 0, -m 1, Left.neg_pos_iff.2 hm0, Left.neg_pos_iff.2 hm1, ?_⟩))
      linear_combination (norm := module) -hm
    · exfalso
      simp [hm1, hx, hm0.ne] at hm
    · refine Or.inl (Or.inr (Or.inr ⟨-m 0, m 1, Left.neg_pos_iff.2 hm0, hm1, ?_⟩))
      linear_combination (norm := module) -hm
    · exfalso
      simp [hm0, hy, hm1.ne] at hm
    · rw [Fin.exists_fin_two] at hmne
      exact False.elim (not_and_or.2 hmne ⟨hm0, hm1⟩)
    · exfalso
      simp [hm0, hy, hm1.ne.symm] at hm
    · refine Or.inl (Or.inr (Or.inr ⟨m 0, -m 1, hm0, Left.neg_pos_iff.2 hm1, ?_⟩))
      rwa [neg_smul]
    · exfalso
      simp [hm1, hx, hm0.ne.symm] at hm
    · refine Or.inr (Or.inr (Or.inr ⟨m 0, m 1, hm0, hm1, ?_⟩))
      rwa [smul_neg]

Same Ray or Negated Same Ray Condition for Linear Dependence

Informal description

For any two vectors $x, y$ in an $R$-module $M$, the following are equivalent: 1. Either $x$ and $y$ lie on the same ray, or $x$ and $-y$ lie on the same ray. 2. The vectors $x$ and $y$ are linearly dependent (i.e., not linearly independent). Here, two vectors lie on the same ray if one is a nonnegative scalar multiple of the other.

sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent theorem

{x y : M} : SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

Full source

/-- 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_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent {x y : M} :
    SameRaySameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y)SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y] := by
  rw [← sameRay_or_sameRay_neg_iff_not_linearIndependent]
  by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0 <;> simp [hx, hy]

Same ray or negated same ray condition for linear dependence of nonzero vectors

Informal description

For any two vectors $x, y$ in an $R$-module $M$, the following are equivalent: 1. Either $x$ and $y$ lie on the same ray, or both $x$ and $y$ are nonzero and $x$ lies on the same ray as $-y$. 2. The vectors $x$ and $y$ are linearly dependent (i.e., not linearly independent). Here, two vectors lie on the same ray if one is a nonnegative scalar multiple of the other.

SameRay.exists_pos_left theorem

(h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) : ∃ r : R, 0 < r ∧ r • x = y

Full source

theorem exists_pos_left (h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) :
    ∃ r : R, 0 < r ∧ r • x = y :=
  let ⟨r₁, r₂, hr₁, hr₂, h⟩ := h.exists_pos hx hy
  ⟨r₂⁻¹ * r₁, mul_pos (inv_pos.2 hr₂) hr₁, by rw [mul_smul, h, inv_smul_smul₀ hr₂.ne']⟩

Existence of Positive Scaling Factor for Nonzero Vectors on the Same Ray

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. For any nonzero vectors $x, y \in M$ that lie on the same ray, there exists a positive element $r \in R$ such that $r \cdot x = y$.

SameRay.exists_pos_right theorem

(h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) : ∃ r : R, 0 < r ∧ x = r • y

Full source

theorem exists_pos_right (h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) :
    ∃ r : R, 0 < r ∧ x = r • y :=
  (h.symm.exists_pos_left hy hx).imp fun _ => And.imp_right Eq.symm

Existence of Positive Scaling Factor for Nonzero Vectors on the Same Ray (Right Version)

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. For any nonzero vectors $x, y \in M$ that lie on the same ray, there exists a positive element $r \in R$ such that $x = r \cdot y$.

SameRay.exists_nonneg_left theorem

(h : SameRay R x y) (hx : x ≠ 0) : ∃ r : R, 0 ≤ r ∧ r • x = y

Full source

/-- 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 exists_nonneg_left (h : SameRay R x y) (hx : x ≠ 0) : ∃ r : R, 0 ≤ r ∧ r • x = y := by
  obtain rfl | hy := eq_or_ne y 0
  · exact ⟨0, le_rfl, zero_smul _ _⟩
  · exact (h.exists_pos_left hx hy).imp fun _ => And.imp_left le_of_lt

Existence of Nonnegative Scaling Factor for Vectors on the Same Ray (Left Version)

Informal description

Given a commutative semiring $R$ with a partial order and strict ordered ring structure, and an $R$-module $M$, if two vectors $x, y \in M$ lie on the same ray and $x$ is nonzero, then there exists a nonnegative scalar $r \in R$ such that $y = r \cdot x$.

SameRay.exists_nonneg_right theorem

(h : SameRay R x y) (hy : y ≠ 0) : ∃ r : R, 0 ≤ r ∧ x = r • y

Full source

/-- 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 exists_nonneg_right (h : SameRay R x y) (hy : y ≠ 0) : ∃ r : R, 0 ≤ r ∧ x = r • y :=
  (h.symm.exists_nonneg_left hy).imp fun _ => And.imp_right Eq.symm

Existence of Nonnegative Scaling Factor for Vectors on the Same Ray (Right Version)

Informal description

Given a commutative semiring $R$ with a partial order and strict ordered ring structure, and an $R$-module $M$, if two vectors $x, y \in M$ lie on the same ray and $y$ is nonzero, then there exists a nonnegative scalar $r \in R$ such that $x = r \cdot y$.

SameRay.exists_eq_smul_add theorem

 (h : SameRay R v₁ v₂) : ∃ a b : R, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)

Full source

/-- 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 exists_eq_smul_add (h : SameRay R v₁ v₂) :
    ∃ a b : R, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂) := by
  rcases h with (rfl | rfl | ⟨r₁, r₂, h₁, h₂, H⟩)
  · use 0, 1
    simp
  · use 1, 0
    simp
  · have h₁₂ : 0 < r₁ + r₂ := add_pos h₁ h₂
    refine
      ⟨r₂ / (r₁ + r₂), r₁ / (r₁ + r₂), div_nonneg h₂.le h₁₂.le, div_nonneg h₁.le h₁₂.le, ?_, ?_, ?_⟩
    · rw [← add_div, add_comm, div_self h₁₂.ne']
    · rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
    · rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']

Convex Combination Representation for Vectors on the Same Ray

Informal description

Given two vectors $v_1$ and $v_2$ in an $R$-module $M$ that lie on the same ray, there exist nonnegative scalars $a, b \in R$ with $a + b = 1$ such that $v_1 = a \cdot (v_1 + v_2)$ and $v_2 = b \cdot (v_1 + v_2)$.

SameRay.exists_eq_smul theorem

 (h : SameRay R v₁ v₂) : ∃ (u : M) (a b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • u ∧ v₂ = b • u

Full source

/-- 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_eq_smul (h : SameRay R v₁ v₂) :
    ∃ (u : M) (a b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • u ∧ v₂ = b • u :=
  ⟨v₁ + v₂, h.exists_eq_smul_add⟩

Convex Combination Representation for Vectors on the Same Ray via Common Vector

Informal description

Given two vectors $v_1$ and $v_2$ in an $R$-module $M$ that lie on the same ray, there exists a vector $u \in M$ and nonnegative scalars $a, b \in R$ with $a + b = 1$ such that $v_1 = a \cdot u$ and $v_2 = b \cdot u$.

exists_pos_left_iff_sameRay theorem

(hx : x ≠ 0) (hy : y ≠ 0) : (∃ r : R, 0 < r ∧ r • x = y) ↔ SameRay R x y

Full source

theorem exists_pos_left_iff_sameRay (hx : x ≠ 0) (hy : y ≠ 0) :
    (∃ r : R, 0 < r ∧ r • x = y) ↔ SameRay R x y := by
  refine ⟨fun h => ?_, fun h => h.exists_pos_left hx hy⟩
  rcases h with ⟨r, hr, rfl⟩
  exact SameRay.sameRay_pos_smul_right x hr

Existence of Positive Scaling Factor Characterizes Same Ray Condition for Nonzero Vectors

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. For any nonzero vectors $x, y \in M$, there exists a positive scalar $r \in R$ such that $r \cdot x = y$ if and only if $x$ and $y$ lie on the same ray.

exists_pos_left_iff_sameRay_and_ne_zero theorem

(hx : x ≠ 0) : (∃ r : R, 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0

Full source

theorem exists_pos_left_iff_sameRay_and_ne_zero (hx : x ≠ 0) :
    (∃ r : R, 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0 := by
  constructor
  · rintro ⟨r, hr, rfl⟩
    simp [hx, hr.le, hr.ne']
  · rintro ⟨hxy, hy⟩
    exact (exists_pos_left_iff_sameRay hx hy).2 hxy

Existence of Positive Scaling Factor Characterizes Same Ray Condition for Nonzero Vectors

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. For any nonzero vector $x \in M$ and any vector $y \in M$, there exists a positive scalar $r \in R$ such that $y = r \cdot x$ if and only if $x$ and $y$ lie on the same ray and $y$ is nonzero.

exists_nonneg_left_iff_sameRay theorem

(hx : x ≠ 0) : (∃ r : R, 0 ≤ r ∧ r • x = y) ↔ SameRay R x y

Full source

theorem exists_nonneg_left_iff_sameRay (hx : x ≠ 0) :
    (∃ r : R, 0 ≤ r ∧ r • x = y) ↔ SameRay R x y := by
  refine ⟨fun h => ?_, fun h => h.exists_nonneg_left hx⟩
  rcases h with ⟨r, hr, rfl⟩
  exact SameRay.sameRay_nonneg_smul_right x hr

Existence of Nonnegative Scaling Factor Characterizes Same Ray Condition

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. For any nonzero vector $x \in M$ and any vector $y \in M$, there exists a nonnegative scalar $r \in R$ such that $y = r \cdot x$ if and only if $x$ and $y$ lie on the same ray.

exists_pos_right_iff_sameRay theorem

(hx : x ≠ 0) (hy : y ≠ 0) : (∃ r : R, 0 < r ∧ x = r • y) ↔ SameRay R x y

Full source

theorem exists_pos_right_iff_sameRay (hx : x ≠ 0) (hy : y ≠ 0) :
    (∃ r : R, 0 < r ∧ x = r • y) ↔ SameRay R x y := by
  rw [SameRay.sameRay_comm]
  simp_rw [eq_comm (a := x)]
  exact exists_pos_left_iff_sameRay hy hx

Existence of Positive Right Scaling Factor Characterizes Same Ray Condition for Nonzero Vectors

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. For any nonzero vectors $x, y \in M$, there exists a positive scalar $r \in R$ such that $x = r \cdot y$ if and only if $x$ and $y$ lie on the same ray.

exists_pos_right_iff_sameRay_and_ne_zero theorem

(hy : y ≠ 0) : (∃ r : R, 0 < r ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0

Full source

theorem exists_pos_right_iff_sameRay_and_ne_zero (hy : y ≠ 0) :
    (∃ r : R, 0 < r ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0 := by
  rw [SameRay.sameRay_comm]
  simp_rw [eq_comm (a := x)]
  exact exists_pos_left_iff_sameRay_and_ne_zero hy

Existence of Positive Right Scaling Factor Characterizes Same Ray Condition for Nonzero Vectors

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. For any nonzero vector $y \in M$ and any vector $x \in M$, there exists a positive scalar $r \in R$ such that $x = r \cdot y$ if and only if $x$ and $y$ lie on the same ray and $x$ is nonzero.

exists_nonneg_right_iff_sameRay theorem

(hy : y ≠ 0) : (∃ r : R, 0 ≤ r ∧ x = r • y) ↔ SameRay R x y

Full source

theorem exists_nonneg_right_iff_sameRay (hy : y ≠ 0) :
    (∃ r : R, 0 ≤ r ∧ x = r • y) ↔ SameRay R x y := by
  rw [SameRay.sameRay_comm]
  simp_rw [eq_comm (a := x)]
  exact exists_nonneg_left_iff_sameRay (R := R) hy

Existence of Nonnegative Scaling Factor from the Right Characterizes Same Ray Condition

Informal description

Let $R$ be a commutative semiring with a partial order and strict ordered ring structure, and let $M$ be an $R$-module. For any nonzero vector $y \in M$ and any vector $x \in M$, there exists a nonnegative scalar $r \in R$ such that $x = r \cdot y$ if and only if $x$ and $y$ lie on the same ray.

Main definitions