Vector product pairs (GPR 22.14)

An orientation of a finitely generated projective k-module M of rank 3 is a k-linear bijection θ : ⋀³ M → k. GPR 22.14 uses θ and the induced orientation θ*⁻¹ of M*, only through the two associated vector products

M × M → M*, (v, w) ↦ v ×θ w, θ(u ∧ v ∧ w) = ⟨u ×θ v, w⟩, M* × M* → M, (φ, ψ) ↦ φ ×θ ψ, θ*⁻¹(φ ∧ ψ ∧ χ) = ⟨χ, φ ×θ ψ⟩,

and it uses those only through three identities: both products are alternating, each is orthogonal to its own arguments, and the two are linked by the Binet–Cauchy identity. This file packages exactly that much data as Module.VectorProductPair k M. It constructs the pair both directly from a basis of size three and from an orientation together with such a basis.

Isolating the identities rather than the orientation is the same move as Module.IsRankOnePairing in Module/Invertible.lean, which isolates what GPR 22.12's twisted matrices need a line bundle for. It buys three things: the algebra ConicAlgebra.TwistedZor built on a pair is a composition algebra with no hypothesis on the rank of M (rank three is what makes pairs exist, not what makes the axioms work); the free case, which is where GPR's localization argument lands, is available directly as Module.VectorProductPair.ofBasis; and the converse direction of GPR 22.15, where the vector products are read off from the multiplication of a reduced octonion algebra, produces a pair directly and never has to exhibit θ.

Main definitions

• Module.VectorProductPair k M : a pair of vector products M × M → M* and M* × M* → M satisfying the three identities of GPR (22.14.2) and Binet–Cauchy.
• Module.VectorProductPair.ofBasis : the pair attached to a basis (u₁, u₂, u₃) of M, whose orientation is θ(u₁ ∧ u₂ ∧ u₃) = 1.
• Module.VectorProductPair.ofOrientationOfBasis : the pair induced by an arbitrary orientation of a based rank-three module.
• Module.Basis.dualCoord : the coordinates of a functional along the dual basis, M* ≃ (ι → k).

Main results

• Module.VectorProductPair.cross_swap, crossDual_swap : the products are anticommutative.
• Module.VectorProductPair.cross_apply_right, apply_crossDual_right : orthogonality to the second argument as well as the first.
• Module.Basis.apply_eq_dotProduct : in the coordinates of a finite basis and its dual basis, the canonical pairing M* × M → k is the dot product. This is what makes a basis of size three produce a vector product pair, and it is stated for an arbitrary finite basis.
• Module.orientationAlternating_mul_dualOrientationAlternating : the primal and dual volume coefficients are inverse, the basis calculation behind Binet–Cauchy.
• Module.Basis.det_mul_det_dualBasis : for a finite basis, the product of the determinant forms of the basis and of its dual basis is the determinant of the matrix of pairings.

Implementation notes

⚠ The orientation is not part of the data. GPR 22.14 starts from (M, θ) with M of rank three; a VectorProductPair is what θ produces. The construction here proves the based calculation by dualizing θ through the canonical exterior-power pairing (GPR 21.7) and checking that the two volume coefficients are inverse. The arbitrary finite-projective case is proved by localization in Composition.Reduced.Orientation.

The three axioms are stated with the left argument in the degenerate position (cross_apply_left, apply_crossDual_left); the right-hand versions follow from anticommutativity, which in turn follows from cross_self. Anticommutativity is therefore not an axiom, and neither is the alternating character of the trilinear form (u, v, w) ↦ ⟨u ×θ v, w⟩, which is the conjunction of the two.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 21.7, 21.8, 22.14.

structure Module.VectorProductPair (k : Type u) (M : Type v) [CommRing k] [AddCommGroup M] [Module k M] : Type (max u v)

A pair of associated vector products on a k-module M (GPR 22.14): k-bilinear maps

× : M × M → M*, ×* : M* × M* → M,

both alternating, each orthogonal to its own arguments, and linked by the Binet–Cauchy identity ⟨v × w, φ ×* ψ⟩ = ⟨φ, v⟩⟨ψ, w⟩ - ⟨φ, w⟩⟨ψ, v⟩.

GPR 22.14 obtains such a pair from an orientation θ : ⋀³ M ≅ k of a rank-three projective module, by θ(u ∧ v ∧ w) = ⟨u × v, w⟩ and θ*⁻¹(φ ∧ ψ ∧ χ) = ⟨χ, φ ×* ψ⟩; the identities below are exactly the alternating character of the two orientations and GPR (22.14.1). The rank plays no role afterwards, so it is not part of this definition — see the module docstring.

• cross : M →ₗ[k] M →ₗ[k] Dual k M

  The vector product M × M → M*, (v, w) ↦ v ×θ w.

• crossDual : Dual k M →ₗ[k] Dual k M →ₗ[k] M

  The vector product M* × M* → M, (φ, ψ) ↦ φ ×θ ψ, of the induced orientation of M*.

• cross_self (v : M) : (self.cross v) v = 0

  The vector product is alternating.

• crossDual_self (φ : Dual k M) : (self.crossDual φ) φ = 0

  The dual vector product is alternating.

• cross_apply_left (v w : M) : ((self.cross v) w) v = 0

  ⟨v × w, v⟩ = θ(v ∧ w ∧ v) = 0.

• apply_crossDual_left (φ ψ : Dual k M) : φ ((self.crossDual φ) ψ) = 0

  ⟨φ, φ ×* ψ⟩ = θ*⁻¹(φ ∧ ψ ∧ φ) = 0.

• cross_apply_crossDual (v w : M) (φ ψ : Dual k M) : ((self.cross v) w) ((self.crossDual φ) ψ) = φ v * ψ w - φ w * ψ v

  The Binet–Cauchy identity linking the two products, GPR (22.14.1).

theorem Module.fin_three_eq_zero_of_apply_eq {X : Type u_1} {N : Type u_2} [Zero N] (f : X → X → X → N) (h₁ : ∀ (v w : X), f v v w = 0) (h₂ : ∀ (v w : X), f v w v = 0) (h₃ : ∀ (v w : X), f v w w = 0) (x : Fin 3 → X) {i j : Fin 3} (hij : x i = x j) (hne : i ≠ j) : f (x 0) (x 1) (x 2) = 0

If a ternary function vanishes whenever any pair of its arguments agrees, then it vanishes on a Fin 3-indexed tuple whenever two distinct entries agree. This is the combinatorial half of map_eq_zero_of_eq' for both alternating forms below. For each vector product, two hypotheses come from fields of VectorProductPair; the third is the derived right-orthogonality identity.

theorem Module.VectorProductPair.ext {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P Q : VectorProductPair k M} (hcross : P.cross = Q.cross) (hcrossDual : P.crossDual = Q.crossDual) : P = Q

Two vector-product pairs are equal when their two bilinear maps are equal.

theorem Module.VectorProductPair.ext_iff {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P Q : VectorProductPair k M} : P = Q ↔ P.cross = Q.cross ∧ P.crossDual = Q.crossDual

theorem Module.VectorProductPair.cross_swap {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : VectorProductPair k M) (v w : M) : (P.cross v) w = -(P.cross w) v

The vector product is anticommutative.

theorem Module.VectorProductPair.crossDual_swap {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : VectorProductPair k M) (φ ψ : Dual k M) : (P.crossDual φ) ψ = -(P.crossDual ψ) φ

The dual vector product is anticommutative.

theorem Module.VectorProductPair.cross_apply_right {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : VectorProductPair k M) (v w : M) : ((P.cross v) w) w = 0

⟨v × w, w⟩ = θ(v ∧ w ∧ w) = 0.

theorem Module.VectorProductPair.apply_crossDual_right {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : VectorProductPair k M) (φ ψ : Dual k M) : ψ ((P.crossDual φ) ψ) = 0

⟨ψ, φ ×* ψ⟩ = θ*⁻¹(φ ∧ ψ ∧ ψ) = 0.

def Module.VectorProductPair.crossAlternating {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : VectorProductPair k M) : M [⋀^Fin 3]→ₗ[k] k

The alternating trilinear form (u, v, w) ↦ ⟨u × v, w⟩ associated to the first vector product.

Equations

• P.crossAlternating = { toMultilinearMap := MultilinearMap.mk' (fun (x : Fin 3 → M) => ((P.cross (x 0)) (x 1)) (x 2)) ⋯ ⋯, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem Module.VectorProductPair.crossAlternating_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : VectorProductPair k M) (x : Fin 3 → M) : P.crossAlternating x = ((P.cross (x 0)) (x 1)) (x 2)

def Module.VectorProductPair.crossDualAlternating {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : VectorProductPair k M) : Dual k M [⋀^Fin 3]→ₗ[k] k

The alternating trilinear form (φ, ψ, χ) ↦ ⟨φ, ψ ×* χ⟩ associated to the dual vector product.

Equations

• P.crossDualAlternating = { toMultilinearMap := MultilinearMap.mk' (fun (x : Fin 3 → Module.Dual k M) => (x 0) ((P.crossDual (x 1)) (x 2))) ⋯ ⋯, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem Module.VectorProductPair.crossDualAlternating_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : VectorProductPair k M) (x : Fin 3 → Dual k M) : P.crossDualAlternating x = (x 0) ((P.crossDual (x 1)) (x 2))

The pair attached to a basis

For a basis (u₁, u₂, u₃), the orientation θ(u₁ ∧ u₂ ∧ u₃) = 1 makes the basis self-dual, and both vector products become the ordinary cross product of k³ read in coordinates. This is the case GPR 22.14 reduces to, and it is the only construction of a pair in this file.

noncomputable def Module.Basis.dualCoord {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : Basis ι k M) : Dual k M ≃ₗ[k] ι → k

The coordinates of a linear functional along the basis dual to b, as an equivalence M* ≃ (ι → k). Together with b.equivFun : M ≃ (ι → k) it makes b self-dual: the canonical pairing becomes the dot product (Module.Basis.apply_eq_dotProduct).

Equations

• b.dualCoord = b.dualBasis.equivFun

@[simp]

theorem Module.Basis.dualCoord_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : Basis ι k M) (φ : Dual k M) (i : ι) : b.dualCoord φ i = φ (b i)

theorem Module.Basis.apply_eq_dotProduct {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : Basis ι k M) (φ : Dual k M) (u : M) : φ u = b.dualCoord φ ⬝ᵥ b.equivFun u

In the coordinates of a finite basis and its dual basis, the canonical pairing is the dot product.

theorem Module.Basis.dualCoord_symm_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : Basis ι k M) (f : ι → k) (u : M) : (b.dualCoord.symm f) u = f ⬝ᵥ b.equivFun u

theorem Module.Basis.apply_equivFun_symm {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : Basis ι k M) (φ : Dual k M) (g : ι → k) : φ (b.equivFun.symm g) = b.dualCoord φ ⬝ᵥ g

noncomputable def Module.crossOfBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) : M →ₗ[k] M →ₗ[k] Dual k M

The cross product of M induced by a basis of size three: the ordinary cross product of the coordinate vectors, read back as a linear functional through the dual basis.

Equations

• Module.crossOfBasis b = (crossProduct.compl₁₂ ↑b.equivFun ↑b.equivFun).compr₂ ↑b.dualCoord.symm

noncomputable def Module.crossDualOfBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) : Dual k M →ₗ[k] Dual k M →ₗ[k] M

The cross product of M* induced by a basis of size three.

Equations

• Module.crossDualOfBasis b = (crossProduct.compl₁₂ ↑b.dualCoord ↑b.dualCoord).compr₂ ↑b.equivFun.symm

@[simp]

theorem Module.crossOfBasis_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) (v w : M) : ((crossOfBasis b) v) w = b.dualCoord.symm ((crossProduct (b.equivFun v)) (b.equivFun w))

@[simp]

theorem Module.crossDualOfBasis_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) (φ ψ : Dual k M) : ((crossDualOfBasis b) φ) ψ = b.equivFun.symm ((crossProduct (b.dualCoord φ)) (b.dualCoord ψ))

noncomputable def Module.VectorProductPair.ofBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) : VectorProductPair k M

The vector product pair attached to a basis (u₁, u₂, u₃) of M: the pair of the orientation θ with θ(u₁ ∧ u₂ ∧ u₃) = 1. The products become the cross product in the coordinates of b; this is self-dual for that orientation, so the axioms are the classical identities u ⬝ᵥ (u ⨯₃ v) = 0 and the Binet–Cauchy identity Matrix.cross_dot_cross.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Module.VectorProductPair.ofBasis_cross {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) : (ofBasis b).cross = crossOfBasis b

@[simp]

theorem Module.VectorProductPair.ofBasis_crossDual {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) : (ofBasis b).crossDual = crossDualOfBasis b

theorem Module.VectorProductPair.crossAlternating_ofBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) : (ofBasis b).crossAlternating = b.det

The trilinear form of the basis-built vector product is the determinant form of the basis.

theorem Module.VectorProductPair.crossDualAlternating_ofBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) : (ofBasis b).crossDualAlternating = b.dualBasis.det

The trilinear form of the basis-built dual vector product is the determinant form of the dual basis.

theorem Module.VectorProductPair.cross_eq_smul_crossOfBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) (P : VectorProductPair k M) : P.cross = P.crossAlternating ⇑b • crossOfBasis b

Relative to a basis of size three, every first vector product is a scalar multiple of the basis-built cross product. The scalar is its oriented volume on that basis.

theorem Module.VectorProductPair.crossDual_eq_smul_crossDualOfBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) (P : VectorProductPair k M) : P.crossDual = P.crossDualAlternating ⇑b.dualBasis • crossDualOfBasis b

Relative to the dual basis, every dual vector product is a scalar multiple of the basis-built dual cross product.

theorem Module.VectorProductPair.cross_coeff_mul_crossDual_coeff {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) (P : VectorProductPair k M) : P.crossAlternating ⇑b * P.crossDualAlternating ⇑b.dualBasis = 1

The two scalar coefficients of a vector-product pair relative to a basis are inverse. This is Binet–Cauchy evaluated on the first two basis vectors and their duals.

theorem Module.VectorProductPair.isUnit_crossAlternating_basis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) (P : VectorProductPair k M) : IsUnit (P.crossAlternating ⇑b)

The volume coefficient of a vector-product pair in any basis is a unit.

theorem Module.VectorProductPair.exists_eq_ofBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Basis (Fin 3) k M) (P : VectorProductPair k M) : ∃ (b' : Basis (Fin 3) k M), P = ofBasis b'

Every vector-product pair on a free module of rank three is the pair attached to a suitably rescaled basis.

The pair attached to an orientation of a based module

theorem Module.alternating_fin_three_cycle {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {N : Type u_1} [AddCommGroup N] [Module k N] (a : M [⋀^Fin 3]→ₗ[k] N) (x y z : M) : a ![x, y, z] = a ![y, z, x]

A cyclic permutation of three arguments preserves an alternating trilinear map.

noncomputable def Module.orientationAlternating {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) : M [⋀^Fin 3]→ₗ[k] k

The alternating volume form obtained from an orientation θ : ⋀³ M ≃ k.

Equations

• Module.orientationAlternating theta = (↑theta).compAlternatingMap (exteriorPower.ιMulti k 3)

@[simp]

theorem Module.orientationAlternating_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) (x : Fin 3 → M) : (orientationAlternating theta) x = theta ((exteriorPower.ιMulti k 3) x)

noncomputable def Module.dualOrientationAlternating {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) : Dual k M [⋀^Fin 3]→ₗ[k] k

The volume form on M* dual to an orientation of M. It evaluates the canonical pairing with the oriented volume element θ⁻¹(1); this is the duality of GPR 21.7.

Equations

• Module.dualOrientationAlternating theta = LinearMap.compAlternatingMap ((Module.Dual.eval k ↥(⋀[k]^3 M)) (theta.symm 1)) (exteriorPower.alternatingMapToDual k M 3)

@[simp]

theorem Module.dualOrientationAlternating_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) (f : Fin 3 → Dual k M) : (dualOrientationAlternating theta) f = ((exteriorPower.pairingDual k M 3) ((exteriorPower.ιMulti k 3) f)) (theta.symm 1)

theorem Module.orientationAlternating_mul_dualOrientationAlternating_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) (x : Fin 3 → M) (f : Fin 3 → Dual k M) : (orientationAlternating theta) x * (dualOrientationAlternating theta) f = Matrix.det fun (i j : Fin 3) => (f i) (x j)

The primal and dual volume forms defined by an orientation multiply to the determinant pairing. This basis-free identity is the scalar form of the perfect exterior-power duality in GPR 21.7.

noncomputable def Module.crossOfOrientation {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) : M →ₗ[k] M →ₗ[k] Dual k M

The vector product M × M → M* induced by an orientation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Module.crossOfOrientation_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) (v w x : M) : (((crossOfOrientation theta) v) w) x = (orientationAlternating theta) ![v, w, x]

noncomputable def Module.crossDualOfOrientation {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] [Module.Finite k M] [Projective k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) : Dual k M →ₗ[k] Dual k M →ₗ[k] M

The vector product M* × M* → M induced by the dual orientation. Projective reflexivity identifies the bidual value of the curried volume form with an element of M.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Module.apply_crossDualOfOrientation {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] [Module.Finite k M] [Projective k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) (f g h : Dual k M) : h (((crossDualOfOrientation theta) f) g) = (dualOrientationAlternating theta) ![f, g, h]

theorem Module.crossOfOrientation_eq_smul_crossOfBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) (b : Basis (Fin 3) k M) : crossOfOrientation theta = (orientationAlternating theta) ⇑b • crossOfBasis b

In a basis, the orientation-induced vector product is its volume coefficient times the standard basis cross product.

theorem Module.crossDualOfOrientation_eq_smul_crossDualOfBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] [Module.Finite k M] [Projective k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) (b : Basis (Fin 3) k M) : crossDualOfOrientation theta = (dualOrientationAlternating theta) ⇑b.dualBasis • crossDualOfBasis b

In the dual basis, the dual orientation-induced product is its volume coefficient times the standard dual cross product.

theorem Module.orientationAlternating_mul_dualOrientationAlternating {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) (b : Basis (Fin 3) k M) : (orientationAlternating theta) ⇑b * (dualOrientationAlternating theta) ⇑b.dualBasis = 1

The volume coefficients of an orientation and its dual are inverse. This is the based form of exterior-power duality in GPR 21.7 and the scalar identity behind GPR (22.14.1).

noncomputable def Module.VectorProductPair.ofOrientationOfBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] [Module.Finite k M] [Projective k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) (b : Basis (Fin 3) k M) : VectorProductPair k M

The based form of GPR 22.14. An orientation of a finite projective module with a basis of size three induces a pair of associated vector products. The products are defined directly from the primal and dual volume forms; the basis is used only to prove Binet–Cauchy.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Module.VectorProductPair.ofOrientationOfBasis_cross {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] [Module.Finite k M] [Projective k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) (b : Basis (Fin 3) k M) : (ofOrientationOfBasis theta b).cross = crossOfOrientation theta

@[simp]

theorem Module.VectorProductPair.ofOrientationOfBasis_crossDual {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] [Module.Finite k M] [Projective k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) (b : Basis (Fin 3) k M) : (ofOrientationOfBasis theta b).crossDual = crossDualOfOrientation theta

theorem Module.VectorProductPair.ofOrientationOfBasis_eq {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] [Module.Finite k M] [Projective k M] (theta : ↥(⋀[k]^3 M) ≃ₗ[k] k) (b b' : Basis (Fin 3) k M) : ofOrientationOfBasis theta b = ofOrientationOfBasis theta b'

The pair constructed from an orientation does not depend on the basis used to verify its axioms.

theorem Module.Basis.det_mul_det_dualBasis {R : Type u} [CommRing R] {N : Type v} [AddCommGroup N] [Module R N] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : Basis ι R N) (x : ι → N) (f : ι → Dual R N) : b.det x * b.dualBasis.det f = (Matrix.of fun (i j : ι) => (f i) (x j)).det

In the coordinates of a finite basis and its dual basis, the product of the two determinant forms is the determinant of the matrix of pairings.