feat(linear_algebra/orientation): add orientation.reindex (#6889)

This forward-ports leanprover-community/mathlib#19236

Mathlib/LinearAlgebra/Alternating.lean

@@ -10,7 +10,7 @@ import Mathlib.LinearAlgebra.LinearIndependent
 import Mathlib.LinearAlgebra.Multilinear.Basis
 import Mathlib.LinearAlgebra.Multilinear.TensorProduct
 
-#align_import linear_algebra.alternating from "leanprover-community/mathlib"@"bd65478311e4dfd41f48bf38c7e3b02fb75d0163"
+#align_import linear_algebra.alternating from "leanprover-community/mathlib"@"0c1d80f5a86b36c1db32e021e8d19ae7809d5b79"
 
 /-!
 # Alternating Maps
@@ -759,6 +759,13 @@ theorem domDomCongr_add (σ : ι ≃ ι') (f g : AlternatingMap R M N ι) :
   rfl
 #align alternating_map.dom_dom_congr_add AlternatingMap.domDomCongr_add
 
+@[simp]
+theorem domDomCongr_smul {S : Type*} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N]
+    (σ : ι ≃ ι') (c : S) (f : AlternatingMap R M N ι) :
+    (c • f).domDomCongr σ = c • f.domDomCongr σ :=
+  rfl
+#align alternating_map.dom_dom_congr_smul AlternatingMap.domDomCongr_smul
+
 /-- `AlternatingMap.domDomCongr` as an equivalence.
 
 This is declared separately because it does not work with dot notation. -/
@@ -777,6 +784,38 @@ def domDomCongrEquiv (σ : ι ≃ ι') : AlternatingMap R M N ι ≃+ Alternatin
 #align alternating_map.dom_dom_congr_equiv_apply AlternatingMap.domDomCongrEquiv_apply
 #align alternating_map.dom_dom_congr_equiv_symm_apply AlternatingMap.domDomCongrEquiv_symm_apply
 
+section DomDomLcongr
+
+variable (S : Type*) [Semiring S] [Module S N] [SMulCommClass R S N]
+
+/-- `alternating_map.dom_dom_congr` as a linear equivalence. -/
+@[simps apply symm_apply]
+def domDomLcongr (σ : ι ≃ ι') : AlternatingMap R M N ι ≃ₗ[S] AlternatingMap R M N ι'
+    where
+  toFun := domDomCongr σ
+  invFun := domDomCongr σ.symm
+  left_inv f := by ext; simp [Function.comp]
+  right_inv m := by ext; simp [Function.comp]
+  map_add' := domDomCongr_add σ
+  map_smul' := domDomCongr_smul σ
+#align alternating_map.dom_dom_lcongr AlternatingMap.domDomLcongr
+
+@[simp]
+theorem domDomLcongr_refl :
+    (domDomLcongr S (Equiv.refl ι) : AlternatingMap R M N ι ≃ₗ[S] AlternatingMap R M N ι) =
+      LinearEquiv.refl _ _ :=
+  LinearEquiv.ext domDomCongr_refl
+#align alternating_map.dom_dom_lcongr_refl AlternatingMap.domDomLcongr_refl
+
+@[simp]
+theorem domDomLcongr_toAddEquiv (σ : ι ≃ ι') :
+    (↑(domDomLcongr S σ : AlternatingMap R M N ι ≃ₗ[S] _) : AlternatingMap R M N ι ≃+ _) =
+      domDomCongrEquiv σ :=
+  rfl
+#align alternating_map.dom_dom_lcongr_to_add_equiv AlternatingMap.domDomLcongr_toAddEquiv
+
+end DomDomLcongr
+
 /-- The results of applying `domDomCongr` to two maps are equal if and only if those maps are. -/
 @[simp]
 theorem domDomCongr_eq_iff (σ : ι ≃ ι') (f g : AlternatingMap R M N ι) :

Mathlib/LinearAlgebra/Determinant.lean

@@ -10,7 +10,7 @@ import Mathlib.Tactic.FieldSimp
 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
 import Mathlib.LinearAlgebra.Matrix.Basis
 
-#align_import linear_algebra.determinant from "leanprover-community/mathlib"@"bd65478311e4dfd41f48bf38c7e3b02fb75d0163"
+#align_import linear_algebra.determinant from "leanprover-community/mathlib"@"0c1d80f5a86b36c1db32e021e8d19ae7809d5b79"
 
 /-!
 # Determinant of families of vectors
@@ -616,6 +616,11 @@ theorem Basis.det_reindex {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Bas
   rw [Basis.det_apply, Basis.toMatrix_reindex', det_reindexAlgEquiv, Basis.det_apply]
 #align basis.det_reindex Basis.det_reindex
 
+theorem Basis.det_reindex' {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M)
+    (e : ι ≃ ι') : (b.reindex e).det = b.det.domDomCongr e :=
+  AlternatingMap.ext fun _ => Basis.det_reindex _ _ _
+#align basis.det_reindex' Basis.det_reindex'
+
 theorem Basis.det_reindex_symm {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M)
     (v : ι → M) (e : ι' ≃ ι) : (b.reindex e.symm).det (v ∘ e) = b.det v := by
   rw [Basis.det_reindex, Function.comp.assoc, e.self_comp_symm, Function.comp.right_id]

Mathlib/LinearAlgebra/Orientation.lean

@@ -6,7 +6,7 @@ Authors: Joseph Myers
 import Mathlib.LinearAlgebra.Ray
 import Mathlib.LinearAlgebra.Determinant
 
-#align_import linear_algebra.orientation from "leanprover-community/mathlib"@"ce11c3c2a285bbe6937e26d9792fda4e51f3fe1a"
+#align_import linear_algebra.orientation from "leanprover-community/mathlib"@"0c1d80f5a86b36c1db32e021e8d19ae7809d5b79"
 
 /-!
 # Orientations of modules
@@ -46,7 +46,7 @@ variable (M : Type*) [AddCommMonoid M] [Module R M]
 
 variable {N : Type*} [AddCommMonoid N] [Module R N]
 
-variable (ι : Type*)
+variable (ι ι' : Type*)
 
 /-- An orientation of a module, intended to be used when `ι` is a `Fintype` with the same
 cardinality as a basis. -/
@@ -85,6 +85,35 @@ theorem Orientation.map_symm (e : M ≃ₗ[R] N) :
     (Orientation.map ι e).symm = Orientation.map ι e.symm := rfl
 #align orientation.map_symm Orientation.map_symm
 
+section Reindex
+
+variable (R M) {ι ι'}
+
+/-- An equivalence between indices implies an equivalence between orientations. -/
+def Orientation.reindex (e : ι ≃ ι') : Orientation R M ι ≃ Orientation R M ι' :=
+  Module.Ray.map <| AlternatingMap.domDomLcongr R e
+#align orientation.reindex Orientation.reindex
+
+@[simp]
+theorem Orientation.reindex_apply (e : ι ≃ ι') (v : AlternatingMap R M R ι) (hv : v ≠ 0) :
+    Orientation.reindex R M e (rayOfNeZero _ v hv) =
+      rayOfNeZero _ (v.domDomCongr e) (mt (v.domDomCongr_eq_zero_iff e).mp hv) :=
+  rfl
+#align orientation.reindex_apply Orientation.reindex_apply
+
+@[simp]
+theorem Orientation.reindex_refl : (Orientation.reindex R M <| Equiv.refl ι) = Equiv.refl _ := by
+  rw [Orientation.reindex, AlternatingMap.domDomLcongr_refl, Module.Ray.map_refl]
+#align orientation.reindex_refl Orientation.reindex_refl
+
+@[simp]
+theorem Orientation.reindex_symm (e : ι ≃ ι') :
+    (Orientation.reindex R M e).symm = Orientation.reindex R M e.symm :=
+  rfl
+#align orientation.reindex_symm Orientation.reindex_symm
+
+end Reindex
+
 /-- A module is canonically oriented with respect to an empty index type. -/
 instance (priority := 100) IsEmpty.oriented [Nontrivial R] [IsEmpty ι] : Module.Oriented R M ι
     where positiveOrientation :=
@@ -123,9 +152,15 @@ protected theorem Orientation.map_neg {ι : Type*} (f : M ≃ₗ[R] N) (x : Orie
   Module.Ray.map_neg _ x
 #align orientation.map_neg Orientation.map_neg
 
+@[simp]
+protected theorem 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
+#align orientation.reindex_neg Orientation.reindex_neg
+
 namespace Basis
 
-variable {ι : Type*}
+variable {ι ι' : Type*}
 
 /-- The value of `Orientation.map` when the index type has the cardinality of a basis, in terms
 of `f.det`. -/
@@ -142,7 +177,7 @@ theorem map_orientation_eq_det_inv_smul [Finite ι] (e : Basis ι R M) (x : Orie
     LinearEquiv.coe_inv_det]
 #align basis.map_orientation_eq_det_inv_smul Basis.map_orientation_eq_det_inv_smul
 
-variable [Fintype ι] [DecidableEq ι]
+variable [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι']
 
 /-- The orientation given by a basis. -/
 protected def orientation [Nontrivial R] (e : Basis ι R M) : Orientation R M ι :=
@@ -154,6 +189,11 @@ theorem orientation_map [Nontrivial R] (e : Basis ι R M) (f : M ≃ₗ[R] N) :
   simp_rw [Basis.orientation, Orientation.map_apply, Basis.det_map']
 #align basis.orientation_map Basis.orientation_map
 
+theorem 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']
+#align basis.orientation_reindex Basis.orientation_reindex
+
 /-- The orientation given by a basis derived using `units_smul`, in terms of the product of those
 units. -/
 theorem orientation_unitsSMul [Nontrivial R] (e : Basis ι R M) (w : ι → Units R) :