[Merged by Bors] - feat(linear_algebra/orientation): add orientation.reindex

src/linear_algebra/alternating.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2020 Zhangir Azerbayev. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser, Zhangir Azerbayev
@@ -581,6 +581,12 @@
  (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 @@
  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 :=

src/linear_algebra/determinant.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
@@ -559,6 +559,11 @@
  (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 :=

src/linear_algebra/orientation.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2021 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
@@ -43,7 +43,7 @@
 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 @@
 @[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 @@
  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 @@
  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 @@
  (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) :