feat(linear_algebra/{basis, determinant, orientation}): determinant o…

…f `adjust_to_orientation` of a basis (#16476)

Performing the operation `adjust_to_orientation` on a basis either preserves the determinant with respect to that basis, or negates it.

Formalized as part of the Sphere Eversion project.

src/linear_algebra/basis.lean

@@ -68,7 +68,7 @@ universe u
 open function set submodule
 open_locale classical big_operators
 
-variables {ι : Type*} {ι' : Type*} {R : Type*} {K : Type*}
+variables {ι : Type*} {ι' : Type*} {R : Type*} {R₂ : Type*} {K : Type*}
 variables {M : Type*} {M' M'' : Type*} {V : Type u} {V' : Type*}
 
 section module
@@ -859,8 +859,8 @@ section module
 open linear_map
 
 variables {v : ι → M}
-variables [ring R] [add_comm_group M] [add_comm_group M'] [add_comm_group M'']
-variables [module R M] [module R M'] [module R M'']
+variables [ring R] [comm_ring R₂] [add_comm_group M] [add_comm_group M'] [add_comm_group M'']
+variables [module R M] [module R₂ M] [module R M'] [module R M'']
 variables {c d : R} {x y : M}
 variables (b : basis ι R M)
 
@@ -1020,6 +1020,25 @@ lemma units_smul_apply {v : basis ι R M} {w : ι → Rˣ} (i : ι) :
 mk_apply
   (v.linear_independent.units_smul w) (units_smul_span_eq_top v.span_eq).ge i
 
+@[simp] lemma coord_units_smul (e : basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) :
+  (e.units_smul w).coord i = (w i)⁻¹ • e.coord i :=
+begin
+  apply e.ext,
+  intros j,
+  transitivity ((e.units_smul w).coord i) ((w j)⁻¹ • (e.units_smul w) j),
+  { congr,
+    simp [basis.units_smul, ← mul_smul], },
+  simp only [basis.coord_apply, linear_map.smul_apply, basis.repr_self, units.smul_def,
+    smul_hom_class.map_smul, finsupp.single_apply],
+  split_ifs with h h,
+  { simp [h] },
+  { simp }
+end
+
+@[simp] lemma repr_units_smul (e : basis ι R₂ M) (w : ι → R₂ˣ) (v : M) (i : ι) :
+  (e.units_smul w).repr v i = (w i)⁻¹ • e.repr v i :=
+congr_arg (λ f : M →ₗ[R₂] R₂, f v) (e.coord_units_smul w i)
+
 /-- A version of `smul_of_units` that uses `is_unit`. -/
 def is_unit_smul (v : basis ι R M) {w : ι → R} (hw : ∀ i, is_unit (w i)):
   basis ι R M :=

src/linear_algebra/determinant.lean

@@ -550,11 +550,24 @@ begin
     exact e.det.map_eq_zero_of_eq _ (by simp [hik, function.update_apply]) hik, },
 end
 
+/-- If a basis is multiplied columnwise by scalars `w : ι → Rˣ`, then the determinant with respect
+to this basis is multiplied by the product of the inverse of these scalars. -/
+lemma basis.det_units_smul (e : basis ι R M) (w : ι → Rˣ) :
+  (e.units_smul w).det = (↑(∏ i, w i)⁻¹ : R) • e.det :=
+begin
+  ext f,
+  change matrix.det (λ i j, (e.units_smul w).repr (f j) i)
+    = (↑(∏ i, w i)⁻¹ : R) • matrix.det (λ i j, e.repr (f j) i),
+  simp only [e.repr_units_smul],
+  convert matrix.det_mul_column (λ i, (↑((w i)⁻¹) : R)) (λ i j, e.repr (f j) i),
+  simp [← finset.prod_inv_distrib]
+end
+
 /-- The determinant of a basis constructed by `units_smul` is the product of the given units. -/
-@[simp] lemma basis.det_units_smul (w : ι → Rˣ) : e.det (e.units_smul w) = ∏ i, w i :=
+@[simp] lemma basis.det_units_smul_self (w : ι → Rˣ) : e.det (e.units_smul w) = ∏ i, w i :=
 by simp [basis.det_apply]
 
 /-- The determinant of a basis constructed by `is_unit_smul` is the product of the given units. -/
 @[simp] lemma basis.det_is_unit_smul {w : ι → R} (hw : ∀ i, is_unit (w i)) :
   e.det (e.is_unit_smul hw) = ∏ i, w i :=
-e.det_units_smul _
+e.det_units_smul_self _

src/linear_algebra/orientation.lean

@@ -108,7 +108,7 @@ lemma orientation_units_smul [nontrivial R] (e : basis ι R M) (w : ι → units
   (e.units_smul w).orientation = (∏ i, w i)⁻¹ • e.orientation :=
 begin
   rw [basis.orientation, basis.orientation, smul_ray_of_ne_zero, ray_eq_iff,
-      e.det.eq_smul_basis_det (e.units_smul w), det_units_smul, units.smul_def, smul_smul],
+      e.det.eq_smul_basis_det (e.units_smul w), det_units_smul_self, units.smul_def, smul_smul],
   norm_cast,
   simp
 end
@@ -207,6 +207,26 @@ begin
       simp [units_smul_apply, hi] }
 end
 
+lemma det_adjust_to_orientation [nontrivial R] [nonempty ι] (e : basis ι R M)
+  (x : orientation R M ι) :
+  (e.adjust_to_orientation x).det = e.det ∨ (e.adjust_to_orientation x).det = - e.det :=
+begin
+  dsimp [basis.adjust_to_orientation],
+  split_ifs,
+  { left,
+    refl },
+  { right,
+    simp [e.det_units_smul, ← units.coe_prod, finset.prod_update_of_mem] }
+end
+
+@[simp] lemma abs_det_adjust_to_orientation [nontrivial R] [nonempty ι] (e : basis ι R M)
+  (x : orientation R M ι) (v : ι → M) :
+  |(e.adjust_to_orientation x).det v| = |e.det v| :=
+begin
+  cases e.det_adjust_to_orientation x with h h;
+  simp [h]
+end
+
 end basis
 
 end linear_ordered_comm_ring