From 0c1d80f5a86b36c1db32e021e8d19ae7809d5b79 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 28 Jul 2023 10:11:09 +0000
Subject: [PATCH] feat(linear_algebra/orientation): add `orientation.reindex`
 (#19236)

---
 src/linear_algebra/alternating.lean | 30 ++++++++++++++++++++++++
 src/linear_algebra/determinant.lean |  5 ++++
 src/linear_algebra/orientation.lean | 36 ++++++++++++++++++++++++++---
 3 files changed, 68 insertions(+), 3 deletions(-)

diff --git a/src/linear_algebra/alternating.lean b/src/linear_algebra/alternating.lean
index 0fa1eccdefb48..4f23645d2b111 100644
--- a/src/linear_algebra/alternating.lean
+++ b/src/linear_algebra/alternating.lean
@@ -581,6 +581,12 @@ rfl
   (f + g).dom_dom_congr σ = f.dom_dom_congr σ + g.dom_dom_congr σ :=
 rfl
 
+@[simp] lemma dom_dom_congr_smul {S : Type*}
+  [monoid S] [distrib_mul_action S N] [smul_comm_class R S N] (σ : ι ≃ ι') (c : S)
+  (f : alternating_map R M N ι) :
+  (c • f).dom_dom_congr σ = c • f.dom_dom_congr σ :=
+rfl
+
 /-- `alternating_map.dom_dom_congr` as an equivalence.
 
 This is declared separately because it does not work with dot notation. -/
@@ -593,6 +599,30 @@ def dom_dom_congr_equiv (σ : ι ≃ ι') :
   right_inv := λ m, by { ext, simp [function.comp] },
   map_add' := dom_dom_congr_add σ }
 
+section dom_dom_lcongr
+variables (S : Type*) [semiring S] [module S N] [smul_comm_class R S N]
+
+/-- `alternating_map.dom_dom_congr` as a linear equivalence. -/
+@[simps apply symm_apply]
+def dom_dom_lcongr (σ : ι ≃ ι') : alternating_map R M N ι ≃ₗ[S] alternating_map R M N ι' :=
+{ to_fun := dom_dom_congr σ,
+  inv_fun := dom_dom_congr σ.symm,
+  left_inv := λ f, by { ext, simp [function.comp] },
+  right_inv := λ m, by { ext, simp [function.comp] },
+  map_add' := dom_dom_congr_add σ,
+  map_smul' := dom_dom_congr_smul σ }
+
+@[simp] lemma dom_dom_lcongr_refl :
+  (dom_dom_lcongr S (equiv.refl ι) : alternating_map R M N ι ≃ₗ[S] alternating_map R M N ι) =
+    linear_equiv.refl _ _ :=
+linear_equiv.ext dom_dom_congr_refl
+
+@[simp] lemma dom_dom_lcongr_to_add_equiv (σ : ι ≃ ι') :
+  (dom_dom_lcongr S σ : alternating_map R M N ι ≃ₗ[S] alternating_map R M N ι').to_add_equiv
+    = dom_dom_congr_equiv σ := rfl
+
+end dom_dom_lcongr
+
 /-- The results of applying `dom_dom_congr` to two maps are equal if and only if those maps are. -/
 @[simp] lemma dom_dom_congr_eq_iff (σ : ι ≃ ι') (f g : alternating_map R M N ι) :
   f.dom_dom_congr σ = g.dom_dom_congr σ ↔ f = g :=
diff --git a/src/linear_algebra/determinant.lean b/src/linear_algebra/determinant.lean
index 80d805eccb482..c005163173ff9 100644
--- a/src/linear_algebra/determinant.lean
+++ b/src/linear_algebra/determinant.lean
@@ -559,6 +559,11 @@ lemma basis.det_reindex {ι' : Type*} [fintype ι'] [decidable_eq ι']
   (b.reindex e).det v = b.det (v ∘ e) :=
 by rw [basis.det_apply, basis.to_matrix_reindex', det_reindex_alg_equiv, basis.det_apply]
 
+lemma basis.det_reindex' {ι' : Type*} [fintype ι'] [decidable_eq ι']
+  (b : basis ι R M) (e : ι ≃ ι') :
+  (b.reindex e).det = b.det.dom_dom_congr e :=
+alternating_map.ext $ λ _, basis.det_reindex _ _ _
+
 lemma basis.det_reindex_symm {ι' : Type*} [fintype ι'] [decidable_eq ι']
   (b : basis ι R M) (v : ι → M) (e : ι' ≃ ι) :
   (b.reindex e.symm).det (v ∘ e) = b.det v :=
diff --git a/src/linear_algebra/orientation.lean b/src/linear_algebra/orientation.lean
index a17ec1101eba4..107bd5f34b839 100644
--- a/src/linear_algebra/orientation.lean
+++ b/src/linear_algebra/orientation.lean
@@ -43,7 +43,7 @@ section ordered_comm_semiring
 variables (R : Type*) [strict_ordered_comm_semiring R]
 variables (M : Type*) [add_comm_monoid M] [module R M]
 variables {N : Type*} [add_comm_monoid N] [module R N]
-variables (ι : Type*)
+variables (ι ι' : Type*)
 
 /-- An orientation of a module, intended to be used when `ι` is a `fintype` with the same
 cardinality as a basis. -/
@@ -73,6 +73,27 @@ by rw [orientation.map, alternating_map.dom_lcongr_refl, module.ray.map_refl]
 @[simp] lemma orientation.map_symm (e : M ≃ₗ[R] N) :
   (orientation.map ι e).symm = orientation.map ι e.symm := rfl
 
+section reindex
+variables (R M) {ι ι'}
+
+/-- An equivalence between indices implies an equivalence between orientations. -/
+def orientation.reindex (e : ι ≃ ι') : orientation R M ι ≃ orientation R M ι' :=
+module.ray.map $ alternating_map.dom_dom_lcongr R e
+
+@[simp] lemma orientation.reindex_apply (e : ι ≃ ι') (v : alternating_map R M R ι)
+  (hv : v ≠ 0) :
+  orientation.reindex R M e (ray_of_ne_zero _ v hv) = ray_of_ne_zero _ (v.dom_dom_congr e)
+      (mt (v.dom_dom_congr_eq_zero_iff e).mp hv) := rfl
+
+@[simp] lemma orientation.reindex_refl :
+  (orientation.reindex R M $ equiv.refl ι) = equiv.refl _ :=
+by rw [orientation.reindex, alternating_map.dom_dom_lcongr_refl, module.ray.map_refl]
+
+@[simp] lemma orientation.reindex_symm (e : ι ≃ ι') :
+  (orientation.reindex R M e).symm = orientation.reindex R M e.symm := rfl
+
+end reindex
+
 /-- A module is canonically oriented with respect to an empty index type. -/
 @[priority 100] instance is_empty.oriented [nontrivial R] [is_empty ι] :
   module.oriented R M ι :=
@@ -107,9 +128,14 @@ variables {M N : Type*} [add_comm_group M] [add_comm_group N] [module R M] [modu
   orientation.map ι f (-x) = - orientation.map ι f x :=
 module.ray.map_neg _ x
 
+@[simp] protected lemma orientation.reindex_neg {ι ι' : Type*} (e : ι ≃ ι')
+  (x : orientation R M ι) :
+  orientation.reindex R M e (-x) = - orientation.reindex R M e x :=
+module.ray.map_neg _ x
+
 namespace basis
 
-variables {ι : Type*}
+variables {ι ι' : Type*}
 
 /-- The value of `orientation.map` when the index type has the cardinality of a basis, in terms
 of `f.det`. -/
@@ -125,7 +151,7 @@ begin
       basis.det_self, mul_one, smul_eq_mul, mul_comm, mul_smul, linear_equiv.coe_inv_det],
 end
 
-variables [fintype ι] [decidable_eq ι]
+variables [fintype ι] [decidable_eq ι] [fintype ι'] [decidable_eq ι']
 
 /-- The orientation given by a basis. -/
 protected def orientation [nontrivial R] (e : basis ι R M) : orientation R M ι :=
@@ -135,6 +161,10 @@ 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']
 
+lemma orientation_reindex [nontrivial R] (e : basis ι R M)
+  (eι : ι ≃ ι') : (e.reindex eι).orientation = orientation.reindex R M eι e.orientation :=
+by simp_rw [basis.orientation, orientation.reindex_apply, basis.det_reindex']
+
 /-- The orientation given by a basis derived using `units_smul`, in terms of the product of those
 units. -/
 lemma orientation_units_smul [nontrivial R] (e : basis ι R M) (w : ι → units R) :