chore: rename Finsupp.total (#16277)

to `Finsupp.linearCombination`.

Author: PatrickMassot

Archive/Sensitivity.lean

@@ -425,7 +425,8 @@ theorem huang_degree_theorem (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
     _ =
         |(coeffs y).sum fun (i : Q m.succ) (a : ℝ) =>
             a • (ε q ∘ f m.succ ∘ fun i : Q m.succ => e i) i| := by
-      erw [(f m.succ).map_finsupp_total, (ε q).map_finsupp_total, Finsupp.total_apply]
+      erw [(f m.succ).map_finsupp_linearCombination, (ε q).map_finsupp_linearCombination,
+           Finsupp.linearCombination_apply]
     _ ≤ ∑ p ∈ (coeffs y).support, |coeffs y p * (ε q <| f m.succ <| e p)| :=
       (norm_sum_le _ fun p => coeffs y p * _)
     _ = ∑ p ∈ (coeffs y).support, |coeffs y p| * ite (p ∈ q.adjacent) 1 0 := by

Mathlib/Algebra/Algebra/Subalgebra/Operations.lean

@@ -67,7 +67,7 @@ theorem mem_of_finset_sum_eq_one_of_pow_smul_mem
   exact ⟨⟨_, hn i⟩, rfl⟩
 
 theorem mem_of_span_eq_top_of_smul_pow_mem
-    (s : Set S) (l : s →₀ S) (hs : Finsupp.total S ((↑) : s → S) l = 1)
+    (s : Set S) (l : s →₀ S) (hs : Finsupp.linearCombination S ((↑) : s → S) l = 1)
     (hs' : s ⊆ S') (hl : ∀ i, l i ∈ S') (x : S) (H : ∀ r : s, ∃ n : ℕ, (r : S) ^ n • x ∈ S') :
     x ∈ S' :=
   mem_of_finset_sum_eq_one_of_pow_smul_mem S' l.support (↑) l hs (fun x => hs' x.2) hl x H

Mathlib/Algebra/Category/ModuleCat/Projective.lean

@@ -59,11 +59,11 @@ instance moduleCat_enoughProjectives : EnoughProjectives (ModuleCat.{max u v} R)
         f := Finsupp.basisSingleOne.constr ℕ _root_.id
         epi := (epi_iff_range_eq_top _).mpr
             (range_eq_top.2 fun m => ⟨Finsupp.single m (1 : R), by
-              -- Porting note: simp [Finsupp.total_single] fails but rw succeeds
+              -- Porting note: simp [Finsupp.linearCombination_single] fails but rw succeeds
               dsimp [Basis.constr]
               simp only [Finsupp.lmapDomain_id, comp_id]
               -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-              erw [Finsupp.total_single]
+              erw [Finsupp.linearCombination_single]
               rw [one_smul]
               rfl ⟩) }⟩
 

Mathlib/Algebra/DirectSum/Module.lean

@@ -28,7 +28,7 @@ universe u v w u₁
 
 namespace DirectSum
 
-open DirectSum
+open DirectSum Finsupp
 
 section General
 
@@ -335,7 +335,7 @@ theorem IsInternal.collectedBasis_coe (h : IsInternal A) {α : ι → Type*}
   -- Porting note: was
   -- simp only [IsInternal.collectedBasis, toModule, coeLinearMap, Basis.coe_ofRepr,
   --   Basis.repr_symm_apply, DFinsupp.lsum_apply_apply, DFinsupp.mapRange.linearEquiv_apply,
-  --   DFinsupp.mapRange.linearEquiv_symm, DFinsupp.mapRange_single, Finsupp.total_single,
+  --   DFinsupp.mapRange.linearEquiv_symm, DFinsupp.mapRange_single, linearCombination_single,
   --   LinearEquiv.ofBijective_apply, LinearEquiv.symm_symm, LinearEquiv.symm_trans_apply, one_smul,
   --   sigmaFinsuppAddEquivDFinsupp_apply, sigmaFinsuppEquivDFinsupp_single,
   --   sigmaFinsuppLequivDFinsupp_apply]
@@ -346,7 +346,7 @@ theorem IsInternal.collectedBasis_coe (h : IsInternal A) {α : ι → Type*}
     sigmaFinsuppAddEquivDFinsupp_apply]
   rw [DFinsupp.mapRange.linearEquiv_symm]
   erw [DFinsupp.mapRange.linearEquiv_apply]
-  simp only [DFinsupp.mapRange_single, Basis.repr_symm_apply, Finsupp.total_single, one_smul,
+  simp only [DFinsupp.mapRange_single, Basis.repr_symm_apply, linearCombination_single, one_smul,
     toModule]
   erw [DFinsupp.lsum_single]
   simp only [Submodule.coeSubtype]

Mathlib/Algebra/Lie/BaseChange.lean

@@ -169,10 +169,10 @@ def baseChange : LieSubmodule A (A ⊗[R] L) (A ⊗[R] M) :=
       intro x m hm
       simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
         Submodule.mem_toAddSubmonoid] at hm ⊢
-      obtain ⟨c, rfl⟩ := (Finsupp.mem_span_iff_total _ _ _).mp hm
+      obtain ⟨c, rfl⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp hm
       refine x.induction_on (by simp) (fun a y ↦ ?_) (fun y z hy hz ↦ ?_)
       · change toEnd A (A ⊗[R] L) (A ⊗[R] M) _ _ ∈ _
-        simp_rw [Finsupp.total_apply, Finsupp.sum, map_sum, map_smul, toEnd_apply_apply]
+        simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum, map_smul, toEnd_apply_apply]
         suffices ∀ n : (N : Submodule R M).map (TensorProduct.mk R A M 1),
             ⁅a ⊗ₜ[R] y, (n : A ⊗[R] M)⁆ ∈ (N : Submodule R M).baseChange A by
           exact Submodule.sum_mem _ fun n _ ↦ Submodule.smul_mem _ _ (this n)

Mathlib/Algebra/Module/FinitePresentation.lean

@@ -48,6 +48,8 @@ For finitely presented algebras, see `Algebra.FinitePresentation`
 in file `Mathlib.RingTheory.FinitePresentation`.
 -/
 
+open Finsupp
+
 section Semiring
 variable (R M) [Semiring R] [AddCommMonoid M] [Module R M]
 
@@ -57,7 +59,7 @@ and the kernel of the presentation `Rˢ → M` is also finitely generated.
 -/
 class Module.FinitePresentation : Prop where
   out : ∃ (s : Finset M), Submodule.span R (s : Set M) = ⊤ ∧
-    (LinearMap.ker (Finsupp.total R ((↑) : s → M))).FG
+    (LinearMap.ker (Finsupp.linearCombination R ((↑) : s → M))).FG
 
 instance (priority := 100) [h : Module.FinitePresentation R M] : Module.Finite R M := by
   obtain ⟨s, hs₁, _⟩ := h
@@ -78,10 +80,10 @@ theorem Module.FinitePresentation.equiv_quotient [fp : Module.FinitePresentation
       Module.Free R L ∧ Module.Finite R L ∧ K.FG := by
   obtain ⟨ι, ⟨hι₁, hι₂⟩⟩ := fp
   use ι →₀ R, inferInstance, inferInstance
-  use LinearMap.ker (Finsupp.total R Subtype.val)
+  use LinearMap.ker (Finsupp.linearCombination R Subtype.val)
   refine ⟨(LinearMap.quotKerEquivOfSurjective _ ?_).symm, inferInstance, inferInstance, hι₂⟩
   apply LinearMap.range_eq_top.mp
-  simpa only [Finsupp.range_total, Subtype.range_coe_subtype, Finset.setOf_mem]
+  simpa only [Finsupp.range_linearCombination, Subtype.range_coe_subtype, Finset.setOf_mem]
 
 -- Ideally this should be an instance but it makes mathlib much slower.
 lemma Module.finitePresentation_of_finite [IsNoetherianRing R] [h : Module.Finite R M] :
@@ -119,12 +121,12 @@ lemma Module.finitePresentation_of_free_of_surjective [Module.Free R M] [Module.
   constructor
   · intro hx
     refine ⟨b.repr.symm (x.mapDomain σ), ?_, ?_⟩
-    · simp [Finsupp.apply_total, hσ₂, hx]
+    · simp [Finsupp.apply_linearCombination, hσ₂, hx]
     · simp only [f, LinearMap.comp_apply, b.repr.apply_symm_apply,
         LinearEquiv.coe_toLinearMap, Finsupp.lmapDomain_apply]
       rw [← Finsupp.mapDomain_comp, hσ₁, Finsupp.mapDomain_id]
   · rintro ⟨y, hy, rfl⟩
-    simp [f, hπ, ← Finsupp.apply_total, hy]
+    simp [f, hπ, ← Finsupp.apply_linearCombination, hy]
 
 -- Ideally this should be an instance but it makes mathlib much slower.
 variable (R M) in
@@ -145,12 +147,12 @@ lemma Module.finitePresentation_of_surjective [h : Module.FinitePresentation R M
   classical
   obtain ⟨s, hs, hs'⟩ := h
   obtain ⟨t, ht⟩ := hl'
-  have H : Function.Surjective (Finsupp.total R ((↑) : s → M)) :=
-    LinearMap.range_eq_top.mp (by rw [Finsupp.range_total, Subtype.range_val, ← hs]; rfl)
-  apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ Finsupp.total R Subtype.val)
+  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → M)) :=
+    LinearMap.range_eq_top.mp (by rw [range_linearCombination, Subtype.range_val, ← hs]; rfl)
+  apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ linearCombination R Subtype.val)
     (hl.comp H)
   choose σ hσ using (show _ from H)
-  have : Finsupp.total R Subtype.val '' (σ '' t) = t := by
+  have : Finsupp.linearCombination R Subtype.val '' (σ '' t) = t := by
     simp only [Set.image_image, hσ, Set.image_id']
   rw [LinearMap.ker_comp, ← ht, ← this, ← Submodule.map_span, Submodule.comap_map_eq,
     ← Finset.coe_image]
@@ -161,11 +163,11 @@ lemma Module.FinitePresentation.fg_ker [Module.Finite R M]
     (LinearMap.ker l).FG := by
   classical
   obtain ⟨s, hs, hs'⟩ := h
-  have H : Function.Surjective (Finsupp.total R ((↑) : s → N)) :=
-    LinearMap.range_eq_top.mp (by rw [Finsupp.range_total, Subtype.range_val, ← hs]; rfl)
-  obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.total R Subtype.val) := by
+  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → N)) :=
+    LinearMap.range_eq_top.mp (by rw [range_linearCombination, Subtype.range_val, ← hs]; rfl)
+  obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.linearCombination R Subtype.val) := by
     choose f hf using show _ from hl
-    exact ⟨Finsupp.total R (fun i ↦ f i), by ext; simp [hf]⟩
+    exact ⟨Finsupp.linearCombination R (fun i ↦ f i), by ext; simp [hf]⟩
   have : (LinearMap.ker l).map (LinearMap.range f).mkQ = ⊤ := by
     rw [← top_le_iff]
     rintro x -
@@ -192,9 +194,9 @@ lemma Module.finitePresentation_of_ker [Module.FinitePresentation R N]
     · rw [Submodule.map_top, LinearMap.range_eq_top.mpr hl]; exact Module.Finite.out
     · rw [top_inf_eq, ← Submodule.fg_top]; exact Module.Finite.out
   refine ⟨s, hs, ?_⟩
-  let π := Finsupp.total R ((↑) : s → M)
+  let π := Finsupp.linearCombination R ((↑) : s → M)
   have H : Function.Surjective π :=
-    LinearMap.range_eq_top.mp (by rw [Finsupp.range_total, Subtype.range_val, ← hs]; rfl)
+    LinearMap.range_eq_top.mp (by rw [range_linearCombination, Subtype.range_val, ← hs]; rfl)
   have inst : Module.Finite R (LinearMap.ker (l ∘ₗ π)) := by
     constructor
     rw [Submodule.fg_top]; exact Module.FinitePresentation.fg_ker _ (hl.comp H)
@@ -227,23 +229,24 @@ lemma Module.FinitePresentation.exists_lift_of_isLocalizedModule
     [h : Module.FinitePresentation R M] (g : M →ₗ[R] N') :
     ∃ (h : M →ₗ[R] N) (s : S), f ∘ₗ h = s • g := by
   obtain ⟨σ, hσ, τ, hτ⟩ := h
-  let π := Finsupp.total R ((↑) : σ → M)
+  let π := Finsupp.linearCombination R ((↑) : σ → M)
   have hπ : Function.Surjective π :=
-    LinearMap.range_eq_top.mp (by rw [Finsupp.range_total, Subtype.range_val, ← hσ]; rfl)
+    LinearMap.range_eq_top.mp (by rw [range_linearCombination, Subtype.range_val, ← hσ]; rfl)
   classical
   choose s hs using IsLocalizedModule.surj S f
   let i : σ → N :=
     fun x ↦ (∏ j ∈ σ.erase x.1, (s (g j)).2) • (s (g x)).1
   let s₀ := ∏ j ∈ σ, (s (g j)).2
-  have hi : f ∘ₗ Finsupp.total R i = (s₀ • g) ∘ₗ π := by
+  have hi : f ∘ₗ Finsupp.linearCombination R i = (s₀ • g) ∘ₗ π := by
     ext j
-    simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply, Finsupp.total_single,
-      one_smul, LinearMap.map_smul_of_tower, ← hs, LinearMap.smul_apply, i, s₀, π]
+    simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply,
+      linearCombination_single, one_smul, LinearMap.map_smul_of_tower, ← hs, LinearMap.smul_apply,
+      i, s₀, π]
     rw [← mul_smul, Finset.prod_erase_mul]
     exact j.prop
-  have : ∀ x : τ, ∃ s : S, s • (Finsupp.total R i x) = 0 := by
+  have : ∀ x : τ, ∃ s : S, s • (Finsupp.linearCombination R i x) = 0 := by
     intros x
-    convert_to ∃ s : S, s • (Finsupp.total R i x) = s • 0
+    convert_to ∃ s : S, s • (Finsupp.linearCombination R i x) = s • 0
     · simp only [smul_zero]
     apply IsLocalizedModule.exists_of_eq (S := S) (f := f)
     rw [← LinearMap.comp_apply, map_zero, hi, LinearMap.comp_apply]
@@ -252,7 +255,7 @@ lemma Module.FinitePresentation.exists_lift_of_isLocalizedModule
     exact Submodule.subset_span x.prop
   choose s' hs' using this
   let s₁ := ∏ i : τ, s' i
-  have : LinearMap.ker π ≤ LinearMap.ker (s₁ • Finsupp.total R i) := by
+  have : LinearMap.ker π ≤ LinearMap.ker (s₁ • Finsupp.linearCombination R i) := by
     rw [← hτ, Submodule.span_le]
     intro x hxσ
     simp only [s₁]

Mathlib/Algebra/Module/Projective.lean

@@ -72,7 +72,7 @@ open Finsupp
   definitions. -/
 class Module.Projective (R : Type*) [Semiring R] (P : Type*) [AddCommMonoid P] [Module R P] :
     Prop where
-  out : ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (Finsupp.total R id) s
+  out : ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (Finsupp.linearCombination R id) s
 
 namespace Module
 
@@ -82,11 +82,11 @@ variable {R : Type*} [Semiring R] {P : Type*} [AddCommMonoid P] [Module R P] {M
   [AddCommMonoid M] [Module R M] {N : Type*} [AddCommMonoid N] [Module R N]
 
 theorem projective_def :
-    Projective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (Finsupp.total R id) s :=
+    Projective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (linearCombination R id) s :=
   ⟨fun h => h.1, fun h => ⟨h⟩⟩
 
 theorem projective_def' :
-    Projective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Finsupp.total R id ∘ₗ s = .id := by
+    Projective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Finsupp.linearCombination R id ∘ₗ s = .id := by
   simp_rw [projective_def, DFunLike.ext_iff, Function.LeftInverse, comp_apply, id_apply]
 
 /-- A projective R-module has the property that maps from it lift along surjections. -/
@@ -95,20 +95,20 @@ theorem projective_lifting_property [h : Projective R P] (f : M →ₗ[R] N) (g
   /-
     Here's the first step of the proof.
     Recall that `X →₀ R` is Lean's way of talking about the free `R`-module
-    on a type `X`. The universal property `Finsupp.total` says that to a map
+    on a type `X`. The universal property `Finsupp.linearCombination` says that to a map
     `X → N` from a type to an `R`-module, we get an associated R-module map
     `(X →₀ R) →ₗ N`. Apply this to a (noncomputable) map `P → M` coming from the map
     `P →ₗ N` and a random splitting of the surjection `M →ₗ N`, and we get
     a map `φ : (P →₀ R) →ₗ M`.
     -/
-  let φ : (P →₀ R) →ₗ[R] M := Finsupp.total _ fun p => Function.surjInv hf (g p)
+  let φ : (P →₀ R) →ₗ[R] M := Finsupp.linearCombination _ fun p => Function.surjInv hf (g p)
   -- By projectivity we have a map `P →ₗ (P →₀ R)`;
   cases' h.out with s hs
   -- Compose to get `P →ₗ M`. This works.
   use φ.comp s
   ext p
   conv_rhs => rw [← hs p]
-  simp [φ, Finsupp.total_apply, Function.surjInv_eq hf, map_finsupp_sum]
+  simp [φ, Finsupp.linearCombination_apply, Function.surjInv_eq hf, map_finsupp_sum]
 
 /-- A module which satisfies the universal property is projective: If all surjections of
 `R`-modules `(P →₀ R) →ₗ[R] P` have `R`-linear left inverse maps, then `P` is
@@ -117,8 +117,8 @@ theorem Projective.of_lifting_property'' {R : Type u} [Semiring R] {P : Type v}
     [Module R P] (huniv : ∀ (f : (P →₀ R) →ₗ[R] P), Function.Surjective f →
       ∃ h : P →ₗ[R] (P →₀ R), f.comp h = .id) :
     Projective R P :=
-  projective_def'.2 <| huniv (Finsupp.total R (id : P → P))
-    (total_surjective _ Function.surjective_id)
+  projective_def'.2 <| huniv (Finsupp.linearCombination R (id : P → P))
+    (linearCombination_surjective _ Function.surjective_id)
 
 variable {Q : Type*} [AddCommMonoid Q] [Module R Q]
 
@@ -152,9 +152,9 @@ theorem Projective.of_basis {ι : Type*} (b : Basis ι R P) : Projective R P :=
   -- get it from `ι → (P →₀ R)` coming from `b`.
   use b.constr ℕ fun i => Finsupp.single (b i) (1 : R)
   intro m
-  simp only [b.constr_apply, mul_one, id, Finsupp.smul_single', Finsupp.total_single,
+  simp only [b.constr_apply, mul_one, id, Finsupp.smul_single', Finsupp.linearCombination_single,
     map_finsupp_sum]
-  exact b.total_repr m
+  exact b.linearCombination_repr m
 
 instance (priority := 100) Projective.of_free [Module.Free R P] : Module.Projective R P :=
   .of_basis <| Module.Free.chooseBasis R P
@@ -164,7 +164,7 @@ variable [IsScalarTower R₀ R M] [AddCommGroup N] [Module R₀ N]
 
 theorem Projective.of_split [Module.Projective R M]
     (i : P →ₗ[R] M) (s : M →ₗ[R] P) (H : s.comp i = LinearMap.id) : Module.Projective R P := by
-  obtain ⟨g, hg⟩ := projective_lifting_property (Finsupp.total R id) s
+  obtain ⟨g, hg⟩ := projective_lifting_property (Finsupp.linearCombination R id) s
     (fun x ↦ ⟨Finsupp.single x 1, by simp⟩)
   refine ⟨g.comp i, fun x ↦ ?_⟩
   rw [LinearMap.comp_apply, ← LinearMap.comp_apply, hg,
@@ -178,7 +178,7 @@ theorem Projective.of_equiv [Module.Projective R M]
 theorem Projective.iff_split : Module.Projective R P ↔
     ∃ (M : Type max u v) (_ : AddCommGroup M) (_ : Module R M) (_ : Module.Free R M)
       (i : P →ₗ[R] M) (s : M →ₗ[R] P), s.comp i = LinearMap.id :=
-  ⟨fun ⟨i, hi⟩ ↦ ⟨P →₀ R, _, _, inferInstance, i, Finsupp.total R id, LinearMap.ext hi⟩,
+  ⟨fun ⟨i, hi⟩ ↦ ⟨P →₀ R, _, _, inferInstance, i, Finsupp.linearCombination R id, LinearMap.ext hi⟩,
     fun ⟨_, _, _, _, i, s, H⟩ ↦ Projective.of_split i s H⟩
 
 /-- A quotient of a projective module is projective iff it is a direct summand. -/
@@ -197,11 +197,11 @@ instance Projective.tensorProduct [hM : Module.Projective R M] [hN : Module.Proj
     fapply Projective.of_split (R := R) (M := ((M →₀ R) ⊗[R₀] (N →₀ R₀)))
     · exact (AlgebraTensorModule.map sM (LinearMap.id (R := R₀) (M := N →₀ R₀)))
     · exact (AlgebraTensorModule.map
-        (Finsupp.total R id) (LinearMap.id (R := R₀) (M := N →₀ R₀)))
+        (Finsupp.linearCombination R id) (LinearMap.id (R := R₀) (M := N →₀ R₀)))
     · ext; simp [hsM _]
   fapply Projective.of_split (R := R) (M := (M ⊗[R₀] (N →₀ R₀)))
   · exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) sN)
-  · exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) (Finsupp.total R₀ id))
+  · exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) (linearCombination R₀ id))
   · ext; simp [hsN _]
 
 end Ring

Mathlib/AlgebraicGeometry/StructureSheaf.lean

@@ -799,9 +799,9 @@ theorem toBasicOpen_surjective (f : R) : Function.Surjective (toBasicOpen R f) :
     apply PrimeSpectrum.vanishingIdeal_anti_mono ht_cover
     exact PrimeSpectrum.subset_vanishingIdeal_zeroLocus {f} (Set.mem_singleton f)
   replace hn := Ideal.mul_mem_right f _ hn
-  erw [← pow_succ, Finsupp.mem_span_image_iff_total] at hn
+  erw [← pow_succ, Finsupp.mem_span_image_iff_linearCombination] at hn
   rcases hn with ⟨b, b_supp, hb⟩
-  rw [Finsupp.total_apply_of_mem_supported R b_supp] at hb
+  rw [Finsupp.linearCombination_apply_of_mem_supported R b_supp] at hb
   dsimp at hb
   -- Finally, we have all the ingredients.
   -- We claim that our preimage is given by `(∑ (i : ι) ∈ t, b i * a i) / f ^ (n+1)`