refactor(linear_algebra/finsupp): replace mem_span_iff_total (#7735)

This PR renames the existing `mem_span_iff_total` to `mem_span_image_iff_total` and the existing `span_eq_map_total` to `span_image_eq_map_total`, and replaces them with slightly simpler lemmas about sets in the module, rather than indexed families.

As usual in the linear algebra library, there is tension between using sets and using indexed families, but as `span` is defined in terms of sets I think the new lemmas merit taking the simpler names.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebraic_geometry/structure_sheaf.lean

@@ -716,7 +716,7 @@ begin
     exact subset_vanishing_ideal_zero_locus {f} (set.mem_singleton f) },
 
   replace hn := ideal.mul_mem_left _ f hn,
-  erw [←pow_succ, finsupp.mem_span_iff_total] at hn,
+  erw [←pow_succ, finsupp.mem_span_image_iff_total] at hn,
   rcases hn with ⟨b, b_supp, hb⟩,
   rw finsupp.total_apply_of_mem_supported R b_supp at hb,
   dsimp at hb,

src/analysis/normed_space/inner_product.lean

@@ -2739,7 +2739,7 @@ begin
       have hxv' : (⟨x, hxu⟩ : u) ∉ (coe ⁻¹' v : set u) := by simp [huv, hxv],
       obtain ⟨l, hl, rfl⟩ :
         ∃ l ∈ finsupp.supported 𝕜 𝕜 (coe ⁻¹' v : set u), (finsupp.total ↥u E 𝕜 coe) l = y,
-      { rw ← finsupp.mem_span_iff_total,
+      { rw ← finsupp.mem_span_image_iff_total,
         simp [huv, inter_eq_self_of_subset_left, hy] },
       exact hu.inner_finsupp_eq_zero hxv' hl }
 end

src/field_theory/algebraic_closure.lean

@@ -156,7 +156,8 @@ by { rw [to_splitting_field, eval_X_self, ← alg_hom.coe_to_ring_hom, hom_eval
 
 theorem span_eval_ne_top : span_eval k ≠ ⊤ :=
 begin
-  rw [ideal.ne_top_iff_one, span_eval, ideal.span, ← set.image_univ, finsupp.mem_span_iff_total],
+  rw [ideal.ne_top_iff_one, span_eval, ideal.span, ← set.image_univ,
+    finsupp.mem_span_image_iff_total],
   rintros ⟨v, _, hv⟩,
   replace hv := congr_arg (to_splitting_field k v.support) hv,
   rw [alg_hom.map_one, finsupp.total_apply, finsupp.sum, alg_hom.map_sum, finset.sum_eq_zero] at hv,

src/field_theory/fixed.lean

@@ -78,7 +78,7 @@ begin
   rw coe_insert at hs ⊢,
   rw linear_independent_insert (mt mem_coe.1 has) at hs,
   rw linear_independent_insert' (mt mem_coe.1 has), refine ⟨ih hs.1, λ ha, _⟩,
-  rw finsupp.mem_span_iff_total at ha, rcases ha with ⟨l, hl, hla⟩,
+  rw finsupp.mem_span_image_iff_total at ha, rcases ha with ⟨l, hl, hla⟩,
   rw [finsupp.total_apply_of_mem_supported F hl] at hla,
   suffices : ∀ i ∈ s, l i ∈ fixed_points G F,
   { replace hla := (sum_apply _ _ (λ i, l i • to_fun G F i)).symm.trans (congr_fun hla 1),

src/linear_algebra/affine_space/combination.lean

@@ -537,7 +537,7 @@ begin
   by_cases hn : nonempty ι,
   { cases hn with i0,
     rw [vector_span_range_eq_span_range_vsub_right k p i0, ←set.image_univ,
-        finsupp.mem_span_iff_total,
+        finsupp.mem_span_image_iff_total,
         finset.weighted_vsub_eq_weighted_vsub_of_point_of_sum_eq_zero s w p h (p i0),
         finset.weighted_vsub_of_point_apply],
     let w' := set.indicator ↑s w,
@@ -587,7 +587,7 @@ begin
   { by_cases hn : nonempty ι,
     { cases hn with i0,
       rw [vector_span_range_eq_span_range_vsub_right k p i0, ←set.image_univ,
-          finsupp.mem_span_iff_total],
+          finsupp.mem_span_image_iff_total],
       rintros ⟨l, hl, hv⟩,
       use insert i0 l.support,
       set w := (l : ι → k) -

src/linear_algebra/basis.lean

@@ -395,7 +395,7 @@ lemma constr_range [nonempty ι] {f : ι  → M'} :
   (b.constr S f).range = span R (range f) :=
 by rw [b.constr_def S f, linear_map.range_comp, linear_map.range_comp, linear_equiv.range,
        ← finsupp.supported_univ, finsupp.lmap_domain_supported, ←set.image_univ,
-       ← finsupp.span_eq_map_total, set.image_id]
+       ← finsupp.span_image_eq_map_total, set.image_id]
 
 end constr
 

src/linear_algebra/dual.lean

@@ -388,7 +388,7 @@ lemma mem_of_mem_span {H : set ι} {x : M} (hmem : x ∈ submodule.span R (e ''
   ∀ i : ι, ε i x ≠ 0 → i ∈ H :=
 begin
   intros i hi,
-  rcases (finsupp.mem_span_iff_total _).mp hmem with ⟨l, supp_l, rfl⟩,
+  rcases (finsupp.mem_span_image_iff_total _).mp hmem with ⟨l, supp_l, rfl⟩,
   apply not_imp_comm.mp ((finsupp.mem_supported' _ _).mp supp_l i),
   rwa [← lc_def, h.dual_lc] at hi
 end

src/linear_algebra/finsupp.lean

@@ -468,7 +468,16 @@ begin
   apply total_emb_domain R ⟨f, hf⟩ l
 end
 
-theorem span_eq_map_total (s : set α):
+/-- A version of `finsupp.range_total` which is useful for going in the other direction -/
+theorem span_eq_range_total (s : set M) :
+  span R s = (finsupp.total s M R coe).range :=
+by rw [range_total, subtype.range_coe_subtype, set.set_of_mem_eq]
+
+theorem mem_span_iff_total (s : set M) (x : M) :
+  x ∈ span R s ↔ ∃ l : s →₀ R, finsupp.total s M R coe l = x :=
+(set_like.ext_iff.1 $ span_eq_range_total _ _) x
+
+theorem span_image_eq_map_total (s : set α):
   span R (v '' s) = submodule.map (finsupp.total α M R v) (supported R R s) :=
 begin
   apply span_eq_of_le,
@@ -487,9 +496,9 @@ begin
     refine sum_mem _ _, simp [this] }
 end
 
-theorem mem_span_iff_total {s : set α} {x : M} :
+theorem mem_span_image_iff_total {s : set α} {x : M} :
   x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, finsupp.total α M R v l = x :=
-by rw span_eq_map_total; simp
+by { rw span_image_eq_map_total, simp, }
 
 variables (α) (M) (v)
 
@@ -500,15 +509,15 @@ The subset is indicated by a set `s : set α` of indices.
 -/
 protected def total_on (s : set α) : supported R R s →ₗ[R] span R (v '' s) :=
 linear_map.cod_restrict _ ((finsupp.total _ _ _ v).comp (submodule.subtype (supported R R s))) $
-  λ ⟨l, hl⟩, (mem_span_iff_total _).2 ⟨l, hl, rfl⟩
+  λ ⟨l, hl⟩, (mem_span_image_iff_total _).2 ⟨l, hl, rfl⟩
 
 variables {α} {M} {v}
 
 theorem total_on_range (s : set α) : (finsupp.total_on α M R v s).range = ⊤ :=
 begin
   rw [finsupp.total_on, linear_map.range_eq_map, linear_map.map_cod_restrict,
     ← linear_map.range_le_iff_comap, range_subtype, map_top, linear_map.range_comp, range_subtype],
-  exact (span_eq_map_total _ _).le
+  exact (span_image_eq_map_total _ _).le
 end
 
 theorem total_comp (f : α' → α) :
@@ -763,7 +772,7 @@ lemma submodule.exists_finset_of_mem_supr
 begin
   obtain ⟨f, hf, rfl⟩ : ∃ f ∈ finsupp.supported R R (⋃ i, ↑(p i)), finsupp.total M M R id f = m,
   { have aux : (id : M → M) '' (⋃ (i : ι), ↑(p i)) = (⋃ (i : ι), ↑(p i)) := set.image_id _,
-    rwa [supr_eq_span, ← aux, finsupp.mem_span_iff_total R] at hm },
+    rwa [supr_eq_span, ← aux, finsupp.mem_span_image_iff_total R] at hm },
   let t : finset M := f.support,
   have ht : ∀ x : {x // x ∈ t}, ∃ i, ↑x ∈ p i,
   { intros x,
@@ -786,7 +795,7 @@ end
 
 lemma mem_span_finset {s : finset M} {x : M} :
   x ∈ span R (↑s : set M) ↔ ∃ f : M → R, ∑ i in s, f i • i = x :=
-⟨λ hx, let ⟨v, hvs, hvx⟩ := (finsupp.mem_span_iff_total _).1
+⟨λ hx, let ⟨v, hvs, hvx⟩ := (finsupp.mem_span_image_iff_total _).1
     (show x ∈ span R (id '' (↑s : set M)), by rwa set.image_id) in
   ⟨v, hvx ▸ (finsupp.total_apply_of_mem_supported _ hvs).symm⟩,
 λ ⟨f, hf⟩, hf ▸ sum_mem _ (λ i hi, smul_mem _ _ $ subset_span hi)⟩
@@ -799,7 +808,7 @@ lemma mem_span_set {m : M} {s : set M} :
 begin
   conv_lhs { rw ←set.image_id s },
   simp_rw ←exists_prop,
-  exact finsupp.mem_span_iff_total R,
+  exact finsupp.mem_span_image_iff_total R,
 end
 
 /-- If `subsingleton R`, then `M ≃ₗ[R] ι →₀ R` for any type `ι`. -/

src/linear_algebra/linear_independent.lean

@@ -186,7 +186,7 @@ family of vectors. See also `linear_independent.map'` for a special case assumin
 lemma linear_independent.map (hv : linear_independent R v) {f : M →ₗ[R] M'}
   (hf_inj : disjoint (span R (range v)) f.ker) : linear_independent R (f ∘ v) :=
 begin
-  rw [disjoint, ← set.image_univ, finsupp.span_eq_map_total, map_inf_eq_map_inf_comap,
+  rw [disjoint, ← set.image_univ, finsupp.span_image_eq_map_total, map_inf_eq_map_inf_comap,
     map_le_iff_le_comap, comap_bot, finsupp.supported_univ, top_inf_eq] at hf_inj,
   unfold linear_independent at hv ⊢,
   rw [hv, le_bot_iff] at hf_inj,
@@ -453,7 +453,7 @@ lemma linear_independent.disjoint_span_image (hv : linear_independent R v) {s t
   (hs : disjoint s t) :
   disjoint (submodule.span R $ v '' s) (submodule.span R $ v '' t) :=
 begin
-  simp only [disjoint_def, finsupp.mem_span_iff_total],
+  simp only [disjoint_def, finsupp.mem_span_image_iff_total],
   rintros _ ⟨l₁, hl₁, rfl⟩ ⟨l₂, hl₂, H⟩,
   rw [hv.injective_total.eq_iff] at H, subst l₂,
   have : l₁ = 0 := finsupp.disjoint_supported_supported hs (submodule.mem_inf.2 ⟨hl₁, hl₂⟩),
@@ -621,7 +621,7 @@ end
 lemma linear_independent_iff_not_smul_mem_span :
   linear_independent R v ↔ (∀ (i : ι) (a : R), a • (v i) ∈ span R (v '' (univ \ {i})) → a = 0) :=
 ⟨ λ hv i a ha, begin
-  rw [finsupp.span_eq_map_total, mem_map] at ha,
+  rw [finsupp.span_image_eq_map_total, mem_map] at ha,
   rcases ha with ⟨l, hl, e⟩,
   rw sub_eq_zero.1 (linear_independent_iff.1 hv (l - finsupp.single i a) (by simp [e])) at hl,
   by_contra hn,
@@ -630,7 +630,7 @@ end, λ H, linear_independent_iff.2 $ λ l hl, begin
   ext i, simp only [finsupp.zero_apply],
   by_contra hn,
   refine hn (H i _ _),
-  refine (finsupp.mem_span_iff_total _).2 ⟨finsupp.single i (l i) - l, _, _⟩,
+  refine (finsupp.mem_span_image_iff_total _).2 ⟨finsupp.single i (l i) - l, _, _⟩,
   { rw finsupp.mem_supported',
     intros j hj,
     have hij : j = i :=

src/ring_theory/adjoin/basic.lean

@@ -220,14 +220,14 @@ begin
     change r ∈ (adjoin (adjoin R s) t).to_submodule at hr,
     haveI := classical.dec_eq A,
     haveI := classical.dec_eq R,
-    rw [← hq', ← set.image_id q, finsupp.mem_span_iff_total (adjoin R s)] at hr,
+    rw [← hq', ← set.image_id q, finsupp.mem_span_image_iff_total (adjoin R s)] at hr,
     rcases hr with ⟨l, hlq, rfl⟩,
     have := @finsupp.total_apply A A (adjoin R s),
     rw [this, finsupp.sum],
     refine sum_mem _ _,
     intros z hz, change (l z).1 * _ ∈ _,
     have : (l z).1 ∈ (adjoin R s).to_submodule := (l z).2,
-    rw [← hp', ← set.image_id p, finsupp.mem_span_iff_total R] at this,
+    rw [← hp', ← set.image_id p, finsupp.mem_span_image_iff_total R] at this,
     rcases this with ⟨l2, hlp, hl⟩,
     have := @finsupp.total_apply A A R,
     rw this at hl,

src/ring_theory/integral_closure.lean

@@ -192,12 +192,12 @@ begin
   cases HS with y hy,
   obtain ⟨lx, hlx1, hlx2⟩ :
     ∃ (l : A →₀ R) (H : l ∈ finsupp.supported R R ↑y), (finsupp.total A A R id) l = x,
-  { rwa [←(@finsupp.mem_span_iff_total A A R _ _ _ id ↑y x), set.image_id ↑y, hy] },
+  { rwa [←(@finsupp.mem_span_image_iff_total A A R _ _ _ id ↑y x), set.image_id ↑y, hy] },
   have hyS : ∀ {p}, p ∈ y → p ∈ S := λ p hp, show p ∈ S.to_submodule,
     by { rw ← hy, exact subset_span hp },
   have : ∀ (jk : (↑(y.product y) : set (A × A))), jk.1.1 * jk.1.2 ∈ S.to_submodule :=
     λ jk, S.mul_mem (hyS (finset.mem_product.1 jk.2).1) (hyS (finset.mem_product.1 jk.2).2),
-  rw [← hy, ← set.image_id ↑y] at this, simp only [finsupp.mem_span_iff_total] at this,
+  rw [← hy, ← set.image_id ↑y] at this, simp only [finsupp.mem_span_image_iff_total] at this,
   choose ly hly1 hly2,
   let S₀ : set R := ring.closure ↑(lx.frange ∪ finset.bUnion finset.univ (finsupp.frange ∘ ly)),
   refine is_integral_of_subring S₀ _,

src/ring_theory/noetherian.lean

@@ -203,13 +203,13 @@ begin
       exact this.1 } },
   intros x hx,
   have : f x ∈ map f s, { rw mem_map, exact ⟨x, hx, rfl⟩ },
-  rw [← ht1,← set.image_id ↑t1, finsupp.mem_span_iff_total] at this,
+  rw [← ht1,← set.image_id ↑t1, finsupp.mem_span_image_iff_total] at this,
   rcases this with ⟨l, hl1, hl2⟩,
   refine mem_sup.2 ⟨(finsupp.total M M R id).to_fun
     ((finsupp.lmap_domain R R g : (P →₀ R) → M →₀ R) l), _,
     x - finsupp.total M M R id ((finsupp.lmap_domain R R g : (P →₀ R) → M →₀ R) l),
     _, add_sub_cancel'_right _ _⟩,
-  { rw [← set.image_id (g '' ↑t1), finsupp.mem_span_iff_total], refine ⟨_, _, rfl⟩,
+  { rw [← set.image_id (g '' ↑t1), finsupp.mem_span_image_iff_total], refine ⟨_, _, rfl⟩,
     haveI : inhabited P := ⟨0⟩,
     rw [← finsupp.lmap_domain_supported _ _ g, mem_map],
     refine ⟨l, hl1, _⟩,
@@ -578,7 +578,7 @@ begin
       exact finset.smul_sum.symm } },
   rw linear_map.range_eq_top,
   rintro ⟨n, hn⟩, change n ∈ N at hn,
-  rw [← hs, ← set.image_id ↑s, finsupp.mem_span_iff_total] at hn,
+  rw [← hs, ← set.image_id ↑s, finsupp.mem_span_image_iff_total] at hn,
   rcases hn with ⟨l, hl1, hl2⟩,
   refine ⟨λ x, l x, subtype.ext _⟩,
   change ∑ i in s.attach, l i • (i : M) = n,

src/ring_theory/power_basis.lean

@@ -81,11 +81,11 @@ begin
   { ext n,
     simp_rw [set.mem_range, set.mem_image, finset.mem_coe, finset.mem_range],
     exact ⟨λ ⟨⟨i, hi⟩, hy⟩, ⟨i, hi, hy⟩, λ ⟨i, hi, hy⟩, ⟨⟨i, hi⟩, hy⟩⟩ },
-  simp only [this, finsupp.mem_span_iff_total, degree_lt_iff_coeff_zero, exists_iff_exists_finsupp,
-    coeff, aeval, eval₂_ring_hom', eval₂_eq_sum, polynomial.sum, support, finsupp.mem_supported',
-    finsupp.total, finsupp.sum, algebra.smul_def, eval₂_zero, exists_prop, linear_map.id_coe,
-    eval₂_one, id.def, not_lt, finsupp.coe_lsum, linear_map.coe_smul_right, finset.mem_range,
-    alg_hom.coe_mk, finset.mem_coe],
+  simp only [this, finsupp.mem_span_image_iff_total, degree_lt_iff_coeff_zero,
+    exists_iff_exists_finsupp, coeff, aeval, eval₂_ring_hom', eval₂_eq_sum, polynomial.sum, support,
+    finsupp.mem_supported', finsupp.total, finsupp.sum, algebra.smul_def, eval₂_zero, exists_prop,
+    linear_map.id_coe, eval₂_one, id.def, not_lt, finsupp.coe_lsum, linear_map.coe_smul_right,
+    finset.mem_range, alg_hom.coe_mk, finset.mem_coe],
   simp_rw [@eq_comm _ y],
   exact iff.rfl
 end