feat: Over a finite ring, a module is finite iff it is finite dimensional (#17707)

From PFR

Author: YaelDillies

Mathlib/FieldTheory/AxGrothendieck.lean

@@ -48,8 +48,7 @@ theorem ax_grothendieck_of_locally_finite {ι K R : Type*} [Field K] [Finite K]
         (mem_union_left _ (mem_biUnion.2 ⟨i, mem_univ _, mem_image_of_mem _ hk⟩))
     letI := isNoetherian_adjoin_finset s fun x _ => Algebra.IsIntegral.isIntegral (R := K) x
     letI := Module.IsNoetherian.finite K (Algebra.adjoin K (s : Set R))
-    letI : Finite (Algebra.adjoin K (s : Set R)) :=
-      FiniteDimensional.finite_of_finite K (Algebra.adjoin K (s : Set R))
+    letI : Finite (Algebra.adjoin K (s : Set R)) := Module.finite_of_finite K
     -- The restriction of the polynomial map, `ps`, to the subalgebra generated by `s`
     let res : (ι → Algebra.adjoin K (s : Set R)) → ι → Algebra.adjoin K (s : Set R) := fun x i =>
       ⟨eval (fun j : ι => (x j : R)) (ps i), eval_mem (hs₁ _) fun i => (x i).2⟩

Mathlib/FieldTheory/PrimitiveElement.lean

@@ -63,7 +63,7 @@ theorem exists_primitive_element_of_finite_top [Finite E] : ∃ α : E, F⟮α
 /-- Primitive element theorem for finite dimensional extension of a finite field. -/
 theorem exists_primitive_element_of_finite_bot [Finite F] [FiniteDimensional F E] :
     ∃ α : E, F⟮α⟯ = ⊤ :=
-  haveI : Finite E := FiniteDimensional.finite_of_finite F E
+  haveI : Finite E := Module.finite_of_finite F
   exists_primitive_element_of_finite_top F E
 
 end PrimitiveElementFinite

Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

@@ -107,11 +107,6 @@ instance finiteDimensional_pi' {ι : Type*} [Finite ι] (M : ι → Type*) [∀
 noncomputable def fintypeOfFintype [Fintype K] [FiniteDimensional K V] : Fintype V :=
   Module.fintypeOfFintype (@finsetBasis K V _ _ _ (iff_fg.2 inferInstance))
 
-theorem finite_of_finite [Finite K] [FiniteDimensional K V] : Finite V := by
-  cases nonempty_fintype K
-  haveI := fintypeOfFintype K V
-  infer_instance
-
 variable {K V}
 
 /-- If a vector space has a finite basis, then it is finite-dimensional. -/

Mathlib/RingTheory/Finiteness.lean

@@ -537,6 +537,22 @@ lemma exists_fin' [Module.Finite R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[
   refine ⟨n, Basis.constr (Pi.basisFun R _) ℕ s, ?_⟩
   rw [← LinearMap.range_eq_top, Basis.constr_range, hs]
 
+variable (R) in
+lemma _root_.Module.finite_of_finite [Finite R] [Module.Finite R M] : Finite M := by
+  obtain ⟨n, f, hf⟩ := exists_fin' R M; exact .of_surjective f hf
+
+@[deprecated (since := "2024-10-13")]
+alias _root_.FiniteDimensional.finite_of_finite := finite_of_finite
+
+-- See note [lower instance priority]
+instance (priority := 100) of_finite [Finite M] : Module.Finite R M := by
+  cases nonempty_fintype M
+  exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Submodule.span_univ⟩⟩
+
+/-- A module over a finite ring has finite dimension iff it is finite. -/
+lemma _root_.Module.finite_iff_finite [Finite R] : Module.Finite R M ↔ Finite M :=
+  ⟨fun _ ↦ finite_of_finite R, fun _ ↦ .of_finite⟩
+
 theorem of_surjective [hM : Module.Finite R M] (f : M →ₗ[R] N) (hf : Surjective f) :
     Module.Finite R N :=
   ⟨by
@@ -620,6 +636,12 @@ instance span_singleton (x : M) : Module.Finite R (R ∙ x) :=
 instance span_finset (s : Finset M) : Module.Finite R (span R (s : Set M)) :=
   ⟨(Submodule.fg_top _).mpr ⟨s, rfl⟩⟩
 
+lemma _root_.Set.Finite.submoduleSpan [Finite R] {s : Set M} (hs : s.Finite) :
+    (Submodule.span R s : Set M).Finite := by
+  lift s to Finset M using hs
+  rw [Set.Finite, ← Module.finite_iff_finite (R := R)]
+  dsimp
+  infer_instance
 
 theorem Module.End.isNilpotent_iff_of_finite {R M : Type*} [CommSemiring R] [AddCommMonoid M]
     [Module R M] [Module.Finite R M] {f : End R M} :

Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

@@ -166,10 +166,10 @@ instance finiteDimensional_of_noetherian [IsNoetherian R S] :
     (LinearMap.range_eq_top.mpr Ideal.Quotient.mk_surjective)
   exact Algebra.algebra_ext _ _ (fun r => rfl)
 
+-- We want to be able to refer to `hfin`
+set_option linter.unusedVariables false in
 lemma finite_of_finite [IsNoetherian R S] (hfin : Finite (ResidueField R)) :
-    Finite (ResidueField S) := by
-  have := @finiteDimensional_of_noetherian R S
-  exact FiniteDimensional.finite_of_finite (ResidueField R) (ResidueField S)
+    Finite (ResidueField S) := Module.finite_of_finite (ResidueField R)
 
 end FiniteDimensional