feat: drop finite-dimensionality assumption from PerfectPairing.restrictScalarsField (#18940)

Author: ocfnash

Mathlib.lean

@@ -3349,6 +3349,7 @@ import Mathlib.LinearAlgebra.LinearIndependent
 import Mathlib.LinearAlgebra.LinearPMap
 import Mathlib.LinearAlgebra.Matrix.AbsoluteValue
 import Mathlib.LinearAlgebra.Matrix.Adjugate
+import Mathlib.LinearAlgebra.Matrix.BaseChange
 import Mathlib.LinearAlgebra.Matrix.Basis
 import Mathlib.LinearAlgebra.Matrix.BilinearForm
 import Mathlib.LinearAlgebra.Matrix.Block

Mathlib/Data/Matrix/Mul.lean

@@ -880,6 +880,18 @@ theorem submatrix_mulVec_equiv [Fintype n] [Fintype o] [NonUnitalNonAssocSemirin
     M.submatrix e₁ e₂ *ᵥ v = (M *ᵥ (v ∘ e₂.symm)) ∘ e₁ :=
   funext fun _ => Eq.symm (dotProduct_comp_equiv_symm _ _ _)
 
+@[simp]
+theorem submatrix_id_mul_left [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type*}
+    (M : Matrix m n α) (N : Matrix o p α) (e₁ : l → m) (e₂ : n ≃ o) :
+    M.submatrix e₁ id * N.submatrix e₂ id = M.submatrix e₁ e₂.symm * N := by
+  ext; simp [mul_apply, ← e₂.bijective.sum_comp]
+
+@[simp]
+theorem submatrix_id_mul_right [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type*}
+    (M : Matrix m n α) (N : Matrix o p α) (e₁ : l → p) (e₂ : o ≃ n) :
+    M.submatrix id e₂ * N.submatrix id e₁ = M * N.submatrix e₂.symm e₁ := by
+  ext; simp [mul_apply, ← e₂.bijective.sum_comp]
+
 theorem submatrix_vecMul_equiv [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α]
     (M : Matrix m n α) (v : l → α) (e₁ : l ≃ m) (e₂ : o → n) :
     v ᵥ* M.submatrix e₁ e₂ = ((v ∘ e₁.symm) ᵥ* M) ∘ e₂ :=

Mathlib/LinearAlgebra/Dual.lean

@@ -418,7 +418,7 @@ theorem linearCombination_dualBasis (f : ι →₀ R) (i : ι) :
 
 @[deprecated (since := "2024-08-29")] alias total_dualBasis := linearCombination_dualBasis
 
-theorem dualBasis_repr (l : Dual R M) (i : ι) : b.dualBasis.repr l i = l (b i) := by
+@[simp] theorem dualBasis_repr (l : Dual R M) (i : ι) : b.dualBasis.repr l i = l (b i) := by
   rw [← linearCombination_dualBasis b, Basis.linearCombination_repr b.dualBasis l]
 
 theorem dualBasis_apply (i : ι) (m : M) : b.dualBasis i m = b.repr m i :=

Mathlib/LinearAlgebra/Matrix/BaseChange.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2024 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
+import Mathlib.Algebra.Field.Subfield.Defs
+
+/-!
+# Matrices and base change
+
+This file is a home for results about base change for matrices.
+
+## Main results:
+ * `Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_right`: if an invertible matrix over `L` takes
+   values in subfield `K ⊆ L`, then so does its (right) inverse.
+ * `Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left`: if an invertible matrix over `L` takes
+   values in subfield `K ⊆ L`, then so does its (left) inverse.
+
+-/
+
+namespace Matrix
+
+open scoped Matrix
+
+variable {m n L : Type*} [Fintype m] [Fintype n] [DecidableEq m] [Field L]
+  (e : m ≃ n) (K : Subfield L) {A : Matrix m n L} {B : Matrix n m L} (hAB : A * B = 1)
+
+include e hAB
+
+lemma mem_subfield_of_mul_eq_one_of_mem_subfield_right
+    (h_mem : ∀ i j, A i j ∈ K) (i : n) (j : m) :
+    B i j ∈ K := by
+  let A' : Matrix m m K := of fun i j ↦ ⟨A.submatrix id e i j, h_mem i (e j)⟩
+  have hA' : A'.map K.subtype = A.submatrix id e := rfl
+  have hA : IsUnit A' := by
+    have h_unit : IsUnit (A.submatrix id e) :=
+      isUnit_of_right_inverse (B := B.submatrix e id) (by simpa)
+    have h_det : (A.submatrix id e).det = K.subtype A'.det := by
+      simp [A', K.subtype.map_det, map, submatrix]
+    simpa [isUnit_iff_isUnit_det, h_det] using h_unit
+  obtain ⟨B', hB⟩ := exists_right_inverse_iff_isUnit.mpr hA
+  suffices (B'.submatrix e.symm id).map K.subtype = B by simp [← this]
+  replace hB : A * (B'.submatrix e.symm id).map K.subtype = 1 := by
+    replace hB := congr_arg (fun C ↦ C.map K.subtype) hB
+    simp_rw [map_mul] at hB
+    rw [hA', ← e.symm_symm, ← submatrix_id_mul_left] at hB
+    simpa using hB
+  classical
+  simpa [← Matrix.mul_assoc, (mul_eq_one_comm_of_equiv e).mp hAB] using congr_arg (B * ·) hB
+
+lemma mem_subfield_of_mul_eq_one_of_mem_subfield_left
+    (h_mem : ∀ i j, B i j ∈ K) (i : m) (j : n) :
+    A i j ∈ K := by
+  replace hAB : Bᵀ * Aᵀ = 1 := by simpa using congr_arg transpose hAB
+  rw [← A.transpose_apply]
+  simp_rw [← B.transpose_apply] at h_mem
+  exact mem_subfield_of_mul_eq_one_of_mem_subfield_right e K hAB (fun i j ↦ h_mem j i) j i
+
+end Matrix

Mathlib/LinearAlgebra/Matrix/Basis.lean

@@ -230,6 +230,12 @@ theorem Basis.toMatrix_reindex' [DecidableEq ι] [DecidableEq ι'] (b : Basis ι
     Matrix.reindex_apply, Matrix.submatrix_apply, Function.comp_apply, e.apply_symm_apply,
     Finsupp.mapDomain_equiv_apply]
 
+@[simp]
+lemma Basis.toMatrix_mulVec_repr (m : M) :
+    b'.toMatrix b *ᵥ b.repr m = b'.repr m := by
+  classical
+  simp [← LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrix_mulVec_repr]
+
 end Fintype
 
 /-- A generalization of `Basis.toMatrix_self`, in the opposite direction. -/

Mathlib/LinearAlgebra/PerfectPairing.lean

@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.LinearAlgebra.Dual
+import Mathlib.LinearAlgebra.Matrix.Basis
+import Mathlib.LinearAlgebra.Matrix.BaseChange
+import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
 
 /-!
 # Perfect pairings of modules
@@ -21,6 +24,7 @@ to connect 1 and 2.
 
  * `PerfectPairing`
  * `PerfectPairing.flip`
+ * `PerfectPairing.dual`
  * `PerfectPairing.toDualLeft`
  * `PerfectPairing.toDualRight`
  * `PerfectPairing.restrict`
@@ -161,6 +165,11 @@ include p in
 theorem reflexive_right : IsReflexive R N :=
   p.flip.reflexive_left
 
+include p in
+theorem finrank_eq [Module.Finite R M] [Module.Free R M] :
+    finrank R M = finrank R N :=
+  ((Module.Free.chooseBasis R M).toDualEquiv.trans p.toDualRight.symm).finrank_eq
+
 private lemma restrict_aux
     {M' N' : Type*} [AddCommGroup M'] [Module R M'] [AddCommGroup N'] [Module R N']
     (i : M' →ₗ[R] M) (j : N' →ₗ[R] N)
@@ -206,6 +215,61 @@ section RestrictScalars
 
 open Submodule (span)
 
+/-- If a perfect pairing over a field `L` takes values in a subfield `K` along two `K`-subspaces
+whose `L` span is full, then these subspaces induce a `K`-structure in the sense of
+[*Algebra I*, Bourbaki : Chapter II, §8.1 Definition 1][bourbaki1989]. -/
+lemma exists_basis_basis_of_span_eq_top_of_mem_algebraMap
+    {K L : Type*} [Field K] [Field L] [Algebra K L]
+    [Module L M] [Module L N] [Module K M] [Module K N] [IsScalarTower K L M]
+    (p : PerfectPairing L M N)
+    (M' : Submodule K M) (N' : Submodule K N)
+    (hM : span L (M' : Set M) = ⊤)
+    (hN : span L (N' : Set N) = ⊤)
+    (hp : ∀ᵉ (x ∈ M') (y ∈ N'), p x y ∈ (algebraMap K L).range) :
+    ∃ (n : ℕ) (b : Basis (Fin n) L M) (b' : Basis (Fin n) K M'), ∀ i, b i = b' i := by
+  classical
+  have : IsReflexive L M := p.reflexive_left
+  have : IsReflexive L N := p.reflexive_right
+  obtain ⟨v, hv₁, hv₂, hv₃⟩ := exists_linearIndependent L (M' : Set M)
+  rw [hM] at hv₂
+  let b : Basis _ L M := Basis.mk hv₃ <| by rw [← hv₂, Subtype.range_coe_subtype, Set.setOf_mem_eq]
+  have : Fintype v := Set.Finite.fintype <| Module.Finite.finite_basis b
+  set v' : v → M' := fun i ↦ ⟨i, hv₁ (Subtype.coe_prop i)⟩
+  have hv' : LinearIndependent K v' := by
+    replace hv₃ := hv₃.restrict_scalars (R := K) <| by
+      simp_rw [← Algebra.algebraMap_eq_smul_one]
+      exact NoZeroSMulDivisors.algebraMap_injective K L
+    rw [show ((↑) : v → M) = M'.subtype ∘ v' from rfl] at hv₃
+    exact hv₃.of_comp
+  suffices span K (Set.range v') = ⊤ by
+    let e := (Module.Finite.finite_basis b).equivFin
+    let b' : Basis _ K M' := Basis.mk hv' (by rw [this])
+    exact ⟨_, b.reindex e, b'.reindex e, fun i ↦ by simp [b, b']⟩
+  suffices span K v = M' by
+    apply Submodule.map_injective_of_injective M'.injective_subtype
+    rw [Submodule.map_span, ← Set.image_univ, Set.image_image]
+    simpa
+  refine le_antisymm (Submodule.span_le.mpr hv₁) fun m hm ↦ ?_
+  obtain ⟨w, hw₁, hw₂, hw₃⟩ := exists_linearIndependent L (N' : Set N)
+  rw [hN] at hw₂
+  let bN : Basis _ L N := Basis.mk hw₃ <| by rw [← hw₂, Subtype.range_coe_subtype, Set.setOf_mem_eq]
+  have : Fintype w := Set.Finite.fintype <| Module.Finite.finite_basis bN
+  have e : v ≃ w := Fintype.equivOfCardEq <| by rw [← Module.finrank_eq_card_basis b,
+    ← Module.finrank_eq_card_basis bN, p.finrank_eq]
+  let bM := bN.dualBasis.map p.toDualLeft.symm
+  have hbM (j : w) (x : M) (hx : x ∈ M') : bM.repr x j = p x (j : N) := by simp [bM, bN]
+  have hj (j : w) : bM.repr m j ∈ (algebraMap K L).range := (hbM _ _ hm) ▸ hp m hm j (hw₁ j.2)
+  replace hp (i : w) (j : v) :
+      (bN.dualBasis.map p.toDualLeft.symm).toMatrix b i j ∈ (algebraMap K L).fieldRange := by
+    simp only [Basis.toMatrix, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
+      toDualLeft_apply, Basis.dualBasis_repr]
+    exact hp (b j) (by simpa [b] using hv₁ j.2) (bN i) (by simpa [bN] using hw₁ i.2)
+  have hA (i j) : b.toMatrix bM i j ∈ (algebraMap K L).range :=
+    Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left e _ (by simp) hp i j
+  have h_span : span K v = span K (Set.range b) := by simp [b]
+  rw [h_span, Basis.mem_span_iff_repr_mem, ← Basis.toMatrix_mulVec_repr bM b m]
+  exact fun i ↦ Subring.sum_mem _ fun j _ ↦ Subring.mul_mem _ (hA i j) (hj j)
+
 variable {S : Type*}
   [CommRing S] [Algebra S R] [Module S M] [Module S N] [IsScalarTower S R M] [IsScalarTower S R N]
   [NoZeroSMulDivisors S R] [Nontrivial R]
@@ -272,18 +336,23 @@ def restrictScalars
       p.flip.restrictScalarsAux_surjective j i h₂ (fun m n ↦ hp n m)⟩}
 
 /-- Restriction of scalars for a perfect pairing taking values in a subfield. -/
-def restrictScalarsField {K : Type*} [Field K] [Algebra K R]
-    [Module K M] [Module K N] [IsScalarTower K R M] [IsScalarTower K R N]
-    [Module K M'] [Module K N'] [FiniteDimensional K M']
+def restrictScalarsField {K L : Type*} [Field K] [Field L] [Algebra K L]
+    [Module L M] [Module L N] [Module K M] [Module K N] [IsScalarTower K L M] [IsScalarTower K L N]
+    [Module K M'] [Module K N']
     (i : M' →ₗ[K] M) (j : N' →ₗ[K] N)
     (hi : Injective i) (hj : Injective j)
-    (hM : span R (LinearMap.range i : Set M) = ⊤)
-    (hN : span R (LinearMap.range j : Set N) = ⊤)
-    (hp : ∀ m n, p (i m) (j n) ∈ (algebraMap K R).range) :
-    PerfectPairing K M' N' :=
-  PerfectPairing.mkOfInjective _
-    (p.restrictScalarsAux_injective i j hi hN hp)
+    (hM : span L (LinearMap.range i : Set M) = ⊤)
+    (hN : span L (LinearMap.range j : Set N) = ⊤)
+    (p : PerfectPairing L M N)
+    (hp : ∀ m n, p (i m) (j n) ∈ (algebraMap K L).range) :
+    PerfectPairing K M' N' := by
+  suffices FiniteDimensional K M' from mkOfInjective _ (p.restrictScalarsAux_injective i j hi hN hp)
     (p.flip.restrictScalarsAux_injective j i hj hM (fun m n ↦ hp n m))
+  obtain ⟨n, -, b', -⟩ := p.exists_basis_basis_of_span_eq_top_of_mem_algebraMap _ _ hM hN <| by
+    rintro - ⟨m, rfl⟩ - ⟨n, rfl⟩
+    exact hp m n
+  have : FiniteDimensional K (LinearMap.range i) := FiniteDimensional.of_fintype_basis b'
+  exact Finite.equiv (LinearEquiv.ofInjective i hi).symm
 
 end RestrictScalars
 
@@ -341,6 +410,12 @@ def toPerfectPairing : PerfectPairing R N M where
 
 end LinearEquiv
 
+/-- A perfect pairing induces a perfect pairing between dual spaces. -/
+def PerfectPairing.dual (p : PerfectPairing R M N) :
+    PerfectPairing R (Dual R M) (Dual R N) :=
+  let _i := p.reflexive_right
+  (p.toDualRight.symm.trans (evalEquiv R N)).toPerfectPairing
+
 namespace Submodule
 
 open LinearEquiv

docs/references.bib

@@ -607,7 +607,7 @@ @Book{            bourbaki1987
 
 @Book{            bourbaki1989,
   author        = {Bourbaki, N.},
-  title         = {Algebra. {II}. {C}hapters 1–3},
+  title         = {Algebra. {I}. {C}hapters 1–3},
   series        = {Elements of Mathematics},
   note          = {Translated from the French},
   year          = {1998},