feat: generalize Module.Finite.trans (#9380)

Add `span_eq_closure` and `closure_induction` which say that `Submodule.span R s` is generated by `R • s` as an AddSubmonoid. I feel that the existing `span_induction` should be replaced by `closure_induction` as the latter is stronger, and allow us to remove the commutativity condition in `span_smul_of_span_eq_top` in Algebra/Tower and generalize `Module.Finite.trans` to allow a non-commutative base ring.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Author: alreadydone

Mathlib/Algebra/Algebra/Tower.lean

@@ -305,39 +305,31 @@ theorem smul_mem_span_smul_of_mem {s : Set S} {t : Set A} {k : S} (hks : k ∈ s
     fun b c hc => by rw [IsScalarTower.smul_assoc]; exact smul_mem _ _ hc
 #align submodule.smul_mem_span_smul_of_mem Submodule.smul_mem_span_smul_of_mem
 
-variable [SMulCommClass R S A]
-
-theorem smul_mem_span_smul {s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S} {x : A}
-    (hx : x ∈ span R t) : k • x ∈ span R (s • t) :=
-  span_induction hx (fun x hx => smul_mem_span_smul_of_mem (hs.symm ▸ mem_top) hx)
-    (by rw [smul_zero]; exact zero_mem _)
-    (fun x y ihx ihy => by rw [smul_add]; exact add_mem ihx ihy)
-    fun c x hx => smul_comm c k x ▸ smul_mem _ _ hx
-#align submodule.smul_mem_span_smul Submodule.smul_mem_span_smul
-
-theorem smul_mem_span_smul' {s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S} {x : A}
-    (hx : x ∈ span R (s • t)) : k • x ∈ span R (s • t) :=
-  span_induction hx
-    (fun x hx => by
-      let ⟨p, _hp, q, hq, hpq⟩ := Set.mem_smul.1 hx
-      rw [← hpq, smul_smul]
-      exact smul_mem_span_smul_of_mem (hs.symm ▸ mem_top) hq)
-    (by rw [smul_zero]; exact zero_mem _)
-    (fun x y ihx ihy => by rw [smul_add]; exact add_mem ihx ihy)
-    fun c x hx => smul_comm c k x ▸ smul_mem _ _ hx
-#align submodule.smul_mem_span_smul' Submodule.smul_mem_span_smul'
-
 theorem span_smul_of_span_eq_top {s : Set S} (hs : span R s = ⊤) (t : Set A) :
     span R (s • t) = (span S t).restrictScalars R :=
   le_antisymm
-    (span_le.2 fun _x hx =>
-      let ⟨p, _q, _hps, hqt, hpqx⟩ := Set.mem_smul.1 hx
-      hpqx ▸ (span S t).smul_mem p (subset_span hqt))
-    fun _p hp =>
-    span_induction hp (fun x hx => one_smul S x ▸ smul_mem_span_smul hs (subset_span hx))
-      (zero_mem _) (fun _ _ => add_mem) fun _k _x hx => smul_mem_span_smul' hs hx
+    (span_le.2 fun _x ⟨p, _hps, _q, hqt, hpqx⟩ ↦ hpqx ▸ (span S t).smul_mem p (subset_span hqt))
+    fun p hp ↦ closure_induction hp (zero_mem _) (fun _ _ ↦ add_mem) fun s0 y hy ↦ by
+      refine span_induction (hs ▸ mem_top : s0 ∈ span R s)
+        (fun x hx ↦ subset_span ⟨x, hx, y, hy, rfl⟩) ?_ ?_ ?_
+      · rw [zero_smul]; apply zero_mem
+      · intro _ _; rw [add_smul]; apply add_mem
+      · intro r s0 hy; rw [IsScalarTower.smul_assoc]; exact smul_mem _ r hy
 #align submodule.span_smul_of_span_eq_top Submodule.span_smul_of_span_eq_top
 
+-- The following two lemmas were originally used to prove `span_smul_of_span_eq_top`
+-- but are now not needed.
+theorem smul_mem_span_smul' {s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S} {x : A}
+    (hx : x ∈ span R (s • t)) : k • x ∈ span R (s • t) := by
+  rw [span_smul_of_span_eq_top hs] at hx ⊢; exact (span S t).smul_mem k hx
+#align submodule.smul_mem_span_smul' Submodule.smul_mem_span_smul'
+
+theorem smul_mem_span_smul {s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S} {x : A}
+    (hx : x ∈ span R t) : k • x ∈ span R (s • t) := by
+  rw [span_smul_of_span_eq_top hs]
+  exact (span S t).smul_mem k (span_le_restrictScalars R S t hx)
+#align submodule.smul_mem_span_smul Submodule.smul_mem_span_smul
+
 end Module
 
 section Algebra

Mathlib/LinearAlgebra/Span.lean

@@ -180,6 +180,39 @@ theorem span_induction' {p : ∀ x, x ∈ span R s → Prop}
       fun r x hx => Exists.elim hx fun hx' hx => ⟨smul_mem _ _ hx', H2 r _ _ hx⟩
 #align submodule.span_induction' Submodule.span_induction'
 
+open AddSubmonoid in
+theorem span_eq_closure {s : Set M} : (span R s).toAddSubmonoid = closure (@univ R • s) := by
+  refine le_antisymm
+    (fun x hx ↦ span_induction hx (fun x hx ↦ subset_closure ⟨1, trivial, x, hx, one_smul R x⟩)
+      (zero_mem _) (fun _ _ ↦ add_mem) fun r m hm ↦ closure_induction hm ?_ ?_ fun _ _ h h' ↦ ?_)
+    (closure_le.2 ?_)
+  · rintro _ ⟨r, -, m, hm, rfl⟩; exact smul_mem _ _ (subset_span hm)
+  · rintro _ ⟨r', -, m, hm, rfl⟩; exact subset_closure ⟨r * r', trivial, m, hm, mul_smul r r' m⟩
+  · rw [smul_zero]; apply zero_mem
+  · rw [smul_add]; exact add_mem h h'
+
+/-- A variant of `span_induction` that combines `∀ x ∈ s, p x` and `∀ r x, p x → p (r • x)`
+into a single condition `∀ r, ∀ x ∈ s, p (r • x)`, which can be easier to verify. -/
+@[elab_as_elim]
+theorem closure_induction {p : M → Prop} (h : x ∈ span R s) (H0 : p 0)
+    (H1 : ∀ x y, p x → p y → p (x + y)) (H2 : ∀ r : R, ∀ x ∈ s, p (r • x)) : p x := by
+  rw [← mem_toAddSubmonoid, span_eq_closure] at h
+  refine AddSubmonoid.closure_induction h ?_ H0 H1
+  rintro _ ⟨r, -, m, hm, rfl⟩
+  exact H2 r m hm
+
+/-- A dependent version of `Submodule.closure_induction`. -/
+theorem closure_induction' {p : ∀ x, x ∈ span R s → Prop}
+    (H0 : p 0 (Submodule.zero_mem _))
+    (H1 : ∀ x hx y hy, p x hx → p y hy → p (x + y) (Submodule.add_mem _ ‹_› ‹_›))
+    (H2 : ∀ (r x) (h : x ∈ s), p (r • x) (Submodule.smul_mem _ _ <| subset_span h)) {x}
+    (hx : x ∈ span R s) : p x hx := by
+  refine Exists.elim ?_ fun (hx : x ∈ span R s) (hc : p x hx) ↦ hc
+  refine closure_induction hx ⟨zero_mem _, H0⟩
+    (fun x y hx hy ↦ Exists.elim hx fun hx' hx ↦
+      Exists.elim hy fun hy' hy ↦ ⟨add_mem hx' hy', H1 _ _ _ _ hx hy⟩)
+    fun r x hx ↦ ⟨smul_mem _ _ (subset_span hx), H2 r x hx⟩
+
 @[simp]
 theorem span_span_coe_preimage : span R (((↑) : span R s → M) ⁻¹' s) = ⊤ :=
   eq_top_iff.2 fun x ↦ Subtype.recOn x fun x hx _ ↦ by

Mathlib/RingTheory/FiniteType.lean

@@ -461,7 +461,7 @@ theorem mvPolynomial_aeval_of_surjective_of_closure [AddCommMonoid M] [CommSemir
   intro f
   induction' f using induction_on with m f g ihf ihg r f ih
   · have : m ∈ closure S := hS.symm ▸ mem_top _
-    refine' closure_induction this (fun m hm => _) _ _
+    refine' AddSubmonoid.closure_induction this (fun m hm => _) _ _
     · exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
     · exact ⟨1, AlgHom.map_one _⟩
     · rintro m₁ m₂ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
@@ -487,7 +487,7 @@ theorem freeAlgebra_lift_of_surjective_of_closure [CommSemiring R] {S : Set M}
   intro f
   induction' f using induction_on with m f g ihf ihg r f ih
   · have : m ∈ closure S := hS.symm ▸ mem_top _
-    refine' closure_induction this (fun m hm => _) _ _
+    refine' AddSubmonoid.closure_induction this (fun m hm => _) _ _
     · exact ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩
     · exact ⟨1, AlgHom.map_one _⟩
     · rintro m₁ m₂ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
@@ -640,7 +640,7 @@ theorem mvPolynomial_aeval_of_surjective_of_closure [CommMonoid M] [CommSemiring
   intro f
   induction' f using induction_on with m f g ihf ihg r f ih
   · have : m ∈ closure S := hS.symm ▸ mem_top _
-    refine' closure_induction this (fun m hm => _) _ _
+    refine' Submonoid.closure_induction this (fun m hm => _) _ _
     · exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
     · exact ⟨1, AlgHom.map_one _⟩
     · rintro m₁ m₂ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
@@ -665,7 +665,7 @@ theorem freeAlgebra_lift_of_surjective_of_closure [CommSemiring R] {S : Set M}
   intro f
   induction' f using induction_on with m f g ihf ihg r f ih
   · have : m ∈ closure S := hS.symm ▸ mem_top _
-    refine' closure_induction this (fun m hm => _) _ _
+    refine' Submonoid.closure_induction this (fun m hm => _) _ _
     · exact ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩
     · exact ⟨1, AlgHom.map_one _⟩
     · rintro m₁ m₂ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩

Mathlib/RingTheory/Finiteness.lean

@@ -676,7 +676,7 @@ variable {R}
 
 section Algebra
 
-theorem trans {R : Type*} (A M : Type*) [CommSemiring R] [Semiring A] [Algebra R A]
+theorem trans {R : Type*} (A M : Type*) [Semiring R] [Semiring A] [Module R A]
     [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] :
     ∀ [Finite R A] [Finite A M], Finite R M
   | ⟨⟨s, hs⟩⟩, ⟨⟨t, ht⟩⟩ =>