chore(linear_algebra/basic): review (#2616)

* several new `simp` lemmas;
* use `linear_equiv.coe_coe` instead of `coe_apply`;
* rename `sup_quotient_to_quotient_inf` to `quotient_inf_to_sup_quotient` because it better reflects the definition; similarly for `equiv`.
* make `general_linear_group` reducible.

src/algebra/module.lean

@@ -372,6 +372,11 @@ protected theorem submodule.exists [ring R] [add_comm_group M] [module R M] {p :
   (∃ x, q x) ↔ (∃ x (hx : x ∈ p), q ⟨x, hx⟩) :=
 set_coe.exists
 
+protected theorem submodule.forall [ring R] [add_comm_group M] [module R M] {p : submodule R M}
+  {q : p → Prop} :
+  (∀ x, q x) ↔ (∀ x (hx : x ∈ p), q ⟨x, hx⟩) :=
+set_coe.forall
+
 namespace submodule
 variables [ring R] [add_comm_group M] [add_comm_group M₂]
 
@@ -403,7 +408,7 @@ lemma neg_mem (hx : x ∈ p) : -x ∈ p := by rw ← neg_one_smul R; exact p.smu
 
 lemma sub_mem (hx : x ∈ p) (hy : y ∈ p) : x - y ∈ p := p.add_mem hx (p.neg_mem hy)
 
-lemma neg_mem_iff : -x ∈ p ↔ x ∈ p :=
+@[simp] lemma neg_mem_iff : -x ∈ p ↔ x ∈ p :=
 ⟨λ h, by simpa using neg_mem p h, neg_mem p⟩
 
 lemma add_mem_iff_left (h₁ : y ∈ p) : x + y ∈ p ↔ x ∈ p :=
@@ -419,7 +424,7 @@ begin
   exact finset.induction_on t (by simp [p.zero_mem]) (by simp [p.add_mem] {contextual := tt})
 end
 
-lemma smul_mem_iff' (u : units R) : (u:R) • x ∈ p ↔ x ∈ p :=
+@[simp] lemma smul_mem_iff' (u : units R) : (u:R) • x ∈ p ↔ x ∈ p :=
 ⟨λ h, by simpa only [smul_smul, u.inv_mul, one_smul] using p.smul_mem ↑u⁻¹ h, p.smul_mem u⟩
 
 instance : has_add p := ⟨λx y, ⟨x.1 + y.1, add_mem _ x.2 y.2⟩⟩
@@ -428,14 +433,17 @@ instance : inhabited p := ⟨0⟩
 instance : has_neg p := ⟨λx, ⟨-x.1, neg_mem _ x.2⟩⟩
 instance : has_scalar R p := ⟨λ c x, ⟨c • x.1, smul_mem _ c x.2⟩⟩
 
-@[simp] lemma mk_eq_zero (x) (h : x ∈ p) : (⟨x, h⟩ : p) = 0 ↔ x = 0 := subtype.ext
+@[simp] lemma mk_eq_zero {x} (h : x ∈ p) : (⟨x, h⟩ : p) = 0 ↔ x = 0 := subtype.ext
 
 variables {p}
+@[simp, norm_cast] lemma coe_eq_coe {x y : p} : (x : M) = y ↔ x = y := subtype.ext.symm
+@[simp, norm_cast] lemma coe_eq_zero {x : p} : (x : M) = 0 ↔ x = 0 := @coe_eq_coe _ _ _ _ _ _ x 0
 @[simp, norm_cast] lemma coe_add (x y : p) : (↑(x + y) : M) = ↑x + ↑y := rfl
 @[simp, norm_cast] lemma coe_zero : ((0 : p) : M) = 0 := rfl
 @[simp, norm_cast] lemma coe_neg (x : p) : ((-x : p) : M) = -x := rfl
 @[simp, norm_cast] lemma coe_smul (r : R) (x : p) : ((r • x : p) : M) = r • ↑x := rfl
 @[simp, norm_cast] lemma coe_mk (x : M) (hx : x ∈ p) : ((⟨x, hx⟩ : p) : M) = x := rfl
+@[simp] lemma coe_mem (x : p) : (x : M) ∈ p := x.2
 
 @[simp] protected lemma eta (x : p) (hx : (x : M) ∈ p) : (⟨x, hx⟩ : p) = x := subtype.eta x hx
 

src/analysis/convex/cone.lean

@@ -372,11 +372,9 @@ begin
   rcases riesz_extension.exists_top s f nonneg dense with ⟨⟨g_dom, g⟩, ⟨hpg, hfg⟩, htop, hgs⟩,
   clear hpg,
   refine ⟨g.comp (linear_equiv.of_top _ htop).symm, _, _⟩;
-    simp only [comp_apply, linear_equiv.coe_apply, linear_equiv.of_top_symm_apply],
-  { intro s, refine (hfg _).symm, refl },
-  { intros x hx,
-    apply hgs,
-    exact hx }
+    simp only [comp_apply, linear_equiv.coe_coe, linear_equiv.of_top_symm_apply],
+  { exact λ x, (hfg (submodule.coe_mk _ _).symm).symm },
+  { exact λ x hx, hgs ⟨x, _⟩ hx }
 end
 
 /-- Hahn-Banach theorem: if `N : E → ℝ` is a sublinear map, `f` is a linear map

src/analysis/normed_space/finite_dimension.lean

@@ -165,7 +165,7 @@ begin
                       ∘ (equiv_fun_basis b_basis)) := B.comp A,
   convert this,
   ext x,
-  simp only [linear_equiv.coe_apply, function.comp_app, coe_fn_coe_base, linear_map.comp_apply],
+  dsimp,
   rw linear_equiv.symm_apply_apply
 end
 

src/linear_algebra/basic.lean

@@ -31,7 +31,7 @@ Many of the relevant definitions, including `module`, `submodule`, and `linear_m
 ## Main statements
 
 * The first and second isomorphism laws for modules are proved as `quot_ker_equiv_range` and
-  `sup_quotient_equiv_quotient_inf`.
+  `quotient_inf_equiv_sup_quotient`.
 
 ## Notations
 
@@ -495,7 +495,7 @@ def map (f : M →ₗ[R] M₂) (p : submodule R M) : submodule R M₂ :=
   smul  := by rintro a _ ⟨b, hb, rfl⟩;
               exact ⟨_, p.smul_mem _ hb, f.map_smul _ _⟩ }
 
-lemma map_coe (f : M →ₗ[R] M₂) (p : submodule R M) :
+@[simp] lemma map_coe (f : M →ₗ[R] M₂) (p : submodule R M) :
   (map f p : set M₂) = f '' p := rfl
 
 @[simp] lemma mem_map {f : M →ₗ[R] M₂} {p : submodule R M} {x : M₂} :
@@ -682,7 +682,9 @@ begin
 end
 
 section
+
 variables {p p'}
+
 lemma mem_sup : x ∈ p ⊔ p' ↔ ∃ (y ∈ p) (z ∈ p'), y + z = x :=
 ⟨λ h, begin
   rw [← span_eq p, ← span_eq p', ← span_union] at h,
@@ -699,6 +701,10 @@ end,
 by rintro ⟨y, hy, z, hz, rfl⟩; exact add_mem _
   ((le_sup_left : p ≤ p ⊔ p') hy)
   ((le_sup_right : p' ≤ p ⊔ p') hz)⟩
+
+lemma mem_sup' : x ∈ p ⊔ p' ↔ ∃ (y : p) (z : p'), (y:M) + z = x :=
+mem_sup.trans $ by simp only [submodule.exists, coe_mk]
+
 end
 
 lemma mem_span_singleton {y : M} : x ∈ span R ({y} : set M) ↔ ∃ a:R, a • y = x :=
@@ -886,6 +892,10 @@ module.of_core $ by refine {smul := (•), ..};
 
 end quotient
 
+lemma quot_hom_ext ⦃f g : quotient p →ₗ[R] M₂⦄ (h : ∀ x, f (quotient.mk x) = g (quotient.mk x)) :
+  f = g :=
+linear_map.ext $ λ x, quotient.induction_on' x h
+
 end submodule
 
 namespace submodule
@@ -939,7 +949,9 @@ def range (f : M →ₗ[R] M₂) : submodule R M₂ := map f ⊤
 theorem range_coe (f : M →ₗ[R] M₂) : (range f : set M₂) = set.range f := set.image_univ
 
 @[simp] theorem mem_range {f : M →ₗ[R] M₂} : ∀ {x}, x ∈ range f ↔ ∃ y, f y = x :=
-set.ext_iff.1 (range_coe f).
+set.ext_iff.1 (range_coe f)
+
+theorem mem_range_self (f : M →ₗ[R] M₂) (x : M) : f x ∈ f.range := mem_range.2 ⟨x, rfl⟩
 
 @[simp] theorem range_id : range (linear_map.id : M →ₗ[R] M) = ⊤ := map_id _
 
@@ -958,6 +970,10 @@ by rw [range, map_le_iff_le_comap, eq_top_iff]
 lemma map_le_range {f : M →ₗ[R] M₂} {p : submodule R M} : map f p ≤ range f :=
 map_mono le_top
 
+lemma range_coprod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
+  (f.coprod g).range = f.range ⊔ g.range :=
+submodule.ext $ λ x, by simp [mem_sup]
+
 lemma sup_range_inl_inr :
   (inl R M M₂).range ⊔ (inr R M M₂).range = ⊤ :=
 begin
@@ -971,6 +987,10 @@ begin
   simp
 end
 
+/-- Restrict the codomain of a linear map `f` to `f.range`. -/
+@[reducible] def range_restrict (f : M →ₗ[R] M₂) : M →ₗ[R] f.range :=
+f.cod_restrict f.range f.mem_range_self
+
 /-- The kernel of a linear map `f : M → M₂` is defined to be `comap f ⊥`. This is equivalent to the
 set of `x : M` such that `f x = 0`. The kernel is a submodule of `M`. -/
 def ker (f : M →ₗ[R] M₂) : submodule R M := comap f ⊥
@@ -979,6 +999,8 @@ def ker (f : M →ₗ[R] M₂) : submodule R M := comap f ⊥
 
 @[simp] theorem ker_id : ker (linear_map.id : M →ₗ[R] M) = ⊥ := rfl
 
+@[simp] theorem map_coe_ker (f : M →ₗ[R] M₂) (x : ker f) : f x = 0 := mem_ker.1 x.2
+
 theorem ker_comp (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) : ker (g.comp f) = comap f (ker g) := rfl
 
 theorem ker_le_ker_comp (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) : ker f ≤ ker (g.comp f) :=
@@ -1110,6 +1132,10 @@ by rw [ker, ← prod_bot, comap_prod_prod]; refl
 
 end linear_map
 
+lemma submodule.sup_eq_range [ring R] [add_comm_group M] [module R M] (p q : submodule R M) :
+  p ⊔ q = (p.subtype.coprod q.subtype).range :=
+submodule.ext $ λ x, by simp [submodule.mem_sup, submodule.exists]
+
 namespace linear_map
 variables [field K]
 variables [add_comm_group V] [vector_space K V]
@@ -1177,13 +1203,24 @@ maximal submodule of `p` is just `p `. -/
 @[simp] lemma map_subtype_top : map p.subtype (⊤ : submodule R p) = p :=
 by simp
 
+@[simp] lemma comap_subtype_eq_top {p p' : submodule R M} :
+  p'.comap p.subtype = ⊤ ↔ p ≤ p' :=
+eq_top_iff.trans $ map_le_iff_le_comap.symm.trans $ by rw [map_subtype_top]
+
+@[simp] lemma comap_subtype_self : p.comap p.subtype = ⊤ :=
+comap_subtype_eq_top.2 (le_refl _)
+
+@[simp] lemma range_range_restrict (f : M →ₗ[R] M₂) :
+  f.range_restrict.range = ⊤ :=
+by simp [range_cod_restrict]
+
 @[simp] theorem ker_of_le (p p' : submodule R M) (h : p ≤ p') : (of_le h).ker = ⊥ :=
 by rw [of_le, ker_cod_restrict, ker_subtype]
 
 lemma range_of_le (p q : submodule R M) (h : p ≤ q) : (of_le h).range = comap q.subtype p :=
 by rw [← map_top, of_le, linear_map.map_cod_restrict, map_top, range_subtype]
 
-lemma disjoint_iff_comap_eq_bot (p q : submodule R M) :
+lemma disjoint_iff_comap_eq_bot {p q : submodule R M} :
   disjoint p q ↔ comap p.subtype q = ⊥ :=
 by rw [eq_bot_iff, ← map_le_map_iff p.ker_subtype, map_bot, map_comap_subtype]; refl
 
@@ -1374,7 +1411,8 @@ section
 variables {module_M : module R M} {module_M₂ : module R M₂}
 variables (e e' : M ≃ₗ[R] M₂)
 
-@[simp] theorem coe_apply (b : M) : (e : M →ₗ[R] M₂) b = e b := rfl
+@[simp, norm_cast] theorem coe_coe : ⇑(e : M →ₗ[R] M₂) = e := rfl
+@[simp] lemma coe_to_equiv : ⇑(e.to_equiv) = e := rfl
 
 section
 variables {e e'}
@@ -1409,11 +1447,20 @@ def trans : M ≃ₗ[R] M₃ :=
 /-- A linear equivalence is an additive equivalence. -/
 def to_add_equiv : M ≃+ M₂ := { map_add' := e.add, .. e }
 
+@[simp] lemma coe_to_add_equiv : ⇑(e.to_add_equiv) = e := rfl
+
 @[simp] theorem trans_apply (c : M) :
   (e₁.trans e₂) c = e₂ (e₁ c) := rfl
 @[simp] theorem apply_symm_apply (c : M₂) : e (e.symm c) = c := e.6 c
 @[simp] theorem symm_apply_apply (b : M) : e.symm (e b) = b := e.5 b
 
+@[simp] lemma trans_refl : e.trans (refl R M₂) = e := to_equiv_injective e.to_equiv.trans_refl
+@[simp] lemma refl_trans : (refl R M).trans e = e := to_equiv_injective e.to_equiv.refl_trans
+
+lemma symm_apply_eq {x y} : e.symm x = y ↔ x = e y := e.to_equiv.symm_apply_eq
+
+lemma eq_symm_apply {x y} : y = e.symm x ↔ e y = x := e.to_equiv.eq_symm_apply
+
 @[simp] theorem map_add (a b : M) : e (a + b) = e a + e b := e.add a b
 @[simp] theorem map_zero : e 0 = 0 := e.to_linear_map.map_zero
 @[simp] theorem map_neg (a : M) : e (-a) = -e a := e.to_linear_map.map_neg a
@@ -1431,6 +1478,12 @@ e.to_add_equiv.map_ne_zero_iff
 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
+protected lemma image_eq_preimage (s : set M) : e '' s = e.symm ⁻¹' s :=
+e.to_equiv.image_eq_preimage s
+
+lemma map_eq_comap {p : submodule R M} : (p.map e : submodule R M₂) = p.comap e.symm :=
+submodule.ext' $ by simp [e.image_eq_preimage]
+
 end
 
 section prod
@@ -1527,10 +1580,8 @@ lemma eq_bot_of_equiv [module R M₂] (e : p ≃ₗ[R] (⊥ : submodule R M₂))
   p = ⊥ :=
 begin
   refine bot_unique (submodule.le_def'.2 $ assume b hb, (submodule.mem_bot R).2 _),
-  have := e.symm_apply_apply ⟨b, hb⟩,
-  rw [← e.coe_apply, submodule.eq_zero_of_bot_submodule ((e : p →ₗ[R] (⊥ : submodule R M₂)) ⟨b, hb⟩),
-    ← e.symm.coe_apply, linear_map.map_zero] at this,
-  exact congr_arg (coe : p → M) this.symm
+  rw [← p.mk_eq_zero hb, ← e.map_eq_zero_iff],
+  apply submodule.eq_zero_of_bot_submodule
 end
 end
 
@@ -1667,29 +1718,29 @@ let F : f.ker.quotient →ₗ[R] f.range :=
 open submodule
 
 /--
-Canonical linear map from the quotient p/(p ∩ p') to (p+p')/p', mapping x + (p ∩ p') to x + p',
-where p and p' are submodules of an ambient module.
+Canonical linear map from the quotient `p/(p ∩ p')` to `(p+p')/p'`, mapping `x + (p ∩ p')`
+to `x + p'`, where `p` and `p'` are submodules of an ambient module.
 -/
-def sup_quotient_to_quotient_inf (p p' : submodule R M) :
+def quotient_inf_to_sup_quotient (p p' : submodule R M) :
   (comap p.subtype (p ⊓ p')).quotient →ₗ[R] (comap (p ⊔ p').subtype p').quotient :=
 (comap p.subtype (p ⊓ p')).liftq
   ((comap (p ⊔ p').subtype p').mkq.comp (of_le le_sup_left)) begin
 rw [ker_comp, of_le, comap_cod_restrict, ker_mkq, map_comap_subtype],
 exact comap_mono (inf_le_inf_right _ le_sup_left) end
 
 /--
-Second Isomorphism Law : the canonical map from p/(p ∩ p') to (p+p')/p' as a linear isomorphism.
+Second Isomorphism Law : the canonical map from `p/(p ∩ p')` to `(p+p')/p'` as a linear isomorphism.
 -/
-noncomputable def sup_quotient_equiv_quotient_inf (p p' : submodule R M) :
+noncomputable def quotient_inf_equiv_sup_quotient (p p' : submodule R M) :
   (comap p.subtype (p ⊓ p')).quotient ≃ₗ[R] (comap (p ⊔ p').subtype p').quotient :=
-{ .. sup_quotient_to_quotient_inf p p',
+{ .. quotient_inf_to_sup_quotient p p',
   .. show (comap p.subtype (p ⊓ p')).quotient ≃ (comap (p ⊔ p').subtype p').quotient, from
-    @equiv.of_bijective _ _ (sup_quotient_to_quotient_inf p p') begin
+    @equiv.of_bijective _ _ (quotient_inf_to_sup_quotient p p') begin
       constructor,
-      { rw [← ker_eq_bot, sup_quotient_to_quotient_inf, ker_liftq_eq_bot],
+      { rw [← ker_eq_bot, quotient_inf_to_sup_quotient, ker_liftq_eq_bot],
         rw [ker_comp, ker_mkq],
         rintros ⟨x, hx1⟩ hx2, exact ⟨hx1, hx2⟩ },
-      rw [← range_eq_top, sup_quotient_to_quotient_inf, range_liftq, eq_top_iff'],
+      rw [← range_eq_top, quotient_inf_to_sup_quotient, range_liftq, eq_top_iff'],
       rintros ⟨x, hx⟩, rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩,
       use [⟨y, hy⟩, trivial], apply (submodule.quotient.eq _).2,
       change y - (y + z) ∈ p', rwa [sub_add_eq_sub_sub, sub_self, zero_sub, neg_mem_iff]
@@ -1850,7 +1901,7 @@ begin
     rw [std_basis_same],
     exact hb _ ((hu trivial).resolve_left hiI) },
   exact sum_mem _ (assume i hiI, mem_supr_of_mem _ i $ mem_supr_of_mem _ hiI $
-    linear_map.mem_range.2 ⟨_, rfl⟩)
+    (std_basis R φ i).mem_range_self (b i))
 end
 
 lemma supr_range_std_basis_eq_infi_ker_proj {I J : set ι}
@@ -1921,13 +1972,12 @@ instance automorphism_group.to_linear_map_is_monoid_hom :
   map_mul := λ f g, rfl }
 
 /-- The group of invertible linear maps from `M` to itself -/
-def general_linear_group := units (M →ₗ[R] M)
+@[reducible] def general_linear_group := units (M →ₗ[R] M)
 
 namespace general_linear_group
 variables {R M}
 
-instance : group (general_linear_group R M) := by delta general_linear_group; apply_instance
-instance : inhabited (general_linear_group R M) := ⟨1⟩
+instance : has_coe_to_fun (general_linear_group R M) := by apply_instance
 
 /-- An invertible linear map `f` determines an equivalence from `M` to itself. -/
 def to_linear_equiv (f : general_linear_group R M) : (M ≃ₗ[R] M) :=
@@ -1952,22 +2002,12 @@ equivalences between `M` and itself. -/
 def general_linear_equiv : general_linear_group R M ≃* (M ≃ₗ[R] M) :=
 { to_fun := to_linear_equiv,
   inv_fun := of_linear_equiv,
-  left_inv := λ f,
-  begin
-    delta to_linear_equiv of_linear_equiv,
-    cases f with f f_inv, cases f, cases f_inv,
-    congr
-  end,
-  right_inv := λ f,
-  begin
-    delta to_linear_equiv of_linear_equiv,
-    cases f,
-    congr
-  end,
+  left_inv := λ f, by { ext, refl },
+  right_inv := λ f, by { ext, refl },
   map_mul' := λ x y, by {ext, refl} }
 
 @[simp] lemma general_linear_equiv_to_linear_map (f : general_linear_group R M) :
-  ((general_linear_equiv R M).to_equiv f).to_linear_map = f.val :=
+  (general_linear_equiv R M f : M →ₗ[R] M) = f :=
 by {ext, refl}
 
 end general_linear_group