feat(linear_algebra,algebra,group_theory): miscellaneous lemmas linking some additive monoid and module operations (#11525)

This adds:
* `submodule.map_to_add_submonoid`
* `submodule.sup_to_add_submonoid`
* `submodule.supr_to_add_submonoid`

As well as some missing `add_submonoid` lemmas copied from the `submodule` API:
* `add_submonoid.closure_singleton_le_iff_mem`
* `add_submonoid.mem_supr`
* `add_submonoid.supr_eq_closure`

Finally, it generalizes some indices in `supr` and `infi` lemmas from `Type*` to `Sort*`.

This is pre-work for removing a redundant hypothesis from `submodule.mul_induction_on`.

Author: eric-wieser

src/algebra/algebra/bilinear.lean

@@ -51,10 +51,18 @@ variables (R)
 def lmul_left (r : A) : A →ₗ[R] A :=
 lmul R A r
 
+@[simp] lemma lmul_left_to_add_monoid_hom (r : A) :
+  (lmul_left R r : A →+ A) = add_monoid_hom.mul_left r :=
+fun_like.coe_injective rfl
+
 /-- The multiplication on the right in an algebra is a linear map. -/
 def lmul_right (r : A) : A →ₗ[R] A :=
 (lmul R A).to_linear_map.flip r
 
+@[simp] lemma lmul_right_to_add_monoid_hom (r : A) :
+  (lmul_right R r : A →+ A) = add_monoid_hom.mul_right r :=
+fun_like.coe_injective rfl
+
 /-- Simultaneous multiplication on the left and right is a linear map. -/
 def lmul_left_right (vw: A × A) : A →ₗ[R] A :=
 (lmul_right R vw.2).comp (lmul_left R vw.1)

src/group_theory/submonoid/basic.lean

@@ -318,6 +318,24 @@ lemma closure_union (s t : set M) : closure (s ∪ t) = closure s ⊔ closure t
 lemma closure_Union {ι} (s : ι → set M) : closure (⋃ i, s i) = ⨆ i, closure (s i) :=
 (submonoid.gi M).gc.l_supr
 
+@[simp, to_additive]
+lemma closure_singleton_le_iff_mem (m : M) (p : submonoid M) :
+  closure {m} ≤ p ↔ m ∈ p :=
+by rw [closure_le, singleton_subset_iff, set_like.mem_coe]
+
+@[to_additive]
+lemma mem_supr {ι : Sort*} (p : ι → submonoid M) {m : M} :
+  (m ∈ ⨆ i, p i) ↔ (∀ N, (∀ i, p i ≤ N) → m ∈ N) :=
+begin
+  rw [← closure_singleton_le_iff_mem, le_supr_iff],
+  simp only [closure_singleton_le_iff_mem],
+end
+
+@[to_additive]
+lemma supr_eq_closure {ι : Sort*} (p : ι → submonoid M) :
+  (⨆ i, p i) = submonoid.closure (⋃ i, (p i : set M)) :=
+by simp_rw [submonoid.closure_Union, submonoid.closure_eq]
+
 end submonoid
 
 namespace monoid_hom

src/linear_algebra/basic.lean

@@ -556,6 +556,10 @@ def map (f : M →ₛₗ[σ₁₂] M₂) (p : submodule R M) : submodule R₂ M
 @[simp] lemma map_coe (f : M →ₛₗ[σ₁₂] M₂) (p : submodule R M) :
   (map f p : set M₂) = f '' p := rfl
 
+lemma map_to_add_submonoid (f : M →ₛₗ[σ₁₂] M₂) (p : submodule R M) :
+  (p.map f).to_add_submonoid = p.to_add_submonoid.map f :=
+set_like.coe_injective rfl
+
 @[simp] lemma mem_map {f : M →ₛₗ[σ₁₂] M₂} {p : submodule R M} {x : M₂} :
   x ∈ map f p ↔ ∃ y, y ∈ p ∧ f y = x := iff.rfl
 
@@ -697,15 +701,15 @@ lemma map_sup_comap_of_surjective (p q : submodule R₂ M₂) :
   (p.comap f ⊔ q.comap f).map f = p ⊔ q :=
 (gi_map_comap hf).l_sup_u _ _
 
-lemma map_supr_comap_of_sujective (S : ι → submodule R₂ M₂) :
+lemma map_supr_comap_of_sujective {ι : Sort*} (S : ι → submodule R₂ M₂) :
   (⨆ i, (S i).comap f).map f = supr S :=
 (gi_map_comap hf).l_supr_u _
 
 lemma map_inf_comap_of_surjective (p q : submodule R₂ M₂) :
   (p.comap f ⊓ q.comap f).map f = p ⊓ q :=
 (gi_map_comap hf).l_inf_u _ _
 
-lemma map_infi_comap_of_surjective (S : ι → submodule R₂ M₂) :
+lemma map_infi_comap_of_surjective {ι : Sort*} (S : ι → submodule R₂ M₂) :
   (⨅ i, (S i).comap f).map f = infi S :=
 (gi_map_comap hf).l_infi_u _
 
@@ -739,13 +743,15 @@ lemma map_injective_of_injective : function.injective (map f) :=
 lemma comap_inf_map_of_injective (p q : submodule R M) : (p.map f ⊓ q.map f).comap f = p ⊓ q :=
 (gci_map_comap hf).u_inf_l _ _
 
-lemma comap_infi_map_of_injective (S : ι → submodule R M) : (⨅ i, (S i).map f).comap f = infi S :=
+lemma comap_infi_map_of_injective {ι : Sort*} (S : ι → submodule R M) :
+  (⨅ i, (S i).map f).comap f = infi S :=
 (gci_map_comap hf).u_infi_l _
 
 lemma comap_sup_map_of_injective (p q : submodule R M) : (p.map f ⊔ q.map f).comap f = p ⊔ q :=
 (gci_map_comap hf).u_sup_l _ _
 
-lemma comap_supr_map_of_injective (S : ι → submodule R M) : (⨆ i, (S i).map f).comap f = supr S :=
+lemma comap_supr_map_of_injective {ι : Sort*} (S : ι → submodule R M) :
+  (⨆ i, (S i).map f).comap f = supr S :=
 (gci_map_comap hf).u_supr_l _
 
 lemma map_le_map_iff_of_injective (p q : submodule R M) : p.map f ≤ q.map f ↔ p ≤ q :=
@@ -772,7 +778,7 @@ lemma eq_zero_of_bot_submodule : ∀(b : (⊥ : submodule R M)), b = 0
 
 /-- The infimum of a family of invariant submodule of an endomorphism is also an invariant
 submodule. -/
-lemma _root_.linear_map.infi_invariant {σ : R →+* R} [ring_hom_surjective σ] {ι : Type*}
+lemma _root_.linear_map.infi_invariant {σ : R →+* R} [ring_hom_surjective σ] {ι : Sort*}
   (f : M →ₛₗ[σ] M) {p : ι → submodule R M} (hf : ∀ i, ∀ v ∈ (p i), f v ∈ p i) :
   ∀ v ∈ infi p, f v ∈ infi p :=
 begin
@@ -1021,9 +1027,28 @@ by rintro ⟨y, hy, z, hz, rfl⟩; exact add_mem _
 lemma mem_sup' : x ∈ p ⊔ p' ↔ ∃ (y : p) (z : p'), (y:M) + z = x :=
 mem_sup.trans $ by simp only [set_like.exists, coe_mk]
 
+variables (p p')
+
 lemma coe_sup : ↑(p ⊔ p') = (p + p' : set M) :=
 by { ext, rw [set_like.mem_coe, mem_sup, set.mem_add], simp, }
 
+lemma sup_to_add_submonoid :
+  (p ⊔ p').to_add_submonoid = p.to_add_submonoid ⊔ p'.to_add_submonoid :=
+begin
+  ext x,
+  rw [mem_to_add_submonoid, mem_sup, add_submonoid.mem_sup],
+  refl,
+end
+
+lemma sup_to_add_subgroup {R M : Type*} [ring R] [add_comm_group M] [module R M]
+  (p p' : submodule R M) :
+  (p ⊔ p').to_add_subgroup = p.to_add_subgroup ⊔ p'.to_add_subgroup :=
+begin
+  ext x,
+  rw [mem_to_add_subgroup, mem_sup, add_subgroup.mem_sup],
+  refl,
+end
+
 end
 
 /- This is the character `∙`, with escape sequence `\.`, and is thus different from the scalar
@@ -1176,6 +1201,27 @@ le_antisymm
   (supr_le $ assume i, subset.trans (assume m hm, set.mem_Union.mpr ⟨i, hm⟩) subset_span)
   (span_le.mpr $ Union_subset_iff.mpr $ assume i m hm, mem_supr_of_mem i hm)
 
+lemma supr_to_add_submonoid {ι : Sort*} (p : ι → submodule R M) :
+  (⨆ i, p i).to_add_submonoid = ⨆ i, (p i).to_add_submonoid :=
+begin
+  refine le_antisymm (λ x, _) (supr_le $ λ i, to_add_submonoid_mono $ le_supr _ i),
+  simp_rw [supr_eq_span, add_submonoid.supr_eq_closure, mem_to_add_submonoid, coe_to_add_submonoid],
+  intros hx,
+  refine submodule.span_induction hx (λ x hx, _) _ (λ x y hx hy, _) (λ r x hx, _),
+  { exact add_submonoid.subset_closure hx },
+  { exact add_submonoid.zero_mem _ },
+  { exact add_submonoid.add_mem _ hx hy },
+  { apply add_submonoid.closure_induction hx,
+    { rintros x ⟨_, ⟨i, rfl⟩, hix : x ∈ p i⟩,
+      apply add_submonoid.subset_closure (set.mem_Union.mpr ⟨i, _⟩),
+      exact smul_mem _ r hix },
+    { rw smul_zero,
+      exact add_submonoid.zero_mem _ },
+    { intros x y hx hy,
+      rw smul_add,
+      exact add_submonoid.add_mem _ hx hy, } }
+end
+
 lemma span_singleton_le_iff_mem (m : M) (p : submodule R M) : (R ∙ m) ≤ p ↔ m ∈ p :=
 by rw [span_le, singleton_subset_iff, set_like.mem_coe]