# Orientations of modules #

This file defines orientations of modules.

## Main definitions #

- `Orientation` is a type synonym for `Module.Ray` for the case where the module is that of alternating maps from a module to its underlying ring. An orientation may be associated with an alternating map or with a basis.

- `Module.Oriented` is a type class for a choice of orientation of a module that is considered the positive orientation.

## Implementation notes #

`Orientation` is defined for an arbitrary index type, but the main intended use case is when that index type is a `Fintype` and there exists a basis of the same cardinality.

## References #

- https://en.wikipedia.org/wiki/Orientation_(vector_space)

source
@[reducible, inline]
abbrev Orientation (R : Type u_1) [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] (M : Type u_2) [AddCommMonoid M] [Module R M] (ι : Type u_4) :
Type (max (max u_4 u_1) u_2)

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

Equations

- Orientation R M ι = Module.Ray R (M [⋀^ι]→ₗ[R] R)

Instances For

source
class Module.Oriented (R : Type u_1) [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] (M : Type u_2) [AddCommMonoid M] [Module R M] (ι : Type u_4) :
Type (max (max u_1 u_2) u_4)

A type class fixing an orientation of a module.

- positiveOrientation : Orientation R M ι

  Fix a positive orientation.

Instances

source
def Orientation.map {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid 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 (AlternatingMap.domLCongr R R ι R e)

Instances For

source
@[simp]
theorem Orientation.map_apply {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (ι : Type u_4) (e : M ≃ₗ[R] N) (v : M [⋀^ι]→ₗ[R] R) (hv : v ≠ 0) :
(map ι e) (rayOfNeZero R v hv) = rayOfNeZero R (v.compLinearMap ↑e.symm) ⋯
source
@[simp]
theorem Orientation.map_refl {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] (ι : Type u_4) :
map ι (LinearEquiv.refl R M) = Equiv.refl (Orientation R M ι)
source
@[simp]
theorem Orientation.map_symm {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (ι : Type u_4) (e : M ≃ₗ[R] N) :
(map ι e).symm = map ι e.symm
source
def Orientation.reindex (R : Type u_1) [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] (M : Type u_2) [AddCommMonoid 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 (AlternatingMap.domDomCongrₗ R e)

Instances For

source
@[simp]
theorem Orientation.reindex_apply (R : Type u_1) [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] (M : Type u_2) [AddCommMonoid M] [Module R M] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') (v : M [⋀^ι]→ₗ[R] R) (hv : v ≠ 0) :
(reindex R M e) (rayOfNeZero R v hv) = rayOfNeZero R (AlternatingMap.domDomCongr e v) ⋯
source
@[simp]
theorem Orientation.reindex_refl (R : Type u_1) [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] (M : Type u_2) [AddCommMonoid M] [Module R M] {ι : Type u_4} :
reindex R M (Equiv.refl ι) = Equiv.refl (Orientation R M ι)
source
@[simp]
theorem Orientation.reindex_symm (R : Type u_1) [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] (M : Type u_2) [AddCommMonoid M] [Module R M] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') :
(reindex R M e).symm = reindex R M e.symm
source
@[instance 100]
instance IsEmpty.oriented {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] (ι : Type u_4) [IsEmpty ι] :
Module.Oriented R M ι

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

Equations

- IsEmpty.oriented ι = { positiveOrientation := rayOfNeZero R (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ }

source
@[simp]
theorem Orientation.map_positiveOrientation_of_isEmpty {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (ι : Type u_4) [IsEmpty ι] (f : M ≃ₗ[R] N) :
(map ι f) positiveOrientation = positiveOrientation
source
@[simp]
theorem Orientation.map_of_isEmpty {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] (ι : Type u_4) [IsEmpty ι] (x : Orientation R M ι) (f : M ≃ₗ[R] M) :
(map ι f) x = x
source
@[simp]
theorem Orientation.map_neg {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {ι : Type u_4} (f : M ≃ₗ[R] N) (x : Orientation R M ι) :
(map ι f) (-x) = -(map ι f) x
source
@[simp]
theorem Orientation.reindex_neg {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') (x : Orientation R M ι) :
(reindex R M e) (-x) = -(reindex R M e) x
source
theorem Module.Basis.map_orientation_eq_det_inv_smul {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [Finite ι] (e : Basis ι R M) (x : Orientation R M ι) (f : M ≃ₗ[R] M) :
(Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x

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

source
def Module.Basis.orientation {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (e : Basis ι R M) :
Orientation R M ι

The orientation given by a basis.

Equations

- e.orientation = rayOfNeZero R e.det ⋯

Instances For

source
theorem Module.Basis.orientation_map {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (e : Basis ι R M) (f : M ≃ₗ[R] N) :
(e.map f).orientation = (Orientation.map ι f) e.orientation
source
theorem Module.Basis.orientation_reindex {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} {ι' : Type u_5} [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι'] (e : Basis ι R M) (eι : ι ≃ ι') :
(e.reindex eι).orientation = (Orientation.reindex R M eι) e.orientation
source
theorem Module.Basis.orientation_unitsSMul {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (e : Basis ι R M) (w : ι → R ˣ) :
(e.unitsSMul 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
@[simp]
theorem Module.Basis.orientation_isEmpty {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] [IsEmpty ι] (b : Basis ι R M) :
b.orientation = positiveOrientation
source
theorem Orientation.eq_or_eq_neg_of_isEmpty {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [IsEmpty ι] (o : Orientation R M ι) :
o = positiveOrientation ∨ o = -positiveOrientation

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 Module.Basis.orientation_eq_iff_det_pos {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (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 Module.Basis.orientation_eq_or_eq_neg {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (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 Module.Basis.orientation_ne_iff_eq_neg {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (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 Module.Basis.orientation_comp_linearEquiv_eq_iff_det_pos {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (e : Basis ι R M) (f : M ≃ₗ[R] M) :
(e.map f).orientation = e.orientation ↔ 0 < LinearMap.det ↑f

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

source
theorem Module.Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (e : Basis ι R M) (f : M ≃ₗ[R] M) :
(e.map f).orientation = -e.orientation ↔ LinearMap.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 Module.Basis.orientation_neg_single {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (e : Basis ι R M) (i : ι) :
(e.unitsSMul (Function.update 1 i (-1))).orientation = -e.orientation

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

source
def Module.Basis.adjustToOrientation {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] [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.adjustToOrientation x = if e.orientation = x then e else e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))

Instances For

source
@[simp]
theorem Module.Basis.orientation_adjustToOrientation {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Nonempty ι] (e : Basis ι R M) (x : Orientation R M ι) :
(e.adjustToOrientation x).orientation = x

`adjust_to_orientation` gives a basis with the required orientation.

source
theorem Module.Basis.adjustToOrientation_apply_eq_or_eq_neg {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Nonempty ι] (e : Basis ι R M) (x : Orientation R M ι) (i : ι) :
(e.adjustToOrientation x) i = e i ∨ (e.adjustToOrientation x) i = -e i

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

source
theorem Module.Basis.det_adjustToOrientation {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Nonempty ι] (e : Basis ι R M) (x : Orientation R M ι) :
(e.adjustToOrientation x).det = e.det ∨ (e.adjustToOrientation x).det = -e.det
source
@[simp]
theorem Module.Basis.abs_det_adjustToOrientation {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Nonempty ι] (e : Basis ι R M) (x : Orientation R M ι) (v : ι → M) :
|(e.adjustToOrientation x).det v| = |e.det v|
source
theorem Orientation.eq_or_eq_neg {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [FiniteDimensional R M] (x₁ x₂ : Orientation R M ι) (h : Fintype.card ι = Module.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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [FiniteDimensional R M] (x₁ x₂ : Orientation R M ι) (h : Fintype.card ι = Module.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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [FiniteDimensional R M] (x : Orientation R M ι) (f : M ≃ₗ[R] M) (h : Fintype.card ι = Module.finrank R M) :
(map ι f) x = (LinearEquiv.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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [FiniteDimensional R M] (x : Orientation R M ι) (f : M ≃ₗ[R] M) (h : Fintype.card ι = Module.finrank R M) :
(map ι f) x = x ↔ 0 < LinearMap.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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] (x : Orientation R M ι) (f : M ≃ₗ[R] M) (h : Fintype.card ι = Module.finrank R M) :
(map ι f) x = -x ↔ LinearMap.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
def Orientation.someBasis {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [Nonempty ι] [DecidableEq ι] [FiniteDimensional R M] (x : Orientation R M ι) (h : Fintype.card ι = Module.finrank R M) :
Module.Basis ι R M

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

Equations

- x.someBasis h = ((Module.finBasis R M).reindex (Fintype.equivFinOfCardEq h).symm).adjustToOrientation x

Instances For

source
@[simp]
theorem Orientation.someBasis_orientation {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [Nonempty ι] [DecidableEq ι] [FiniteDimensional R M] (x : Orientation R M ι) (h : Fintype.card ι = Module.finrank R M) :
(x.someBasis h).orientation = x

`some_basis` gives a basis with the required orientation.