feat(*/sub*/pointwise): lemmas about pointwise scalar actions (#17814)

Author: eric-wieser

src/algebra/algebra/tower.lean

@@ -256,7 +256,7 @@ span_induction hx (λ x hx, let ⟨p, q, hp, hq, hpq⟩ := set.mem_smul.1 hx in
   (λ x y ihx ihy, by { rw smul_add, exact add_mem ihx ihy })
   (λ c x hx, smul_comm c k x ▸ smul_mem _ _ hx)
 
-theorem span_smul {s : set S} (hs : span R s = ⊤) (t : set A) :
+theorem span_smul_of_span_eq_top {s : set S} (hs : span R s = ⊤) (t : set A) :
   span R (s • t) = (span S t).restrict_scalars R :=
 le_antisymm (span_le.2 $ λ x hx, let ⟨p, q, hps, hqt, hpqx⟩ := set.mem_smul.1 hx in
   hpqx ▸ (span S t).smul_mem p (subset_span hqt)) $

src/algebra/module/submodule/pointwise.lean

@@ -179,6 +179,13 @@ open_locale pointwise
 lemma smul_mem_pointwise_smul (m : M) (a : α) (S : submodule R M) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set M))
 
+/-- See also `submodule.smul_bot`. -/
+@[simp] lemma smul_bot' (a : α) : a • (⊥ : submodule R M) = ⊥ := map_bot _
+/-- See also `submodule.smul_sup`. -/
+lemma smul_sup' (a : α) (S T : submodule R M) : a • (S ⊔ T) = a • S ⊔ a • T := map_sup _ _ _
+lemma smul_span (a : α) (s : set M) : a • span R s = span R (a • s) := map_span _ _
+lemma span_smul (a : α) (s : set M) : span R (a • s) = a • span R s := eq.symm (span_image _).symm
+
 instance pointwise_central_scalar [distrib_mul_action αᵐᵒᵖ M] [smul_comm_class αᵐᵒᵖ R M]
   [is_central_scalar α M] :
   is_central_scalar α (submodule R M) :=

src/group_theory/subgroup/pointwise.lean

@@ -244,8 +244,11 @@ lemma mem_smul_pointwise_iff_exists (m : G) (a : α) (S : subgroup G) :
   m ∈ a • S ↔ ∃ (s : G), s ∈ S ∧ a • s = m :=
 (set.mem_smul_set : m ∈ a • (S : set G) ↔ _)
 
-@[simp] lemma smul_bot (a : α) : a • (⊥ : subgroup G) = ⊥ :=
-by simp [set_like.ext_iff, mem_smul_pointwise_iff_exists, eq_comm]
+@[simp] lemma smul_bot (a : α) : a • (⊥ : subgroup G) = ⊥ := map_bot _
+lemma smul_sup (a : α) (S T : subgroup G) : a • (S ⊔ T) = a • S ⊔ a • T := map_sup _ _ _
+
+lemma smul_closure (a : α) (s : set G) : a • closure s = closure (a • s) :=
+monoid_hom.map_closure _ _
 
 instance pointwise_central_scalar [mul_distrib_mul_action αᵐᵒᵖ G] [is_central_scalar α G] :
   is_central_scalar α (subgroup G) :=

src/group_theory/submonoid/pointwise.lean

@@ -197,6 +197,12 @@ lemma mem_smul_pointwise_iff_exists (m : M) (a : α) (S : submonoid M) :
   m ∈ a • S ↔ ∃ (s : M), s ∈ S ∧ a • s = m :=
 (set.mem_smul_set : m ∈ a • (S : set M) ↔ _)
 
+@[simp] lemma smul_bot (a : α) : a • (⊥ : submonoid M) = ⊥ := map_bot _
+lemma smul_sup (a : α) (S T : submonoid M) : a • (S ⊔ T) = a • S ⊔ a • T := map_sup _ _ _
+
+lemma smul_closure (a : α) (s : set M) : a • closure s = closure (a • s) :=
+monoid_hom.map_mclosure _ _
+
 instance pointwise_central_scalar [mul_distrib_mul_action αᵐᵒᵖ M] [is_central_scalar α M] :
   is_central_scalar α (submonoid M) :=
 ⟨λ a S, congr_arg (λ f : monoid.End M, S.map f) $ monoid_hom.ext $ by exact op_smul_eq_smul _⟩
@@ -293,6 +299,16 @@ open_locale pointwise
 lemma smul_mem_pointwise_smul (m : A) (a : α) (S : add_submonoid A) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set A))
 
+lemma mem_smul_pointwise_iff_exists (m : A) (a : α) (S : add_submonoid A) :
+  m ∈ a • S ↔ ∃ (s : A), s ∈ S ∧ a • s = m :=
+(set.mem_smul_set : m ∈ a • (S : set A) ↔ _)
+
+@[simp] lemma smul_bot (a : α) : a • (⊥ : add_submonoid A) = ⊥ := map_bot _
+lemma smul_sup (a : α) (S T : add_submonoid A) : a • (S ⊔ T) = a • S ⊔ a • T := map_sup _ _ _
+
+@[simp] lemma smul_closure (a : α) (s : set A) : a • closure s = closure (a • s) :=
+add_monoid_hom.map_mclosure _ _
+
 instance pointwise_central_scalar [distrib_mul_action αᵐᵒᵖ A] [is_central_scalar α A] :
   is_central_scalar α (add_submonoid A) :=
 ⟨λ a S, congr_arg (λ f : add_monoid.End A, S.map f) $
@@ -313,10 +329,6 @@ lemma mem_pointwise_smul_iff_inv_smul_mem {a : α} {S : add_submonoid A} {x : A}
   x ∈ a • S ↔ a⁻¹ • x ∈ S :=
 mem_smul_set_iff_inv_smul_mem
 
-lemma mem_smul_pointwise_iff_exists (m : A) (a : α) (S : add_submonoid A) :
-  m ∈ a • S ↔ ∃ (s : A), s ∈ S ∧ a • s = m :=
-(set.mem_smul_set : m ∈ a • (S : set A) ↔ _)
-
 lemma mem_inv_pointwise_smul_iff {a : α} {S : add_submonoid A} {x : A} : x ∈ a⁻¹ • S ↔ a • x ∈ S :=
 mem_inv_smul_set_iff
 

src/ring_theory/finiteness.lean

@@ -502,7 +502,7 @@ lemma trans {R : Type*} (A B : Type*) [comm_semiring R] [comm_semiring A] [algeb
 | ⟨⟨s, hs⟩⟩ ⟨⟨t, ht⟩⟩ := ⟨submodule.fg_def.2
   ⟨set.image2 (•) (↑s : set A) (↑t : set B),
     set.finite.image2 _ s.finite_to_set t.finite_to_set,
-    by rw [set.image2_smul, submodule.span_smul hs (↑t : set B),
+    by rw [set.image2_smul, submodule.span_smul_of_span_eq_top hs (↑t : set B),
       ht, submodule.restrict_scalars_top]⟩⟩
 
 end algebra

src/ring_theory/ideal/operations.lean

@@ -195,10 +195,6 @@ begin
   simpa
 end
 
-lemma span_smul_eq (r : R) (s : set M) : span R (r • s) = r • span R s :=
-by rw [← ideal_span_singleton_smul, span_smul_span, ←set.image2_eq_Union,
-    set.image2_singleton_left, set.image_smul]
-
 lemma mem_of_span_top_of_smul_mem (M' : submodule R M)
   (s : set R) (hs : ideal.span s = ⊤) (x : M) (H : ∀ r : s, (r : R) • x ∈ M') : x ∈ M' :=
 begin

src/ring_theory/local_properties.lean

@@ -417,7 +417,7 @@ begin
     by simp_rw [algebra.algebra_map_eq_smul_one, smul_assoc, one_smul],
   rw [← e, this] at hx₁,
   replace hx₁ := congr_arg (submodule.span R) hx₁,
-  rw submodule.span_smul_eq at hx₁,
+  rw submodule.span_smul at hx₁,
   replace hx : _ ∈ y' • submodule.span R (s : set S') := set.smul_mem_smul_set hx,
   rw hx₁ at hx,
   erw [← g.map_smul, ← submodule.map_span (g : S →ₗ[R] S')] at hx,

src/ring_theory/subring/pointwise.lean

@@ -62,6 +62,12 @@ lemma mem_smul_pointwise_iff_exists (m : M) (r : R) (S : subring R) :
   r ∈ m • S ↔ ∃ (s : R), s ∈ S ∧ m • s = r :=
 (set.mem_smul_set : r ∈ m • (S : set R) ↔ _)
 
+@[simp] lemma smul_bot (a : M) : a • (⊥ : subring R) = ⊥ := map_bot _
+lemma smul_sup (a : M) (S T : subring R) : a • (S ⊔ T) = a • S ⊔ a • T := map_sup _ _ _
+
+lemma smul_closure (a : M) (s : set R) : a • closure s = closure (a • s) :=
+ring_hom.map_closure _ _
+
 instance pointwise_central_scalar [mul_semiring_action Mᵐᵒᵖ R] [is_central_scalar M R] :
   is_central_scalar M (subring R) :=
 ⟨λ a S, congr_arg (λ f, S.map f) $ ring_hom.ext $ by exact op_smul_eq_smul _⟩

src/ring_theory/subsemiring/pointwise.lean

@@ -58,6 +58,12 @@ lemma mem_smul_pointwise_iff_exists (m : M) (r : R) (S : subsemiring R) :
   r ∈ m • S ↔ ∃ (s : R), s ∈ S ∧ m • s = r :=
 (set.mem_smul_set : r ∈ m • (S : set R) ↔ _)
 
+@[simp] lemma smul_bot (a : M) : a • (⊥ : subsemiring R) = ⊥ := map_bot _
+lemma smul_sup (a : M) (S T : subsemiring R) : a • (S ⊔ T) = a • S ⊔ a • T := map_sup _ _ _
+
+lemma smul_closure (a : M) (s : set R) : a • closure s = closure (a • s) :=
+ring_hom.map_sclosure _ _
+
 instance pointwise_central_scalar [mul_semiring_action Mᵐᵒᵖ R] [is_central_scalar M R] :
   is_central_scalar M (subsemiring R) :=
 ⟨λ a S, congr_arg (λ f, S.map f) $ ring_hom.ext $ by exact op_smul_eq_smul _⟩