linear_algebra.orientation

@[reducible]

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

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) [strict_ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] (ι : Type u_4) :

Type (max u_1 u_2 u_4)

positive_orientation : orientation R M ι

A type class fixing an orientation of a module.

Instances of this typeclass

is_empty.oriented

Instances of other typeclasses for module.oriented

module.oriented.has_sizeof_inst

source

def orientation.map {R : Type u_1} [strict_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) (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} [strict_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) (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} [strict_ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (ι : Type u_4) :

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

source

@[simp]

theorem orientation.map_symm {R : Type u_1} [strict_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) (e : M ≃ₗ[R] N) :

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

source

def orientation.reindex (R : Type u_1) [strict_ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') :

orientation R M ι ≃ orientation R M ι'

An equivalence between indices implies an equivalence between orientations.

Equations

orientation.reindex R M e = module.ray.map (alternating_map.dom_dom_lcongr R e)

source

@[simp]

theorem orientation.reindex_apply (R : Type u_1) [strict_ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') (v : alternating_map R M R ι) (hv : v ≠ 0) :

⇑(orientation.reindex R M e) (ray_of_ne_zero R v hv) = ray_of_ne_zero R (alternating_map.dom_dom_congr e v) _

source

@[simp]

theorem orientation.reindex_refl (R : Type u_1) [strict_ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] {ι : Type u_4} :

orientation.reindex R M (equiv.refl ι) = equiv.refl (orientation R M ι)

source

@[simp]

theorem orientation.reindex_symm (R : Type u_1) [strict_ordered_comm_semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') :

(orientation.reindex R M e).symm = orientation.reindex R M e.symm

source

@[protected, instance]

def is_empty.oriented {R : Type u_1} [strict_ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (ι : Type u_4) [nontrivial R] [is_empty ι] :

module.oriented R M ι

A module is canonically oriented with respect to an empty index type.

Equations

is_empty.oriented ι = {positive_orientation := ray_of_ne_zero R (⇑alternating_map.const_linear_equiv_of_is_empty 1) _}

source

@[simp]

theorem orientation.map_positive_orientation_of_is_empty {R : Type u_1} [strict_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) [nontrivial R] [is_empty ι] (f : M ≃ₗ[R] N) :

⇑(orientation.map ι f) module.oriented.positive_orientation = module.oriented.positive_orientation

source

@[simp]

theorem orientation.map_of_is_empty {R : Type u_1} [strict_ordered_comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] (ι : Type u_4) [is_empty ι] (x : orientation R M ι) (f : M ≃ₗ[R] M) :

⇑(orientation.map ι f) x = x

source

@[protected, simp]

theorem orientation.map_neg {R : Type u_1} [strict_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} (f : M ≃ₗ[R] N) (x : orientation R M ι) :

⇑(orientation.map ι f) (-x) = -⇑(orientation.map ι f) x

source

@[protected, simp]

theorem orientation.reindex_neg {R : Type u_1} [strict_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} {ι' : Type u_4} (e : ι ≃ ι') (x : orientation R M ι) :

⇑(orientation.reindex R M e) (-x) = -⇑(orientation.reindex R M e) x

source

theorem basis.map_orientation_eq_det_inv_smul {R : Type u_1} [strict_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [finite ι] (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

@[protected]

noncomputable def basis.orientation {R : Type u_1} [strict_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} [strict_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.orientation_reindex {R : Type u_1} [strict_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} {ι' : Type u_5} [fintype ι] [decidable_eq ι] [fintype ι'] [decidable_eq ι'] [nontrivial R] (e : basis ι R M) (eι : ι ≃ ι') :

(e.reindex eι).orientation = ⇑(orientation.reindex R M eι) e.orientation

source

theorem basis.orientation_units_smul {R : Type u_1} [strict_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 = (finset.univ.prod (λ (i : ι), w i))⁻¹ • e.orientation

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

source

@[simp]

theorem basis.orientation_is_empty {R : Type u_1} [strict_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [fintype ι] [decidable_eq ι] [nontrivial R] [is_empty ι] (b : basis ι R M) :

b.orientation = module.oriented.positive_orientation

source

theorem orientation.eq_or_eq_neg_of_is_empty {R : Type u_1} [linear_ordered_comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [nontrivial R] [is_empty ι] (o : orientation R M ι) :

o = module.oriented.positive_orientation ∨ o = -module.oriented.positive_orientation

A module M over a linearly ordered commutative ring has precisely two "orientations" with respect to an empty index type. (Note that these are only orientations of M of in the conventional mathematical sense if M is zero-dimensional.)

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} [fintype ι] [decidable_eq ι] (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} [fintype ι] [decidable_eq ι] (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} [fintype ι] [decidable_eq ι] (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} [fintype ι] [decidable_eq ι] (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} [fintype ι] [decidable_eq ι] (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} [fintype ι] [decidable_eq ι] [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} [fintype ι] [decidable_eq ι] [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} [fintype ι] [decidable_eq ι] [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} [fintype ι] [decidable_eq ι] [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 basis.det_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} [fintype ι] [decidable_eq ι] [nontrivial R] [nonempty ι] (e : basis ι R M) (x : orientation R M ι) :

(e.adjust_to_orientation x).det = e.det ∨ (e.adjust_to_orientation x).det = -e.det

source

@[simp]

theorem basis.abs_det_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} [fintype ι] [decidable_eq ι] [nontrivial R] [nonempty ι] (e : basis ι R M) (x : orientation R M ι) (v : ι → M) :

|⇑((e.adjust_to_orientation x).det) v| = |⇑(e.det) v|

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} [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} [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} [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} [fintype ι] (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} [fintype ι] (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} [fintype ι] [finite_dimensional R M] [nonempty ι] [decidable_eq ι] (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} [fintype ι] [finite_dimensional R M] [nonempty ι] [decidable_eq ι] (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.

mathlib3 documentation

Orientations of modules #

Main definitions #

Implementation notes #

References #