feat(topology/algebra/module): define fst and snd, review (#2247)

* feat(topology/algebra/module): define `fst` and `snd`, review

* Fix compile

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: urkud

src/geometry/manifold/mfderiv.lean

@@ -223,15 +223,15 @@ def mfderiv_within (f : M → M') (s : set M) (x : M) : tangent_space I x →L[
 if h : mdifferentiable_within_at I I' f s x then
 (fderiv_within 𝕜 (written_in_ext_chart_at I I' x f) ((ext_chart_at I x).inv_fun ⁻¹' s ∩ range I.to_fun)
   ((ext_chart_at I x).to_fun x) : _)
-else continuous_linear_map.zero
+else 0
 
 /-- Let `f` be a function between two smooth manifolds. Then `mfderiv I I' f x` is the derivative of
 `f` at `x`, as a continuous linear map from the tangent space at `x` to the tangent space at `f x`. -/
 def mfderiv (f : M → M') (x : M) : tangent_space I x →L[𝕜] tangent_space I' (f x) :=
 if h : mdifferentiable_at I I' f x then
 (fderiv_within 𝕜 (written_in_ext_chart_at I I' x f : E → E') (range I.to_fun)
   ((ext_chart_at I x).to_fun x) : _)
-else continuous_linear_map.zero
+else 0
 
 set_option class.instance_max_depth 60
 
@@ -351,11 +351,11 @@ set_option class.instance_max_depth 60
 
 lemma mfderiv_within_zero_of_not_mdifferentiable_within_at
   (h : ¬ mdifferentiable_within_at I I' f s x) : mfderiv_within I I' f s x = 0 :=
-by { simp [mfderiv_within, h], refl }
+by simp [mfderiv_within, h]
 
 lemma mfderiv_zero_of_not_mdifferentiable_at
   (h : ¬ mdifferentiable_at I I' f x) : mfderiv I I' f x = 0 :=
-by { simp [mfderiv, h], refl }
+by simp [mfderiv, h]
 
 theorem has_mfderiv_within_at.mono (h : has_mfderiv_within_at I I' f t x f') (hst : s ⊆ t) :
   has_mfderiv_within_at I I' f s x f' :=
@@ -676,8 +676,8 @@ begin
   by_cases h : mdifferentiable_within_at I I' f s x,
   { exact ((h.has_mfderiv_within_at).congr_of_mem_nhds_within hL hx).mfderiv_within hs },
   { unfold mfderiv_within,
-    rw [dif_neg, dif_neg],
-    assumption,
+    rw [dif_neg h, dif_neg],
+    refl,
     rwa ← mdifferentiable_within_at_congr_of_mem_nhds_within I I' hL hx }
 end
 
@@ -896,7 +896,7 @@ variables {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
 
 lemma has_mfderiv_at_const (c : M') (x : M) :
   has_mfderiv_at I I' (λy : M, c) x
-  (continuous_linear_map.zero : tangent_space I x →L[𝕜] tangent_space I' c) :=
+  (0 : tangent_space I x →L[𝕜] tangent_space I' c) :=
 begin
   refine ⟨continuous_const.continuous_at, _⟩,
   have : (ext_chart_at I' c).to_fun ∘ (λ (y : M), c) ∘ (ext_chart_at I x).inv_fun =
@@ -907,7 +907,7 @@ end
 
 theorem has_mfderiv_within_at_const (c : M') (s : set M) (x : M) :
   has_mfderiv_within_at I I' (λy : M, c) s x
-  (continuous_linear_map.zero : tangent_space I x →L[𝕜] tangent_space I' c) :=
+  (0 : tangent_space I x →L[𝕜] tangent_space I' c) :=
 (has_mfderiv_at_const I I' c x).has_mfderiv_within_at
 
 lemma mdifferentiable_at_const : mdifferentiable_at I I' (λy : M, c) x :=
@@ -923,12 +923,12 @@ lemma mdifferentiable_on_const : mdifferentiable_on I I' (λy : M, c) s :=
 (mdifferentiable_const I I').mdifferentiable_on
 
 @[simp] lemma mfderiv_const : mfderiv I I' (λy : M, c) x =
-  (continuous_linear_map.zero : tangent_space I x →L[𝕜] tangent_space I' c) :=
+  (0 : tangent_space I x →L[𝕜] tangent_space I' c) :=
 has_mfderiv_at.mfderiv (has_mfderiv_at_const I I' c x)
 
 lemma mfderiv_within_const (hxs : unique_mdiff_within_at I s x) :
   mfderiv_within I I' (λy : M, c) s x =
-  (continuous_linear_map.zero : tangent_space I x →L[𝕜] tangent_space I' c) :=
+  (0 : tangent_space I x →L[𝕜] tangent_space I' c) :=
 begin
   rw mdifferentiable.mfderiv_within (mdifferentiable_at_const I I') hxs,
   { exact mfderiv_const I I' },
@@ -1140,8 +1140,7 @@ begin
     change ¬(∃(f' : tangent_space (model_with_corners_self 𝕜 E) x →L[𝕜]
                     tangent_space (model_with_corners_self 𝕜 E') (f x)),
             has_fderiv_within_at f f' s x) at h,
-    simp [fderiv_within, h],
-    refl }
+    simp [fderiv_within, h] }
 end
 
 /-- For maps between vector spaces, mfderiv and fderiv coincide -/

src/topology/algebra/module.lean

@@ -200,11 +200,11 @@ variables
 /-- Coerce continuous linear maps to linear maps. -/
 instance : has_coe (M →L[R] M₂) (M →ₗ[R] M₂) := ⟨to_linear_map⟩
 
-protected lemma continuous (f : M →L[R] M₂) : continuous f := f.2
-
 /-- Coerce continuous linear maps to functions. -/
 instance to_fun : has_coe_to_fun $ M →L[R] M₂ := ⟨_, λ f, f.to_fun⟩
 
+protected lemma continuous (f : M →L[R] M₂) : continuous f := f.2
+
 @[ext] theorem ext {f g : M →L[R] M₂} (h : ∀ x, f x = g x) : f = g :=
 by cases f; cases g; congr' 1; ext x; apply h
 
@@ -223,10 +223,7 @@ variables (c : R) (f g : M →L[R] M₂) (h : M₂ →L[R] M₃) (x y z : M)
 @[simp, squash_cast] lemma coe_coe : ((f : M →ₗ[R] M₂) : (M → M₂)) = (f : M → M₂) := rfl
 
 /-- The continuous map that is constantly zero. -/
-def zero : M →L[R] M₂ :=
-⟨0, by exact continuous_const⟩
-
-instance: has_zero (M →L[R] M₂) := ⟨zero⟩
+instance: has_zero (M →L[R] M₂) := ⟨⟨0, continuous_const⟩⟩
 instance : inhabited (M →L[R] M₂) := ⟨0⟩
 
 @[simp] lemma zero_apply : (0 : M →L[R] M₂) x = 0 := rfl
@@ -266,8 +263,8 @@ instance : has_neg (M →L[R] M₂) := ⟨λ f, ⟨-f, f.2.neg⟩⟩
 @[move_cast] lemma coe_neg' : (((-f) : M →L[R] M₂) : M → M₂) = -(f : M → M₂) := rfl
 
 instance : add_comm_group (M →L[R] M₂) :=
-by refine {zero := 0, add := (+), neg := has_neg.neg, ..};
-   intros; ext; simp; cc
+by { refine {zero := 0, add := (+), neg := has_neg.neg, ..}; intros; ext;
+  apply_rules [zero_add, add_assoc, add_zero, add_left_neg, add_comm] }
 
 lemma sub_apply (x : M) : (f - g) x = f x - g x := rfl
 @[simp, move_cast] lemma coe_sub : (((f - g) : M →L[R] M₂) : M →ₗ[R] M₂) = (f : M →ₗ[R] M₂) - g := rfl
@@ -323,10 +320,46 @@ instance [topological_add_group M] : ring (M →L[R] M) :=
   ..continuous_linear_map.add_comm_group }
 
 /-- The cartesian product of two bounded linear maps, as a bounded linear map. -/
-def prod (f₁ : M →L[R] M₂) (f₂ : M →L[R] M₃) : M →L[R] (M₂ × M₃) :=
+protected def prod (f₁ : M →L[R] M₂) (f₂ : M →L[R] M₃) : M →L[R] (M₂ × M₃) :=
 { cont := f₁.2.prod_mk f₂.2,
   ..f₁.to_linear_map.prod f₂.to_linear_map }
 
+@[simp, move_cast] lemma coe_prod (f₁ : M →L[R] M₂) (f₂ : M →L[R] M₃) :
+  (f₁.prod f₂ : M →ₗ[R] M₂ × M₃) = linear_map.prod f₁ f₂ :=
+rfl
+
+@[simp, move_cast] lemma prod_apply (f₁ : M →L[R] M₂) (f₂ : M →L[R] M₃) (x : M) :
+  f₁.prod f₂ x = (f₁ x, f₂ x) :=
+rfl
+
+variables (R M M₂)
+
+/-- `prod.fst` as a `continuous_linear_map`. -/
+protected def fst : M × M₂ →L[R] M :=
+{ cont := continuous_fst, to_linear_map := linear_map.fst R M M₂ }
+
+/-- `prod.snd` as a `continuous_linear_map`. -/
+protected def snd : M × M₂ →L[R] M₂ :=
+{ cont := continuous_snd, to_linear_map := linear_map.snd R M M₂ }
+
+variables {R M M₂}
+
+@[simp, move_cast] lemma coe_fst :
+  (continuous_linear_map.fst R M M₂ : M × M₂ →ₗ[R] M) = linear_map.fst R M M₂ :=
+rfl
+
+@[simp, move_cast] lemma coe_fst' :
+  (continuous_linear_map.fst R M M₂ : M × M₂ → M) = prod.fst :=
+rfl
+
+@[simp, move_cast] lemma coe_snd :
+  (continuous_linear_map.snd R M M₂ : M × M₂ →ₗ[R] M₂) = linear_map.snd R M M₂ :=
+rfl
+
+@[simp, move_cast] lemma coe_snd' :
+  (continuous_linear_map.snd R M M₂ : M × M₂ → M₂) = prod.snd :=
+rfl
+
 end general_ring
 
 section comm_ring
@@ -502,6 +535,10 @@ by { ext, refl }
   (e₁.trans e₂).to_linear_equiv = e₁.to_linear_equiv.trans e₂.to_linear_equiv :=
 by { ext, refl }
 
+theorem bijective (e : M ≃L[R] M₂) : function.bijective e := e.to_linear_equiv.to_equiv.bijective
+theorem injective (e : M ≃L[R] M₂) : function.injective e := e.to_linear_equiv.to_equiv.injective
+theorem surjective (e : M ≃L[R] M₂) : function.surjective e := e.to_linear_equiv.to_equiv.surjective
+
 @[simp] theorem apply_symm_apply (e : M ≃L[R] M₂) (c : M₂) : e (e.symm c) = c := e.1.6 c
 @[simp] theorem symm_apply_apply (e : M ≃L[R] M₂) (b : M) : e.symm (e b) = b := e.1.5 b