Basis.orientation_eq_or_eq_neg
theorem Basis.orientation_eq_or_eq_neg :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (e : Basis ι R M) (x : Orientation R M ι),
x = e.orientation ∨ x = -e.orientation
This theorem states that given a basis `e` of a module `M` over a linearly ordered commutative ring `R`, where `ι` is a finite type corresponding in cardinality to the basis, any orientation `x` of the module is either equal to the orientation determined by the basis or its negation. In other words, for any orientation, it can always be expressed via the given basis `e` or the negative of it. This holds true irrespective of the specific orientation we start with.
More concisely: Given a linearly ordered commutative ring R, a finite basis e of an R-module M, and any orientation x of M, there exists an integer i in the finite type ι such that x = e(i) or x = -e(i).
|
Orientation.eq_or_eq_neg
theorem Orientation.eq_or_eq_neg :
∀ {R : Type u_1} [inst : LinearOrderedField R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [_i : FiniteDimensional R M] (x₁ x₂ : Orientation R M ι),
Fintype.card ι = FiniteDimensional.finrank R M → x₁ = x₂ ∨ x₁ = -x₂
This theorem states that given a linearly ordered field `R` and an `R`-module `M`, if the index type `ι` has the same cardinality as the finite dimension of the module `M` (i.e., `Fintype.card ι = FiniteDimensional.finrank R M`), then any two orientations `x₁` and `x₂` of the module `M` are either equal or negations of each other. An orientation of a module is essentially a choice of direction for the module, and the theorem implies that the only distinct orientations possible (assuming the condition on the cardinality/dimension) are opposites of each other.
More concisely: Given a linearly ordered field `R` and a finite-dimensional `R`-module `M` of cardinality `ι`, any two orientations of `M` are either equal or negations of each other.
|
Orientation.someBasis_orientation
theorem Orientation.someBasis_orientation :
∀ {R : Type u_1} [inst : LinearOrderedField R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [_i : FiniteDimensional R M] [inst_4 : Nonempty ι] [inst_5 : DecidableEq ι]
(x : Orientation R M ι) (h : Fintype.card ι = FiniteDimensional.finrank R M), (x.someBasis h).orientation = x
The theorem `Orientation.someBasis_orientation` states that for any given linear ordered field `R`, additively commutative group `M` and a module `M` over `R`, and a type `ι` which is a fintype, if `M` is also a finite dimensional vector space over `R`, and `ι` is nonempty and has decidable equality, then for any given orientation `x` of this module, if the number of elements in `ι` is equal to the rank (or finite dimension) of the module `M`, then the orientation of the basis obtained from `x` using the `someBasis` function is equal to `x`.
In simpler terms, if you have an orientation of a module which is also a finite dimensional vector space, and the number of basis vectors matches the dimension of the space, then getting the basis from the orientation and then finding its orientation takes you back to the original orientation.
More concisely: If `R` is a linear ordered field, `M` is an additively commutative group and a finite dimensional vector space over `R`, `ι` is a nonempty fintype with decidable equality, and `x` is an orientation of `M`, then `x` is the orientation of the basis obtained from `x` using `someBasis` if and only if `ι` has size equal to the rank of `M`.
|
Basis.adjustToOrientation_apply_eq_or_eq_neg
theorem Basis.adjustToOrientation_apply_eq_or_eq_neg :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] [inst_5 : Nonempty ι] (e : Basis ι R M)
(x : Orientation R M ι) (i : ι), (e.adjustToOrientation x) i = e i ∨ (e.adjustToOrientation x) i = -e i
The theorem `Basis.adjustToOrientation_apply_eq_or_eq_neg` asserts that for any linearly ordered commutative ring `R`, any additive commutative group `M` that is also an `R`-module, any finite type `ι` with decidable equality, any nonempty `ι`, any basis `e` of `M` over `R` indexed by `ι`, any orientation `x` of the `R`-module `M` indexed by `ι`, and any index `i` of type `ι`, the `i`-th basis vector adjusted to the orientation `x` is either equal to the original `i`-th basis vector or its negation. This means that adjusting a basis to an orientation does not change the basis vectors, except possibly by negating them.
More concisely: For any linearly ordered commutative ring R, additive commutative group M as an R-module, finite type ι with decidable equality, nonempty ι, a basis e of M over R indexed by ι, and an orientation x of M indexed by ι, the i-th basis vector adjusted to the orientation x is either equal to the original i-th basis vector or its negation for all i ∈ ι.
|
Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg
theorem Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (e : Basis ι R M) (f : M ≃ₗ[R] M),
(e.map f).orientation = -e.orientation ↔ LinearMap.det ↑f < 0
The theorem `Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg` states that for any linearly ordered commutative ring `R`, an additive commutative group `M` which is a module over `R`, a finite type `ι`, and a basis `e` of `M` with index type `ι`, given a linear equivalence `f` from `M` to `M`, the orientation of the basis `e` composed with the linear equivalence `f` is the negation of the orientation of `e` if and only if the determinant of the linear map corresponding to `f` is negative.
More concisely: For a linearly ordered commutative ring `R`, an additive commutative group `M` as an `R`-module, a finite index type `ι`, and a basis `e` of `M`, the orientation of `e` composed with a linear equivalence `f` is the negation of `e`'s orientation if and only if the determinant of `f` is negative.
|
Basis.orientation_unitsSMul
theorem Basis.orientation_unitsSMul :
∀ {R : Type u_1} [inst : StrictOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_4} [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (e : Basis ι R M) (w : ι → Rˣ),
(e.unitsSMul w).orientation = (Finset.univ.prod fun i => w i)⁻¹ • e.orientation
This theorem, `Basis.orientation_unitsSMul`, states that for any strict ordered commutative ring `R`, an additive commutative group `M`, a module `R M`, and a type `ι` which is finite and has decidable equality, given a basis `e` of the module and a function `w` that maps `ι` to the group of units of `R`, the orientation of the basis obtained by scaling the elements of `e` using `w` (using the `unitsSMul` function) is equal to the inverse of the product of all elements in the image of `w` (taken over the entire type `ι`) scaled by the orientation of the original basis `e`. This product is taken with respect to the natural order on `ι`, using the `Finset.univ.prod` function.
More concisely: For any strict ordered commutative ring R, additive commutative group M, R-module M, finite type ι with decidable equality, basis e of M, and function w from ι to the group of units of R, the orientation of the basis e scaled using w is equal to the inverse of the product of w(i) scaled by the orientation of e, for all i in ι, with respect to the natural order on ι.
|
Basis.orientation.proof_2
theorem Basis.orientation.proof_2 :
∀ {R : Type u_1} [inst : StrictOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (e : Basis ι R M), e.det ≠ 0
The theorem `Basis.orientation.proof_2` asserts that for a given basis `e` of a module `M` over a strictly ordered commutative ring `R` with a finite type `ι`, the determinant of the basis `e` is never zero. This theorem holds regardless of the decidable equality of the elements in the type `ι`. Essentially, this theorem is stating that the determinant of a basis in a module over a strictly ordered commutative ring is always non-zero.
More concisely: For every finite type ι and a strictly ordered commutative ring R with a basis e of a module M over R, the determinant of e is non-zero.
|
Orientation.map_eq_det_inv_smul
theorem Orientation.map_eq_det_inv_smul :
∀ {R : Type u_1} [inst : LinearOrderedField R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [_i : FiniteDimensional R M] (x : Orientation R M ι) (f : M ≃ₗ[R] M),
Fintype.card ι = FiniteDimensional.finrank R M → (Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x
The theorem `Orientation.map_eq_det_inv_smul` states that for a certain linear-ordered field `R`, a module `M` over `R`, an index type `ι` which is a finite type, and assuming that `M` is finite-dimensional over `R`, given an orientation `x` of `M` and a linear equivalence `f` from `M` to itself, if the cardinality of `ι` equals the rank of the module `M` (i.e., dimension of the vector space), the orientation resulting from applying the map `f` to `x` is equal to the inverse of the determinant of `f` scaled by `x`. In other words, the action of the map on the orientation is simply scaling by the reciprocal of the determinant of the linear equivalence.
More concisely: For a finite-dimensional module M over a linear-ordered field R with finite index type ι, if orientation x of M and linear equivalence f of M have cardinality of ι equal to the rank of M, then the orientation of M obtained by applying f is equal to the inverse of the determinant of f scaled by x.
|
Basis.orientation_adjustToOrientation
theorem Basis.orientation_adjustToOrientation :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] [inst_5 : Nonempty ι] (e : Basis ι R M)
(x : Orientation R M ι), (e.adjustToOrientation x).orientation = x
The theorem `Basis.orientation_adjustToOrientation` states that for any linearly ordered commutative ring `R`, an additive group `M` that is also a module over `R`, a finite type `ι` (with a decidable equality and at least one element), a basis `e` of `M` over `R` indexed by `ι`, and an orientation `x` of the module, the orientation of the basis adjusted to the orientation `x` is indeed `x`. In essence, this theorem guarantees that the function `adjustToOrientation` correctly adjusts the basis to have the specified orientation.
More concisely: For any commutative ring R, module M over R with basis e indexed by a finite type ι and decidable equality, and orientation x of M, the adjusted basis e adjusted to orientation x equals x.
|
Basis.orientation_neg_single
theorem Basis.orientation_neg_single :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (e : Basis ι R M) (i : ι),
(e.unitsSMul (Function.update 1 i (-1))).orientation = -e.orientation
This theorem states that for any linearly ordered commutative ring `R`, any additive commutative group `M` which is also a `R`-module, any finite indexed type `ι`, any decidable equality on `ι`, any basis `e` of `M` over `R` indexed by `ι`, and any index `i`, the orientation of the basis obtained by scaling the `i`-th vector of `e` by `-1` is the negation of the orientation of `e`. Here, the scaling is performed using the function `unitsSMul` and the function update is used to replace the `i`-th coordinate of the constant function `1` by `-1`.
More concisely: For any linearly ordered commutative ring `R`, any additive commutative `R`-module `M` with a basis `e` indexed by a finite decidable type `ι`, the orientation of `e` is negated by scaling the `i`-th basis vector `-e(i)` using the multiplicative identity of `R` and the function `unitsSMul`.
|
Basis.map_orientation_eq_det_inv_smul
theorem Basis.map_orientation_eq_det_inv_smul :
∀ {R : Type u_1} [inst : StrictOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_4} [inst_3 : Finite ι],
Basis ι R M → ∀ (x : Orientation R M ι) (f : M ≃ₗ[R] M), (Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x
This theorem states that given a strict ordered commutative ring `R`, an additive commutative group `M` that is a module over `R`, and a finite type `ι`, if `ι` forms a basis for `M`, then for any orientation `x` of `M` and any linear equivalence `f` from `M` to itself, the orientation obtained by mapping `x` under `f` is equal to the inverse of the determinant of `f` scaled by `x`. In other words, applying a linear transformation to an orientation scales the orientation by the inverse determinant of the transformation.
More concisely: Given a strict ordered commutative ring `R`, an additive commutative `R`-module `M` with finite basis `ι`, any orientation `x` of `M`, and any linear equivalence `f` from `M` to itself, the orientation `f(x)` is equal to the inverse determinant of `f` scaled by `x`.
|
Basis.orientation_ne_iff_eq_neg
theorem Basis.orientation_ne_iff_eq_neg :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (e : Basis ι R M) (x : Orientation R M ι),
x ≠ e.orientation ↔ x = -e.orientation
The theorem `Basis.orientation_ne_iff_eq_neg` states that for any linearly ordered commutative ring `R`, additive commutative group `M` and `M` is an `R`-module, and for any finite type `ι` with decidable equality, given a basis `e` of `M` over `R` indexed by `ι` and any orientation `x` of the `R`-module `M`, the orientation `x` is not equal to the orientation determined by the basis `e` if and only if `x` is equal to the negation of the orientation determined by the basis `e`. In simpler terms, an orientation of a module is the negation of the orientation given by a basis if and only if it is not the same as the orientation given by the basis.
More concisely: For any linearly ordered commutative ring R, additive commutative group M as an R-module, finite type ι with decidable equality, basis e of M over R indexed by ι, and orientation x of M, x is the negation of the orientation determined by e if and only if x is not equal to the orientation determined by e.
|
Basis.orientation_eq_iff_det_pos
theorem Basis.orientation_eq_iff_det_pos :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (e₁ e₂ : Basis ι R M),
e₁.orientation = e₂.orientation ↔ 0 < e₁.det ⇑e₂
This theorem states that for any linear ordered commutative ring `R`, any additive commutative group `M` which is also an `R`-module, any finite type `ι`, and for any two bases `e₁` and `e₂` of `M` indexed by `ι`, the orientation defined by `e₁` is equal to the orientation defined by `e₂` if and only if the determinant of the matrix representing `e₁` with respect to `e₂` is positive. This theorem relates the concepts of orientation and determinant in the context of linear algebra.
More concisely: For any linear ordered commutative ring `R`, any additive commutative `R`-module `M` of finite type, and two bases `e₁` and `e₂` of `M`, their orientations are equal if and only if the determinant of the change-of-basis matrix from `e₁` to `e₂` is positive.
|
Orientation.ne_iff_eq_neg
theorem Orientation.ne_iff_eq_neg :
∀ {R : Type u_1} [inst : LinearOrderedField R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [_i : FiniteDimensional R M] (x₁ x₂ : Orientation R M ι),
Fintype.card ι = FiniteDimensional.finrank R M → (x₁ ≠ x₂ ↔ x₁ = -x₂)
This theorem states that for a linear ordered field `R`, an additive commutative group `M` which is also a module over `R`, an index type `ι` which is a finite type, and for two orientations `x₁` and `x₂` of the module `M` indexed by `ι`, if the number of elements in `ι` (i.e., the cardinality of `ι`) is equal to the finite rank or dimension of the module `M`, then the orientation `x₁` is not equal to the orientation `x₂` if and only if `x₁` is the negation of `x₂`. In other words, when the conditions about cardinality and finite rank are met, two orientations being different is equivalent to one being the negation of the other.
More concisely: For a linear ordered field `R`, a finite-dimensional additive commutative `R`-module `M`, and two orientations `x₁` and `x₂` of `M` indexed by a finite type `ι`, `x₁` and `x₂` are oppositely oriented if and only if they represent different orientations.
|
Orientation.map_eq_neg_iff_det_neg
theorem Orientation.map_eq_neg_iff_det_neg :
∀ {R : Type u_1} [inst : LinearOrderedField R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] (x : Orientation R M ι) (f : M ≃ₗ[R] M),
Fintype.card ι = FiniteDimensional.finrank R M → ((Orientation.map ι f) x = -x ↔ LinearMap.det ↑f < 0)
This theorem states that for a given linear ordered field `R`, and a module `M` over `R` with an additively commutative group structure, if we also have a finite type `ι` which indexes the basis of our module such that the cardinality of `ι` equals the rank of our module, then the composition of an alternating map with the same linear equivalence on each argument transforms our orientation into its negative if and only if the determinant of the linear equivalence is less than zero. In other words, the orientation flips if and only if the determinant of the linear equivalence is negative.
More concisely: For a linear ordered field `R`, a module `M` over `R` with finite basis `ι`, and a linear equivalence `A` between two `ι`-tuples of `M`, the orientation of `A` flips if and only if the determinant of `A` is negative.
|
Orientation.eq_or_eq_neg_of_isEmpty
theorem Orientation.eq_or_eq_neg_of_isEmpty :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : IsEmpty ι] (o : Orientation R M ι), o = positiveOrientation ∨ o = -positiveOrientation
The theorem `Orientation.eq_or_eq_neg_of_isEmpty` states that for any linearly ordered commutative ring `R` and any module `M` over `R`, if the index type `ι` is empty, then any "orientation" of `M` (in the sense defined by the `Orientation` type constructor) is either equal to the positive orientation or its negation. Note that such an "orientation" of `M` corresponds to the conventional mathematical concept of an orientation only if `M` is zero-dimensional.
More concisely: For any commutative ring `R` and module `M` over `R` with an empty index type `ι`, the orientation of `M` is either the positive orientation or its negation.
|
Orientation.map_eq_iff_det_pos
theorem Orientation.map_eq_iff_det_pos :
∀ {R : Type u_1} [inst : LinearOrderedField R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [_i : FiniteDimensional R M] (x : Orientation R M ι) (f : M ≃ₗ[R] M),
Fintype.card ι = FiniteDimensional.finrank R M → ((Orientation.map ι f) x = x ↔ 0 < LinearMap.det ↑f)
This theorem states that for a linearly ordered field `R`, a module `M` over `R`, and an index type `ι` that is a finite type, if `M` is also finite-dimensional over `R` and the cardinality of `ι` equals the rank of `M`, then for any orientation `x` of `M` and any linear equivalence `f` from `M` to itself, the orientation obtained by mapping `x` through `f` is the same as `x` if and only if the determinant of the matrix representation of `f` is positive. This provides a condition to check whether a given linear transformation preserves the orientation of the space.
More concisely: For a linearly ordered field `R`, a finite-dimensional `R`-module `M`, and a finite index type `ι`, if `x` is an orientation of `M`, `f` is a linear equivalence from `M` to itself, and the cardinality of `ι` equals the rank of `M`, then `x` and the orientation obtained by mapping `x` through `f` are equal if and only if the determinant of `f`'s matrix representation is positive.
|
Basis.orientation_comp_linearEquiv_eq_iff_det_pos
theorem Basis.orientation_comp_linearEquiv_eq_iff_det_pos :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{ι : Type u_3} [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (e : Basis ι R M) (f : M ≃ₗ[R] M),
(e.map f).orientation = e.orientation ↔ 0 < LinearMap.det ↑f
This theorem states that for a given linear ordered commutative ring `R`, an additive commutative group `M` which is also a module over `R`, a finite type `ι`, and a basis `e` of `M` over `R` indexed by `ι`, the orientation of the basis transformed by a linear equivalence `f` is equal to the original orientation if and only if the determinant of `f` is positive. In simpler terms, the orientation (which reflects the 'direction' of a basis) remains the same after applying a transformation, if the determinant of that transformation is positive. In this context, the determinant provides a measure of how the transformation changes the area or volume of the space.
More concisely: For a linear ordered commutative ring `R`, an additive commutative group `M` as an `R`-module, a finite index set `ι`, and a basis `e` of `M`, the orientation of `e` is preserved under a linear equivalence `f : M ≃ₑₓ M` if and only if the determinant of `f` is positive.
|