feat(linear_algebra): lemmas on associatedness of determinants of lin…

…ear maps (#15587)

`det f` equals `det f'` up to units if `f'` is `f` composed with a linear equiv.

First a homogeneous form where `f f' : M → M`, then a heterogeneous form where `f f' : M → N` and the equivs `e e' : N → M`.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/linear_algebra/determinant.lean

@@ -409,6 +409,25 @@ have is_unit (linear_map.to_matrix (finite_dimensional.fin_basis 𝕜 M)
     by simp only [linear_map.det_to_matrix, is_unit_iff_ne_zero.2 hf],
 linear_equiv.of_is_unit_det this
 
+lemma linear_map.associated_det_of_eq_comp (e : M ≃ₗ[R] M) (f f' : M →ₗ[R] M)
+  (h : ∀ x, f x = f' (e x)) : associated f.det f'.det :=
+begin
+  suffices : associated (f' ∘ₗ ↑e).det f'.det,
+  { convert this using 2, ext x, exact h x },
+  rw [← mul_one f'.det, linear_map.det_comp],
+  exact associated.mul_left _ (associated_one_iff_is_unit.mpr e.is_unit_det')
+end
+
+lemma linear_map.associated_det_comp_equiv {N : Type*} [add_comm_group N] [module R N]
+  (f : N →ₗ[R] M) (e e' : M ≃ₗ[R] N) :
+  associated (f ∘ₗ ↑e).det (f ∘ₗ ↑e').det :=
+begin
+  refine linear_map.associated_det_of_eq_comp (e.trans e'.symm) _ _ _,
+  intro x,
+  simp only [linear_map.comp_apply, linear_equiv.coe_coe, linear_equiv.trans_apply,
+             linear_equiv.apply_symm_apply],
+end
+
 /-- The determinant of a family of vectors with respect to some basis, as an alternating
 multilinear map. -/
 def basis.det : alternating_map R M R ι :=