Transporting orientations along linear equivalences

Orientation transport commutes with composition, and determinants characterize when transported rays agree. Integral unit signs retain or reverse orientations; signed Jacobians determine their compatibility under linear equivalences.

Main results

• Orientation.map_trans: transport along a composite is the composite of the transports.
• Orientation.map_reindex: transport along a linear equivalence commutes with reindexing.
• Orientation.reindex_trans: reindexing along a composite is the composite of the reindexings.
• Orientation.map_units_smul, Orientation.reindex_units_smul: transport and reindexing commute with scaling by units.
• Orientation.map_eq_map_iff_det_mul_pos: f and g transport x to the same orientation if and only if 0 < det f * det g.
• Orientation.map_eq_map_of_det_pos: two linear equivalences whose relative map has positive determinant transport an orientation to the same orientation.
• Orientation.intCast_units_smul_eq_ite: an integer unit acts by retention or reversal.
• Orientation.intCast_units_smul_injective: the two signs give distinct orientations.
• Orientation.reindex_perm: reindexing along a permutation multiplies by its sign.
• Orientation.map_units_smul_eq_iff_det_mul_pos: the signed-Jacobian compatibility criterion.
• Orientation.map_units_smul_eq_units_smul_map_iff_det_mul_pos: the same criterion between two spaces, relative to a reference linear equivalence.
• Orientation.map_linearEquiv_neg: transport along the negation of an n-dimensional space multiplies an orientation by (-1) ^ n.
• Orientation.intCast_units_smul_ite_eq: the relative sign reconstructs an orientation.

@[simp]

theorem Orientation.map_trans {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] {ι : Type u_5} (e : M ≃ₗ[R] N) (f : N ≃ₗ[R] P) (x : Orientation R M ι) : (map ι (e ≪≫ₗ f)) x = (map ι f) ((map ι e) x)

Transporting an orientation along a composite of linear equivalences is the same as transporting it along each in turn.

theorem Orientation.map_reindex {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_5} {ι' : Type u_6} (e : M ≃ₗ[R] N) (f : ι ≃ ι') (x : Orientation R M ι) : (map ι' e) ((reindex R M f) x) = (reindex R N f) ((map ι e) x)

Transporting an orientation along a linear equivalence commutes with reindexing its index type.

theorem Orientation.reindex_trans {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_5} {ι' : Type u_6} {ι'' : Type u_7} (e : ι ≃ ι') (e' : ι' ≃ ι'') (x : Orientation R M ι) : (reindex R M (e.trans e')) x = (reindex R M e') ((reindex R M e) x)

Reindexing an orientation along a composite of equivalences is the same as reindexing it along each in turn.

@[simp]

theorem Orientation.map_units_smul {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_5} (e : M ≃ₗ[R] N) (u : Rˣ) (x : Orientation R M ι) : (map ι e) (u • x) = u • (map ι e) x

Transporting an orientation along a linear equivalence commutes with scaling by a unit.

@[simp]

theorem Orientation.reindex_units_smul {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_5} {ι' : Type u_6} (e : ι ≃ ι') (u : Rˣ) (x : Orientation R M ι) : (reindex R M e) (u • x) = u • (reindex R M e) x

Reindexing an orientation commutes with scaling by a unit.

theorem Orientation.intCast_units_smul_eq_ite {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} (u : ℤˣ) (o : Orientation R M ι) : (Units.map ↑(Int.castRingHom R)) u • o = if u = 1 then o else -o

Integral unit signs act on orientations by retaining or reversing the ray.

theorem Orientation.intCast_units_smul_injective {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [IsDomain R] (o : Orientation R M ι) : Function.Injective fun (u : ℤˣ) => (Units.map ↑(Int.castRingHom R)) u • o

Distinct integral unit signs induce distinct orientations.

theorem Orientation.reindex_perm {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) (o : Orientation R M ι) : (reindex R M σ) o = (Units.map ↑(Int.castRingHom R)) (Equiv.Perm.sign σ) • o

Reindexing an orientation along a permutation of its index type multiplies it by the sign of the permutation.

theorem Orientation.map_eq_map_iff_det_mul_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 g : M ≃ₗ[R] M) (h : Fintype.card ι = Module.finrank R M) : (map ι f) x = (map ι g) x ↔ 0 < LinearMap.det ↑f * LinearMap.det ↑g

When the index type has cardinality equal to the finite dimension, two self-equivalences transport an orientation to the same orientation if and only if their determinants have the same sign.

theorem Orientation.map_eq_map_of_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] {N : Type u_4} [AddCommGroup N] [Module R N] (x : Orientation R M ι) (S T : M ≃ₗ[R] N) (h : Fintype.card ι = Module.finrank R M) (hdet : 0 < LinearMap.det ↑(S ≪≫ₗ T.symm)) : (map ι S) x = (map ι T) x

Two linear equivalences S and T such that S.trans T.symm has positive determinant transport an orientation to the same orientation.

theorem Orientation.map_units_smul_eq_iff_det_mul_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] (o : Orientation R M ι) (A : M ≃ₗ[R] M) (u v : Rˣ) (hι : Fintype.card ι = Module.finrank R M) : (map ι A) (u • o) = v • o ↔ 0 < ↑u * ↑v * LinearMap.det ↑A

The signed Jacobian criterion for transporting orientations with arbitrary unit scalars.

theorem Orientation.map_units_smul_eq_units_smul_map_iff_det_mul_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] {N : Type u_4} [AddCommGroup N] [Module R N] (o : Orientation R M ι) (A C : M ≃ₗ[R] N) (u v : Rˣ) (hι : Fintype.card ι = Module.finrank R M) : (map ι A) (u • o) = v • (map ι C) o ↔ 0 < ↑u * ↑v * LinearMap.det ↑(A ≪≫ₗ C.symm)

The signed Jacobian criterion for transporting orientations between two spaces: a linear equivalence A : M ≃ N carries u • o to v • C o, where C : M ≃ N is a reference equivalence, exactly when u v det (C⁻¹ ∘ A) is positive.

theorem Orientation.map_linearEquiv_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 : Orientation R M ι) (h : Fintype.card ι = Module.finrank R M) : (map ι (LinearEquiv.neg R)) x = (-1) ^ Module.finrank R M • x

Transport along the negation of a space of dimension n multiplies an orientation by (-1) ^ n.

theorem Orientation.intCast_units_smul_ite_eq {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] (model o : Orientation R M ι) (hι : Fintype.card ι = Module.finrank R M) : (Units.map ↑(Int.castRingHom R)) (if o = model then 1 else -1) • model = o

The sign distinguishing two orientations reconstructs the second from the first when the index type has the dimension of the space.