chore: tidy results around Module.Finite (leanprover-community#33614)

In particular this replaces many chains of `Module.finite_def` and `Submodule.fg_top` with `Module.Finite.iff_fg`, or aliases for the forward and reverse implications.

This also golfs some `FiniteDimensional` results in terms of their `Finite` counterparts, and adds `Submodule.fg_range` as a shorthand for a common case of `Submodule.fg_map`.

Author: eric-wieser

Mathlib/Algebra/Module/FinitePresentation.lean

@@ -154,7 +154,7 @@ lemma Module.finitePresentation_of_projective [Projective R M] [Module.Finite R
     FinitePresentation R M :=
   have ⟨_n, _f, _g, surj, _, hfg⟩ := Finite.exists_comp_eq_id_of_projective R M
   Module.finitePresentation_of_free_of_surjective _ surj
-    (Finite.iff_fg.mp <| LinearMap.ker_eq_range_of_comp_eq_id hfg ▸ inferInstance)
+    (LinearMap.ker_eq_range_of_comp_eq_id hfg ▸ .of_finite)
 
 variable {ι} [Finite ι]
 
@@ -215,15 +215,14 @@ lemma Module.finitePresentation_of_ker [Module.FinitePresentation R N]
   obtain ⟨s, hs⟩ : (⊤ : Submodule R M).FG := by
     apply Submodule.fg_of_fg_map_of_fg_inf_ker l
     · rw [Submodule.map_top, LinearMap.range_eq_top.mpr hl]; exact Module.Finite.fg_top
-    · rw [top_inf_eq, ← Submodule.fg_top]; exact Module.Finite.fg_top
+    · rw [top_inf_eq, ← Module.Finite.iff_fg]; infer_instance
   refine ⟨s, hs, ?_⟩
   let π := Finsupp.linearCombination R ((↑) : s → M)
   have H : Function.Surjective π :=
     LinearMap.range_eq_top.mp
       (by rw [range_linearCombination, Subtype.range_val, ← hs])
-  have inst : Module.Finite R (LinearMap.ker (l ∘ₗ π)) := by
-    constructor
-    rw [Submodule.fg_top]; exact Module.FinitePresentation.fg_ker _ (hl.comp H)
+  have inst : Module.Finite R (LinearMap.ker (l ∘ₗ π)) :=
+    .of_fg <| Module.FinitePresentation.fg_ker _ (hl.comp H)
   let f : LinearMap.ker (l ∘ₗ π) →ₗ[R] LinearMap.ker l := LinearMap.restrict π (fun x ↦ id)
   have e : π ∘ₗ Submodule.subtype _ = Submodule.subtype _ ∘ₗ f := by ext; rfl
   have hf : Function.Surjective f := by
@@ -255,8 +254,8 @@ lemma Module.finitePresentation_of_split_exact
   refine Module.finitePresentation_of_surjective (LinearMap.fst _ _ _ ∘ₗ e.toLinearMap)
     (Prod.fst_surjective.comp e.surjective) ?_
   rw [LinearMap.ker_comp, Submodule.comap_equiv_eq_map_symm,
-    LinearMap.exact_iff.mp Function.Exact.inr_fst, ← Submodule.map_top]
-  exact .map _ (.map _ (Module.Finite.fg_top))
+    LinearMap.exact_iff.mp Function.Exact.inr_fst, ← LinearMap.range_comp]
+  exact Submodule.fg_range _
 
 /-- Given an exact sequence `0 → M → N → P → 0`
 with `N` finitely presented and `P` projective, then `M` is also finitely presented. -/
@@ -323,9 +322,8 @@ lemma Module.FinitePresentation.trans (S : Type*) [CommRing S] [Algebra R S]
   · obtain ⟨a, ha⟩ := K.mkQ_surjective (e m)
     exact ⟨a, by simp [f, ha]⟩
   · have : Module.Finite S
-        (Submodule.restrictScalars R (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ))) := by
-      change Module.Finite S (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ))
-      simpa [Finite.iff_fg]
+        (Submodule.restrictScalars R (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ))) :=
+      .of_fg <| show (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ)).FG by simpa
     simp only [f, LinearMap.ker_restrictScalars, ← Module.Finite.iff_fg]
     exact Module.Finite.trans S _
 
@@ -340,11 +338,10 @@ instance {A} [CommRing A] [Algebra R A] [Module.FinitePresentation R M] :
   have : Function.Exact ((LinearMap.ker f).subtype.baseChange A) (f.baseChange A) :=
     lTensor_exact A f.exact_subtype_ker_map hf
   rw [LinearMap.exact_iff] at this
-  rw [this, ← Submodule.map_top]
-  apply Submodule.FG.map
+  rw [this]
   have : Module.Finite R (LinearMap.ker f) :=
-    ⟨(Submodule.fg_top _).mpr (Module.FinitePresentation.fg_ker f hf)⟩
-  exact Module.Finite.fg_top (R := A) (M := A ⊗[R] LinearMap.ker f)
+    .of_fg (Module.FinitePresentation.fg_ker f hf)
+  exact Submodule.fg_range _
 
 open TensorProduct in
 lemma FinitePresentation.of_isBaseChange

Mathlib/Algebra/Module/ZLattice/Basic.lean

@@ -486,7 +486,7 @@ theorem ZLattice.FG [hs : IsZLattice K L] : L.FG := by
 @[deprecated (since := "2025-08-11")] alias Zlattice.FG := ZLattice.FG
 
 theorem ZLattice.module_finite [IsZLattice K L] : Module.Finite ℤ L :=
-  Module.Finite.iff_fg.mpr (ZLattice.FG K L)
+  .of_fg (ZLattice.FG K L)
 
 instance instModuleFinite_of_discrete_submodule {E : Type*} [NormedAddCommGroup E]
     [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology L] :

Mathlib/Analysis/Normed/Module/FiniteDimension.lean

@@ -390,17 +390,16 @@ with norm at most `R` which is at distance at least `1` of all these points. -/
 theorem exists_norm_le_le_norm_sub_of_finset {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R)
     (h : ¬FiniteDimensional 𝕜 E) (s : Finset E) : ∃ x : E, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖ := by
   let F := Submodule.span 𝕜 (s : Set E)
-  haveI : FiniteDimensional 𝕜 F :=
-    Module.finite_def.2
-      ((Submodule.fg_top _).2 (Submodule.fg_def.2 ⟨s, Finset.finite_toSet _, rfl⟩))
+  have hF : F.FG := ⟨s, rfl⟩
+  haveI : FiniteDimensional 𝕜 F := .of_fg hF
   have Fclosed : IsClosed (F : Set E) := Submodule.closed_of_finiteDimensional _
   have : ∃ x, x ∉ F := by
     contrapose! h
     have : (⊤ : Submodule 𝕜 E) = F := by
       ext x
       simp [h]
-    have : FiniteDimensional 𝕜 (⊤ : Submodule 𝕜 E) := by rwa [this]
-    exact Module.finite_def.2 ((Submodule.fg_top _).1 (Module.finite_def.1 this))
+    rw [← this] at hF
+    exact .of_fg_top hF
   obtain ⟨x, xR, hx⟩ : ∃ x : E, ‖x‖ ≤ R ∧ ∀ y : E, y ∈ F → 1 ≤ ‖x - y‖ :=
     riesz_lemma_of_norm_lt hc hR Fclosed this
   have hx' : ∀ y : E, y ∈ F → 1 ≤ ‖y - x‖ := by

Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean

@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Module.Projective
 public import Mathlib.LinearAlgebra.Dimension.Finite
 public import Mathlib.LinearAlgebra.FiniteDimensional.Defs
 public import Mathlib.LinearAlgebra.Matrix.ToLin
+import Mathlib.RingTheory.Finiteness.Lattice
 
 /-!
 # Finite-dimensional vector spaces
@@ -187,31 +188,23 @@ instance finiteDimensional_inf_right (S₁ S₂ : Submodule K V) [FiniteDimensio
 /-- The sup of two finite-dimensional submodules is
 finite-dimensional. -/
 instance finiteDimensional_sup (S₁ S₂ : Submodule K V) [h₁ : FiniteDimensional K S₁]
-    [h₂ : FiniteDimensional K S₂] : FiniteDimensional K (S₁ ⊔ S₂ : Submodule K V) := by
-  unfold FiniteDimensional at *
-  rw [finite_def] at *
-  exact (fg_top _).2 (((fg_top S₁).1 h₁).sup ((fg_top S₂).1 h₂))
+    [h₂ : FiniteDimensional K S₂] : FiniteDimensional K (S₁ ⊔ S₂ : Submodule K V) :=
+  finite_sup _ _
 
 /-- The submodule generated by a finite supremum of finite-dimensional submodules is
 finite-dimensional.
 
 Note that strictly this only needs `∀ i ∈ s, FiniteDimensional K (S i)`, but that doesn't
 work well with typeclass search. -/
 instance finiteDimensional_finset_sup {ι : Type*} (s : Finset ι) (S : ι → Submodule K V)
-    [∀ i, FiniteDimensional K (S i)] : FiniteDimensional K (s.sup S : Submodule K V) := by
-  refine
-    @Finset.sup_induction _ _ _ _ s S (fun i => FiniteDimensional K ↑i) (finiteDimensional_bot K V)
-      ?_ fun i _ => by infer_instance
-  intro S₁ hS₁ S₂ hS₂
-  exact Submodule.finiteDimensional_sup S₁ S₂
+    [∀ i, FiniteDimensional K (S i)] : FiniteDimensional K (s.sup S : Submodule K V) :=
+  Submodule.finite_finset_sup _ _
 
 /-- The submodule generated by a supremum of finite-dimensional submodules, indexed by a finite
 sort is finite-dimensional. -/
 instance finiteDimensional_iSup {ι : Sort*} [Finite ι] (S : ι → Submodule K V)
-    [∀ i, FiniteDimensional K (S i)] : FiniteDimensional K ↑(⨆ i, S i) := by
-  cases nonempty_fintype (PLift ι)
-  rw [← iSup_plift_down, ← Finset.sup_univ_eq_iSup]
-  exact Submodule.finiteDimensional_finset_sup _ _
+    [∀ i, FiniteDimensional K (S i)] : FiniteDimensional K ↑(⨆ i, S i) :=
+  Submodule.finite_iSup _
 
 end DivisionRing
 

Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

@@ -237,7 +237,7 @@ variable [DivisionRing K] [AddCommGroup V] [Module K V]
 
 /-- A submodule is finitely generated if and only if it is finite-dimensional -/
 theorem fg_iff_finiteDimensional (s : Submodule K V) : s.FG ↔ FiniteDimensional K s :=
-  (fg_top s).symm.trans Module.finite_def.symm
+  Module.Finite.iff_fg.symm
 
 end DivisionRing
 

Mathlib/RingTheory/Finiteness/Basic.lean

@@ -87,6 +87,11 @@ theorem FG.map {N : Submodule R M} (hs : N.FG) : (N.map f).FG :=
   let ⟨t, ht⟩ := fg_def.1 hs
   fg_def.2 ⟨f '' t, ht.1.image _, by rw [span_image, ht.2]⟩
 
+/-- Maps from a finite module have a finite range. -/
+@[simp] lemma fg_range [Module.Finite R M] (f : M →ₛₗ[σ] P) : f.range.FG := by
+  rw [LinearMap.range_eq_map]
+  exact Module.Finite.fg_top.map f
+
 theorem fg_of_fg_map_injective (hf : Function.Injective f) {N : Submodule R M}
     (hfn : (N.map f).FG) : N.FG :=
   let ⟨t, ht⟩ := hfn
@@ -97,6 +102,10 @@ theorem fg_of_fg_map_injective (hf : Function.Injective f) {N : Submodule R M}
       rw [← LinearMap.coe_range, ← span_le, ht, ← map_top]
       exact map_mono le_top⟩
 
+theorem fg_map_iff (hf : Function.Injective f) {N : Submodule R M} :
+    (N.map f).FG ↔ N.FG :=
+  ⟨(fg_of_fg_map_injective _ hf ·), (.map _)⟩
+
 end
 
 variable {P : Type*} [AddCommMonoid P] [Module R P]
@@ -108,10 +117,13 @@ theorem fg_of_fg_map {R M P : Type*} [Ring R] [AddCommGroup M] [Module R M] [Add
     (hfn : (N.map f).FG) : N.FG :=
   fg_of_fg_map_injective f (LinearMap.ker_eq_bot.1 hf) hfn
 
-theorem fg_top (N : Submodule R M) : (⊤ : Submodule R N).FG ↔ N.FG :=
-  ⟨fun h => N.range_subtype ▸ map_top N.subtype ▸ h.map _, fun h =>
-    fg_of_fg_map_injective N.subtype Subtype.val_injective <| by rwa [map_top, range_subtype]⟩
+/-- The top submodule of another submodule `N` is FG iff `N` is `FG`.
+
+See also `Module.Finite.fg_top`. -/
+protected theorem fg_top (N : Submodule R M) : (⊤ : Submodule R N).FG ↔ N.FG := by
+  rw [← fg_map_iff N.subtype Subtype.val_injective, map_top, range_subtype]
 
+/-- See also `Module.Finite.equiv_iff`. -/
 theorem fg_of_linearEquiv (e : M ≃ₗ[R] P) (h : (⊤ : Submodule R P).FG) : (⊤ : Submodule R M).FG :=
   e.symm.range ▸ map_top (e.symm : P →ₗ[R] M) ▸ h.map _
 
@@ -294,28 +306,36 @@ instance [Module.Finite R M] : Module.Finite R Mᵐᵒᵖ := equiv (MulOpposite.
 
 instance ulift [Module.Finite R M] : Module.Finite R (ULift M) := equiv ULift.moduleEquiv.symm
 
+/-- A submodule is finite as a module iff it is finitely generated. -/
 theorem iff_fg {N : Submodule R M} : Module.Finite R N ↔ N.FG := Module.finite_def.trans N.fg_top
 
+/-- A finitely-generated submodule is finite as a module. -/
+alias ⟨_, of_fg⟩ := iff_fg
+
+/-- A submodule that is finite as a module is finitely generated. -/
+theorem _root_.Submodule.FG.of_finite {N : Submodule R M} [Module.Finite R N] : N.FG :=
+  iff_fg.1 ‹_›
+
 variable (R M)
 
-instance bot : Module.Finite R (⊥ : Submodule R M) := iff_fg.mpr fg_bot
+instance bot : Module.Finite R (⊥ : Submodule R M) := .of_fg fg_bot
 
-instance top [Module.Finite R M] : Module.Finite R (⊤ : Submodule R M) := iff_fg.mpr fg_top
+instance top [Module.Finite R M] : Module.Finite R (⊤ : Submodule R M) := .of_fg fg_top
 
 variable {M}
 
 /-- The submodule generated by a finite set is `R`-finite. -/
 theorem span_of_finite {A : Set M} (hA : Set.Finite A) :
     Module.Finite R (Submodule.span R A) :=
-  ⟨(Submodule.fg_top _).mpr ⟨hA.toFinset, hA.coe_toFinset.symm ▸ rfl⟩⟩
+  .of_fg ⟨hA.toFinset, hA.coe_toFinset.symm ▸ rfl⟩
 
 /-- The submodule generated by a single element is `R`-finite. -/
 instance span_singleton (x : M) : Module.Finite R (R ∙ x) :=
   Module.Finite.span_of_finite R <| Set.finite_singleton _
 
 /-- The submodule generated by a finset is `R`-finite. -/
 instance span_finset (s : Finset M) : Module.Finite R (span R (s : Set M)) :=
-  ⟨(Submodule.fg_top _).mpr ⟨s, rfl⟩⟩
+  .of_fg ⟨s, rfl⟩
 
 variable {R}
 
@@ -364,8 +384,8 @@ variable {R V} [Ring R] [AddCommGroup V] [Module R V]
 /-- The sup of two fg submodules is finite. Also see `Submodule.FG.sup`. -/
 instance finite_sup (S₁ S₂ : Submodule R V) [h₁ : Module.Finite R S₁]
     [h₂ : Module.Finite R S₂] : Module.Finite R (S₁ ⊔ S₂ : Submodule R V) := by
-  rw [finite_def] at *
-  exact (fg_top _).2 (((fg_top S₁).1 h₁).sup ((fg_top S₂).1 h₂))
+  rw [Finite.iff_fg] at *
+  exact .sup h₁ h₂
 
 /-- The submodule generated by a finite supremum of finite-dimensional submodules is
 finite-dimensional.

Mathlib/RingTheory/Finiteness/Defs.lean

@@ -118,29 +118,31 @@ variable (R A B M N : Type*)
 
 /-- A module over a semiring is `Module.Finite` if it is finitely generated as a module. -/
 protected class Module.Finite [Semiring R] [AddCommMonoid M] [Module R M] : Prop where
-  fg_top : (⊤ : Submodule R M).FG
+  of_fg_top ::
+    fg_top : (⊤ : Submodule R M).FG
 
 attribute [inherit_doc Module.Finite] Module.Finite.fg_top
 
 namespace Module
 
 variable [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
 
+/-- See also `Module.Finite.iff_fg` for a version when `M` is itself a submodule. -/
 theorem finite_def {R M} [Semiring R] [AddCommMonoid M] [Module R M] :
     Module.Finite R M ↔ (⊤ : Submodule R M).FG :=
-  ⟨fun h => h.1, fun h => ⟨h⟩⟩
+  ⟨(·.fg_top), .of_fg_top⟩
 
 namespace Finite
 
 open Submodule Set
 
 theorem iff_addMonoid_fg {M : Type*} [AddCommMonoid M] : Module.Finite ℕ M ↔ AddMonoid.FG M :=
-  ⟨fun h => AddMonoid.fg_def.2 <| (Submodule.fg_iff_addSubmonoid_fg ⊤).1 (finite_def.1 h), fun h =>
-    finite_def.2 <| (Submodule.fg_iff_addSubmonoid_fg ⊤).2 (AddMonoid.fg_def.1 h)⟩
+  ⟨fun h => AddMonoid.fg_def.2 <| (Submodule.fg_iff_addSubmonoid_fg ⊤).1 h.fg_top, fun h =>
+    .of_fg_top <| (Submodule.fg_iff_addSubmonoid_fg ⊤).2 (AddMonoid.fg_def.1 h)⟩
 
 theorem iff_addGroup_fg {G : Type*} [AddCommGroup G] : Module.Finite ℤ G ↔ AddGroup.FG G :=
-  ⟨fun h => AddGroup.fg_def.2 <| (Submodule.fg_iff_addSubgroup_fg ⊤).1 (finite_def.1 h), fun h =>
-    finite_def.2 <| (Submodule.fg_iff_addSubgroup_fg ⊤).2 (AddGroup.fg_def.1 h)⟩
+  ⟨fun h => AddGroup.fg_def.2 <| (Submodule.fg_iff_addSubgroup_fg ⊤).1 h.fg_top, fun h =>
+    .of_fg_top <| (Submodule.fg_iff_addSubgroup_fg ⊤).2 (AddGroup.fg_def.1 h)⟩
 
 variable {R M N}
 

Mathlib/RingTheory/Finiteness/Finsupp.lean

@@ -117,7 +117,7 @@ theorem _root_.Module.Finite.of_submodule_quotient (N : Submodule R M) [Module.F
     [Module.Finite R (M ⧸ N)] : Module.Finite R M where
   fg_top := fg_of_fg_map_of_fg_inf_ker N.mkQ
     (by simpa only [map_top, range_mkQ] using Module.finite_def.mp ‹_›) <| by
-    simpa only [top_inf_eq, ker_mkQ] using Module.Finite.iff_fg.mp ‹_›
+    simpa only [top_inf_eq, ker_mkQ] using .of_finite
 
 end Submodule
 

Mathlib/RingTheory/Finiteness/NilpotentKer.lean

@@ -47,7 +47,7 @@ lemma Module.finite_of_surjective_of_ker_le_nilradical
     · simpa [LinearMap.range_eq_top_of_surjective (φ.toLinearMap.restrictScalars R) hφ] using
         Module.Finite.fg_top
     · have : Module.Finite R ((S ⧸ I) ⊗[S] ↑(I ^ n)) := by
-        have : Module.Finite S ↑(I ^ n) := Module.Finite.iff_fg.mpr (.pow hf₃ _)
+        have : Module.Finite S ↑(I ^ n) := .of_fg (.pow hf₃ _)
         exact .trans (S ⧸ I) _
       let ψ : (S ⧸ I) ⊗[S] ↑(I ^ n) →ₗ[S] (S ⧸ I ^ (n + 1)) := by
         refine ?_ ∘ₗ (TensorProduct.quotTensorEquivQuotSMul _ I).toLinearMap

Mathlib/RingTheory/Flat/EquationalCriterion.lean

@@ -273,7 +273,7 @@ theorem exists_factorization_of_isFinitelyPresented [Flat R M] {P : Type*} [AddC
     [Module R P] [FinitePresentation R P] (h₁ : P →ₗ[R] M) :
       ∃ (k : ℕ) (h₂ : P →ₗ[R] (Fin k →₀ R)) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂ := by
   have ⟨_, K, ϕ, hK⟩ := FinitePresentation.exists_fin R P
-  haveI : Module.Finite R K := Module.Finite.iff_fg.mpr hK
+  haveI : Module.Finite R K := .of_fg hK
   have : (h₁ ∘ₗ ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0 := by
     simp_rw [comp_assoc, (LinearMap.exact_subtype_mkQ K).linearMap_comp_eq_zero, comp_zero]
   obtain ⟨k, a, y, hay, ha⟩ := exists_factorization_of_comp_eq_zero_of_free this