Rays in modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines rays in modules.
Main definitions #
-
same_ray: two vectors belong to the same ray if they are proportional with a nonnegative coefficient. -
module.rayis a type for the equivalence class of nonzero vectors in a module with some common positive multiple.
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).
same_ray is reflexive.
same_ray is symmetric.
If x and y are nonzero vectors on the same ray, then there exist positive numbers r₁ r₂
such that r₁ • x = r₂ • y.
same_ray is transitive unless the vector in the middle is zero and both other vectors are
nonzero.
A vector is in the same ray as a nonnegative multiple of itself.
A vector is in the same ray as a positive multiple of itself.
A vector is in the same ray as a nonnegative multiple of one it is in the same ray as.
A vector is in the same ray as a positive multiple of one it is in the same ray as.
A nonnegative multiple of a vector is in the same ray as that vector.
A positive multiple of a vector is in the same ray as that vector.
A nonnegative multiple of a vector is in the same ray as one it is in the same ray as.
A positive multiple of a vector is in the same ray as one it is in the same ray as.
If two vectors are on the same ray then they remain so after applying a linear map.
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.
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.
If two vectors are on the same ray then both scaled by the same action are also on the same ray.
If x and y are on the same ray as z, then so is x + y.
If y and z are on the same ray as x, then so is y + z.
Nonzero vectors, as used to define rays. This type depends on an unused argument R so that
ray_vector.setoid can be an instance.
Equations
- ray_vector R M = {v // v ≠ 0}
Equations
The setoid of the same_ray relation for the subtype of nonzero vectors.
Equations
- ray_vector.setoid R M = {r := λ (x y : ray_vector R M), same_ray R ↑x ↑y, iseqv := _}
A ray (equivalence class of nonzero vectors with common positive multiples) in a module.
Equations
- module.ray R M = quotient (ray_vector.setoid R M)
Instances for module.ray
Equivalence of nonzero vectors, in terms of same_ray.
The ray given by a nonzero vector.
Equations
- ray_of_ne_zero R v h = ⟦⟨v, h⟩⟧
An induction principle for module.ray, used as induction x using module.ray.ind.
The rays given by two nonzero vectors are equal if and only if those vectors
satisfy same_ray.
The ray given by a positive multiple of a nonzero vector.
An equivalence between modules implies an equivalence between ray vectors.
Equations
An equivalence between modules implies an equivalence between rays.
Equations
Any invertible action preserves the non-zeroness of ray vectors. This is primarily of interest
when G = Rˣ
Equations
- ray_vector.mul_action = {to_has_smul := {smul := λ (r : G), subtype.map (has_smul.smul r) _}, one_smul := _, mul_smul := _}
Any invertible action preserves the non-zeroness of rays. This is primarily of interest when
G = Rˣ
Equations
- module.ray.mul_action = {to_has_smul := {smul := λ (r : G), quotient.map (has_smul.smul r) _}, one_smul := _, mul_smul := _}
The action via linear_equiv.apply_distrib_mul_action corresponds to module.ray.map.
Scaling by a positive unit is a no-op.
An arbitrary ray_vector giving a ray.
Equations
The ray of some_ray_vector.
An arbitrary nonzero vector giving a ray.
Equations
- x.some_vector = ↑(x.some_ray_vector)
some_vector is nonzero.
The ray of some_vector.
same_ray.neg as an iff.
Alias of the forward direction of same_ray_neg_iff.
Alias of the reverse direction of same_ray_neg_iff.
If a vector is in the same ray as its negation, that vector is zero.
Negating a nonzero vector.
Equations
- ray_vector.has_neg = {neg := λ (v : ray_vector R M), ⟨-↑v, _⟩}
Negating a nonzero vector commutes with coercion to the underlying module.
Negating a nonzero vector twice produces the original vector.
Equations
If two nonzero vectors are equivalent, so are their negations.
Negating a ray.
Equations
- module.ray.has_neg R = {neg := quotient.map (λ (v : ray_vector R M), -v) _}
The ray given by the negation of a nonzero vector.
Negating a ray twice produces the original ray.
Equations
- module.ray.has_involutive_neg = {neg := has_neg.neg (module.ray.has_neg R), neg_neg := _}
A ray does not equal its own negation.
Scaling by a negative unit is negation.
same_ray follows from membership of mul_action.orbit for the units.pos_subgroup.
Scaling by an inverse unit is the same as scaling by itself.
A nonzero vector is in the same ray as a multiple of itself if and only if that multiple is positive.
A multiple of a nonzero vector is in the same ray as that vector if and only if that multiple is positive.
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.
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.
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.
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.
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₂).
If vectors v₁ and v₂ are on the same ray, then they are nonnegative multiples of the same
vector. Actually, this vector can be assumed to be v₁ + v₂, see same_ray.exists_eq_smul_add.