feat(topology/algebra/module): 2 new ext lemmas (#6211)

Add ext lemmas for maps `f : M × M₂ →L[R] M₃` and `f : R →L[R] M`.

Author: urkud

src/analysis/normed_space/bounded_linear_maps.lean

@@ -398,14 +398,12 @@ variables {𝕜}
 lemma is_bounded_bilinear_map.is_bounded_linear_map_deriv (h : is_bounded_bilinear_map 𝕜 f) :
   is_bounded_linear_map 𝕜 (λp : E × F, h.deriv p) :=
 begin
-  rcases h.bound with ⟨C, Cpos, hC⟩,
+  rcases h.bound with ⟨C, Cpos : 0 < C, hC⟩,
   refine is_linear_map.with_bound ⟨λp₁ p₂, _, λc p, _⟩ (C + C) (λp, _),
-  { ext q,
-    simp [h.add_left, h.add_right], abel },
-  { ext q,
-    simp [h.smul_left, h.smul_right, smul_add] },
+  { ext; simp [h.add_left, h.add_right]; abel },
+  { ext; simp [h.smul_left, h.smul_right, smul_add] },
   { refine continuous_linear_map.op_norm_le_bound _
-      (mul_nonneg (add_nonneg (le_of_lt Cpos) (le_of_lt Cpos)) (norm_nonneg _)) (λq, _),
+      (mul_nonneg (add_nonneg Cpos.le Cpos.le) (norm_nonneg _)) (λq, _),
     calc ∥f (p.1, q.2) + f (q.1, p.2)∥
       ≤ C * ∥p.1∥ * ∥q.2∥ + C * ∥q.1∥ * ∥p.2∥ : norm_add_le_of_le (hC _ _) (hC _ _)
     ... ≤ C * ∥p∥ * ∥q∥ + C * ∥q∥ * ∥p∥ : by apply_rules [add_le_add, mul_le_mul, norm_nonneg,

src/linear_algebra/prod.lean

@@ -95,16 +95,20 @@ section
 variables (R M M₂)
 
 /-- The left injection into a product is a linear map. -/
-def inl : M →ₗ[R] M × M₂ := by refine ⟨add_monoid_hom.inl _ _, _, _⟩; intros; simp
+def inl : M →ₗ[R] M × M₂ := prod linear_map.id 0
 
 /-- The right injection into a product is a linear map. -/
-def inr : M₂ →ₗ[R] M × M₂ := by refine ⟨add_monoid_hom.inr _ _, _, _⟩; intros; simp
+def inr : M₂ →ₗ[R] M × M₂ := prod 0 linear_map.id
 
 end
 
 @[simp] theorem inl_apply (x : M) : inl R M M₂ x = (x, 0) := rfl
 @[simp] theorem inr_apply (x : M₂) : inr R M M₂ x = (0, x) := rfl
 
+theorem inl_eq_prod : inl R M M₂ = prod linear_map.id 0 := rfl
+
+theorem inr_eq_prod : inr R M M₂ = prod 0 linear_map.id := rfl
+
 theorem inl_injective : function.injective (inl R M M₂) :=
 λ _, by simp
 
@@ -138,10 +142,6 @@ theorem fst_eq_coprod : fst R M M₂ = coprod linear_map.id 0 := by ext; simp
 
 theorem snd_eq_coprod : snd R M M₂ = coprod 0 linear_map.id := by ext; simp
 
-theorem inl_eq_prod : inl R M M₂ = prod linear_map.id 0 := rfl
-
-theorem inr_eq_prod : inr R M M₂ = prod 0 linear_map.id := rfl
-
 /-- Taking the product of two maps with the same codomain is equivalent to taking the product of
 their domains. -/
 @[simps] def coprod_equiv [semimodule S M₃] [smul_comm_class R S M₃] :
@@ -155,6 +155,10 @@ their domains. -/
   map_smul' := λ r a,
     by { ext, simp only [smul_add, smul_apply, prod.smul_snd, prod.smul_fst, coprod_apply] } }
 
+theorem prod_ext_iff {f g : M × M₂ →ₗ[R] M₃} :
+  f = g ↔ f.comp (inl _ _ _) = g.comp (inl _ _ _) ∧ f.comp (inr _ _ _) = g.comp (inr _ _ _) :=
+(coprod_equiv ℕ).symm.injective.eq_iff.symm.trans prod.ext_iff
+
 /--
 Split equality of linear maps from a product into linear maps over each component, to allow `ext`
 to apply lemmas specific to `M →ₗ M₃` and `M₂ →ₗ M₃`.
@@ -164,10 +168,7 @@ See note [partially-applied ext lemmas]. -/
   (hl : f.comp (inl _ _ _) = g.comp (inl _ _ _))
   (hr : f.comp (inr _ _ _) = g.comp (inr _ _ _)) :
   f = g :=
-begin
-  refine (coprod_equiv ℕ).symm.injective _,
-  simp only [coprod_equiv_symm_apply, hl, hr],
-end
+prod_ext_iff.2 ⟨hl, hr⟩
 
 /-- `prod.map` of two linear maps. -/
 def prod_map (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) : (M × M₂) →ₗ[R] (M₃ × M₄) :=

src/topology/algebra/module.lean

@@ -309,6 +309,12 @@ lemma map_sum {ι : Type*} (s : finset ι) (g : ι → M) :
 
 @[simp, norm_cast] lemma coe_coe : ((f : M →ₗ[R] M₂) : (M → M₂)) = (f : M → M₂) := rfl
 
+@[ext] theorem ext_ring [topological_space R] {f g : R →L[R] M} (h : f 1 = g 1) : f = g :=
+coe_inj.1 $ linear_map.ext_ring h
+
+theorem ext_ring_iff [topological_space R] {f g : R →L[R] M} : f = g ↔ f 1 = g 1 :=
+⟨λ h, h ▸ rfl, ext_ring⟩
+
 /-- If two continuous linear maps are equal on a set `s`, then they are equal on the closure
 of the `submodule.span` of this set. -/
 lemma eq_on_closure_span [t2_space M₂] {s : set M} {f g : M →L[R] M₂} (h : set.eq_on f g s) :
@@ -440,6 +446,24 @@ rfl
   f₁.prod f₂ x = (f₁ x, f₂ x) :=
 rfl
 
+section
+
+variables (R M M₂)
+
+/-- The left injection into a product is a continuous linear map. -/
+def inl : M →L[R] M × M₂ := (id R M).prod 0
+
+/-- The right injection into a product is a continuous linear map. -/
+def inr : M₂ →L[R] M × M₂ := (0 : M₂ →L[R] M).prod (id R M₂)
+
+end
+
+@[simp] lemma inl_apply (x : M) : inl R M M₂ x = (x, 0) := rfl
+@[simp] lemma inr_apply (x : M₂) : inr R M M₂ x = (0, x) := rfl
+
+@[simp, norm_cast] lemma coe_inl : (inl R M M₂ : M →ₗ[R] M × M₂) = linear_map.inl R M M₂ := rfl
+@[simp, norm_cast] lemma coe_inr : (inr R M M₂ : M₂ →ₗ[R] M × M₂) = linear_map.inr R M M₂ := rfl
+
 instance [topological_space R] [topological_semimodule R M] [topological_semimodule R M₂] :
   topological_semimodule R (M × M₂) :=
 ⟨(continuous_fst.smul (continuous_fst.comp continuous_snd)).prod_mk
@@ -595,10 +619,7 @@ by ext; simp [← continuous_linear_map.map_smul_of_tower]
 @[simp]
 lemma smul_right_one_eq_iff {f f' : M₂} :
   smul_right (1 : R →L[R] R) f = smul_right (1 : R →L[R] R) f' ↔ f = f' :=
-⟨λ h, have (smul_right (1 : R →L[R] R) f : R → M₂) 1 = (smul_right (1 : R →L[R] R) f' : R → M₂) 1,
-        by rw h,
-      by simp at this; assumption,
-  λ h, by rw h⟩
+by simp only [ext_ring_iff, smul_right_apply, one_apply, one_smul]
 
 lemma smul_right_comp [topological_semimodule R R] {x : M₂} {c : R} :
   (smul_right (1 : R →L[R] R) x).comp (smul_right (1 : R →L[R] R) c) =
@@ -772,6 +793,21 @@ lemma smul_apply : (c • f) x = c • (f x) := rfl
 @[simp] lemma comp_smul [linear_map.compatible_smul M₂ M₃ S R] : h.comp (c • f) = c • (h.comp f) :=
 by { ext x, exact h.map_smul_of_tower c (f x) }
 
+/-- `continuous_linear_map.prod` as an `equiv`. -/
+@[simps apply] def prod_equiv : ((M →L[R] M₂) × (M →L[R] M₃)) ≃ (M →L[R] M₂ × M₃) :=
+{ to_fun := λ f, f.1.prod f.2,
+  inv_fun := λ f, ⟨(fst _ _ _).comp f, (snd _ _ _).comp f⟩,
+  left_inv := λ f, by ext; refl,
+  right_inv := λ f, by ext; refl }
+
+lemma prod_ext_iff {f g : M × M₂ →L[R] M₃} :
+  f = g ↔ f.comp (inl _ _ _) = g.comp (inl _ _ _) ∧ f.comp (inr _ _ _) = g.comp (inr _ _ _) :=
+by { simp only [← coe_inj, linear_map.prod_ext_iff], refl }
+
+@[ext] lemma prod_ext {f g : M × M₂ →L[R] M₃} (hl : f.comp (inl _ _ _) = g.comp (inl _ _ _))
+  (hr : f.comp (inr _ _ _) = g.comp (inr _ _ _)) : f = g :=
+prod_ext_iff.2 ⟨hl, hr⟩
+
 variables [has_continuous_add M₂]
 
 instance : semimodule S (M →L[R] M₂) :=
@@ -785,13 +821,10 @@ instance : semimodule S (M →L[R] M₂) :=
 variables (S) [has_continuous_add M₃]
 
 /-- `continuous_linear_map.prod` as a `linear_equiv`. -/
-def prodₗ : ((M →L[R] M₂) × (M →L[R] M₃)) ≃ₗ[S] (M →L[R] M₂ × M₃) :=
-{ to_fun := λ f, f.1.prod f.2,
-  inv_fun := λ f, ⟨(fst _ _ _).comp f, (snd _ _ _).comp f⟩,
-  map_add' := λ f g, rfl,
+@[simps apply] def prodₗ : ((M →L[R] M₂) × (M →L[R] M₃)) ≃ₗ[S] (M →L[R] M₂ × M₃) :=
+{ map_add' := λ f g, rfl,
   map_smul' := λ c f, rfl,
-  left_inv := λ f, by ext; refl,
-  right_inv := λ f, by ext; refl }
+  .. prod_equiv }
 
 end smul