feat(LinearAlgebra/Transvection): the determinant of a transvection is equal to 1. (#32757)

Prove that the determinant of a transvection is equal to 1

The proof goes by showing that the determinant of `LinearMap.transvection f v` is `1 + f v` (even if `f v` is nonzero).

I first treat the case of a field, distinguishing whether `f v = 0` (so that we get
a transvection) or not (so that we have a dilation).

Then, by base change to the field of fractions, I can handle the case of a domain. Finally, the general case is treated by base change from the “universal case” where the base ring is the ring of polynomials in $$2n$$ indeterminates corresponding to the coefficients of $$f$$ and $$v$$.

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

Author: AntoineChambert-Loir

Mathlib/LinearAlgebra/Basis/VectorSpace.lean

@@ -9,6 +9,7 @@ public import Mathlib.LinearAlgebra.FreeModule.Basic
 public import Mathlib.LinearAlgebra.LinearIndependent.Lemmas
 public import Mathlib.LinearAlgebra.LinearPMap
 public import Mathlib.LinearAlgebra.Projection
+public import Mathlib.Tactic.Field
 
 /-!
 # Bases in a vector space
@@ -331,3 +332,104 @@ theorem quotient_prod_linearEquiv (p : Submodule K V) : Nonempty (((V ⧸ p) ×
       (prodEquivOfIsCompl q p hq.symm)
 
 end DivisionRing
+
+section Field
+
+open Submodule LinearMap Module
+
+variable {K : Type*} {V : Type*} [Field K] [AddCommGroup V] [Module K V]
+
+variable {f : V →ₗ[K] K} {v : V}
+
+/-- In a vector space, given a nonzero linear form `f`,
+a nonzero vector `v` such that `f v ≠ 0`,
+there exists a basis `b` with an index `i`
+such that `v = b i` and `f = (f v) • b.coord i`. -/
+theorem exists_basis_of_pairing_ne_zero
+    (hfv : f v ≠ 0) :
+    ∃ (n : Set V) (b : Module.Basis n K V) (i : n),
+      v = b i ∧ f = (f v) • b.coord i := by
+  set b₁ := Basis.ofVectorSpace K (ker f)
+  set s : Set V := (ker f).subtype '' Set.range b₁
+  have hs : span K s = ker f := by
+    simp only [s, span_image]
+    simp
+  set n := insert v s
+  have H₁ : LinearIndepOn K _root_.id n := by
+    apply LinearIndepOn.id_insert
+    · apply LinearIndepOn.image
+      · exact b₁.linearIndependent.linearIndepOn_id
+      · simp
+    · simp [hs, hfv]
+  have H₂ : ⊤ ≤ span K n := by
+    rintro x -
+    simp only [n, mem_span_insert']
+    use -f x / f v
+    simp only [hs, mem_ker, map_add, map_smul, smul_eq_mul]
+    field
+  set b := Basis.mk H₁ (by simpa using H₂)
+  set i : n := ⟨v, s.mem_insert v⟩
+  have hi : b i = v := by simp [b, i]
+  refine ⟨n, b, i, by simp [b, i], ?_⟩
+  rw [← hi]
+  apply b.ext
+  intro j
+  by_cases h : i = j
+  · simp [h]
+  · suffices f (b j) = 0 by
+      simp [Finsupp.single_eq_of_ne h, this]
+    rw [← mem_ker, ← hs, Basis.coe_mk]
+    apply subset_span
+    apply Or.resolve_left (Set.mem_insert_iff.mpr j.prop)
+    simp [← hi, b, Subtype.coe_inj, Ne.symm h]
+
+/-- In a vector space, given a nonzero linear form `f`,
+a nonzero vector `v` such that `f v = 0`,
+there exists a basis `b` with two distinct indices `i`, `j`
+such that `v = b i` and `f = b.coord j`. -/
+theorem exists_basis_of_pairing_eq_zero
+    (hfv : f v = 0) (hf : f ≠ 0) (hv : v ≠ 0) :
+    ∃ (n : Set V) (b : Basis n K V) (i j : n),
+      i ≠ j ∧ v = b i ∧ f = b.coord j := by
+  lift v to ker f using hfv
+  have : LinearIndepOn K _root_.id {v} := by simpa using hv
+  set b₁ : Basis _ K (ker f) := .extend this
+  obtain ⟨w, hw⟩ : ∃ w, f w = 1 := by
+    simp only [ne_eq, DFunLike.ext_iff, not_forall] at hf
+    rcases hf with ⟨w, hw⟩
+    use (f w)⁻¹ • w
+    simp_all
+  set s : Set V := (ker f).subtype '' Set.range b₁
+  have hs : span K s = ker f := by
+    simp only [s, span_image]
+    simp
+  have hvs : ↑v ∈ s := by
+    refine ⟨v, ?_, by simp⟩
+    simp [b₁, this.subset_extend _ _]
+  set n := insert w s
+  have H₁ : LinearIndepOn K _root_.id n := by
+    apply LinearIndepOn.id_insert
+    · apply LinearIndepOn.image
+      · exact b₁.linearIndependent.linearIndepOn_id
+      · simp
+    · simp [hs, hw]
+  have H₂ : ⊤ ≤ span K n := by
+    rintro x -
+    simp only [n, mem_span_insert']
+    use -f x
+    simp [hs, hw]
+  set b := Basis.mk H₁ (by simpa using H₂)
+  refine ⟨n, b, ⟨v, by simp [n, hvs]⟩, ⟨w, by simp [n]⟩, ?_, by simp [b], ?_⟩
+  · apply_fun (f ∘ (↑))
+    simp [hw]
+  · apply b.ext
+    intro i
+    rw [Basis.coord_apply, Basis.repr_self]
+    simp only [b, Basis.mk_apply]
+    rcases i with ⟨x, rfl | ⟨x, hx, rfl⟩⟩
+    · simp [hw]
+    · suffices x ≠ w by simp [this]
+      apply_fun f
+      simp [hw]
+
+end Field

Mathlib/LinearAlgebra/Determinant.lean

@@ -185,6 +185,13 @@ theorem coe_det [DecidableEq M] :
   · congr -- use the correct `DecidableEq` instance
   rfl
 
+theorem _root_.Module.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 (Module.Basis s R M)
+  · rcases H with ⟨s, ⟨hs⟩⟩
+    exact Module.Free.of_basis hs
+  · classical simp [LinearMap.coe_det, H] at hf
+
 end
 
 -- Auxiliary lemma, the `simp` normal form goes in the other direction

Mathlib/LinearAlgebra/Transvection.lean

@@ -6,6 +6,7 @@ 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
@@ -18,9 +19,14 @@ public import Mathlib.Tactic.Positivity
 * When `f : Module.Dual R V` and `v : V`,
   `LinearMap.transvection f v` is the linear map given by `x ↦ x + f x • v`,
 
+* `LinearMap.transvection.det` shows that the determinant of
+  `LinearMap.transvection f v` is equal to `1 + f v`.
+
 * If, moreover, `f v = 0`, then `LinearEquiv.transvection` shows that it is
  a linear equivalence.
 
+* `LinearEquiv.transvection.det` shows that it has determinant `1`.
+
 ## Note on terminology
 
 In the mathematical litterature, linear maps of the form `LinearMap.transvection f v`
@@ -77,21 +83,21 @@ theorem comp_of_right_eq {f g : Dual R V} {v : V} (hf : f v = 0) :
 
 @[simp]
 theorem of_left_eq_zero (v : V) :
-    transvection (0 : Dual R V) v = LinearMap.id := by
+    transvection (0 : Dual R V) v = id := by
   ext
   simp [transvection]
 
 @[simp]
 theorem of_right_eq_zero (f : Dual R V) :
-    transvection f 0 = LinearMap.id := by
+    transvection f 0 = id := by
   ext
   simp [transvection]
 
 theorem eq_id_of_finrank_le_one
     {R V : Type*} [CommSemiring R] [AddCommMonoid V] [Module R V]
     [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
+    transvection f v = id := by
   interval_cases h : finrank R V
   · have : Subsingleton V := (finrank_eq_zero_iff_of_free R V).mp h
     simp [Subsingleton.eq_zero v]
@@ -161,24 +167,24 @@ theorem trans_of_right_eq {f g : Dual R V} {v : V}
 
 @[simp]
 theorem of_left_eq_zero (v : V) (hv := LinearMap.zero_apply v) :
-    transvection hv = LinearEquiv.refl R V := by
+    transvection hv = refl R V := by
   ext; simp [transvection]
 
 @[simp]
 theorem of_right_eq_zero (f : Dual R V) (hf := f.map_zero) :
-    transvection hf = LinearEquiv.refl R V := by
+    transvection hf = refl R V := by
   ext; simp [transvection]
 
 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']
+  simp [symm_apply_eq, comp_of_left_eq_apply hv']
 
 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]
+  ext; simp [symm_apply_eq, comp_of_right_eq_apply hf]
 
 end LinearEquiv.transvection
 
@@ -219,3 +225,154 @@ theorem _root_.IsBaseChange.transvection (f : Dual R V) (v : V) :
 end LinearMap.transvection
 
 end baseChange
+
+section determinant
+
+namespace LinearMap.transvection
+
+open Polynomial Module
+
+open scoped TensorProduct
+
+section Field
+
+variable {K : Type*} {V : Type*} [Field K] [AddCommGroup V] [Module K V]
+
+variable {f : Dual K V} {v : V}
+
+/-- Determinant of transvections, over a field.
+
+See `LinearMap.Transvection.det` for the general result. -/
+private theorem det_ofField [FiniteDimensional K V] (f : Dual K V) (v : V) :
+    (LinearMap.transvection f v).det = 1 + f v := by
+  classical
+  by_cases hfv : f v = 0
+  · by_cases hv : v = 0
+    · simp [hv]
+    by_cases hf : f = 0
+    · simp [hf]
+    obtain ⟨ι, b, i, j, hi, hj⟩ := exists_basis_of_pairing_eq_zero hfv hf hv
+    have : Fintype ι := FiniteDimensional.fintypeBasisIndex b
+    rw [← det_toMatrix b]
+    suffices toMatrix b b (LinearMap.transvection f v) = Matrix.transvection i j 1 by
+      rw [this, Matrix.det_transvection_of_ne i j hi 1, hfv, add_zero]
+    ext x y
+    rw [toMatrix_apply, transvection.apply, Matrix.transvection]
+    simp only [hj.2, Basis.coord_apply, Basis.repr_self, hj.1, map_add, map_smul,
+      Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.coe_add, Pi.add_apply, Matrix.add_apply]
+    apply congr_arg₂
+    · by_cases h : x = y
+      · rw [h]; simp
+      · rw [Finsupp.single_eq_of_ne h, Matrix.one_apply_ne h]
+    · by_cases h : i = x ∧ j = y
+      · rw [h.1, h.2]; simp
+      · rcases not_and_or.mp h with h' | h' <;>
+          simp [Finsupp.single_eq_of_ne' h',
+            Finsupp.single_eq_of_ne h',
+            Matrix.single_apply_of_ne (h := h)]
+  · obtain ⟨ι, b, i, hv, hf⟩ := exists_basis_of_pairing_ne_zero hfv
+    have : Fintype ι := FiniteDimensional.fintypeBasisIndex b
+    rw [← det_toMatrix b]
+    suffices toMatrix b b (transvection f v) =
+      Matrix.diagonal (Function.update 1 i (1 + f v)) by
+      rw [this]
+      simp only [Matrix.det_diagonal]
+      rw [Finset.prod_eq_single i]
+      · simp
+      · intro j _ hj
+        simp [Function.update_of_ne hj]
+      · simp
+    ext x y
+    rw [toMatrix_apply, transvection.apply, Matrix.diagonal]
+    simp only [map_add, Basis.repr_self, map_smul, Finsupp.coe_add, Finsupp.coe_smul,
+      Pi.add_apply, Pi.smul_apply, smul_eq_mul, Matrix.of_apply]
+    rw [hv, Function.update_apply, Basis.repr_self, Pi.one_apply, hf]
+    simp only [smul_apply, Basis.coord_apply, Basis.repr_self, smul_eq_mul,
+      Finsupp.single_eq_same, mul_one]
+    split_ifs with hxy hxi
+    · simp [← hxy, hxi]
+    · rw [Finsupp.single_eq_of_ne hxi]; simp [hxy]
+    · rw [Finsupp.single_eq_of_ne hxy, zero_add, mul_assoc]
+      convert mul_zero _
+      by_cases hxi : x = i
+      · simp [← hxi, Finsupp.single_eq_of_ne hxy]
+      · simp [Finsupp.single_eq_of_ne hxi]
+
+end Field
+
+variable {R V : Type*} [CommRing R] [AddCommGroup V] [Module R V]
+
+/-- Determinant of a transvection, over a domain.
+
+See `LinearMap.transvection.det` for the general case. -/
+private theorem det_ofDomain [Free R V] [Module.Finite R V] [IsDomain R]
+    (f : Dual R V) (v : V) :
+    (transvection f v).det = 1 + f v := by
+  let K := FractionRing R
+  let : Field K := inferInstance
+  apply FaithfulSMul.algebraMap_injective R K
+  have := det_ofField (f.baseChange K) (1 ⊗ₜ[R] v)
+  rw [← transvection.baseChange, det_baseChange,
+    ← algebraMap.coe_one (R := R) (A := K)] at this
+  simpa [Algebra.algebraMap_eq_smul_one, add_smul] using this
+
+open IsBaseChange
+
+@[simp] theorem det [Free R V] [Module.Finite R V]
+    (f : Dual R V) (v : V) :
+    (transvection f v).det = 1 + f v := by
+  rcases subsingleton_or_nontrivial R with hR | hR
+  · subsingleton
+  let b := finBasis R V
+  set n := finrank R V
+  let S := MvPolynomial (Fin n ⊕ Fin n) ℤ
+  let γ : S →+* R :=
+    (MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) (fun i ↦ b.coord i v)) :
+      MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R)
+  have : IsDomain S := inferInstance
+  let _ : Algebra S R := RingHom.toAlgebra γ
+  let _ : Module S V := compHom V γ
+  have _ : IsScalarTower S R V := IsScalarTower.of_compHom S R V
+  have ibc := IsBaseChange.of_fintype_basis S b
+  set ε := Fintype.linearCombination S (fun i ↦ b i)
+  set M := Fin n → S
+  have hε (i) : ε (Pi.single i 1) = b i := by
+    rw [Fintype.linearCombination_apply_single, one_smul]
+  let fM : Dual S M :=
+    Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
+  let vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
+  have hf : ibc.toDual fM = f := by
+    apply b.ext
+    intro i
+    rw [← hε, toDual_comp_apply, Fintype.linearCombination_apply_single,
+      one_smul, RingHom.algebraMap_toAlgebra, hε]
+    apply MvPolynomial.aeval_X
+  have hv : ε vM = v := by
+    rw [of_fintype_basis_eq]
+    ext i
+    rw [RingHom.algebraMap_toAlgebra]
+    simp only [vM, γ, Function.comp_apply]
+    apply MvPolynomial.aeval_X
+  rw [← hf, ← hv, ← IsBaseChange.transvection, det_endHom, det_ofDomain]
+  rw [map_add, map_one, add_right_inj, toDual_comp_apply]
+
+/-- Determinant of a transvection.
+
+It is not necessary to assume that the module is finite and free
+because `LinearMap.det` is identically 1 otherwise. -/
+@[simp] theorem _root_.LinearEquiv.det_eq_one
+    {f : Dual R V} {v : V} (hfv : f v = 0) :
+    (LinearEquiv.transvection hfv).det = 1 := by
+  rw [← Units.val_inj, LinearEquiv.coe_det,
+    LinearEquiv.transvection.coe_toLinearMap hfv, Units.val_one]
+  by_contra! h
+  have : Free R V := Free.of_det_ne_one h
+  have : Module.Finite R V := finite_of_det_ne_one h
+  apply h
+  rw [transvection.det, hfv, add_zero]
+
+end transvection
+
+end LinearMap
+
+end determinant