[Merged by Bors] - feat(linear_algebra/basic): some lemmas about span and restrict_scalars

src/algebra/algebra/basic.lean

@@ -1393,17 +1393,6 @@ variables [add_comm_monoid N] [module R N] [module S N] [is_scalar_tower R S N]
 
 variables {S M N}
 
-namespace submodule
-
-variables (R S M)
-
-/-- If `S` is an `R`-algebra, then the `R`-module generated by a set `X` is included in the
-`S`-module generated by `X`. -/
-lemma span_le_restrict_scalars (X : set M) : span R (X : set M) ≤ restrict_scalars R (span S X) :=
-submodule.span_le.mpr submodule.subset_span
-
-end submodule
-
 @[simp]
 lemma linear_map.ker_restrict_scalars (f : M →ₗ[S] N) :
   (f.restrict_scalars R).ker = f.ker.restrict_scalars R :=
@@ -1422,7 +1411,7 @@ variables [module R M] [module A M] [is_scalar_tower R A M]
 lemma span_eq_restrict_scalars (X : set M) (hsur : function.surjective (algebra_map R A)) :
   span R X = restrict_scalars R (span A X) :=
 begin
-  apply (span_le_restrict_scalars R A M X).antisymm (λ m hm, _),
+  apply (span_le_restrict_scalars R A X).antisymm (λ m hm, _),
   refine span_induction hm subset_span (zero_mem _) (λ _ _, add_mem _) (λ a m hm, _),
   obtain ⟨r, rfl⟩ := hsur a,
   simpa [algebra_map_smul] using smul_mem _ r hm

src/algebra/module/submodule.lean

@@ -211,23 +211,29 @@ variables (S) [semiring S] [module S M] [module R M] [has_scalar S R] [is_scalar
 `V.restrict_scalars S` is the `S`-submodule of the `S`-module given by restriction of scalars,
 corresponding to `V`, an `R`-submodule of the original `R`-module.
 -/
-@[simps]
 def restrict_scalars (V : submodule R M) : submodule S M :=
-{ carrier := V.carrier,
+{ carrier := V,
   zero_mem' := V.zero_mem,
   smul_mem' := λ c m h, V.smul_of_tower_mem c h,
   add_mem' := λ x y hx hy, V.add_mem hx hy }
 
 @[simp]
-lemma restrict_scalars_mem (V : submodule R M) (m : M) :
-  m ∈ V.restrict_scalars S ↔ m ∈ V :=
+lemma coe_restrict_scalars (V : submodule R M) : (V.restrict_scalars S : set M) = V :=
+rfl
+
+@[simp]
+lemma restrict_scalars_mem (V : submodule R M) (m : M) : m ∈ V.restrict_scalars S ↔ m ∈ V :=
 iff.refl _
 
+@[simp]
+lemma restrict_scalars_self (V : submodule R M) : V.restrict_scalars R = V :=
+set_like.coe_injective rfl
+
 variables (R S M)
 
 lemma restrict_scalars_injective :
   function.injective (restrict_scalars S : submodule R M → submodule S M) :=
-λ V₁ V₂ h, ext $ by convert set.ext_iff.1 (set_like.ext'_iff.1 h); refl
+λ V₁ V₂ h, ext $ set.ext_iff.1 (set_like.ext'_iff.1 h : _)
 
 @[simp] lemma restrict_scalars_inj {V₁ V₂ : submodule R M} :
   restrict_scalars S V₁ = restrict_scalars S V₂ ↔ V₁ = V₂ :=

src/linear_algebra/basic.lean

@@ -62,6 +62,7 @@ open function
 open_locale big_operators pointwise
 
 variables {R : Type*} {R₁ : Type*} {R₂ : Type*} {R₃ : Type*} {R₄ : Type*}
+variables {S : Type*}
 variables {K : Type*} {K₂ : Type*}
 variables {M : Type*} {M' : Type*} {M₁ : Type*} {M₂ : Type*} {M₃ : Type*} {M₄ : Type*}
 variables {N : Type*} {N₂ : Type*}
@@ -219,7 +220,7 @@ add_monoid_hom.map_sum ((add_monoid_hom.eval b).comp to_add_monoid_hom') f _
 
 section smul_right
 
-variables {S : Type*} [semiring S] [module R S] [module S M] [is_scalar_tower R S M]
+variables [semiring S] [module R S] [module S M] [is_scalar_tower R S M]
 
 /-- When `f` is an `R`-linear map taking values in `S`, then `λb, f b • x` is an `R`-linear map. -/
 def smul_right (f : M₁ →ₗ[R] S) (x : M) : M₁ →ₗ[R] M :=
@@ -338,7 +339,7 @@ end add_comm_monoid
 
 section module
 
-variables {S : Type*} [semiring R] [semiring S]
+variables [semiring R] [semiring S]
   [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃]
   [module R M] [module R M₂] [module R M₃]
   [module S M₂] [module S M₃] [smul_comm_class R S M₂] [smul_comm_class R S M₃]
@@ -800,9 +801,15 @@ span_le.2 $ subset.trans h subset_span
 lemma span_eq_of_le (h₁ : s ⊆ p) (h₂ : p ≤ span R s) : span R s = p :=
 le_antisymm (span_le.2 h₁) h₂
 
-@[simp] lemma span_eq : span R (p : set M) = p :=
+lemma span_eq : span R (p : set M) = p :=
 span_eq_of_le _ (subset.refl _) subset_span
 
+/-- A version of `submodule.span_eq` for when the span is by a smaller ring. -/
+@[simp] lemma span_coe_eq_restrict_scalars
+  [semiring S] [has_scalar S R] [module S M] [is_scalar_tower S R M] :
+  span S (p : set M) = p.restrict_scalars S :=
+span_eq (p.restrict_scalars S)
+
 lemma map_span [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M) :
   (span R s).map f = span R₂ (f '' s) :=
 eq.symm $ span_eq_of_le _ (set.image_subset f subset_span) $
@@ -1055,6 +1062,26 @@ span_eq_of_le _ (set.insert_subset.mpr ⟨h, subset_span⟩) (span_mono $ subset
 
 lemma span_span : span R (span R s : set M) = span R s := span_eq _
 
+variables (R S s)
+
+/-- If `R` is "smaller" ring than `S` then the span by `R` is smaller than the span by `S`. -/
+lemma span_le_restrict_scalars [semiring S] [has_scalar R S] [module S M] [is_scalar_tower R S M] :
+  span R s ≤ (span S s).restrict_scalars R :=
+submodule.span_le.2 submodule.subset_span
+
+/-- A version of `submodule.span_le_restrict_scalars` with coercions. -/
+@[simp] lemma span_subset_span [semiring S] [has_scalar R S] [module S M] [is_scalar_tower R S M] :
+  ↑(span R s) ⊆ (span S s : set M) :=
+span_le_restrict_scalars R S s
+
+/-- Taking the span by a large ring of the span by the small ring is the same as taking the span
+by just the large ring. -/
+lemma span_span_of_tower [semiring S] [has_scalar R S] [module S M] [is_scalar_tower R S M] :
+  span S (span R s : set M) = span S s :=
+le_antisymm (span_le.2 $ span_subset_span R S s) (span_mono subset_span)
+
+variables {R S s}
+
 lemma span_eq_bot : span R (s : set M) = ⊥ ↔ ∀ x ∈ s, (x:M) = 0 :=
 eq_bot_iff.trans ⟨
   λ H x h, (mem_bot R).1 $ H $ subset_span h,

src/linear_algebra/finsupp.lean

@@ -336,7 +336,7 @@ A slight rearrangement from `lsum` gives us
 the bijection underlying the free-forgetful adjunction for R-modules.
 -/
 noncomputable def lift : (X → M) ≃+ ((X →₀ R) →ₗ[R] M) :=
-(add_equiv.arrow_congr (equiv.refl X) (ring_lmap_equiv_self R M ℕ).to_add_equiv.symm).trans
+(add_equiv.arrow_congr (equiv.refl X) (ring_lmap_equiv_self R ℕ M).to_add_equiv.symm).trans
   (lsum _ : _ ≃ₗ[ℕ] _).to_add_equiv
 
 @[simp]

src/linear_algebra/pi.lean

@@ -302,7 +302,7 @@ Otherwise, `S = ℕ` shows that the equivalence is additive.
 See note [bundled maps over different rings]. -/
 def pi_ring : ((ι → R) →ₗ[R] M) ≃ₗ[S] (ι → M) :=
 (linear_map.lsum R (λ i : ι, R) S).symm.trans
-  (Pi_congr_right $ λ i, linear_map.ring_lmap_equiv_self R M S)
+  (Pi_congr_right $ λ i, linear_map.ring_lmap_equiv_self R S M)
 
 variables {ι R M}
 

src/ring_theory/finiteness.lean

@@ -99,7 +99,7 @@ begin
   rw [finite_def, fg_def] at hM ⊢,
   obtain ⟨S, hSfin, hSgen⟩ := hM,
   refine ⟨S, hSfin, eq_top_iff.2 _⟩,
-  have := submodule.span_le_restrict_scalars R A M S,
+  have := submodule.span_le_restrict_scalars R A S,
   rw hSgen at this,
   exact this
 end