[Merged by Bors] - feat(linear_algebra/orientation): composing with linear equivs and determinant

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/linear_algebra/orientation.lean

@@ -351,6 +351,14 @@ 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] [is_domain R] (e : basis ι R M)
+  (f : M ≃ₗ[R] M) : (e.map f).orientation = (f.det)⁻¹ • e.orientation :=
+begin
+  simp_rw [basis.orientation, smul_ray_of_ne_zero, ray_eq_iff],
+  rw [(e.map f).det.eq_smul_basis_det e, e.det_map, ←linear_equiv.coe_coe, e.det_comp f.symm e,
+      e.det_self, mul_one, units.smul_def, linear_equiv.coe_inv_det],
+end
+
 end basis
 
 end ordered_comm_ring
@@ -369,6 +377,21 @@ begin
   exact same_ray_pos_smul_left _ hr,
 end
 
+/-- Scaling by an inverse unit is the same as scaling by itself. -/
+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]
 
@@ -460,6 +483,25 @@ 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, 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, units_inv_smul, units_smul_eq_neg_iff, linear_equiv.coe_det]
+
 end basis
 
 end linear_ordered_comm_ring
@@ -510,6 +552,49 @@ 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⟩
+
 end orientation
 
+namespace alternating_map
+
+variables [fintype ι] [finite_dimensional R M]
+
+open finite_dimensional
+
+/-- 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 orientation_comp_linear_equiv_eq_iff_det_pos (f : alternating_map R M R ι) (hf : f ≠ 0)
+  (g : M ≃ₗ[R] M) (h : fintype.card ι = finrank R M) :
+  ray_of_ne_zero R (f.comp_linear_map ↑g)
+                   ((not_iff_not.2 (f.comp_linear_equiv_eq_zero_iff g)).2 hf)
+    = ray_of_ne_zero R f hf ↔ 0 < (g : M →ₗ[R] M).det :=
+begin
+  have e := (fin_basis R M).reindex (fintype.equiv_fin_of_card_eq h).symm,
+  rw [ray_eq_iff, (f.comp_linear_map ↑g).eq_smul_basis_det e, f.eq_smul_basis_det e,
+      comp_linear_map_apply, smul_apply, basis.det_comp, basis.det_self, mul_one, smul_eq_mul,
+      mul_comm, mul_smul, ←f.eq_smul_basis_det e, same_ray_smul_left_iff hf (g : M →ₗ[R] M).det]
+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 negation of that orientation if and
+only if the determinant is negative. -/
+lemma orientation_comp_linear_equiv_eq_neg_iff_det_neg (f : alternating_map R M R ι) (hf : f ≠ 0)
+  (g : M ≃ₗ[R] M) (h : fintype.card ι = finrank R M) :
+  ray_of_ne_zero R (f.comp_linear_map ↑g)
+                   ((not_iff_not.2 (f.comp_linear_equiv_eq_zero_iff g)).2 hf)
+    = -ray_of_ne_zero R f hf ↔ (g : M →ₗ[R] M).det < 0 :=
+begin
+  rw [←orientation.ne_iff_eq_neg _ _ h, not_iff_comm,
+      orientation_comp_linear_equiv_eq_iff_det_pos _ _ _ h, not_lt],
+  exact (is_unit.ne_zero g.is_unit_det').symm.le_iff_lt
+end
+
+end alternating_map
+
 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]