feat(algebra/module/submodule_lattice): add lemmas for nat submodules (…

…#7221)

This has been suggested by @eric-wieser (who also wrote everything) in #7200.

This also:
* Merges `span_nat_eq_add_group_closure` and `submodule.span_eq_add_submonoid.closure` which are the same statement into `submodule.span_nat_eq_add_submonoid_closure`, which generalizes the former from `semiring` to `add_comm_monoid`.
* Renames `span_int_eq_add_group_closure` to `submodule.span_nat_eq_add_subgroup_closure`, and generalizes it from `ring` to `add_comm_group`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/algebra/basic.lean

@@ -1252,26 +1252,6 @@ end algebra
 
 end ring
 
-section nat
-
-variables (R : Type*) [semiring R]
-
-section span_nat
-open submodule
-
-lemma span_nat_eq_add_group_closure (s : set R) :
-  (span ℕ s).to_add_submonoid = add_submonoid.closure s :=
-eq.symm $ add_submonoid.closure_eq_of_le subset_span $ λ x hx, span_induction hx
-  (λ x hx, add_submonoid.subset_closure hx) (add_submonoid.zero_mem _)
-  (λ _ _, add_submonoid.add_mem _) (λ _ _ _, add_submonoid.nsmul_mem _ ‹_› _)
-
-@[simp] lemma span_nat_eq (s : add_submonoid R) : (span ℕ (s : set R)).to_add_submonoid = s :=
-by rw [span_nat_eq_add_group_closure, s.closure_eq]
-
-end span_nat
-
-end nat
-
 section int
 
 variables (R : Type*) [ring R]
@@ -1284,26 +1264,10 @@ instance algebra_int : algebra ℤ R :=
 
 variables {R}
 
-section
 variables {S : Type*} [ring S]
 
 instance int_algebra_subsingleton : subsingleton (algebra ℤ S) :=
 ⟨λ P Q, by { ext, simp, }⟩
-end
-
-section span_int
-open submodule
-
-lemma span_int_eq_add_group_closure (s : set R) :
-  (span ℤ s).to_add_subgroup = add_subgroup.closure s :=
-eq.symm $ add_subgroup.closure_eq_of_le _ subset_span $ λ x hx, span_induction hx
-  (λ x hx, add_subgroup.subset_closure hx) (add_subgroup.zero_mem _)
-  (λ _ _, add_subgroup.add_mem _) (λ _ _ _, add_subgroup.gsmul_mem _ ‹_› _)
-
-@[simp] lemma span_int_eq (s : add_subgroup R) : (span ℤ (s : set R)).to_add_subgroup = s :=
-by rw [span_int_eq_add_group_closure, s.closure_eq]
-
-end span_int
 
 end int
 

src/algebra/module/submodule_lattice.lean

@@ -159,4 +159,35 @@ show s ≤ Sup S, from le_Sup hs
 
 end submodule
 
+section nat_submodule
+
+/-- An additive submonoid is equivalent to a ℕ-submodule. -/
+def add_submonoid.to_nat_submodule : add_submonoid M ≃o submodule ℕ M :=
+{ to_fun := λ S,
+  { smul_mem' := λ r s hs, S.nsmul_mem hs _, ..S },
+  inv_fun := submodule.to_add_submonoid,
+  left_inv := λ ⟨S, _, _⟩, rfl,
+  right_inv := λ ⟨S, _, _, _⟩, rfl,
+  map_rel_iff' := λ a b, iff.rfl }
+
+@[simp]
+lemma add_submonoid.to_nat_submodule_symm :
+  ⇑(add_submonoid.to_nat_submodule.symm : _ ≃o add_submonoid M) = submodule.to_add_submonoid := rfl
+
+@[simp]
+lemma add_submonoid.coe_to_nat_submodule (S : add_submonoid M) :
+  (S.to_nat_submodule : set M) = S := rfl
+
+@[simp]
+lemma add_submonoid.to_nat_submodule_to_add_submonoid (S : add_submonoid M) :
+  S.to_nat_submodule.to_add_submonoid = S :=
+add_submonoid.to_nat_submodule.symm_apply_apply S
+
+@[simp]
+lemma submodule.to_add_submonoid_to_nat_submodule (S : submodule ℕ M) :
+  S.to_add_submonoid.to_nat_submodule = S :=
+add_submonoid.to_nat_submodule.apply_symm_apply S
+
+end nat_submodule
+
 end add_comm_monoid

src/linear_algebra/basic.lean

@@ -759,16 +759,28 @@ preserved under addition and scalar multiplication, then `p` holds for all eleme
   (H2 : ∀ (a:R) x, p x → p (a • x)) : p x :=
 (@span_le _ _ _ _ _ _ ⟨p, H0, H1, H2⟩).2 Hs h
 
-lemma span_eq_add_submonoid.closure {M : Type*} [add_comm_monoid M] (S : set M) :
-  (span ℕ S).to_add_submonoid = add_submonoid.closure S :=
+lemma span_nat_eq_add_submonoid_closure (s : set M) :
+  (span ℕ s).to_add_submonoid = add_submonoid.closure s :=
 begin
-  refine (add_submonoid.closure_eq_of_le (by exact subset_span) _).symm,
-  rintros m (hm : m ∈ (span ℕ S)),
-  exact submodule.span_induction hm (λ s hs, add_submonoid.subset_closure hs)
-    (add_submonoid.zero_mem _) (λ x y hx hy, add_submonoid.add_mem _ hx hy)
-    (λ a m hm, add_submonoid.nsmul_mem _ hm _)
+  refine eq.symm (add_submonoid.closure_eq_of_le subset_span _),
+  apply add_submonoid.to_nat_submodule.symm.to_galois_connection.l_le _,
+  rw span_le,
+  exact add_submonoid.subset_closure,
 end
 
+@[simp] lemma span_nat_eq (s : add_submonoid M) : (span ℕ (s : set M)).to_add_submonoid = s :=
+by rw [span_nat_eq_add_submonoid_closure, s.closure_eq]
+
+lemma span_int_eq_add_subgroup_closure {M : Type*} [add_comm_group M] (s : set M) :
+  (span ℤ s).to_add_subgroup = add_subgroup.closure s :=
+eq.symm $ add_subgroup.closure_eq_of_le _ subset_span $ λ x hx, span_induction hx
+  (λ x hx, add_subgroup.subset_closure hx) (add_subgroup.zero_mem _)
+  (λ _ _, add_subgroup.add_mem _) (λ _ _ _, add_subgroup.gsmul_mem _ ‹_› _)
+
+@[simp] lemma span_int_eq {M : Type*} [add_comm_group M] (s : add_subgroup M) :
+  (span ℤ (s : set M)).to_add_subgroup = s :=
+by rw [span_int_eq_add_subgroup_closure, s.closure_eq]
+
 section
 variables (R M)