feat(linear_algebra/orientation): composing with linear equivs and de…

…terminant (#10737)

Add lemmas that composing an alternating map with a linear equiv using
`comp_linear_map`, or composing a basis with a linear equiv using
`basis.map`, produces the same orientation if and only if the
determinant of that linear equiv is positive.





Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/order/ring.lean

@@ -760,6 +760,16 @@ def function.injective.linear_ordered_semiring {β : Type*}
   .. pullback_nonzero f zero one,
   .. hf.ordered_semiring f zero one add mul }
 
+@[simp] lemma units.inv_pos {u : units α} : (0 : α) < ↑u⁻¹ ↔ (0 : α) < u :=
+have ∀ {u : units α}, (0 : α) < u → (0 : α) < ↑u⁻¹ := λ u h,
+  (zero_lt_mul_left h).mp $ u.mul_inv.symm ▸ zero_lt_one,
+⟨this, this⟩
+
+@[simp] lemma units.inv_neg {u : units α} : ↑u⁻¹ < (0 : α) ↔ ↑u < (0 : α) :=
+have ∀ {u : units α}, ↑u < (0 : α) → ↑u⁻¹ < (0 : α) := λ u h,
+  neg_of_mul_pos_left (by exact (u.mul_inv.symm ▸ zero_lt_one)) h.le,
+⟨this, this⟩
+
 end linear_ordered_semiring
 
 section mono

src/analysis/normed_space/units.lean

@@ -70,7 +70,7 @@ begin
   nontriviality R,
   apply metric.is_open_iff.mpr,
   rintros x' ⟨x, rfl⟩,
-  refine ⟨∥(↑x⁻¹ : R)∥⁻¹, inv_pos.mpr (units.norm_pos x⁻¹), _⟩,
+  refine ⟨∥(↑x⁻¹ : R)∥⁻¹, _root_.inv_pos.mpr (units.norm_pos x⁻¹), _⟩,
   intros y hy,
   rw [metric.mem_ball, dist_eq_norm] at hy,
   exact (x.unit_of_nearby y hy).is_unit

src/linear_algebra/determinant.lean

@@ -486,6 +486,10 @@ lemma basis.det_map (b : basis ι R M) (f : M ≃ₗ[R] M') (v : ι → M') :
   (b.map f).det v = b.det (f.symm ∘ v) :=
 by { rw [basis.det_apply, basis.to_matrix_map, basis.det_apply] }
 
+lemma basis.det_map' (b : basis ι R M) (f : M ≃ₗ[R] M') :
+  (b.map f).det = b.det.comp_linear_map f.symm :=
+alternating_map.ext $ b.det_map f
+
 @[simp] lemma pi.basis_fun_det : (pi.basis_fun R ι).det = matrix.det_row_alternating :=
 begin
   ext M,

src/linear_algebra/orientation.lean

@@ -276,7 +276,7 @@ section ordered_comm_ring
 local attribute [instance] ray_vector.same_ray_setoid
 
 variables {R : Type*} [ordered_comm_ring R]
-variables {M : Type*} [add_comm_group M] [module R M]
+variables {M N : Type*} [add_comm_group M] [add_comm_group N] [module R M] [module R N]
 
 /-- If two vectors are in the same ray, so are their negations. -/
 lemma same_ray.neg {v₁ v₂ : M} : same_ray R v₁ v₂ → same_ray R (-v₁) (-v₂) :=
@@ -367,8 +367,26 @@ variables {R} {ι : Type*} [fintype ι] [decidable_eq ι]
 protected def orientation [nontrivial R] (e : basis ι R M) : orientation R M ι :=
 ray_of_ne_zero R _ e.det_ne_zero
 
+lemma orientation_map [nontrivial R] (e : basis ι R M)
+  (f : M ≃ₗ[R] N) : (e.map f).orientation = orientation.map ι f e.orientation :=
+by simp_rw [basis.orientation, orientation.map_apply, basis.det_map']
+
+/-- The value of `orientation.map` when the index type has the cardinality of a basis, in terms
+of `f.det`. -/
+lemma map_orientation_eq_det_inv_smul [nontrivial R] [is_domain R] (e : basis ι R M)
+  (x : orientation R M ι) (f : M ≃ₗ[R] M) : orientation.map ι f x = (f.det)⁻¹ • x :=
+begin
+  induction x using module.ray.ind with g hg,
+  rw [orientation.map_apply, smul_ray_of_ne_zero, ray_eq_iff, units.smul_def,
+      (g.comp_linear_map ↑f.symm).eq_smul_basis_det e, g.eq_smul_basis_det e,
+      alternating_map.comp_linear_map_apply, alternating_map.smul_apply, basis.det_comp,
+      basis.det_self, mul_one, smul_eq_mul, mul_comm, mul_smul, linear_equiv.coe_inv_det],
+end
+
 end basis
 
+variables {R} {ι : Type*} [fintype ι] [decidable_eq ι]
+
 end ordered_comm_ring
 
 section linear_ordered_comm_ring
@@ -385,6 +403,21 @@ begin
   exact same_ray_pos_smul_left _ hr,
 end
 
+/-- Scaling by an inverse unit is the same as scaling by itself. -/
+@[simp] lemma units_inv_smul (u : units R) (v : module.ray R M) :
+  u⁻¹ • v = u • v :=
+begin
+  induction v using module.ray.ind with v hv,
+  rw [smul_ray_of_ne_zero, smul_ray_of_ne_zero, ray_eq_iff],
+  have : ∀ {u : units R}, 0 < (u : R) → same_ray R (u⁻¹ • v) (u • v) :=
+    λ u h, ((same_ray.refl v).pos_smul_left $ units.inv_pos.mpr h).pos_smul_right h,
+  cases lt_or_lt_iff_ne.2 u.ne_zero,
+  { rw [←units.neg_neg u, units.neg_inv, (- u).neg_smul, units.neg_smul],
+    refine (this _).neg,
+    exact neg_pos_of_neg h },
+  { exact this h, },
+end
+
 section
 variables [no_zero_smul_divisors R M]
 
@@ -476,6 +509,27 @@ begin
   exact hx
 end
 
+/-- 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. -/
+lemma orientation_ne_iff_eq_neg (e : basis ι R M) (x : orientation R M ι) :
+  x ≠ e.orientation ↔ x = -e.orientation :=
+⟨λ h, (e.orientation_eq_or_eq_neg x).resolve_left h,
+ λ h, h.symm ▸ (module.ray.ne_neg_self e.orientation).symm⟩
+
+/-- Composing a basis with a linear equiv gives the same orientation if and only if the
+determinant is positive. -/
+lemma orientation_comp_linear_equiv_eq_iff_det_pos (e : basis ι R M) (f : M ≃ₗ[R] M) :
+  (e.map f).orientation = e.orientation ↔ 0 < (f : M →ₗ[R] M).det :=
+by rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_self_iff,
+  linear_equiv.coe_det]
+
+/-- Composing a basis with a linear equiv gives the negation of that orientation if and only if
+the determinant is negative. -/
+lemma orientation_comp_linear_equiv_eq_neg_iff_det_neg (e : basis ι R M) (f : M ≃ₗ[R] M) :
+  (e.map f).orientation = -e.orientation ↔ (f : M →ₗ[R] M).det < 0 :=
+by rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_neg_iff,
+  linear_equiv.coe_det]
+
 end basis
 
 end linear_ordered_comm_ring
@@ -526,6 +580,38 @@ begin
     simp [h₁, h₂]
 end
 
+/-- 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. -/
+lemma ne_iff_eq_neg (x₁ x₂ : orientation R M ι) (h : fintype.card ι = finrank R M) :
+  x₁ ≠ x₂ ↔ x₁ = -x₂ :=
+⟨λ hn, (eq_or_eq_neg x₁ x₂ h).resolve_left hn, λ he, he.symm ▸ (module.ray.ne_neg_self x₂).symm⟩
+
+/-- The value of `orientation.map` when the index type has cardinality equal to the finite
+dimension, in terms of `f.det`. -/
+lemma map_eq_det_inv_smul (x : orientation R M ι) (f : M ≃ₗ[R] M)
+  (h : fintype.card ι = finrank R M) :
+  orientation.map ι f x = (f.det)⁻¹ • x :=
+begin
+  have e := (fin_basis R M).reindex (fintype.equiv_fin_of_card_eq h).symm,
+  exact e.map_orientation_eq_det_inv_smul x f
+end
+
+/-- 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. -/
+lemma map_eq_iff_det_pos (x : orientation R M ι) (f : M ≃ₗ[R] M)
+  (h : fintype.card ι = finrank R M) :
+  orientation.map ι f x = x ↔  0 < (f : M →ₗ[R] M).det :=
+by rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_self_iff, linear_equiv.coe_det]
+
+/-- 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. -/
+lemma map_eq_neg_iff_det_neg (x : orientation R M ι) (f : M ≃ₗ[R] M)
+  (h : fintype.card ι = finrank R M) :
+  orientation.map ι f x = -x ↔ (f : M →ₗ[R] M).det < 0 :=
+by rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_neg_iff, linear_equiv.coe_det]
+
 end orientation
 
 end linear_ordered_field

src/ring_theory/subring/basic.lean

@@ -1003,7 +1003,7 @@ end actions
 def units.pos_subgroup (R : Type*) [linear_ordered_semiring R] :
   subgroup (units R) :=
 { carrier := {x | (0 : R) < x},
-  inv_mem' := λ x (hx : (0 : R) < x), (zero_lt_mul_left hx).mp $ x.mul_inv.symm ▸ zero_lt_one,
+  inv_mem' := λ x, units.inv_pos.mpr,
   ..(pos_submonoid R).comap (units.coe_hom R)}
 
 @[simp] lemma units.mem_pos_subgroup {R : Type*} [linear_ordered_semiring R]