feat(topology/algebra/module): ker, range, cod_restrict, subtype_val, coprod (#2525)

Also move `smul_right` to `general_ring` and define some
maps/equivalences useful for the inverse/implicit function theorem.

Author: urkud

src/algebra/group/units.lean

@@ -39,6 +39,8 @@ variables [monoid α]
 
 @[to_additive] instance : has_coe (units α) α := ⟨val⟩
 
+@[simp, to_additive] lemma coe_mk (a : α) (b h₁ h₂) : ↑(units.mk a b h₁ h₂) = a := rfl
+
 @[ext, to_additive] theorem ext :
   function.injective (coe : units α → α)
 | ⟨v, i₁, vi₁, iv₁⟩ ⟨v', i₂, vi₂, iv₂⟩ e :=

src/topology/algebra/module.lean

@@ -1,8 +1,7 @@
 /-
 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo
-
+Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov
 -/
 import topology.algebra.ring
 import ring_theory.algebra
@@ -173,6 +172,7 @@ notation M ` →L[`:25 R `] ` M₂ := continuous_linear_map R M M₂
 /-- Continuous linear equivalences between modules. We only put the type classes that are necessary
 for the definition, although in applications `M` and `M₂` will be topological modules over the
 topological ring `R`. -/
+@[nolint has_inhabited_instance]
 structure continuous_linear_equiv
   (R : Type*) [ring R]
   (M : Type*) [topological_space M] [add_comm_group M]
@@ -339,6 +339,51 @@ rfl
   f₁.prod f₂ x = (f₁ x, f₂ x) :=
 rfl
 
+/-- Kernel of a continuous linear map. -/
+def ker (f : M →L[R] M₂) : submodule R M := (f : M →ₗ[R] M₂).ker
+
+@[norm_cast] lemma ker_coe : (f : M →ₗ[R] M₂).ker = f.ker := rfl
+
+@[simp] lemma mem_ker {f : M →L[R] M₂} {x} : x ∈ f.ker ↔ f x = 0 := linear_map.mem_ker
+
+lemma is_closed_ker [t1_space M₂] : is_closed (f.ker : set M) :=
+continuous_iff_is_closed.1 f.cont _ is_closed_singleton
+
+@[simp] lemma apply_ker (x : f.ker) : f x = 0 := mem_ker.1 x.2
+
+/-- Range of a continuous linear map. -/
+def range (f : M →L[R] M₂) : submodule R M₂ := (f : M →ₗ[R] M₂).range
+
+lemma range_coe : (f.range : set M₂) = set.range f := linear_map.range_coe _
+lemma mem_range {f : M →L[R] M₂} {y} : y ∈ f.range ↔ ∃ x, f x = y := linear_map.mem_range
+
+/-- Restrict codomain of a continuous linear map. -/
+def cod_restrict (f : M →L[R] M₂) (p : submodule R M₂) (h : ∀ x, f x ∈ p) :
+  M →L[R] p :=
+{ cont := continuous_subtype_mk h f.continuous,
+  to_linear_map := (f : M →ₗ[R] M₂).cod_restrict p h}
+
+@[norm_cast] lemma coe_cod_restrict (f : M →L[R] M₂) (p : submodule R M₂) (h : ∀ x, f x ∈ p) :
+  (f.cod_restrict p h : M →ₗ[R] p) = (f : M →ₗ[R] M₂).cod_restrict p h :=
+rfl
+
+@[simp] lemma coe_cod_restrict_apply (f : M →L[R] M₂) (p : submodule R M₂) (h : ∀ x, f x ∈ p) (x) :
+  (f.cod_restrict p h x : M₂) = f x :=
+rfl
+
+/-- Embedding of a submodule into the ambient space as a continuous linear map. -/
+def subtype_val (p : submodule R M) : p →L[R] M :=
+{ cont := continuous_subtype_val,
+  to_linear_map := p.subtype }
+
+@[simp, norm_cast] lemma coe_subtype_val (p : submodule R M) :
+  (subtype_val p : p →ₗ[R] M) = p.subtype :=
+rfl
+
+@[simp, norm_cast] lemma subtype_val_apply (p : submodule R M) (x : p) :
+  (subtype_val p : p → M) x = x :=
+rfl
+
 variables (R M M₂)
 
 /-- `prod.fst` as a `continuous_linear_map`. -/
@@ -367,35 +412,46 @@ def prod_map (f₁ : M →L[R] M₂) (f₂ : M₃ →L[R] M₄) : (M × M₃) 
   (f₁.prod_map f₂ : (M × M₃) →ₗ[R] (M₂ × M₄)) = ((f₁ : M →ₗ[R] M₂).prod_map (f₂ : M₃ →ₗ[R] M₄)) :=
 rfl
 
-@[simp, norm_cast] lemma prod_map_apply (f₁ : M →L[R] M₂) (f₂ : M₃ →L[R] M₄) (x) :
-  f₁.prod_map f₂ x = (f₁ x.1, f₂ x.2) :=
+@[simp, norm_cast] lemma coe_prod_map' (f₁ : M →L[R] M₂) (f₂ : M₃ →L[R] M₄) :
+  ⇑(f₁.prod_map f₂) = prod.map f₁ f₂ :=
 rfl
 
-end general_ring
+/-- The continuous linear map given by `(x, y) ↦ f₁ x + f₂ y`. -/
+def coprod [topological_add_monoid M₃] (f₁ : M →L[R] M₃) (f₂ : M₂ →L[R] M₃) :
+  (M × M₂) →L[R] M₃ :=
+⟨linear_map.coprod f₁ f₂, (f₁.cont.comp continuous_fst).add (f₂.cont.comp continuous_snd)⟩
 
-section comm_ring
-
-variables
-{R : Type*} [comm_ring R] [topological_space R]
-{M : Type*} [topological_space M] [add_comm_group M]
-{M₂ : Type*} [topological_space M₂] [add_comm_group M₂]
-{M₃ : Type*} [topological_space M₃] [add_comm_group M₃]
-[module R M] [module R M₂] [module R M₃] [topological_module R M₃]
+@[norm_cast, simp] lemma coe_coprod [topological_add_monoid M₃]
+  (f₁ : M →L[R] M₃) (f₂ : M₂ →L[R] M₃) :
+  (f₁.coprod f₂ : (M × M₂) →ₗ[R] M₃) = linear_map.coprod f₁ f₂ :=
+rfl
 
-instance : has_scalar R (M →L[R] M₃) :=
-⟨λ c f, ⟨c • f, continuous_const.smul f.2⟩⟩
+@[simp] lemma coprod_apply [topological_add_monoid M₃] (f₁ : M →L[R] M₃) (f₂ : M₂ →L[R] M₃) (x) :
+  f₁.coprod f₂ x = f₁ x.1 + f₂ x.2 := rfl
 
-variables (c : R) (h : M₂ →L[R] M₃) (f g : M →L[R] M₂) (x y z : M)
+/-- Given a right inverse `f₂ : M₂ →L[R] M` to `f₁ : M →L[R] M₂`,
+`proj_ker_of_right_inverse f₁ f₂ h` is the projection `M →L[R] f₁.ker` along `f₂.range`. -/
+def proj_ker_of_right_inverse [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M)
+  (h : function.right_inverse f₂ f₁) :
+  M →L[R] f₁.ker :=
+(id R M - f₂.comp f₁).cod_restrict f₁.ker $ λ x, by simp [h (f₁ x)]
 
-@[simp] lemma smul_comp : (c • h).comp f = c • (h.comp f) := rfl
+@[simp] lemma coe_proj_ker_of_right_inverse_apply [topological_add_group M]
+  (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) (x : M) :
+  (f₁.proj_ker_of_right_inverse f₂ h x : M) = x - f₂ (f₁ x) :=
+rfl
 
-variable [topological_module R M₂]
+@[simp] lemma proj_ker_of_right_inverse_apply_idem [topological_add_group M]
+  (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) (x : f₁.ker) :
+  f₁.proj_ker_of_right_inverse f₂ h x = x :=
+subtype.coe_ext.2 $ by simp
 
-@[simp] lemma smul_apply : (c • f) x = c • (f x) := rfl
-@[simp, norm_cast] lemma coe_apply : (((c • f) : M →L[R] M₂) : M →ₗ[R] M₂) = c • (f : M →ₗ[R] M₂) := rfl
-@[norm_cast] lemma coe_apply' : (((c • f) : M →L[R] M₂) : M → M₂) = c • (f : M → M₂) := rfl
+@[simp] lemma proj_ker_of_right_inverse_comp_inv [topological_add_group M]
+  (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) (y : M₂) :
+  f₁.proj_ker_of_right_inverse f₂ h (f₂ y) = 0 :=
+subtype.coe_ext.2 $ by simp [h y]
 
-@[simp] lemma comp_smul : h.comp (c • f) = c • (h.comp f) := by { ext, simp }
+variables [topological_space R] [topological_module R M₂]
 
 /-- The linear map `λ x, c x • f`.  Associates to a scalar-valued linear map and an element of
 `M₂` the `M₂`-valued linear map obtained by multiplying the two (a.k.a. tensoring by `M₂`) -/
@@ -420,6 +476,36 @@ lemma smul_right_one_eq_iff {f f' : M₂} :
       by simp at this; assumption,
   by cc⟩
 
+lemma smul_right_comp [topological_module R R] {x : M₂} {c : R} :
+  (smul_right 1 x : R →L[R] M₂).comp (smul_right 1 c : R →L[R] R) = smul_right 1 (c • x) :=
+by { ext, simp [mul_smul] }
+
+end general_ring
+
+section comm_ring
+
+variables
+{R : Type*} [comm_ring R] [topological_space R]
+{M : Type*} [topological_space M] [add_comm_group M]
+{M₂ : Type*} [topological_space M₂] [add_comm_group M₂]
+{M₃ : Type*} [topological_space M₃] [add_comm_group M₃]
+[module R M] [module R M₂] [module R M₃] [topological_module R M₃]
+
+instance : has_scalar R (M →L[R] M₃) :=
+⟨λ c f, ⟨c • f, continuous_const.smul f.2⟩⟩
+
+variables (c : R) (h : M₂ →L[R] M₃) (f g : M →L[R] M₂) (x y z : M)
+
+@[simp] lemma smul_comp : (c • h).comp f = c • (h.comp f) := rfl
+
+variable [topological_module R M₂]
+
+@[simp] lemma smul_apply : (c • f) x = c • (f x) := rfl
+@[simp, norm_cast] lemma coe_apply : (((c • f) : M →L[R] M₂) : M →ₗ[R] M₂) = c • (f : M →ₗ[R] M₂) := rfl
+@[norm_cast] lemma coe_apply' : (((c • f) : M →L[R] M₂) : M → M₂) = c • (f : M → M₂) := rfl
+
+@[simp] lemma comp_smul : h.comp (c • f) = c • (h.comp f) := by { ext, simp }
+
 variable [topological_add_group M₂]
 
 instance : module R (M →L[R] M₂) :=
@@ -518,6 +604,10 @@ lemma comp_continuous_iff
   continuous (e ∘ f) ↔ continuous f :=
 e.to_homeomorph.comp_continuous_iff _
 
+/-- An extensionality lemma for `R ≃L[R] M`. -/
+lemma ext₁ [topological_space R] {f g : R ≃L[R] M} (h : f 1 = g 1) : f = g :=
+ext $ funext $ λ x, mul_one x ▸ by rw [← smul_eq_mul, map_smul, h, map_smul]
+
 section
 variables (R M)
 
@@ -623,4 +713,78 @@ by { ext x, refl }
 @[simp] theorem symm_symm_apply (e : M ≃L[R] M₂) (x : M) : e.symm.symm x = e x :=
 rfl
 
+/-- Create a `continuous_linear_equiv` from two `continuous_linear_map`s that are
+inverse of each other. -/
+def equiv_of_inverse (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h₁ : function.left_inverse f₂ f₁)
+  (h₂ : function.right_inverse f₂ f₁) :
+  M ≃L[R] M₂ :=
+{ to_fun := f₁,
+  continuous_to_fun := f₁.continuous,
+  inv_fun := f₂,
+  continuous_inv_fun := f₂.continuous,
+  left_inv := h₁,
+  right_inv := h₂,
+  .. f₁ }
+
+@[simp] lemma equiv_of_inverse_apply (f₁ : M →L[R] M₂) (f₂ h₁ h₂ x) :
+  equiv_of_inverse f₁ f₂ h₁ h₂ x = f₁ x :=
+rfl
+
+@[simp] lemma symm_equiv_of_inverse (f₁ : M →L[R] M₂) (f₂ h₁ h₂) :
+  (equiv_of_inverse f₁ f₂ h₁ h₂).symm = equiv_of_inverse f₂ f₁ h₂ h₁ :=
+rfl
+
+section
+variables (R) [topological_space R] [topological_module R R]
+
+/-- Continuous linear equivalences `R ≃L[R] R` are enumerated by `units R`. -/
+def units_equiv_aut : units R ≃ (R ≃L[R] R) :=
+{ to_fun := λ u, equiv_of_inverse
+    (continuous_linear_map.smul_right 1 ↑u)
+    (continuous_linear_map.smul_right 1 ↑u⁻¹)
+    (λ x, by simp) (λ x, by simp),
+  inv_fun := λ e, ⟨e 1, e.symm 1,
+    by rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, symm_apply_apply],
+    by rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, apply_symm_apply]⟩,
+  left_inv := λ u, units.ext $ by simp,
+  right_inv := λ e, ext₁ $ by simp }
+
+variable {R}
+
+@[simp] lemma units_equiv_aut_apply (u : units R) (x : R) : units_equiv_aut R u x = x * u := rfl
+
+@[simp] lemma units_equiv_aut_apply_symm (u : units R) (x : R) :
+  (units_equiv_aut R u).symm x = x * ↑u⁻¹ := rfl
+
+@[simp] lemma units_equiv_aut_symm_apply (e : R ≃L[R] R) :
+  ↑((units_equiv_aut R).symm e) = e 1 :=
+rfl
+
+end
+
+variables [topological_add_group M]
+
+open continuous_linear_map (id fst snd subtype_val mem_ker)
+
+/-- A pair of continuous linear maps such that `f₁ ∘ f₂ = id` generates a continuous
+linear equivalence `e` between `M` and `M₂ × f₁.ker` such that `(e x).2 = x` for `x ∈ f₁.ker`,
+`(e x).1 = f₁ x`, and `(e (f₂ y)).2 = 0`. The map is given by `e x = (f₁ x, x - f₂ (f₁ x))`. -/
+def equiv_of_right_inverse (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) :
+  M ≃L[R] M₂ × f₁.ker :=
+equiv_of_inverse (f₁.prod (f₁.proj_ker_of_right_inverse f₂ h)) (f₂.coprod (subtype_val f₁.ker))
+  (λ x, by simp)
+  (λ ⟨x, y⟩, by simp [h x])
+
+@[simp] lemma fst_equiv_of_right_inverse (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M)
+  (h : function.right_inverse f₂ f₁) (x : M) :
+  (equiv_of_right_inverse f₁ f₂ h x).1 = f₁ x := rfl
+
+@[simp] lemma snd_equiv_of_right_inverse (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M)
+  (h : function.right_inverse f₂ f₁) (x : M) :
+  ((equiv_of_right_inverse f₁ f₂ h x).2 : M) = x - f₂ (f₁ x) := rfl
+
+@[simp] lemma equiv_of_right_inverse_symm_apply (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M)
+  (h : function.right_inverse f₂ f₁) (y : M₂ × f₁.ker) :
+  (equiv_of_right_inverse f₁ f₂ h).symm y = f₂ y.1 + y.2 := rfl
+
 end continuous_linear_equiv