refactor(LinearAlgebra): Ensure ChooseBasisIndex is finite on trivi…

…al modules (#6322)

This also changes `basisFintypeOfFiniteSpans` to use `Finite` rather than `Fintype`, as it was noncomputable anyway.
This means it has to be renamed to `basis_finite_of_finite_spans` as it now is a proof!



Co-authored-by: Oliver Nash <github@olivernash.org>

Mathlib/FieldTheory/Tower.lean

@@ -75,7 +75,7 @@ theorem rank_mul_rank (F : Type u) (K A : Type v) [CommRing F] [Ring K] [AddComm
 
 /-- Tower law: if `A` is a `K`-module and `K` is an extension of `F` then
 $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$. -/
-theorem FiniteDimensional.finrank_mul_finrank' [Nontrivial K] [Module.Finite F K]
+theorem FiniteDimensional.finrank_mul_finrank' [Module.Finite F K]
     [Module.Finite K A] : finrank F K * finrank K A = finrank F A := by
   letI := nontrivial_of_invariantBasisNumber F
   let b := Module.Free.chooseBasis F K

Mathlib/LinearAlgebra/Contraction.lean

@@ -202,7 +202,7 @@ theorem dualTensorHomEquivOfBasis_symm_cancel_right (x : M →ₗ[R] N) :
 
 variable (R M N P Q)
 
-variable [Module.Free R M] [Module.Finite R M] [Nontrivial R]
+variable [Module.Free R M] [Module.Finite R M]
 
 /-- If `M` is finite free, the natural map $M^* ⊗ N → Hom(M, N)$ is an
 equivalence. -/

Mathlib/LinearAlgebra/Dimension.lean

@@ -30,7 +30,7 @@ import Mathlib.SetTheory.Cardinal.Cofinality
   at most that of the target.
 * `LinearMap.rank_le_of_surjective`: the target of a surjective linear map has dimension
   at most that of that source.
-* `basisFintypeOfFiniteSpans`:
+* `basis_finite_of_finite_spans`:
   the existence of a finite spanning set implies that any basis is finite.
 * `infinite_basis_le_maximal_linearIndependent`:
   if `b` is an infinite basis for a module `M`,
@@ -319,11 +319,13 @@ theorem LinearIndependent.set_finite_of_isNoetherian [IsNoetherian R M] {s : Set
 /--
 Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.
 -/
-def basisFintypeOfFiniteSpans (w : Set M) [Fintype w] (s : span R w = ⊤) {ι : Type w}
-    (b : Basis ι R M) : Fintype ι := by
+lemma basis_finite_of_finite_spans (w : Set M) (hw : w.Finite) (s : span R w = ⊤) {ι : Type w}
+    (b : Basis ι R M) : Finite ι := by
   classical
+  haveI := hw.to_subtype
+  cases nonempty_fintype w
   -- We'll work by contradiction, assuming `ι` is infinite.
-  apply fintypeOfNotInfinite _
+  rw [← not_infinite_iff_finite]
   intro i
   -- Let `S` be the union of the supports of `x ∈ w` expressed as linear combinations of `b`.
   -- This is a finite set since `w` is finite.
@@ -348,7 +350,7 @@ def basisFintypeOfFiniteSpans (w : Set M) [Fintype w] (s : span R w = ⊤) {ι :
   -- giving the desire contradiction.
   refine' b.linearIndependent.not_mem_span_image _ k'
   exact nm
-#align basis_fintype_of_finite_spans basisFintypeOfFiniteSpans
+#align basis_fintype_of_finite_spans basis_finite_of_finite_spansₓ
 
 -- From [Les familles libres maximales d'un module ont-elles le meme cardinal?][lazarus1973]
 /-- Over any ring `R`, if `b` is a basis for a module `M`,
@@ -540,9 +542,10 @@ theorem mk_eq_mk_of_basis (v : Basis ι R M) (v' : Basis ι' R M) :
   classical
   haveI := nontrivial_of_invariantBasisNumber R
   cases fintypeOrInfinite ι
-  · -- `v` is a finite basis, so by `basisFintypeOfFiniteSpans` so is `v'`.
-    haveI : Fintype (range v) := Set.fintypeRange v
-    haveI := basisFintypeOfFiniteSpans _ v.span_eq v'
+  · -- `v` is a finite basis, so by `basis_finite_of_finite_spans` so is `v'`.
+    -- haveI : Finite (range v) := Set.finite_range v
+    haveI := basis_finite_of_finite_spans _ (Set.finite_range v) v.span_eq v'
+    cases nonempty_fintype ι'
     -- We clean up a little:
     rw [Cardinal.mk_fintype, Cardinal.mk_fintype]
     simp only [Cardinal.lift_natCast, Cardinal.natCast_inj]
@@ -606,7 +609,8 @@ but still assumes we have a finite spanning set.
 theorem basis_le_span' {ι : Type _} (b : Basis ι R M) {w : Set M} [Fintype w] (s : span R w = ⊤) :
     #ι ≤ Fintype.card w := by
   haveI := nontrivial_of_invariantBasisNumber R
-  haveI := basisFintypeOfFiniteSpans w s b
+  haveI := basis_finite_of_finite_spans w (toFinite _) s b
+  cases nonempty_fintype ι
   rw [Cardinal.mk_fintype ι]
   simp only [Cardinal.natCast_le]
   exact Basis.le_span'' b s

Mathlib/LinearAlgebra/Dual.lean

@@ -477,7 +477,7 @@ theorem eval_range {ι : Type _} [Finite ι] (b : Basis ι R M) :
 
 section
 
-variable [Finite R M] [Free R M] [Nontrivial R]
+variable [Finite R M] [Free R M]
 
 instance dual_free : Free R (Dual R M) :=
   Free.of_basis (Free.chooseBasis R M).dualBasis
@@ -516,7 +516,7 @@ namespace Module
 
 variable {K : Type u₁} {V : Type u₂}
 
-variable [Field K] [AddCommGroup V] [Module K V]
+variable [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V]
 
 open Module Module.Dual Submodule LinearMap Cardinal Basis FiniteDimensional
 
@@ -526,7 +526,7 @@ variable (K) (V)
 
 -- Porting note: broken dot notation lean4#1910 LinearMap.ker
 theorem eval_ker : LinearMap.ker (eval K V) = ⊥ := by
-  classical exact (Basis.ofVectorSpace K V).eval_ker
+  classical exact (Module.Free.chooseBasis K V).eval_ker
 #align module.eval_ker Module.eval_ker
 
 theorem map_eval_injective : (Submodule.map (eval K V)).Injective := by
@@ -564,16 +564,14 @@ theorem forall_dual_apply_eq_zero_iff (v : V) : (∀ φ : Module.Dual K V, φ v
 
 end
 
--- TODO(jmc): generalize to rings, once `Module.rank` is generalized
-theorem dual_rank_eq [FiniteDimensional K V] :
+theorem dual_rank_eq [Module.Finite K V] :
     Cardinal.lift.{u₁,u₂} (Module.rank K V) = Module.rank K (Dual K V) :=
-  (Basis.ofVectorSpace K V).dual_rank_eq
+  (Module.Free.chooseBasis K V).dual_rank_eq
 #align module.dual_rank_eq Module.dual_rank_eq
 
 -- Porting note: broken dot notation lean4#1910 LinearMap.range
-theorem erange_coe [FiniteDimensional K V] : LinearMap.range (eval K V) = ⊤ :=
-  letI : IsNoetherian K V := IsNoetherian.iff_fg.2 inferInstance
-  (Basis.ofVectorSpace K V).eval_range
+theorem erange_coe [Module.Finite K V] : LinearMap.range (eval K V) = ⊤ :=
+  (Module.Free.chooseBasis K V).eval_range
 #align module.erange_coe Module.erange_coe
 
 section IsReflexive
@@ -593,12 +591,9 @@ class IsReflexive : Prop where
 lemma bijective_dual_eval [IsReflexive R M] : Bijective $ Dual.eval R M :=
   IsReflexive.bijective_dual_eval'
 
-instance IsReflexive.of_finite_of_free [Finite R M] [Free R M] : IsReflexive R M := by
-  cases' h : subsingleton_or_nontrivial R
-  · have := Module.subsingleton R M
-    exact ⟨⟨fun x y _ ↦ by simp, fun x ↦ ⟨0, by simp⟩⟩⟩
-  · exact ⟨⟨LinearMap.ker_eq_bot.mp (Free.chooseBasis R M).eval_ker,
-            LinearMap.range_eq_top.mp (Free.chooseBasis R M).eval_range⟩⟩
+instance IsReflexive.of_finite_of_free [Finite R M] [Free R M] : IsReflexive R M where
+  bijective_dual_eval' := ⟨LinearMap.ker_eq_bot.mp (Free.chooseBasis R M).eval_ker,
+                           LinearMap.range_eq_top.mp (Free.chooseBasis R M).eval_range⟩
 
 variable [IsReflexive R M]
 
@@ -1675,8 +1670,6 @@ variable (R M N)
 
 variable [Module.Finite R M] [Module.Finite R N] [Module.Free R M] [Module.Free R N]
 
-variable [Nontrivial R]
-
 /--
 A linear equivalence between `Dual M ⊗ Dual N` and `Dual (M ⊗ N)` when `M` and `N` are finite free
 modules. It sends `f ⊗ g` to the composition of `TensorProduct.map f g` with the natural

Mathlib/LinearAlgebra/FreeModule/Basic.lean

@@ -80,9 +80,9 @@ variable [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M]
 variable [AddCommMonoid N] [Module R N]
 
 /-- If `Module.Free R M` then `ChooseBasisIndex R M` is the `ι` which indexes the basis
-  `ι → M`. -/
-def ChooseBasisIndex :=
-  (exists_basis (R := R) (M := M)).some.1
+  `ι → M`. Note that this is defined such that this type is finite if `R` is trivial. -/
+def ChooseBasisIndex : Type _ :=
+  ((Module.free_iff_set R M).mp ‹_›).choose
 #align module.free.choose_basis_index Module.Free.ChooseBasisIndex
 
 /-- There is no hope of computing this, but we add the instance anyway to avoid fumbling with
@@ -92,7 +92,7 @@ noncomputable instance : DecidableEq (ChooseBasisIndex R M) := Classical.decEq _
 /-- If `Module.Free R M` then `chooseBasis : ι → M` is the basis.
 Here `ι = ChooseBasisIndex R M`. -/
 noncomputable def chooseBasis : Basis (ChooseBasisIndex R M) R M :=
-  (exists_basis (R := R) (M := M)).some.2
+  ((Module.free_iff_set R M).mp ‹_›).choose_spec.some
 #align module.free.choose_basis Module.Free.chooseBasis
 
 /-- The isomorphism `M ≃ₗ[R] (ChooseBasisIndex R M →₀ R)`. -/

Mathlib/LinearAlgebra/FreeModule/Finite/Basic.lean

@@ -31,12 +31,16 @@ section Ring
 
 variable [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M]
 
-/-- If a free module is finite, then any basis is finite. -/
-noncomputable instance ChooseBasisIndex.fintype [Nontrivial R] [Module.Finite R M] :
+/-- If a free module is finite, then the arbitrary basis is finite. -/
+noncomputable instance ChooseBasisIndex.fintype [Module.Finite R M] :
     Fintype (Module.Free.ChooseBasisIndex R M) := by
-  obtain ⟨h⟩ := id ‹Module.Finite R M›
-  choose s hs using h
-  exact basisFintypeOfFiniteSpans (↑s) hs (chooseBasis _ _)
+  refine @Fintype.ofFinite _ ?_
+  cases subsingleton_or_nontrivial R
+  · have := Module.subsingleton R M
+    rw [ChooseBasisIndex]
+    infer_instance
+  · obtain ⟨s, hs⟩ := id ‹Module.Finite R M›
+    exact basis_finite_of_finite_spans (↑s) s.finite_toSet hs (chooseBasis _ _)
 #align module.free.choose_basis_index.fintype Module.Free.ChooseBasisIndex.fintype
 
 end Ring

Mathlib/LinearAlgebra/FreeModule/Finite/Rank.lean

@@ -83,10 +83,7 @@ variable [AddCommGroup N] [Module R N] [Module.Free R N] [Module.Finite R N]
 
 /-- The finrank of a free module `M` over `R` is the cardinality of `ChooseBasisIndex R M`. -/
 theorem finrank_eq_card_chooseBasisIndex :
-    finrank R M =
-      @card (ChooseBasisIndex R M)
-        (@ChooseBasisIndex.fintype R M _ _ _ _ (nontrivial_of_invariantBasisNumber R) _) := by
-  letI := nontrivial_of_invariantBasisNumber R
+    finrank R M = card (ChooseBasisIndex R M) := by
   simp [finrank, rank_eq_card_chooseBasisIndex]
 #align finite_dimensional.finrank_eq_card_choose_basis_index FiniteDimensional.finrank_eq_card_chooseBasisIndex
 

Mathlib/LinearAlgebra/Trace.lean

@@ -157,7 +157,7 @@ theorem trace_eq_contract_of_basis' [Fintype ι] [DecidableEq ι] (b : Basis ι
 
 variable (R M)
 
-variable [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] [Nontrivial R]
+variable [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N]
 
 /-- When `M` is finite free, the trace of a linear map correspond to the contraction pairing under
 the isomorphism `End(M) ≃ M* ⊗ M`-/
@@ -182,6 +182,7 @@ theorem trace_eq_contract' :
 /-- The trace of the identity endomorphism is the dimension of the free module -/
 @[simp]
 theorem trace_one : trace R M 1 = (finrank R M : R) := by
+  cases subsingleton_or_nontrivial R; simp
   have b := Module.Free.chooseBasis R M
   rw [trace_eq_matrix_trace R b, toMatrix_one, finrank_eq_card_chooseBasisIndex]
   simp