chore: generalize more materials about linear independence over semirings (#20497)

Also add `Finsupp.linearCombination_one_tmul` and `linearIndependent_one_tmul` that connects linear independence to flatness.

Author: alreadydone

Mathlib/LinearAlgebra/Basis/Basic.lean

@@ -161,61 +161,7 @@ theorem basis_singleton_iff {R M : Type*} [Ring R] [Nontrivial R] [AddCommGroup
 
 end Singleton
 
-end Basis
-
-end Module
-
-section Module
-
-open LinearMap
-
-variable {v : ι → M}
-variable [Ring R] [CommRing R₂] [AddCommGroup M]
-variable [Module R M] [Module R₂ M]
-variable {x y : M}
-variable (b : Basis ι R M)
-
-theorem Basis.eq_bot_of_rank_eq_zero [NoZeroDivisors R] (b : Basis ι R M) (N : Submodule R M)
-    (rank_eq : ∀ {m : ℕ} (v : Fin m → N), LinearIndependent R ((↑) ∘ v : Fin m → M) → m = 0) :
-    N = ⊥ := by
-  rw [Submodule.eq_bot_iff]
-  intro x hx
-  contrapose! rank_eq with x_ne
-  refine ⟨1, fun _ => ⟨x, hx⟩, ?_, one_ne_zero⟩
-  rw [Fintype.linearIndependent_iff]
-  rintro g sum_eq i
-  cases' i with _ hi
-  simp only [Function.const_apply, Fin.default_eq_zero, Submodule.coe_mk, Finset.univ_unique,
-    Function.comp_const, Finset.sum_singleton] at sum_eq
-  convert (b.smul_eq_zero.mp sum_eq).resolve_right x_ne
-
-namespace Basis
-
-/-- Any basis is a maximal linear independent set.
--/
-theorem maximal [Nontrivial R] (b : Basis ι R M) : b.linearIndependent.Maximal := fun w hi h => by
-  -- If `w` is strictly bigger than `range b`,
-  apply le_antisymm h
-  -- then choose some `x ∈ w \ range b`,
-  intro x p
-  by_contra q
-  -- and write it in terms of the basis.
-  have e := b.linearCombination_repr x
-  -- This then expresses `x` as a linear combination
-  -- of elements of `w` which are in the range of `b`,
-  let u : ι ↪ w :=
-    ⟨fun i => ⟨b i, h ⟨i, rfl⟩⟩, fun i i' r =>
-      b.injective (by simpa only [Subtype.mk_eq_mk] using r)⟩
-  simp_rw [Finsupp.linearCombination_apply] at e
-  change ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) = ((⟨x, p⟩ : w) : M) at e
-  rw [← Finsupp.sum_embDomain (f := u) (g := fun x r ↦ r • (x : M)),
-      ← Finsupp.linearCombination_apply] at e
-  -- Now we can contradict the linear independence of `hi`
-  refine hi.linearCombination_ne_of_not_mem_support _ ?_ e
-  simp only [Finset.mem_map, Finsupp.support_embDomain]
-  rintro ⟨j, -, W⟩
-  simp only [u, Embedding.coeFn_mk, Subtype.mk_eq_mk] at W
-  apply q ⟨j, W⟩
+variable {v : ι → M} {x y : M}
 
 section Mk
 
@@ -333,6 +279,8 @@ theorem unitsSMul_apply {v : Basis ι R M} {w : ι → Rˣ} (i : ι) : unitsSMul
   mk_apply (LinearIndependent.units_smul v.linearIndependent w)
     (units_smul_span_eq_top v.span_eq).ge i
 
+variable [CommSemiring R₂] [Module R₂ M]
+
 @[simp]
 theorem coord_unitsSMul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) :
     (unitsSMul e w).coord i = (w i)⁻¹ • e.coord i := by
@@ -363,6 +311,62 @@ theorem repr_isUnitSMul {v : Basis ι R₂ M} {w : ι → R₂} (hw : ∀ i, IsU
     (v.isUnitSMul hw).repr x i = (hw i).unit⁻¹ • v.repr x i :=
   repr_unitsSMul _ _ _ _
 
+end Basis
+
+end Module
+
+section Module
+
+open LinearMap
+
+variable {v : ι → M}
+variable [Ring R] [CommRing R₂] [AddCommGroup M]
+variable [Module R M] [Module R₂ M]
+variable {x y : M}
+variable (b : Basis ι R M)
+
+theorem Basis.eq_bot_of_rank_eq_zero [NoZeroDivisors R] (b : Basis ι R M) (N : Submodule R M)
+    (rank_eq : ∀ {m : ℕ} (v : Fin m → N), LinearIndependent R ((↑) ∘ v : Fin m → M) → m = 0) :
+    N = ⊥ := by
+  rw [Submodule.eq_bot_iff]
+  intro x hx
+  contrapose! rank_eq with x_ne
+  refine ⟨1, fun _ => ⟨x, hx⟩, ?_, one_ne_zero⟩
+  rw [Fintype.linearIndependent_iff]
+  rintro g sum_eq i
+  cases' i with _ hi
+  simp only [Function.const_apply, Fin.default_eq_zero, Submodule.coe_mk, Finset.univ_unique,
+    Function.comp_const, Finset.sum_singleton] at sum_eq
+  convert (b.smul_eq_zero.mp sum_eq).resolve_right x_ne
+
+namespace Basis
+
+/-- Any basis is a maximal linear independent set.
+-/
+theorem maximal [Nontrivial R] (b : Basis ι R M) : b.linearIndependent.Maximal := fun w hi h => by
+  -- If `w` is strictly bigger than `range b`,
+  apply le_antisymm h
+  -- then choose some `x ∈ w \ range b`,
+  intro x p
+  by_contra q
+  -- and write it in terms of the basis.
+  have e := b.linearCombination_repr x
+  -- This then expresses `x` as a linear combination
+  -- of elements of `w` which are in the range of `b`,
+  let u : ι ↪ w :=
+    ⟨fun i => ⟨b i, h ⟨i, rfl⟩⟩, fun i i' r =>
+      b.injective (by simpa only [Subtype.mk_eq_mk] using r)⟩
+  simp_rw [Finsupp.linearCombination_apply] at e
+  change ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) = ((⟨x, p⟩ : w) : M) at e
+  rw [← Finsupp.sum_embDomain (f := u) (g := fun x r ↦ r • (x : M)),
+      ← Finsupp.linearCombination_apply] at e
+  -- Now we can contradict the linear independence of `hi`
+  refine hi.linearCombination_ne_of_not_mem_support _ ?_ e
+  simp only [Finset.mem_map, Finsupp.support_embDomain]
+  rintro ⟨j, -, W⟩
+  simp only [u, Embedding.coeFn_mk, Subtype.mk_eq_mk] at W
+  apply q ⟨j, W⟩
+
 section Fin
 
 /-- Let `b` be a basis for a submodule `N` of `M`. If `y : M` is linear independent of `N`

Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

@@ -239,7 +239,14 @@ end TensorProduct
 
 variable (R S M N ι κ : Type*)
   [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
-  [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M]
+  [Semiring S] [Algebra R S]
+
+theorem Finsupp.linearCombination_one_tmul [DecidableEq ι] {v : ι → M} :
+    (linearCombination S ((1 : S) ⊗ₜ[R] v ·)).restrictScalars R =
+      (linearCombination R v).lTensor S ∘ₗ (finsuppScalarRight R S ι).symm := by
+  ext; simp [smul_tmul']
+
+variable [Module S M] [IsScalarTower R S M]
 
 open scoped Classical in
 /-- The tensor product of `ι →₀ M` and `κ →₀ N` is linearly equivalent to `(ι × κ) →₀ (M ⊗ N)`. -/
@@ -362,3 +369,5 @@ theorem finsuppTensorFinsuppRid_self :
     finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ := by
   rw [finsuppTensorFinsupp', finsuppTensorFinsuppLid, finsuppTensorFinsuppRid,
     TensorProduct.lid_eq_rid]
+
+end

Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

@@ -252,6 +252,11 @@ theorem linearCombination_linearCombination {α β : Type*} (A : α → M) (B :
 
 @[deprecated (since := "2024-08-29")] alias total_total := linearCombination_linearCombination
 
+theorem linearCombination_smul [Module R S] [Module S M] [IsScalarTower R S M] {w : α' → S} :
+    linearCombination R (fun i : α × α' ↦ w i.2 • v i.1) = (linearCombination S v).restrictScalars R
+      ∘ₗ mapRange.linearMap (linearCombination R w) ∘ₗ (finsuppProdLEquiv R).toLinearMap := by
+  ext; simp [finsuppProdLEquiv, finsuppProdEquiv, Finsupp.curry]
+
 @[simp]
 theorem linearCombination_fin_zero (f : Fin 0 → M) : linearCombination R f = 0 := by
   ext i

Mathlib/RingTheory/Adjoin/PowerBasis.lean

@@ -33,9 +33,7 @@ noncomputable def adjoin.powerBasisAux {x : S} (hx : IsIntegral K x) :
     IsIntegral K (⟨x, subset_adjoin (Set.mem_singleton x)⟩ : adjoin K ({x} : Set S)) := by
     apply (isIntegral_algebraMap_iff hST).mp
     convert hx
-  apply
-    @Basis.mk (Fin (minpoly K x).natDegree) _ (adjoin K {x}) fun i =>
-      ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ)
+  apply Basis.mk (v := fun i : Fin _ ↦ ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ))
   · have : LinearIndependent K _ := linearIndependent_pow
       (⟨x, self_mem_adjoin_singleton _ _⟩ : adjoin K {x})
     rwa [← minpoly.algebraMap_eq hST] at this

Mathlib/RingTheory/AdjoinRoot.lean

@@ -506,7 +506,7 @@ def powerBasisAux (hf : f ≠ 0) : Basis (Fin f.natDegree) K (AdjoinRoot f) := b
     rw [natDegree_mul hf, natDegree_C, add_zero]
     · rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
   have minpoly_eq : minpoly K (root f) = f' := minpoly_root hf
-  apply @Basis.mk _ _ _ fun i : Fin f.natDegree => root f ^ i.val
+  apply Basis.mk (v := fun i : Fin f.natDegree ↦ root f ^ i.val)
   · rw [← deg_f', ← minpoly_eq]
     exact linearIndependent_pow (root f)
   · rintro y -

Mathlib/RingTheory/AlgebraTower.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 import Mathlib.Algebra.Algebra.Tower
-import Mathlib.Algebra.Module.BigOperators
 import Mathlib.LinearAlgebra.Basis.Basic
 
 /-!
@@ -27,9 +26,7 @@ base rings to be a field, so we also generalize the lemma to rings in this file.
 
 open Pointwise
 
-universe u v w u₁
-
-variable (R : Type u) (S : Type v) (A : Type w) (B : Type u₁)
+variable (R S A B : Type*)
 
 namespace IsScalarTower
 
@@ -39,7 +36,6 @@ variable [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B]
 variable [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B]
 variable [IsScalarTower R S A] [IsScalarTower R S B]
 
-
 /-- Suppose that `R → S → A` is a tower of algebras.
 If an element `r : R` is invertible in `S`, then it is invertible in `A`. -/
 def Invertible.algebraTower (r : R) [Invertible (algebraMap R S r)] :
@@ -91,33 +87,19 @@ open Finsupp
 
 open scoped Classical
 
-universe v₁ w₁
-
 variable {R S A}
-
-section
-variable [Ring R] [Ring S] [AddCommGroup A]
+variable [Semiring R] [Semiring S] [AddCommMonoid A]
 variable [Module R S] [Module S A] [Module R A] [IsScalarTower R S A]
 
-theorem linearIndependent_smul {ι : Type v₁} {b : ι → S} {ι' : Type w₁} {c : ι' → A}
+theorem linearIndependent_smul {ι : Type*} {b : ι → S} {ι' : Type*} {c : ι' → A}
     (hb : LinearIndependent R b) (hc : LinearIndependent S c) :
-    LinearIndependent R fun p : ι × ι' => b p.1 • c p.2 := by
-  rw [linearIndependent_iff'] at hb hc; rw [linearIndependent_iff'']; rintro s g hg hsg ⟨i, k⟩
-  by_cases hik : (i, k) ∈ s
-  · have h1 : ∑ i ∈ s.image Prod.fst ×ˢ s.image Prod.snd, g i • b i.1 • c i.2 = 0 := by
-      rw [← hsg]
-      exact
-        (Finset.sum_subset Finset.subset_product fun p _ hp =>
-            show g p • b p.1 • c p.2 = 0 by rw [hg p hp, zero_smul]).symm
-    rw [Finset.sum_product_right] at h1
-    simp_rw [← smul_assoc, ← Finset.sum_smul] at h1
-    exact hb _ _ (hc _ _ h1 k (Finset.mem_image_of_mem _ hik)) i (Finset.mem_image_of_mem _ hik)
-  exact hg _ hik
-end
+    LinearIndependent R fun p : ι × ι' ↦ b p.1 • c p.2 := by
+  rw [← linearIndependent_equiv' (.prodComm ..) (g := fun p : ι' × ι ↦ b p.2 • c p.1) rfl,
+    LinearIndependent, linearCombination_smul]
+  simpa using Function.Injective.comp hc
+    ((mapRange_injective _ (map_zero _) hb).comp <| Equiv.injective _)
 
 variable (R)
-variable [Semiring R] [Semiring S] [AddCommMonoid A]
-variable [Module R S] [Module S A] [Module R A] [IsScalarTower R S A]
 
 -- LinearIndependent is enough if S is a ring rather than semiring.
 theorem Basis.isScalarTower_of_nonempty {ι} [Nonempty ι] (b : Basis ι S A) : IsScalarTower R S S :=
@@ -197,7 +179,6 @@ variable {A} {C D : Type*} [CommSemiring A] [CommSemiring C] [CommSemiring D] [A
 
 variable [CommSemiring B] [Algebra A B] [Algebra B C] [IsScalarTower A B C] (f : C →ₐ[A] D)
 
-
 /-- Restrict the domain of an `AlgHom`. -/
 def AlgHom.restrictDomain : B →ₐ[A] D :=
   f.comp (IsScalarTower.toAlgHom A B C)

Mathlib/RingTheory/Flat/Basic.lean

@@ -274,6 +274,12 @@ theorem lTensor_preserves_injective_linearMap {N' : Type*} [AddCommGroup N'] [Mo
     Function.Injective (L.lTensor M) :=
   (L.lTensor_inj_iff_rTensor_inj M).2 (rTensor_preserves_injective_linearMap L hL)
 
+theorem linearIndependent_one_tmul {S} [Ring S] [Algebra R S] [Flat R S] {ι} {v : ι → M}
+    (hv : LinearIndependent R v) : LinearIndependent S ((1 : S) ⊗ₜ[R] v ·) := by
+  classical rw [LinearIndependent, ← LinearMap.coe_restrictScalars R,
+    Finsupp.linearCombination_one_tmul]
+  simpa using lTensor_preserves_injective_linearMap _ hv
+
 variable (R M) in
 /-- `M` is flat if and only if `f ⊗ 𝟙 M` is injective whenever `f` is an injective linear map.
   See `Module.Flat.iff_rTensor_preserves_injective_linearMap` to specialize the universe of

Mathlib/RingTheory/Localization/Module.lean

@@ -32,15 +32,11 @@ variable {R : Type*} (Rₛ : Type*)
 
 section IsLocalizedModule
 
-section AddCommMonoid
-variable [CommSemiring R] (S : Submonoid R)
-
 open Submodule
 
-variable [CommSemiring Rₛ] [Algebra R Rₛ] [hT : IsLocalization S Rₛ]
-variable {M M' : Type*} [AddCommMonoid M] [Module R M]
-  [AddCommMonoid M'] [Module R M'] [Module Rₛ M'] [IsScalarTower R Rₛ M'] (f : M →ₗ[R] M')
-  [IsLocalizedModule S f]
+variable [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ]
+  {M Mₛ : Type*} [AddCommMonoid M] [Module R M] [AddCommMonoid Mₛ] [Module R Mₛ]
+  [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f]
 
 include S
 
@@ -53,56 +49,33 @@ theorem span_eq_top_of_isLocalizedModule {v : Set M} (hv : span R v = ⊤) :
   rw [← LinearMap.coe_restrictScalars R, ← LinearMap.map_span, hv]
   exact mem_map_of_mem mem_top
 
-end AddCommMonoid
-
-section AddCommGroup
-
-variable {R : Type*} (Rₛ : Type*) [CommRing R] (S : Submonoid R)
-variable [CommRing Rₛ] [Algebra R Rₛ] [hT : IsLocalization S Rₛ]
-variable {M M' : Type*} [AddCommGroup M] [Module R M]
-  [AddCommGroup M'] [Module R M'] [Module Rₛ M'] [IsScalarTower R Rₛ M'] (f : M →ₗ[R] M')
-  [IsLocalizedModule S f]
-
-include S
-
 theorem LinearIndependent.of_isLocalizedModule {ι : Type*} {v : ι → M}
     (hv : LinearIndependent R v) : LinearIndependent Rₛ (f ∘ v) := by
-  rw [linearIndependent_iff'] at hv ⊢
-  intro t g hg i hi
-  choose! a g' hg' using IsLocalization.exist_integer_multiples S t g
-  have h0 : f (∑ i ∈ t, g' i • v i) = 0 := by
-    apply_fun ((a : R) • ·) at hg
-    rw [smul_zero, Finset.smul_sum] at hg
-    rw [map_sum, ← hg]
-    refine Finset.sum_congr rfl fun i hi => ?_
-    rw [← smul_assoc, ← hg' i hi, map_smul, Function.comp_apply, algebraMap_smul]
-  obtain ⟨s, hs⟩ := (IsLocalizedModule.eq_zero_iff S f).mp h0
-  simp_rw [Finset.smul_sum, Submonoid.smul_def, smul_smul] at hs
-  specialize hv t _ hs i hi
-  rw [← (IsLocalization.map_units Rₛ a).mul_right_eq_zero, ← Algebra.smul_def, ← hg' i hi]
-  exact (IsLocalization.map_eq_zero_iff S _ _).2 ⟨s, hv⟩
-
-variable [Module Rₛ M] [IsScalarTower R Rₛ M]
-
-theorem LinearIndependent.localization {ι : Type*} {b : ι → M} (hli : LinearIndependent R b) :
+  rw [linearIndependent_iff'ₛ] at hv ⊢
+  intro t g₁ g₂ eq i hi
+  choose! a fg hfg using IsLocalization.exist_integer_multiples S (t.disjSum t) (Sum.elim g₁ g₂)
+  simp_rw [Sum.forall, Finset.inl_mem_disjSum, Sum.elim_inl, Finset.inr_mem_disjSum, Sum.elim_inr,
+    Subtype.forall'] at hfg
+  apply_fun ((a : R) • ·) at eq
+  simp_rw [← t.sum_coe_sort, Finset.smul_sum, ← smul_assoc, ← hfg,
+    algebraMap_smul, Function.comp_def, ← map_smul, ← map_sum,
+    t.sum_coe_sort (f := fun x ↦ fg (Sum.inl x) • v x),
+    t.sum_coe_sort (f := fun x ↦ fg (Sum.inr x) • v x)] at eq
+  have ⟨s, eq⟩ := IsLocalizedModule.exists_of_eq (S := S) eq
+  simp_rw [Finset.smul_sum, Submonoid.smul_def, smul_smul] at eq
+  have := congr(algebraMap R Rₛ $(hv t _ _ eq i hi))
+  simpa only [map_mul, (IsLocalization.map_units Rₛ s).mul_right_inj, hfg.1 ⟨i, hi⟩, hfg.2 ⟨i, hi⟩,
+    Algebra.smul_def, (IsLocalization.map_units Rₛ a).mul_right_inj] using this
+
+theorem LinearIndependent.localization [Module Rₛ M] [IsScalarTower R Rₛ M]
+    {ι : Type*} {b : ι → M} (hli : LinearIndependent R b) :
     LinearIndependent Rₛ b := by
   have := isLocalizedModule_id S M Rₛ
   exact hli.of_isLocalizedModule Rₛ S .id
 
-end AddCommGroup
-
-
-variable [CommRing R] (S : Submonoid R)
-
 section Basis
 
-variable [CommRing Rₛ] [Algebra R Rₛ] [hT : IsLocalization S Rₛ]
-
-open Submodule
-
-variable {M Mₛ : Type*} [AddCommGroup M] [AddCommGroup Mₛ] [Module R M] [Module R Mₛ]
-  [Module Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] [IsScalarTower R Rₛ Mₛ]
-  {ι : Type*} (b : Basis ι R M)
+variable {ι : Type*} (b : Basis ι R M)
 
 /-- If `M` has an `R`-basis, then localizing `M` at `S` has a basis over `R` localized at `S`. -/
 noncomputable def Basis.ofIsLocalizedModule : Basis ι Rₛ Mₛ :=
@@ -138,12 +111,12 @@ end IsLocalizedModule
 
 section LocalizationLocalization
 
-variable [CommRing R] (S : Submonoid R) [CommRing Rₛ] [Algebra R Rₛ]
-variable [hT : IsLocalization S Rₛ]
-variable {A : Type*} [CommRing A] [Algebra R A]
-variable (Aₛ : Type*) [CommRing Aₛ] [Algebra A Aₛ]
+variable [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ]
+variable [IsLocalization S Rₛ]
+variable {A : Type*} [CommSemiring A] [Algebra R A]
+variable (Aₛ : Type*) [CommSemiring Aₛ] [Algebra A Aₛ]
 variable [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ]
-variable [hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ]
+variable [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ]
 
 open Submodule