linear_algebra.orientation

def same_ray (R : Type u_1) [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (v₁ v₂ : M) :

Prop

Two vectors are in the same ray if some positive multiples of them are equal (in the typical case over a field, this means each is a positive multiple of the other). Over a field, this is equivalent to mul_action.orbit_rel.

Equations

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

source

theorem same_ray.refl {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (x : M) :

same_ray R x x

same_ray is reflexive.

source

theorem same_ray.symm {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y : M} :

same_ray R x y → same_ray R y x

same_ray is symmetric.

source

theorem same_ray.trans {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y z : M} :

same_ray R x y → same_ray R y z → same_ray R x z

same_ray is transitive.

source

theorem same_ray_comm {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {x y : M} :

same_ray R x y ↔ same_ray R y x

source

theorem equivalence_same_ray (R : Type u_1) [ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] [nontrivial R] :

equivalence (same_ray R)

same_ray is an equivalence relation.

source

theorem same_ray_pos_smul_right {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (v : M) {r : R} (h : 0 < r) :

same_ray R v (r • v)

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

source

theorem same_ray.pos_smul_right {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {v₁ v₂ : M} {r : R} (h : same_ray R v₁ v₂) (hr : 0 < r) :

same_ray R v₁ (r • v₂)

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

source

theorem same_ray_pos_smul_left {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (v : M) {r : R} (h : 0 < r) :

same_ray R (r • v) v

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

source

theorem same_ray.pos_smul_left {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {v₁ v₂ : M} {r : R} (h : same_ray R v₁ v₂) (hr : 0 < r) :

same_ray R (r • v₁) v₂

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

source

theorem same_ray.map {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {v₁ v₂ : M} (f : M →ₗ[R] N) (h : same_ray R v₁ v₂) :

same_ray R (⇑f v₁) (⇑f v₂)

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

source

@[simp]

theorem same_ray_map_iff {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {v₁ v₂ : M} (e : M ≃ₗ[R] N) :

same_ray R (⇑e v₁) (⇑e v₂) ↔ same_ray R v₁ v₂

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

source

theorem same_ray.smul {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {S : Type u_3} [has_scalar S M] [smul_comm_class R S M] {v₁ v₂ : M} (s : S) (h : same_ray R v₁ v₂) :

same_ray R (s • v₁) (s • v₂)

If two vectors are on the same ray then both scaled by the same action are also on the same ray.

source

def same_ray_setoid (R : Type u_1) [ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] [nontrivial R] :

setoid M

The setoid of the same_ray relation for elements of a module.

Equations

same_ray_setoid R M = {r := same_ray R _inst_3, iseqv := _}

source

def ray_vector (M : Type u_2) [add_comm_monoid M] :

Type u_2

Nonzero vectors, as used to define rays.

Equations

ray_vector M = {v // v ≠ 0}

source

def ray_vector.same_ray_setoid (R : Type u_1) [ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] [nontrivial R] :

setoid (ray_vector M)

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

Equations

ray_vector.same_ray_setoid R M = setoid.comap coe (same_ray_setoid R M)

source

theorem equiv_iff_same_ray {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (v₁ v₂ : ray_vector M) :

v₁ ≈ v₂ ↔ same_ray R ↑v₁ ↑v₂

Equivalence of nonzero vectors, in terms of same_ray.

source

@[nolint]

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

Type u_2

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

Equations

module.ray R M = quotient (ray_vector.same_ray_setoid R M)

source

def orientation (R : Type u_1) [ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] (ι : Type u_4) [decidable_eq ι] [nontrivial R] :

Type (max u_2 u_1 u_4)

An orientation of a module, intended to be used when ι is a fintype with the same cardinality as a basis.

source

@[class]

structure module.oriented (R : Type u_1) [ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] (ι : Type u_4) [decidable_eq ι] [nontrivial R] :

Type (max u_1 u_2 u_4)

positive_orientation : orientation R M ι

A type class fixing an orientation of a module.

source

@[protected]

def ray_of_ne_zero (R : Type u_1) [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (v : M) (h : v ≠ 0) :

module.ray R M

The ray given by a nonzero vector.

Equations

ray_of_ne_zero R v h = ⟦⟨v, h⟩⟧

source

theorem module.ray.ind (R : Type u_1) [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] {C : module.ray R M → Prop} (h : ∀ (v : M) (hv : v ≠ 0), C (ray_of_ne_zero R v hv)) (x : module.ray R M) :

C x

An induction principle for module.ray, used as induction x using module.ray.ind.

source

theorem ray_eq_iff (R : Type u_1) [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] {v₁ v₂ : M} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) :

ray_of_ne_zero R v₁ hv₁ = ray_of_ne_zero R v₂ hv₂ ↔ same_ray R v₁ v₂

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

source

@[simp]

theorem ray_pos_smul {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] {v : M} (h : v ≠ 0) {r : R} (hr : 0 < r) (hrv : r • v ≠ 0) :

ray_of_ne_zero R (r • v) hrv = ray_of_ne_zero R v h

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

source

def ray_vector.map_linear_equiv {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] (e : M ≃ₗ[R] N) :

ray_vector M ≃ ray_vector N

An equivalence between modules implies an equivalence between ray vectors.

Equations

ray_vector.map_linear_equiv e = e.to_equiv.subtype_equiv _

source

def module.ray.map {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] [nontrivial R] (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 (ray_vector.map_linear_equiv e) _

source

@[simp]

theorem module.ray.map_apply {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] [nontrivial R] (e : M ≃ₗ[R] N) (v : M) (hv : v ≠ 0) :

⇑(module.ray.map e) (ray_of_ne_zero R v hv) = ray_of_ne_zero R (⇑e v) _

source

@[simp]

theorem module.ray.map_refl {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] :

module.ray.map (linear_equiv.refl R M) = equiv.refl (module.ray R M)

source

@[simp]

theorem module.ray.map_symm {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] [nontrivial R] (e : M ≃ₗ[R] N) :

(module.ray.map e).symm = module.ray.map e.symm

source

def orientation.map {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] (ι : Type u_4) [decidable_eq ι] [nontrivial R] (e : M ≃ₗ[R] N) :

orientation R M ι ≃ orientation R N ι

An equivalence between modules implies an equivalence between orientations.

Equations

orientation.map ι e = module.ray.map (alternating_map.dom_lcongr R R ι R e)

source

@[simp]

theorem orientation.map_apply {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] (ι : Type u_4) [decidable_eq ι] [nontrivial R] (e : M ≃ₗ[R] N) (v : alternating_map R M R ι) (hv : v ≠ 0) :

⇑(orientation.map ι e) (ray_of_ne_zero R v hv) = ray_of_ne_zero R (v.comp_linear_map ↑(e.symm)) _

source

@[simp]

theorem orientation.map_refl {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (ι : Type u_4) [decidable_eq ι] [nontrivial R] :

orientation.map ι (linear_equiv.refl R M) = equiv.refl (orientation R M ι)

source

@[simp]

theorem orientation.map_symm {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] (ι : Type u_4) [decidable_eq ι] [nontrivial R] (e : M ≃ₗ[R] N) :

(orientation.map ι e).symm = orientation.map ι e.symm

source

@[protected, instance]

def ray_vector.mul_action {M : Type u_2} [add_comm_monoid M] {G : Type u_5} [group G] [distrib_mul_action G M] :

mul_action G (ray_vector M)

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_scalar := {smul := λ (r : G), subtype.map (has_scalar.smul r) _}, one_smul := _, mul_smul := _}

source

@[protected, instance]

def module.ray.mul_action {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {G : Type u_5} [group G] [nontrivial R] [distrib_mul_action G M] [smul_comm_class R G M] :

mul_action G (module.ray R M)

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

Equations

module.ray.mul_action = {to_has_scalar := {smul := λ (r : G), quotient.map (has_scalar.smul r) _}, one_smul := _, mul_smul := _}

source

@[simp]

theorem module.ray.linear_equiv_smul_eq_map {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (e : M ≃ₗ[R] M) (v : module.ray R M) :

e • v = ⇑(module.ray.map e) v

The action via linear_equiv.apply_distrib_mul_action corresponds to module.ray.map.

source

@[simp]

theorem smul_ray_of_ne_zero {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {G : Type u_5} [group G] [nontrivial R] [distrib_mul_action G M] [smul_comm_class R G M] (g : G) (v : M) (hv : v ≠ 0) :

g • ray_of_ne_zero R v hv = ray_of_ne_zero R (g • v) _

source

theorem module.ray.units_smul_of_pos {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (u : Rˣ) (hu : 0 < ↑u) (v : module.ray R M) :

u • v = v

Scaling by a positive unit is a no-op.

source

noncomputable def module.ray.some_ray_vector {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (x : module.ray R M) :

ray_vector M

An arbitrary ray_vector giving a ray.

Equations

x.some_ray_vector = quotient.out x

source

@[simp]

theorem module.ray.some_ray_vector_ray {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (x : module.ray R M) :

⟦x.some_ray_vector ⟧ = x

The ray of some_ray_vector.

source

noncomputable def module.ray.some_vector {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (x : module.ray R M) :

M

An arbitrary nonzero vector giving a ray.

Equations

x.some_vector = ↑(x.some_ray_vector)

source

@[simp]

theorem module.ray.some_vector_ne_zero {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (x : module.ray R M) :

x.some_vector ≠ 0

some_vector is nonzero.

source

@[simp]

theorem module.ray.some_vector_ray {R : Type u_1} [ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] [nontrivial R] (x : module.ray R M) :

ray_of_ne_zero R x.some_vector _ = x

The ray of some_vector.

source

theorem same_ray.neg {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {v₁ v₂ : M} :

same_ray R v₁ v₂ → same_ray R (-v₁) (-v₂)

If two vectors are in the same ray, so are their negations.

source

@[simp]

theorem same_ray_neg_iff {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {v₁ v₂ : M} :

same_ray R (-v₁) (-v₂) ↔ same_ray R v₁ v₂

same_ray.neg as an iff.

source

theorem same_ray_neg_swap {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {v₁ v₂ : M} :

same_ray R (-v₁) v₂ ↔ same_ray R v₁ (-v₂)

source

theorem eq_zero_of_same_ray_self_neg {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {v₁ : M} (h : same_ray R v₁ (-v₁)) :

v₁ = 0

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

source

@[protected, instance]

def ray_vector.has_neg {M : Type u_2} [add_comm_group M] :

has_neg (ray_vector M)

Negating a nonzero vector.

Equations

ray_vector.has_neg = {neg := λ (v : ray_vector M), ⟨-↑v, _⟩}

source

@[simp, norm_cast]

theorem ray_vector.coe_neg {M : Type u_2} [add_comm_group M] (v : ray_vector M) :

↑-v = -↑v

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

source

@[protected, simp]

theorem ray_vector.neg_neg {M : Type u_2} [add_comm_group M] (v : ray_vector M) :

--v = v

Negating a nonzero vector twice produces the original vector.

source

@[simp]

theorem ray_vector.equiv_neg_iff (R : Type u_1) [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] (v₁ v₂ : ray_vector M) :

-v₁ ≈ -v₂ ↔ v₁ ≈ v₂

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

source

@[protected, instance]

def module.ray.has_neg (R : Type u_1) [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] :

has_neg (module.ray R M)

Negating a ray.

Equations

module.ray.has_neg R = {neg := quotient.map (λ (v : ray_vector M), -v) _}

source

theorem ray_neg (R : Type u_1) [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] (v : M) (h : v ≠ 0) :

ray_of_ne_zero R (-v) _ = -ray_of_ne_zero R v h

The ray given by the negation of a nonzero vector.

source

@[protected, simp]

theorem module.ray.neg_neg {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] (x : module.ray R M) :

--x = x

Negating a ray twice produces the original ray.

source

theorem module.ray.neg_involutive (R : Type u_1) [ordered_comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] [nontrivial R] :

function.involutive (λ (x : module.ray R M), -x)

Negating a ray is involutive.

source

@[protected]

theorem module.ray.eq_neg_iff_eq_neg {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] (x y : module.ray R M) :

x = -y ↔ y = -x

source

theorem module.ray.ne_neg_self {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] [no_zero_smul_divisors R M] (x : module.ray R M) :

x ≠ -x

A ray does not equal its own negation.

source

theorem module.ray.units_smul_of_neg {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [nontrivial R] (u : Rˣ) (hu : ↑u < 0) (v : module.ray R M) :

u • v = -v

Scaling by a negative unit is negation.

source

@[protected]

noncomputable def basis.orientation {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [fintype ι] [decidable_eq ι] [nontrivial R] (e : basis ι R M) :

orientation R M ι

The orientation given by a basis.

Equations

e.orientation = ray_of_ne_zero R e.det _

source

theorem basis.orientation_map {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] {ι : Type u_4} [fintype ι] [decidable_eq ι] [nontrivial R] (e : basis ι R M) (f : M ≃ₗ[R] N) :

(e.map f).orientation = ⇑(orientation.map ι f) e.orientation

source

theorem basis.map_orientation_eq_det_inv_smul {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [fintype ι] [decidable_eq ι] [nontrivial R] [is_domain R] (e : basis ι R M) (x : orientation R M ι) (f : M ≃ₗ[R] M) :

⇑(orientation.map ι f) x = (⇑linear_equiv.det f)⁻¹ • x

The value of orientation.map when the index type has the cardinality of a basis, in terms of f.det.

source

theorem basis.orientation_units_smul {R : Type u_1} [ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [fintype ι] [decidable_eq ι] [nontrivial R] (e : basis ι R M) (w : ι → Rˣ) :

(e.units_smul w).orientation = (∏ (i : ι), w i)⁻¹ • e.orientation

The orientation given by a basis derived using units_smul, in terms of the product of those units.

source

theorem same_ray_of_mem_orbit {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {v₁ v₂ : M} (h : v₁ ∈ mul_action.orbit ↥(units.pos_subgroup R) v₂) :

same_ray R v₁ v₂

same_ray follows from membership of mul_action.orbit for the units.pos_subgroup.

source

@[simp]

theorem units_inv_smul {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (u : Rˣ) (v : module.ray R M) :

u⁻¹ • v = u • v

Scaling by an inverse unit is the same as scaling by itself.

source

@[simp]

theorem same_ray_smul_right_iff {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {v : M} (hv : v ≠ 0) (r : R) :

same_ray R v (r • v) ↔ 0 < r

A nonzero vector is in the same ray as a multiple of itself if and only if that multiple is positive.

source

@[simp]

theorem same_ray_smul_left_iff {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {v : M} (hv : v ≠ 0) (r : R) :

same_ray R (r • v) v ↔ 0 < r

A multiple of a nonzero vector is in the same ray as that vector if and only if that multiple is positive.

source

@[simp]

theorem same_ray_neg_smul_right_iff {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {v : M} (hv : v ≠ 0) (r : R) :

same_ray R (-v) (r • v) ↔ r < 0

The negation of a nonzero vector is in the same ray as a multiple of that vector if and only if that multiple is negative.

source

@[simp]

theorem same_ray_neg_smul_left_iff {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {v : M} (hv : v ≠ 0) (r : R) :

same_ray R (r • v) (-v) ↔ r < 0

A multiple of a nonzero vector is in the same ray as the negation of that vector if and only if that multiple is negative.

source

@[simp]

theorem units_smul_eq_self_iff {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {u : Rˣ} {v : module.ray R M} :

u • v = v ↔ 0 < ↑u

A nonzero vector is in the same ray as a multiple of itself if and only if that multiple is positive.

source

@[simp]

theorem units_smul_eq_neg_iff {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {u : Rˣ} {v : module.ray R M} :

u • v = -v ↔ ↑u < 0

A nonzero vector is in the same ray as a multiple of itself if and only if that multiple is positive.

source

theorem basis.orientation_eq_iff_det_pos {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] (e₁ e₂ : basis ι R M) :

e₁.orientation = e₂.orientation ↔ 0 < ⇑(e₁.det) ⇑e₂

The orientations given by two bases are equal if and only if the determinant of one basis with respect to the other is positive.

source

theorem basis.orientation_eq_or_eq_neg {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] (e : basis ι R M) (x : orientation R M ι) :

x = e.orientation ∨ x = -e.orientation

Given a basis, any orientation equals the orientation given by that basis or its negation.

source

theorem basis.orientation_ne_iff_eq_neg {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] (e : basis ι R M) (x : orientation R M ι) :

x ≠ e.orientation ↔ x = -e.orientation

Given a basis, an orientation equals the negation of that given by that basis if and only if it does not equal that given by that basis.

source

theorem basis.orientation_comp_linear_equiv_eq_iff_det_pos {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] (e : basis ι R M) (f : M ≃ₗ[R] M) :

(e.map f).orientation = e.orientation ↔ 0 < ⇑linear_map.det ↑f

Composing a basis with a linear equiv gives the same orientation if and only if the determinant is positive.

source

theorem basis.orientation_comp_linear_equiv_eq_neg_iff_det_neg {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] (e : basis ι R M) (f : M ≃ₗ[R] M) :

(e.map f).orientation = -e.orientation ↔ ⇑linear_map.det ↑f < 0

Composing a basis with a linear equiv gives the negation of that orientation if and only if the determinant is negative.

source

@[simp]

theorem basis.orientation_neg_single {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [nontrivial R] (e : basis ι R M) (i : ι) :

(e.units_smul (function.update 1 i (-1))).orientation = -e.orientation

Negating a single basis vector (represented using units_smul) negates the corresponding orientation.

source

noncomputable def basis.adjust_to_orientation {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [nontrivial R] [nonempty ι] (e : basis ι R M) (x : orientation R M ι) :

basis ι R M

Given a basis and an orientation, return a basis giving that orientation: either the original basis, or one constructed by negating a single (arbitrary) basis vector.

Equations

e.adjust_to_orientation x = ite (e.orientation = x) e (e.units_smul (function.update 1 (classical.arbitrary ι) (-1)))

source

@[simp]

theorem basis.orientation_adjust_to_orientation {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [nontrivial R] [nonempty ι] (e : basis ι R M) (x : orientation R M ι) :

(e.adjust_to_orientation x).orientation = x

adjust_to_orientation gives a basis with the required orientation.

source

theorem basis.adjust_to_orientation_apply_eq_or_eq_neg {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [nontrivial R] [nonempty ι] (e : basis ι R M) (x : orientation R M ι) (i : ι) :

⇑(e.adjust_to_orientation x) i = ⇑e i ∨ ⇑(e.adjust_to_orientation x) i = -⇑e i

Every basis vector from adjust_to_orientation is either that from the original basis or its negation.

source

theorem same_ray_iff_mem_orbit (R : Type u_1) [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] (v₁ v₂ : M) :

same_ray R v₁ v₂ ↔ v₁ ∈ mul_action.orbit ↥(units.pos_subgroup R) v₂

same_ray is equivalent to membership of mul_action.orbit for the units.pos_subgroup.

source

theorem same_ray_setoid_eq_orbit_rel (R : Type u_1) [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] :

same_ray_setoid R M = mul_action.orbit_rel ↥(units.pos_subgroup R) M

same_ray_setoid equals mul_action.orbit_rel for the units.pos_subgroup.

source

theorem orientation.eq_or_eq_neg {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] (x₁ x₂ : orientation R M ι) (h : fintype.card ι = finite_dimensional.finrank R M) :

x₁ = x₂ ∨ x₁ = -x₂

If the index type has cardinality equal to the finite dimension, any two orientations are equal or negations.

source

theorem orientation.ne_iff_eq_neg {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] (x₁ x₂ : orientation R M ι) (h : fintype.card ι = finite_dimensional.finrank R M) :

x₁ ≠ x₂ ↔ x₁ = -x₂

If the index type has cardinality equal to the finite dimension, an orientation equals the negation of another orientation if and only if they are not equal.

source

theorem orientation.map_eq_det_inv_smul {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] (x : orientation R M ι) (f : M ≃ₗ[R] M) (h : fintype.card ι = finite_dimensional.finrank R M) :

⇑(orientation.map ι f) x = (⇑linear_equiv.det f)⁻¹ • x

The value of orientation.map when the index type has cardinality equal to the finite dimension, in terms of f.det.

source

theorem orientation.map_eq_iff_det_pos {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] (x : orientation R M ι) (f : M ≃ₗ[R] M) (h : fintype.card ι = finite_dimensional.finrank R M) :

⇑(orientation.map ι f) x = x ↔ 0 < ⇑linear_map.det ↑f

If the index type has cardinality equal to the finite dimension, composing an alternating map with the same linear equiv on each argument gives the same orientation if and only if the determinant is positive.

source

theorem orientation.map_eq_neg_iff_det_neg {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] (x : orientation R M ι) (f : M ≃ₗ[R] M) (h : fintype.card ι = finite_dimensional.finrank R M) :

⇑(orientation.map ι f) x = -x ↔ ⇑linear_map.det ↑f < 0

If the index type has cardinality equal to the finite dimension, composing an alternating map with the same linear equiv on each argument gives the negation of that orientation if and only if the determinant is negative.

source

noncomputable def orientation.some_basis {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] [nonempty ι] (x : orientation R M ι) (h : fintype.card ι = finite_dimensional.finrank R M) :

basis ι R M

If the index type has cardinality equal to the finite dimension, a basis with the given orientation.

Equations

x.some_basis h = ((finite_dimensional.fin_basis R M).reindex (fintype.equiv_fin_of_card_eq h).symm).adjust_to_orientation x

source

@[simp]

theorem orientation.some_basis_orientation {R : Type u_1} [linear_ordered_field R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] [finite_dimensional R M] [nonempty ι] (x : orientation R M ι) (h : fintype.card ι = finite_dimensional.finrank R M) :

(x.some_basis h).orientation = x

some_basis gives a basis with the required orientation.

mathlib documentation

Orientations of modules and rays in modules #

Main definitions #

Implementation notes #

References #