feat(RingTheory/Finiteness): Improve fg_induction (#37484)

- include the FG-hypothesis into motive for `fg_induction`. This is necessary, since it might be that `P (M₁ ⊔ M₂)` is only provable from `P M₁`and `P M₂` if we can use that `M₁` and `M₂` are FG. Also, `M₁.FG` and `M₂.FG` are not provable from `(M₁ ⊔ M₂).FG` in general. This also enables the use of the `induction` tactic with `fg_induction`.
- add `fg_sup_span_induction` that adds one 1-dimensional submodule at a time.
- give expressive names to the induction start and induction step hypotheses.

Co-authored-by: Martin Winter <martin.winter.math@gmail.com>

Author: martinwintermath

Mathlib/RingTheory/Bezout.lean

@@ -38,7 +38,9 @@ theorem iff_span_pair_isPrincipal :
       constructor
       apply Submodule.fg_induction
       · exact fun _ => ⟨⟨_, rfl⟩⟩
-      · rintro _ _ ⟨⟨x, rfl⟩⟩ ⟨⟨y, rfl⟩⟩; rw [← Submodule.span_insert]; exact H _ _
+      · rintro _ _ _ _ ⟨⟨x, rfl⟩⟩ ⟨⟨y, rfl⟩⟩
+        rw [← Submodule.span_insert]
+        exact H _ _
 
 theorem _root_.Function.Surjective.isBezout {S : Type v} [CommRing S] (f : R →+* S)
     (hf : Function.Surjective f) [IsBezout R] : IsBezout S := by

Mathlib/RingTheory/Finiteness/Basic.lean

@@ -127,18 +127,29 @@ protected theorem fg_top (N : Submodule R M) : (⊤ : Submodule R N).FG ↔ N.FG
 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 _
 
-theorem fg_induction (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]
-    (P : Submodule R M → Prop) (h₁ : ∀ x, P (Submodule.span R {x}))
-    (h₂ : ∀ M₁ M₂, P M₁ → P M₂ → P (M₁ ⊔ M₂)) (N : Submodule R M) (hN : N.FG) : P N := by
-  classical
-    obtain ⟨s, rfl⟩ := hN
-    induction s using Finset.induction with
-    | empty =>
-      rw [Finset.coe_empty, span_empty, ← span_zero_singleton]
-      exact h₁ _
-    | insert _ _ _ ih =>
-      rw [Finset.coe_insert, span_insert]
-      exact h₂ _ _ (h₁ _) ih
+theorem fg_induction {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
+    {motive : ∀ N : Submodule R M, N.FG → Prop}
+    (singleton : ∀ x : M, motive (R ∙ x) (fg_span_singleton _))
+    (sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG),
+      motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) (hN₁.sup hN₂))
+    (N : Submodule R M) (hN : N.FG) : motive N hN := by classical
+  obtain ⟨s, rfl⟩ := hN
+  induction s using Finset.induction with
+  | empty => simpa using singleton 0
+  | insert x s hxs ih =>
+    simpa [span_insert, sup_comm] using
+      sup (span R s) (R ∙ x) _ (fg_span_singleton _) ih (singleton x)
+
+theorem fg_sup_span_induction {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
+    {motive : ∀ N : Submodule R M, N.FG → Prop}
+    (bot : motive ⊥ fg_bot)
+    (sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG),
+      motive N hN → motive (N ⊔ (R ∙ x)) (hN.sup <| fg_span_singleton x))
+    (N : Submodule R M) (hN : N.FG) : motive N hN := by classical
+  obtain ⟨s, rfl⟩ := hN
+  induction s using Finset.induction with
+  | empty => simp [bot]
+  | insert x s hxs ih => simpa [span_insert, sup_comm] using sup (span R s) x (by use s) ih
 
 section RestrictScalars
 

Mathlib/RingTheory/Finiteness/Ideal.lean

@@ -49,13 +49,14 @@ theorem fg_ker_comp {R S A : Type*} [CommRing R] [CommRing S] [CommRing A] (f :
 
 theorem exists_radical_pow_le_of_fg {R : Type*} [CommSemiring R] (I : Ideal R) (h : I.radical.FG) :
     ∃ n : ℕ, I.radical ^ n ≤ I := by
-  have := le_refl I.radical
-  revert this
-  refine Submodule.fg_induction _ _ (fun J => J ≤ I.radical → ∃ n : ℕ, J ^ n ≤ I) ?_ ?_ _ h
-  · intro x hx
-    obtain ⟨n, hn⟩ := hx (subset_span (Set.mem_singleton x))
+  suffices hJ : ∀ J : Ideal R, J.FG → J ≤ I.radical → ∃ n : ℕ, J ^ n ≤ I by
+    simpa using hJ I.radical h
+  intro J hJ hJK
+  induction J, hJ using Submodule.fg_induction with
+  | singleton x =>
+    obtain ⟨n, hn⟩ := hJK (subset_span (Set.mem_singleton x))
     exact ⟨n, by rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]⟩
-  · intro J K hJ hK hJK
+  | sup J K _ _ hJ hK =>
     obtain ⟨n, hn⟩ := hJ fun x hx => hJK <| mem_sup_left hx
     obtain ⟨m, hm⟩ := hK fun x hx => hJK <| mem_sup_right hx
     use n + m
@@ -74,15 +75,14 @@ theorem exists_pow_le_of_le_radical_of_fg_radical {R : Type*} [CommSemiring R] {
 lemma exists_pow_le_of_le_radical_of_fg {R : Type*} [CommSemiring R] {I J : Ideal R}
     (h' : I ≤ J.radical) (h : I.FG) :
     ∃ n : ℕ, I ^ n ≤ J := by
-  revert h'
-  apply Submodule.fg_induction _ _ _ _ _ I h
-  · intro x hJ
-    simp only [submodule_span_eq, span_le, Set.singleton_subset_iff, SetLike.mem_coe] at hJ
-    obtain ⟨n, hn⟩ := hJ
+  induction I, h using Submodule.fg_induction with
+  | singleton x =>
+    simp only [submodule_span_eq, span_le, Set.singleton_subset_iff, SetLike.mem_coe] at h'
+    obtain ⟨n, hn⟩ := h'
     refine ⟨n, by simpa [span_singleton_pow, span_le]⟩
-  · intro I₁ I₂ h₁ h₂ hJ
-    obtain ⟨n₁, hn₁⟩ := h₁ (le_sup_left.trans hJ)
-    obtain ⟨n₂, hn₂⟩ := h₂ (le_sup_right.trans hJ)
+  | sup I₁ I₂ _ _ h₁ h₂ =>
+    obtain ⟨n₁, hn₁⟩ := h₁ (le_sup_left.trans h')
+    obtain ⟨n₂, hn₂⟩ := h₂ (le_sup_right.trans h')
     use n₁ + n₂
     exact sup_pow_add_le_pow_sup_pow.trans (sup_le hn₁ hn₂)
 

Mathlib/RingTheory/Flat/EquationalCriterion.lean

@@ -234,14 +234,13 @@ private theorem exists_factorization_of_comp_eq_zero_of_free_aux [Flat R M] {K :
       x = y ∘ₗ a ∧ a ∘ₗ f = 0 := by
   have (K' : Submodule R K) (hK' : K'.FG) : ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] (Fin k →₀ R))
       (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K' ≤ LinearMap.ker (a ∘ₗ f) := by
-    revert n
-    apply Submodule.fg_induction (N := K') (hN := hK')
-    · intro k n f x hfx
-      have : x (f k) = 0 := by simpa using LinearMap.congr_fun hfx k
+    induction K', hK' using Submodule.fg_induction generalizing n with
+    | singleton k =>
+      have : x (f k) = 0 := by simpa using LinearMap.congr_fun h k
       simpa using exists_factorization_of_apply_eq_zero_of_free this
-    · intro K₁ K₂ ih₁ ih₂ n f x hfx
-      obtain ⟨k₁, a₁, y₁, rfl, ha₁⟩ := ih₁ hfx
-      have : y₁ ∘ₗ (a₁ ∘ₗ f) = 0 := by rw [← comp_assoc, hfx]
+    | sup K₁ K₂ _ _ ih₁ ih₂ =>
+      obtain ⟨k₁, a₁, y₁, rfl, ha₁⟩ := ih₁ h
+      have : y₁ ∘ₗ (a₁ ∘ₗ f) = 0 := by rw [← comp_assoc, h]
       obtain ⟨k₂, a₂, y₂, rfl, ha₂⟩ := ih₂ this
       use k₂, a₂ ∘ₗ a₁, y₂
       simp_rw [comp_assoc]