feat(algebra/module/linear_map): interaction of linear maps and point…

…wise operations on sets (#10821)

src/algebra/module/linear_map.lean

@@ -195,6 +195,42 @@ protected lemma map_zero : f 0 = 0 := map_zero f
 @[simp] lemma map_eq_zero_iff (h : function.injective f) {x : M} : f x = 0 ↔ x = 0 :=
 ⟨λ w, by { apply h, simp [w], }, λ w, by { subst w, simp, }⟩
 
+section pointwise
+open_locale pointwise
+
+@[simp] lemma image_smul_setₛₗ (c : R) (s : set M) :
+  f '' (c • s) = (σ c) • f '' s :=
+begin
+  apply set.subset.antisymm,
+  { rintros x ⟨y, ⟨z, zs, rfl⟩, rfl⟩,
+    exact ⟨f z, set.mem_image_of_mem _ zs, (f.map_smulₛₗ _ _).symm ⟩ },
+  { rintros x ⟨y, ⟨z, hz, rfl⟩, rfl⟩,
+    exact (set.mem_image _ _ _).2 ⟨c • z, set.smul_mem_smul_set hz, f.map_smulₛₗ _ _⟩ }
+end
+
+lemma image_smul_set (c : R) (s : set M) :
+  fₗ '' (c • s) = c • fₗ '' s :=
+by simp
+
+lemma preimage_smul_setₛₗ {c : R} (hc : is_unit c) (s : set M₃) :
+  f ⁻¹' (σ c • s) = c • f ⁻¹' s :=
+begin
+  apply set.subset.antisymm,
+  { rintros x ⟨y, ys, hy⟩,
+    refine ⟨(hc.unit.inv : R) • x, _, _⟩,
+    { simp only [←hy, smul_smul, set.mem_preimage, units.inv_eq_coe_inv, map_smulₛₗ, ← σ.map_mul,
+        is_unit.coe_inv_mul, one_smul, ring_hom.map_one, ys] },
+    { simp only [smul_smul, is_unit.mul_coe_inv, one_smul, units.inv_eq_coe_inv] } },
+  { rintros x ⟨y, hy, rfl⟩,
+    refine ⟨f y, hy, by simp only [ring_hom.id_apply, linear_map.map_smulₛₗ]⟩ }
+end
+
+lemma preimage_smul_set {c : R} (hc : is_unit c) (s : set M₂) :
+  fₗ ⁻¹' (c • s) = c • fₗ ⁻¹' s :=
+fₗ.preimage_smul_setₛₗ hc s
+
+end pointwise
+
 variables (M M₂)
 /--
 A typeclass for `has_scalar` structures which can be moved through a `linear_map`.

src/algebra/pointwise.lean

@@ -668,6 +668,10 @@ lemma subsingleton_zero_smul_set [has_zero α] [has_zero β] [smul_with_zero α
   ((0 : α) • s).subsingleton :=
 subsingleton_singleton.mono (zero_smul_subset s)
 
+lemma smul_add_set [monoid α] [add_monoid β] [distrib_mul_action α β] (c : α) (s t : set β) :
+  c • (s + t) = c • s + c • t :=
+image_add (distrib_mul_action.to_add_monoid_hom β c).to_add_hom
+
 section group
 variables [group α] [mul_action α β] {A B : set β} {a : α} {x : β}
 

src/data/equiv/module.lean

@@ -291,12 +291,10 @@ equiv.bijective ⟨(symm : (M ≃ₛₗ[σ] M₂) →
   M₂ ≃ₛₗ[σ'] M) = e.symm :=
 symm_bijective.injective $ ext $ λ x, rfl
 
-include σ'
 @[simp] theorem symm_mk (f h₁ h₂ h₃ h₄) :
   (⟨e, h₁, h₂, f, h₃, h₄⟩ : M ≃ₛₗ[σ] M₂).symm =
   { to_fun := f, inv_fun := e,
     ..(⟨e, h₁, h₂, f, h₃, h₄⟩ : M ≃ₛₗ[σ] M₂).symm } := rfl
-omit σ'
 
 @[simp] lemma coe_symm_mk [module R M] [module R M₂]
   {to_fun inv_fun map_add map_smul left_inv right_inv} :
@@ -307,10 +305,35 @@ protected lemma bijective : function.bijective e := e.to_equiv.bijective
 protected lemma injective : function.injective e := e.to_equiv.injective
 protected lemma surjective : function.surjective e := e.to_equiv.surjective
 
-include σ'
 protected lemma image_eq_preimage (s : set M) : e '' s = e.symm ⁻¹' s :=
 e.to_equiv.image_eq_preimage s
-omit σ'
+
+protected lemma image_symm_eq_preimage (s : set M₂) : e.symm '' s = e ⁻¹' s :=
+e.to_equiv.symm.image_eq_preimage s
+
+section pointwise
+open_locale pointwise
+
+@[simp] lemma image_smul_setₛₗ (c : R) (s : set M) :
+  e '' (c • s) = (σ c) • e '' s :=
+linear_map.image_smul_setₛₗ e.to_linear_map c s
+
+@[simp] lemma preimage_smul_setₛₗ (c : S) (s : set M₂) :
+  e ⁻¹' (c • s) = σ' c • e ⁻¹' s :=
+by rw [← linear_equiv.image_symm_eq_preimage, ← linear_equiv.image_symm_eq_preimage,
+  image_smul_setₛₗ]
+
+include module_M₁ module_N₁
+
+@[simp] lemma image_smul_set (e : M₁ ≃ₗ[R₁] N₁) (c : R₁) (s : set M₁) :
+  e '' (c • s) = c • e '' s :=
+linear_map.image_smul_set e.to_linear_map c s
+
+@[simp] lemma preimage_smul_set (e : M₁ ≃ₗ[R₁] N₁) (c : R₁) (s : set N₁) :
+  e ⁻¹' (c • s) = c • e ⁻¹' s :=
+e.preimage_smul_setₛₗ c s
+
+end pointwise
 
 end
 

src/topology/algebra/module.lean

@@ -282,10 +282,11 @@ variables
 {R₁ : Type*} {R₂ : Type*} {R₃ : Type*} [semiring R₁] [semiring R₂] [semiring R₃]
 {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃}
 {M₁ : Type*} [topological_space M₁] [add_comm_monoid M₁]
+{M'₁ : Type*} [topological_space M'₁] [add_comm_monoid M'₁]
 {M₂ : Type*} [topological_space M₂] [add_comm_monoid M₂]
 {M₃ : Type*} [topological_space M₃] [add_comm_monoid M₃]
 {M₄ : Type*} [topological_space M₄] [add_comm_monoid M₄]
-[module R₁ M₁] [module R₂ M₂] [module R₃ M₃]
+[module R₁ M₁] [module R₁ M'₁] [module R₂ M₂] [module R₃ M₃]
 
 /-- Coerce continuous linear maps to linear maps. -/
 instance : has_coe (M₁ →SL[σ₁₂] M₂) (M₁ →ₛₗ[σ₁₂] M₂) := ⟨to_linear_map⟩
@@ -335,7 +336,7 @@ fun_like.ext f g h
 theorem ext_iff {f g : M₁ →SL[σ₁₂] M₂} : f = g ↔ ∀ x, f x = g x :=
 fun_like.ext_iff
 
-variables (f g : M₁ →SL[σ₁₂] M₂) (c : R₁) (h : M₂ →SL[σ₂₃] M₃) (x y z : M₁)
+variables (f g : M₁ →SL[σ₁₂] M₂) (c : R₁) (h : M₂ →SL[σ₂₃] M₃) (x y z : M₁) (fₗ : M₁ →L[R₁] M'₁)
 
 -- make some straightforward lemmas available to `simp`.
 protected lemma map_zero : f (0 : M₁) = 0 := map_zero f
@@ -744,6 +745,27 @@ rfl
 
 end
 
+section pointwise
+open_locale pointwise
+
+@[simp] lemma image_smul_setₛₗ (c : R₁) (s : set M₁) :
+  f '' (c • s) = (σ₁₂ c) • f '' s :=
+f.to_linear_map.image_smul_setₛₗ c s
+
+lemma image_smul_set (c : R₁) (s : set M₁) :
+  fₗ '' (c • s) = c • fₗ '' s :=
+fₗ.to_linear_map.image_smul_set c s
+
+lemma preimage_smul_setₛₗ {c : R₁} (hc : is_unit c) (s : set M₂) :
+  f ⁻¹' (σ₁₂ c • s) = c • f ⁻¹' s :=
+f.to_linear_map.preimage_smul_setₛₗ hc s
+
+lemma preimage_smul_set {c : R₁} (hc : is_unit c) (s : set M'₁) :
+  fₗ ⁻¹' (c • s) = c • fₗ ⁻¹' s :=
+fₗ.to_linear_map.preimage_smul_set hc s
+
+end pointwise
+
 variables [module R₁ M₂] [topological_space R₁] [has_continuous_smul R₁ M₂]
 
 @[simp]
@@ -1176,10 +1198,11 @@ variables {R₁ : Type*} {R₂ : Type*} {R₃ : Type*} [semiring R₁] [semiring
 {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃]
 [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
 {M₁ : Type*} [topological_space M₁] [add_comm_monoid M₁]
+{M'₁ : Type*} [topological_space M'₁] [add_comm_monoid M'₁]
 {M₂ : Type*} [topological_space M₂] [add_comm_monoid M₂]
 {M₃ : Type*} [topological_space M₃] [add_comm_monoid M₃]
 {M₄ : Type*} [topological_space M₄] [add_comm_monoid M₄]
-[module R₁ M₁] [module R₂ M₂] [module R₃ M₃]
+[module R₁ M₁] [module R₁ M'₁] [module R₂ M₂] [module R₃ M₃]
 
 include σ₂₁
 /-- A continuous linear equivalence induces a continuous linear map. -/
@@ -1463,6 +1486,29 @@ rfl
 rfl
 omit σ₂₁
 
+section pointwise
+open_locale pointwise
+include σ₂₁
+
+@[simp] lemma image_smul_setₛₗ (e : M₁ ≃SL[σ₁₂] M₂) (c : R₁) (s : set M₁) :
+  e '' (c • s) = (σ₁₂ c) • e '' s :=
+e.to_linear_equiv.image_smul_setₛₗ c s
+
+@[simp] lemma preimage_smul_setₛₗ (e : M₁ ≃SL[σ₁₂] M₂) (c : R₂) (s : set M₂) :
+  e ⁻¹' (c • s) = σ₂₁ c • e ⁻¹' s :=
+e.to_linear_equiv.preimage_smul_setₛₗ c s
+omit σ₂₁
+
+@[simp] lemma image_smul_set (e : M₁ ≃L[R₁] M'₁) (c : R₁) (s : set M₁) :
+  e '' (c • s) = c • e '' s :=
+e.to_linear_equiv.image_smul_set c s
+
+@[simp] lemma preimage_smul_set (e : M₁ ≃L[R₁] M'₁) (c : R₁) (s : set M'₁) :
+  e ⁻¹' (c • s) = c • e ⁻¹' s :=
+e.to_linear_equiv.preimage_smul_set c s
+
+end pointwise
+
 variable (M₁)
 
 /-- The continuous linear equivalences from `M` to itself form a group under composition. -/