feat(LinearAlgebra/Transvection): auxiliary lemmas to compute the determinant of transvection in a module (leanprover-community#31138)

Auxiliary results towards the proof that the determinant of a transvection is equal to 1.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: 2 people

Mathlib/LinearAlgebra/Determinant.lean

@@ -312,6 +312,13 @@ lemma isUnit_iff_isUnit_det [Module.Finite R M] [Module.Free R M] (f : M →ₗ[
   let b := Module.Free.chooseBasis R M
   rw [← isUnit_toMatrix_iff b, ← det_toMatrix b, Matrix.isUnit_iff_isUnit_det (toMatrix b b f)]
 
+/-- If a linear map has determinant different from `1`, then the module is free. -/
+theorem free_of_det_ne_one {f : M →ₗ[R] M} (hf : f.det ≠ 1) : Module.Free R M := by
+  by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
+  · rcases H with ⟨s, ⟨hs⟩⟩
+    exact Module.Free.of_basis hs
+  · classical simp [LinearMap.coe_det, H] at hf
+
 /-- If a linear map has determinant different from `1`, then the space is finite-dimensional. -/
 theorem finite_of_det_ne_one {f : M →ₗ[R] M} (hf : f.det ≠ 1) : Module.Finite R M := by
   by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)

Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

@@ -237,6 +237,28 @@ lemma finsuppScalarRight_symm_apply_single (i : ι) (m : M) :
       m ⊗ₜ[R] (Finsupp.single i 1) := by
   simp [finsuppScalarRight, finsuppRight_symm_apply_single]
 
+theorem finsuppScalarRight_smul (s : S) (t) :
+    finsuppScalarRight R M ι (s • t) = s • finsuppScalarRight R M ι t := by
+  induction t using TensorProduct.induction_on with
+  | zero => simp
+  | add x y hx hy => simp [hx, hy]
+  | tmul m x =>
+    simp only [smul_tmul', finsuppScalarRight_apply_tmul, Finsupp.smul_sum]
+    congr
+    ext i n j
+    simp [smul_comm n s m]
+
+variable (R S M ι) in
+/-- When `M` is also an `S`-module, `TensorProduct.finsuppScalarRight R M ι` is `S`-linear. -/
+noncomputable def finsuppScalarRight' :
+    M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M where
+  toAddEquiv := finsuppScalarRight R M ι
+  map_smul' s x := finsuppScalarRight_smul s x
+
+theorem coe_finsuppScalarRight' :
+    ⇑(finsuppScalarRight' R M ι S) = finsuppScalarRight R M ι :=
+  rfl
+
 end TensorProduct
 
 end TensorProduct

Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

@@ -136,6 +136,11 @@ theorem range_linearCombination : LinearMap.range (linearCombination R v) = span
     use single i 1
     simp [hi]
 
+theorem _root_.span_range_eq_top_iff_surjective_finsuppLinearCombination :
+    Submodule.span R (Set.range v) = ⊤ ↔
+      Function.Surjective (Finsupp.linearCombination R v) := by
+  rw [← LinearMap.range_eq_top, range_linearCombination]
+
 theorem lmapDomain_linearCombination (f : α → α') (g : M →ₗ[R] M') (h : ∀ i, g (v i) = v' (f i)) :
     (linearCombination R v').comp (lmapDomain R R f) = g.comp (linearCombination R v) := by
   ext l
@@ -340,6 +345,11 @@ theorem Fintype.range_linearCombination :
   rw [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearMap.range_comp,
       LinearEquiv.range, Submodule.map_top, Finsupp.range_linearCombination]
 
+theorem span_range_eq_top_iff_surjective_fintypeLinearCombination :
+    Submodule.span R (Set.range v) = ⊤ ↔
+      Function.Surjective (Fintype.linearCombination R v) := by
+  rw [← LinearMap.range_eq_top, Fintype.range_linearCombination]
+
 /-- `Fintype.bilinearCombination R S v f` is the linear combination of vectors in `v` with weights
 in `f`. This variant of `Finsupp.linearCombination` is defined on fintype indexed vectors.
 

Mathlib/LinearAlgebra/SpecialLinearGroup.lean

@@ -57,6 +57,7 @@ theorem det_eq_one (u : SpecialLinearGroup R V) :
     LinearMap.det (u : V →ₗ[R] V) = 1 := by
   simp [← LinearEquiv.coe_det, u.prop]
 
+/-- The coercion from `SpecialLinearGroup R V` to the function type `V → V` -/
 instance : CoeFun (SpecialLinearGroup R V) (fun _ ↦ V → V) where
   coe u x := u.val x
 
@@ -69,6 +70,7 @@ theorem ext (u v : SpecialLinearGroup R V) : (∀ x, u x = v x) → u = v :=
 
 section rankOne
 
+/-- If a free module has `Module.finrank` equal to `1`, then its special linear group is trivial. -/
 theorem subsingleton_of_finrank_eq_one [Module.Free R V] (d1 : Module.finrank R V = 1) :
     Subsingleton (SpecialLinearGroup R V) where
   allEq u v := by
@@ -167,6 +169,7 @@ theorem coe_dualMap
 
 end CoeLemmas
 
+/-- The special linear group of a module is a group. -/
 instance : Group (SpecialLinearGroup R V) := fast_instance%
   Function.Injective.group _ Subtype.coe_injective coe_one coe_mul coe_inv coe_div coe_pow coe_zpow
 
@@ -176,18 +179,21 @@ def toLinearEquiv : SpecialLinearGroup R V →* V ≃ₗ[R] V where
   map_one' := coe_one
   map_mul' := coe_mul
 
-theorem toLinearEquiv_apply (A : SpecialLinearGroup R V) (v : V) :
+@[simp] lemma toLinearEquiv_apply (A : SpecialLinearGroup R V) (v : V) :
     A.toLinearEquiv v = A v :=
   rfl
 
+@[simp]
 theorem toLinearEquiv_to_linearMap (A : SpecialLinearGroup R V) :
     (SpecialLinearGroup.toLinearEquiv A) = (A : V →ₗ[R] V) :=
   rfl
 
+@[simp]
 theorem toLinearEquiv_symm_apply (A : SpecialLinearGroup R V) (v : V) :
     A.toLinearEquiv.symm v = A⁻¹ v :=
   rfl
 
+@[simp]
 theorem toLinearEquiv_symm_to_linearMap (A : SpecialLinearGroup R V) :
     A.toLinearEquiv.symm = ((A⁻¹ : SpecialLinearGroup R V) : V →ₗ[R] V) :=
   rfl

Mathlib/LinearAlgebra/Transvection.lean

@@ -3,11 +3,14 @@ Copyright (c) 2025 Antoine Chambert-Loir. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir
 -/
+
 module
 
+public import Mathlib.LinearAlgebra.Charpoly.BaseChange
 public import Mathlib.LinearAlgebra.DFinsupp
 public import Mathlib.LinearAlgebra.Dual.BaseChange
 public import Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
+public import Mathlib.RingTheory.TensorProduct.IsBaseChangePi
 
 /-!
 # Transvections in a module
@@ -16,62 +19,93 @@ public import Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
   `LinearMap.transvection f v` is the linear map given by `x ↦ x + f x • v`,
 
 * If, moreover, `f v = 0`, then `LinearEquiv.transvection` shows that it is
-  a linear equivalence.
+ a linear equivalence.
+
+## Note on terminology
+
+In the mathematical litterature, linear maps of the form `LinearMap.transvection f v`
+are only called “transvections” when `f v = 0`. Otherwise, they are sometimes
+called “dilations” (especially if `f v ≠ -1`).
+
+The definition is almost the same as that of `Module.preReflection f v`,
+up to a sign change, which are interesting when `f v = 2`, because they give “reflections”.
 
 -/
 
 @[expose] public section
 
 namespace LinearMap
 
+open Module
+
 variable {R V : Type*} [CommSemiring R] [AddCommMonoid V] [Module R V]
 
 /-- The transvection associated with a linear form `f` and a vector `v`.
 
-NB. It is only a transvection when `f v = 0`. See also `Module.preReflection`. -/
-def transvection (f : Module.Dual R V) (v : V) : V →ₗ[R] V where
+NB. In mathematics, these linear maps are only called “transvections” when `f v = 0`.
+See also `Module.preReflection` for a similar definition, up to a sign. -/
+def transvection (f : Dual R V) (v : V) : V →ₗ[R] V where
   toFun x := x + f x • v
   map_add' x y := by simp only [map_add]; module
   map_smul' r x := by simp only [map_smul, RingHom.id_apply, smul_eq_mul]; module
 
 namespace transvection
 
-theorem apply (f : Module.Dual R V) (v x : V) :
+theorem apply (f : Dual R V) (v x : V) :
     transvection f v x = x + f x • v :=
   rfl
 
-theorem comp_of_left_eq_apply {f : Module.Dual R V} {v w : V} {x : V} (hw : f w = 0) :
+theorem comp_of_left_eq_apply {f : Dual R V} {v w : V} {x : V} (hw : f w = 0) :
     transvection f v (transvection f w x) = transvection f (v + w) x := by
   simp only [transvection, coe_mk, AddHom.coe_mk, map_add, map_smul, hw, smul_add]
   module
 
-theorem comp_of_left_eq {f : Module.Dual R V} {v w : V} (hw : f w = 0) :
+theorem comp_of_left_eq {f : Dual R V} {v w : V} (hw : f w = 0) :
     (transvection f v) ∘ₗ (transvection f w) = transvection f (v + w) := by
   ext; simp [comp_of_left_eq_apply hw]
 
-theorem comp_of_right_eq_apply {f g : Module.Dual R V} {v : V} {x : V} (hf : f v = 0) :
+theorem comp_of_right_eq_apply {f g : Dual R V} {v : V} {x : V} (hf : f v = 0) :
     (transvection f v) (transvection g v x) = transvection (f + g) v x := by
   simp only [transvection, coe_mk, AddHom.coe_mk, map_add, map_smul, hf, add_apply]
   module
 
-theorem comp_of_right_eq {f g : Module.Dual R V} {v : V} (hf : f v = 0) :
+theorem comp_of_right_eq {f g : Dual R V} {v : V} (hf : f v = 0) :
     (transvection f v) ∘ₗ (transvection g v) = transvection (f + g) v := by
   ext; simp [comp_of_right_eq_apply hf]
 
 @[simp]
 theorem of_left_eq_zero (v : V) :
-    transvection (0 : Module.Dual R V) v = LinearMap.id := by
+    transvection (0 : Dual R V) v = LinearMap.id := by
   ext
   simp [transvection]
 
 @[simp]
-theorem of_right_eq_zero (f : Module.Dual R V) :
+theorem of_right_eq_zero (f : Dual R V) :
     transvection f 0 = LinearMap.id := by
   ext
   simp [transvection]
 
+theorem eq_id_of_finrank_le_one
+    [Free R V] [Module.Finite R V] [StrongRankCondition R]
+    {f : Dual R V} {v : V} (hfv : f v = 0) (h1 : finrank R V ≤ 1) :
+    transvection f v = LinearMap.id := by
+  let b := finBasis R V
+  rcases (by lia : finrank R V = 0 ∨ finrank R V = 1) with h0 | h1
+  · have : Subsingleton V := (finrank_eq_zero_iff_of_free R V).mp h0
+    simp [Subsingleton.eq_zero v]
+  · ext x
+    suffices f x • v = 0 by
+      simp [apply, this]
+    let i : Fin (finrank R V) := ⟨0, by simp [h1]⟩
+    suffices ∀ x, x = b.repr x i • (b i) by
+      rw [this v, map_smul, smul_eq_mul, mul_comm] at hfv
+      rw [this x, this v, map_smul, smul_eq_mul, ← mul_smul, mul_assoc, hfv, mul_zero, zero_smul]
+    intro x
+    have : x = ∑ i, b.repr x i • b i := (Basis.sum_equivFun b x).symm
+    rwa [Finset.sum_eq_single_of_mem i (Finset.mem_univ i) (by grind)] at this
+
 theorem congr {W : Type*} [AddCommMonoid W] [Module R W]
-    (f : Module.Dual R V) (v : V) (e : V ≃ₗ[R] W) :
+    (f : Dual R V) (v : V) (e : V ≃ₗ[R] W) :
     e ∘ₗ (transvection f v) ∘ₗ e.symm = transvection (f ∘ₗ e.symm) (e v) := by
   ext; simp [transvection.apply]
 
@@ -81,10 +115,10 @@ variable {R V : Type*} [CommRing R] [AddCommGroup V] [Module R V]
 
 namespace LinearEquiv
 
-open LinearMap LinearMap.transvection
+open LinearMap LinearMap.transvection Module
 
 /-- The transvection associated with a linear form `f` and a vector `v` such that `f v = 0`. -/
-def transvection {f : Module.Dual R V} {v : V} (h : f v = 0) :
+def transvection {f : Dual R V} {v : V} (h : f v = 0) :
     V ≃ₗ[R] V where
   toFun := LinearMap.transvection f v
   invFun := LinearMap.transvection f (-v)
@@ -98,26 +132,26 @@ def transvection {f : Module.Dual R V} {v : V} (h : f v = 0) :
 
 namespace transvection
 
-theorem apply {f : Module.Dual R V} {v : V} (h : f v = 0) (x : V) :
+theorem apply {f : Dual R V} {v : V} (h : f v = 0) (x : V) :
     transvection h x = x + f x • v :=
   rfl
 
 @[simp]
-theorem coe_toLinearMap {f : Module.Dual R V} {v : V} (h : f v = 0) :
+theorem coe_toLinearMap {f : Dual R V} {v : V} (h : f v = 0) :
     LinearEquiv.transvection h = LinearMap.transvection f v :=
   rfl
 
 @[simp]
-theorem coe_apply {f : Module.Dual R V} {v x : V} {h : f v = 0} :
+theorem coe_apply {f : Dual R V} {v x : V} {h : f v = 0} :
     LinearEquiv.transvection h x = LinearMap.transvection f v x :=
   rfl
 
-theorem trans_of_left_eq {f : Module.Dual R V} {v w : V}
+theorem trans_of_left_eq {f : Dual R V} {v w : V}
     (hv : f v = 0) (hw : f w = 0) (hvw : f (v + w) = 0 := by simp [hv, hw]) :
     (transvection hw).trans (transvection hv) = transvection hvw := by
   ext; simp [comp_of_left_eq_apply hw]
 
-theorem trans_of_right_eq {f g : Module.Dual R V} {v : V}
+theorem trans_of_right_eq {f g : Dual R V} {v : V}
     (hf : f v = 0) (hg : g v = 0) (hfg : (f + g) v = 0 := by simp [hf, hg]) :
     (transvection hg).trans (transvection hf) = transvection hfg := by
   ext; simp [comp_of_right_eq_apply hf]
@@ -128,17 +162,17 @@ theorem of_left_eq_zero (v : V) (hv := LinearMap.zero_apply v) :
   ext; simp [transvection]
 
 @[simp]
-theorem of_right_eq_zero (f : Module.Dual R V) (hf := f.map_zero) :
+theorem of_right_eq_zero (f : Dual R V) (hf := f.map_zero) :
     transvection hf = LinearEquiv.refl R V := by
   ext; simp [transvection]
 
-theorem symm_eq {f : Module.Dual R V} {v : V}
+theorem symm_eq {f : Dual R V} {v : V}
     (hv : f v = 0) (hv' : f (-v) = 0 := by simp [hv]) :
     (transvection hv).symm = transvection hv' := by
   ext;
   simp [LinearEquiv.symm_apply_eq, comp_of_left_eq_apply hv']
 
-theorem symm_eq' {f : Module.Dual R V} {v : V}
+theorem symm_eq' {f : Dual R V} {v : V}
     (hf : f v = 0) (hf' : (-f) v = 0 := by simp [hf]) :
     (transvection hf).symm = transvection hf' := by
   ext; simp [LinearEquiv.symm_apply_eq, comp_of_right_eq_apply hf]
@@ -149,16 +183,16 @@ section baseChange
 
 namespace LinearMap.transvection
 
-open LinearMap LinearEquiv
+open LinearMap LinearEquiv Module
 
 variable {A : Type*} [CommRing A] [Algebra R A]
 
-theorem baseChange (f : Module.Dual R V) (v : V) :
+theorem baseChange (f : Dual R V) (v : V) :
     (transvection f v).baseChange A = transvection (f.baseChange A) (1 ⊗ₜ[R] v) := by
   ext; simp [transvection, TensorProduct.tmul_add]
 
 theorem _root_.LinearEquiv.transvection.baseChange
-    {f : Module.Dual R V} {v : V} (h : f v = 0)
+    {f : Dual R V} {v : V} (h : f v = 0)
     (hA : f.baseChange A (1 ⊗ₜ[R] v) = 0 := by simp [Algebra.algebraMap_eq_smul_one]) :
     (LinearEquiv.transvection h).baseChange R A V V = LinearEquiv.transvection hA := by
   simp [← toLinearMap_inj, transvection.coe_toLinearMap, transvection.baseChange]
@@ -169,7 +203,7 @@ variable {W : Type*} [AddCommMonoid W] [Module R W] [Module A W]
   [IsScalarTower R A W] {ε : V →ₗ[R] W} (ibc : IsBaseChange A ε)
 
 @[simp]
-theorem _root_.IsBaseChange.transvection (f : Module.Dual R V) (v : V) :
+theorem _root_.IsBaseChange.transvection (f : Dual R V) (v : V) :
     ibc.endHom (transvection f v) = transvection (ibc.toDual f) (ε v) := by
   ext w
   induction w using ibc.inductionOn with