chore(linear_algebra/basis): use dot notation, simplify some proofs (#2671)

Author: urkud

src/analysis/normed_space/finite_dimension.lean

@@ -77,14 +77,14 @@ variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
 /-- In finite dimension over a complete field, the canonical identification (in terms of a basis)
 with `𝕜^n` together with its sup norm is continuous. This is the nontrivial part in the fact that
 all norms are equivalent in finite dimension.
-Do not use this statement as its formulation is awkward (in terms of the dimension `n`, as the proof
-is done by induction over `n`) and it is superceded by the fact that every linear map on a
-finite-dimensional space is continuous, in `linear_map.continuous_of_finite_dimensional`. -/
-lemma continuous_equiv_fun_basis {n : ℕ} {ι : Type v} [fintype ι] (ξ : ι → E)
-  (hn : fintype.card ι = n) (hξ : is_basis 𝕜 ξ) : continuous (equiv_fun_basis hξ) :=
+
+This statement is superceded by the fact that every linear map on a finite-dimensional space is
+continuous, in `linear_map.continuous_of_finite_dimensional`. -/
+lemma continuous_equiv_fun_basis {ι : Type v} [fintype ι] (ξ : ι → E) (hξ : is_basis 𝕜 ξ) :
+  continuous (equiv_fun_basis hξ) :=
 begin
   unfreezeI,
-  induction n with n IH generalizing ι E,
+  induction hn : fintype.card ι with n IH generalizing ι E,
   { apply linear_map.continuous_of_bound _ 0 (λx, _),
     have : equiv_fun_basis hξ x = 0,
       by { ext i, exact (fintype.card_eq_zero_iff.1 hn i).elim },
@@ -101,7 +101,7 @@ begin
       have U : uniform_embedding (equiv_fun_basis b_basis).symm.to_equiv,
       { have : fintype.card b = n,
           by { rw ← s_dim, exact (findim_eq_card_basis b_basis).symm },
-        have : continuous (equiv_fun_basis b_basis) := IH (subtype.val : b → s) this b_basis,
+        have : continuous (equiv_fun_basis b_basis) := IH (subtype.val : b → s) b_basis this,
         exact (equiv_fun_basis b_basis).symm.uniform_embedding (linear_map.continuous_on_pi _) this },
       have : is_complete (s : set E),
         from complete_space_coe_iff_is_complete.1 ((complete_space_congr U).1 (by apply_instance)),
@@ -158,7 +158,7 @@ begin
   rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
   letI : fintype b := finite.fintype b_finite,
   have A : continuous (equiv_fun_basis b_basis) :=
-    continuous_equiv_fun_basis _ rfl b_basis,
+    continuous_equiv_fun_basis _ b_basis,
   have B : continuous (f.comp ((equiv_fun_basis b_basis).symm : (b → 𝕜) →ₗ[𝕜] E)) :=
     linear_map.continuous_on_pi _,
   have : continuous ((f.comp ((equiv_fun_basis b_basis).symm : (b → 𝕜) →ₗ[𝕜] E))
@@ -202,20 +202,19 @@ variables {𝕜 E}
 /-- A finite-dimensional subspace is complete. -/
 lemma submodule.complete_of_finite_dimensional (s : submodule 𝕜 E) [finite_dimensional 𝕜 s] :
   is_complete (s : set E) :=
-begin
-  haveI : complete_space s := finite_dimensional.complete 𝕜 s,
-  have : is_complete (range (subtype.val : s → E)),
-  { rw [← image_univ, is_complete_image_iff],
-    { exact complete_univ },
-    { exact isometry_subtype_val.uniform_embedding } },
-  rwa subtype.val_range at this
-end
+complete_space_coe_iff_is_complete.1 (finite_dimensional.complete 𝕜 s)
 
 /-- A finite-dimensional subspace is closed. -/
 lemma submodule.closed_of_finite_dimensional (s : submodule 𝕜 E) [finite_dimensional 𝕜 s] :
   is_closed (s : set E) :=
 is_closed_of_is_complete s.complete_of_finite_dimensional
 
+lemma continuous_linear_map.exists_right_inverse_of_surjective [finite_dimensional 𝕜 F]
+  (f : E →L[𝕜] F) (hf : f.range = ⊤) :
+  ∃ g : F →L[𝕜] E, f.comp g = continuous_linear_map.id 𝕜 F :=
+let ⟨g, hg⟩ := (f : E →ₗ[𝕜] F).exists_right_inverse_of_surjective hf in
+⟨g.to_continuous_linear_map, continuous_linear_map.ext $ linear_map.ext_iff.1 hg⟩
+
 end complete_field
 
 section proper_field

src/linear_algebra/basis.lean

@@ -106,7 +106,7 @@ begin
  exact false.elim (not_nonempty_iff_imp_false.1 h i)
 end
 
-lemma ne_zero_of_linear_independent
+lemma linear_independent.ne_zero
   {i : ι} (ne : 0 ≠ (1:R)) (hv : linear_independent R v) : v i ≠ 0 :=
 λ h, ne $ eq.symm begin
   suffices : (finsupp.single i 1 : ι →₀ R) i = 0, {simpa},
@@ -301,7 +301,7 @@ begin
  exact (disjoint.mono_left (finsupp.supported_mono h))
 end
 
-lemma linear_independent_union {s t : set M}
+lemma linear_independent.union {s t : set M}
   (hs : linear_independent R (λ x, x : s → M)) (ht : linear_independent R (λ x, x : t → M))
   (hst : disjoint (span R s) (span R t)) :
   linear_independent R (λ x, x : (s ∪ t) → M) :=
@@ -346,7 +346,6 @@ lemma linear_independent_Union_of_directed {η : Type*}
   (h : ∀ i, linear_independent R (λ x, x : s i → M)) :
   linear_independent R (λ x, x : (⋃ i, s i) → M) :=
 begin
-  haveI := classical.dec (nonempty η),
   by_cases hη : nonempty η,
   { refine linear_independent_of_finite (⋃ i, s i) (λ t ht ft, _),
     rcases finite_subset_Union ft ht with ⟨I, fi, hI⟩,
@@ -389,9 +388,7 @@ begin
     exact λ x, set.not_mem_empty x (subtype.mem x) },
   { rintros ⟨i⟩ s his ih,
     rw [finset.sup_insert],
-    apply linear_independent_union,
-    { apply hl },
-    { apply ih },
+    refine (hl _).union ih _,
     rw [finset.sup_eq_supr],
     refine (hd i _ _ his).mono_right _,
     { simp only [(span_Union _).symm],
@@ -424,7 +421,7 @@ begin
         simp only [] at hxy,
         rw hxy,
         exact (subset_span (mem_range_self y₂)) },
-      exact false.elim (ne_zero_of_linear_independent zero_eq_one (hindep x₁) h0) } },
+      exact false.elim ((hindep x₁).ne_zero zero_eq_one h0) } },
   rw range_sigma_eq_Union_range,
   apply linear_independent_Union_finite_subtype (λ j, (hindep j).to_subtype_range) hd,
 end
@@ -592,16 +589,14 @@ begin
   { simp }
 end
 
-lemma linear_independent_inl_union_inr {s : set M} {t : set M'}
+lemma linear_independent.inl_union_inr {s : set M} {t : set M'}
   (hs : linear_independent R (λ x, x : s → M))
   (ht : linear_independent R (λ x, x : t → M')) :
   linear_independent R (λ x, x : inl R M M' '' s ∪ inr R M M' '' t → M × M') :=
 begin
-  apply linear_independent_union,
-  exact (hs.image_subtype $ by simp),
-  exact (ht.image_subtype $ by simp),
-  rw [span_image, span_image];
-    simp [disjoint_iff, prod_inf_prod]
+  refine (hs.image_subtype _).union (ht.image_subtype _) _; [simp, simp, skip],
+  simp only [span_image],
+  simp [disjoint_iff, prod_inf_prod]
 end
 
 lemma linear_independent_inl_union_inr' {v : ι → M} {v' : ι' → M'}
@@ -616,20 +611,12 @@ begin
   { apply sum.elim_injective,
     { exact injective_comp prod.injective_inl inj_v },
     { exact injective_comp prod.injective_inr inj_v' },
-    { intros, simp [ne_zero_of_linear_independent zero_eq_one hv] } },
+    { intros, simp [hv.ne_zero zero_eq_one] } },
   { rw sum.elim_range,
-    apply linear_independent_union,
-    { apply linear_independent.to_subtype_range,
-      apply linear_independent.image hv,
-      simp [ker_inl] },
-    { apply linear_independent.to_subtype_range,
-      apply linear_independent.image hv',
-      simp [ker_inr] },
-    { apply disjoint_inl_inr.mono _ _,
-      { rw [set.range_comp, span_image],
-        apply linear_map.map_le_range },
-      { rw [set.range_comp, span_image],
-        apply linear_map.map_le_range } } }
+    refine (hv.image _).to_subtype_range.union (hv'.image _).to_subtype_range _;
+      [simp, simp, skip],
+    apply disjoint_inl_inr.mono _ _;
+      simp only [set.range_comp, span_image, linear_map.map_le_range] }
 end
 
 /-- Dedekind's linear independence of characters -/
@@ -781,7 +768,7 @@ begin
   exact (λ y hy, exists.elim (set.mem_range.1 hy) (λ i hi, by rw ←hi; exact h i))
 end
 
-lemma constr_basis {f : ι → M'} {i : ι} (hv : is_basis R v) :
+@[simp] lemma constr_basis {f : ι → M'} {i : ι} (hv : is_basis R v) :
   (hv.constr f : M → M') (v i) = f i :=
 by simp [is_basis.constr_apply, hv.repr_eq_single, finsupp.sum_single_index]
 
@@ -797,10 +784,10 @@ constr_eq hv $ λ x, rfl
 
 lemma constr_add {g f : ι → M'} (hv : is_basis R v) :
   hv.constr (λi, f i + g i) = hv.constr f + hv.constr g :=
-constr_eq hv $ by simp [constr_basis hv] {contextual := tt}
+constr_eq hv $ λ b, by simp
 
 lemma constr_neg {f : ι → M'} (hv : is_basis R v) : hv.constr (λi, - f i) = - hv.constr f :=
-constr_eq hv $ by simp [constr_basis hv] {contextual := tt}
+constr_eq hv $ λ b, by simp
 
 lemma constr_sub {g f : ι → M'} (hs : is_basis R v) :
   hv.constr (λi, f i - g i) = hs.constr f - hs.constr g :=
@@ -1022,7 +1009,7 @@ lemma linear_independent.insert (hs : linear_independent K (λ b, b : s → V))
 begin
   rw ← union_singleton,
   have x0 : x ≠ 0 := mt (by rintro rfl; apply zero_mem _) hx,
-  apply linear_independent_union hs (linear_independent_singleton x0),
+  apply hs.union (linear_independent_singleton x0),
   rwa [disjoint_span_singleton x0]
 end
 
@@ -1032,7 +1019,6 @@ begin
   rcases zorn.zorn_subset₀ {b | b ⊆ t ∧ linear_independent K (λ x, x : b → V)} _ _
     ⟨hst, hs⟩ with ⟨b, ⟨bt, bi⟩, sb, h⟩,
   { refine ⟨b, bt, sb, λ x xt, _, bi⟩,
-    haveI := classical.dec (x ∈ span K b),
     by_contra hn,
     apply hn,
     rw ← h _ ⟨insert_subset.2 ⟨xt, bt⟩, bi.insert hn⟩ (subset_insert _ _),
@@ -1044,14 +1030,14 @@ begin
 end
 
 lemma exists_subset_is_basis (hs : linear_independent K (λ x, x : s → V)) :
-  ∃b, s ⊆ b ∧ is_basis K (λ i : b, i.val) :=
+  ∃b, s ⊆ b ∧ is_basis K (coe : b → V) :=
 let ⟨b, hb₀, hx, hb₂, hb₃⟩ := exists_linear_independent hs (@subset_univ _ _) in
 ⟨ b, hx,
   @linear_independent.restrict_of_comp_subtype _ _ _ id _ _ _ _ hb₃,
   by simp; exact eq_top_iff.2 hb₂⟩
 
 variables (K V)
-lemma exists_is_basis : ∃b : set V, is_basis K (λ i : b, i.val) :=
+lemma exists_is_basis : ∃b : set V, is_basis K (λ i, i : b → V) :=
 let ⟨b, _, hb⟩ := exists_subset_is_basis linear_independent_empty in ⟨b, hb⟩
 
 variables {K V}
@@ -1101,11 +1087,10 @@ assume t, finset.induction_on t
         ⟨u, subset.trans hust $ union_subset_union (subset.refl _) (by simp [subset_insert]),
           hsu, by simp [eq, hb₂t', hb₁t, hb₁s']⟩)),
 begin
-  letI := classical.dec_pred (λx, x ∈ s),
   have eq : t.filter (λx, x ∈ s) ∪ t.filter (λx, x ∉ s) = t,
   { apply finset.ext.mpr,
     intro x,
-    by_cases x ∈ s; simp *, finish },
+    by_cases x ∈ s; simp * },
   apply exists.elim (this (t.filter (λx, x ∉ s)) (t.filter (λx, x ∈ s))
     (by simp [set.subset_def]) (by simp [set.ext_iff] {contextual := tt}) (by rwa [eq])),
   intros u h,
@@ -1121,50 +1106,42 @@ let ⟨u, hust, hsu, eq⟩ := exists_of_linear_independent_of_finite_span hs thi
 have finite s, from finite_subset u.finite_to_set hsu,
 ⟨this, by rw [←eq]; exact (finset.card_le_of_subset $ finset.coe_subset.mp $ by simp [hsu])⟩
 
-lemma exists_left_inverse_linear_map_of_injective {f : V →ₗ[K] V'}
+lemma linear_map.exists_left_inverse_of_injective (f : V →ₗ[K] V')
   (hf_inj : f.ker = ⊥) : ∃g:V' →ₗ V, g.comp f = linear_map.id :=
 begin
   rcases exists_is_basis K V with ⟨B, hB⟩,
   have hB₀ : _ := hB.1.to_subtype_range,
   have : linear_independent K (λ x, x : f '' B → V'),
   { have h₁ := hB₀.image_subtype
       (show disjoint (span K (range (λ i : B, i.val))) (linear_map.ker f), by simp [hf_inj]),
-    have h₂ : range (λ (i : B), i.val) = B := subtype.range_val B,
-    rwa h₂ at h₁ },
+    rwa B.range_coe_subtype at h₁ },
   rcases exists_subset_is_basis this with ⟨C, BC, hC⟩,
   haveI : inhabited V := ⟨0⟩,
   use hC.constr (C.restrict (inv_fun f)),
-  apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ hB,
-  intros b,
+  refine hB.ext (λ b, _),
   rw image_subset_iff at BC,
-  simp,
-  have := BC (subtype.mem b),
-  rw mem_preimage at this,
-  have : f (b.val) = (subtype.mk (f ↑b) (begin rw ←mem_preimage, exact BC (subtype.mem b) end) : C).val,
-    by simp; unfold_coes,
-  rw this,
-  rw [constr_basis hC],
-  exact left_inverse_inv_fun (linear_map.ker_eq_bot.1 hf_inj) _,
+  have : f b = (⟨f b, BC b.2⟩ : C) := rfl,
+  dsimp,
+  rw [this, constr_basis hC],
+  exact left_inverse_inv_fun (linear_map.ker_eq_bot.1 hf_inj) _
 end
 
-lemma exists_right_inverse_linear_map_of_surjective {f : V →ₗ[K] V'}
+lemma linear_map.exists_right_inverse_of_surjective (f : V →ₗ[K] V')
   (hf_surj : f.range = ⊤) : ∃g:V' →ₗ V, f.comp g = linear_map.id :=
 begin
   rcases exists_is_basis K V' with ⟨C, hC⟩,
   haveI : inhabited V := ⟨0⟩,
   use hC.constr (C.restrict (inv_fun f)),
-  apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ hC,
-  intros c,
-  simp [constr_basis hC],
-  exact right_inverse_inv_fun (linear_map.range_eq_top.1 hf_surj) _
+  refine hC.ext (λ c, _),
+  simp [constr_basis hC, right_inverse_inv_fun (linear_map.range_eq_top.1 hf_surj) c]
 end
 
 open submodule linear_map
+
 theorem quotient_prod_linear_equiv (p : submodule K V) :
   nonempty ((p.quotient × p) ≃ₗ[K] V) :=
 begin
-  haveI := classical.dec_eq (quotient p),
-  rcases exists_right_inverse_linear_map_of_surjective p.range_mkq with ⟨f, hf⟩,
+  rcases p.mkq.exists_right_inverse_of_surjective p.range_mkq with ⟨f, hf⟩,
   have mkf : ∀ x, submodule.quotient.mk (f x) = x := linear_map.ext_iff.1 hf,
   have fp : ∀ x, x - f (p.mkq x) ∈ p :=
     λ x, (submodule.quotient.eq p).1 (mkf (p.mkq x)).symm,
@@ -1182,13 +1159,7 @@ open fintype
 
 theorem vector_space.card_fintype [fintype K] [fintype V] :
   ∃ n : ℕ, card V = (card K) ^ n :=
-begin
-  apply exists.elim (exists_is_basis K V),
-  intros b hb,
-  haveI := classical.dec_pred (λ x, x ∈ b),
-  use card b,
-  exact module.card_fintype hb,
-end
+exists.elim (exists_is_basis K V) $ λ b hb, ⟨card b, module.card_fintype hb⟩
 
 end vector_space
 
@@ -1255,22 +1226,19 @@ section
 variables (R η)
 
 lemma is_basis_fun₀ : is_basis R
-    (λ (ji : Σ (j : η), (λ _, unit) j),
+    (λ (ji : Σ (j : η), unit),
        (std_basis R (λ (i : η), R) (ji.fst)) 1) :=
-begin
-  haveI := classical.dec_eq,
-  apply @is_basis_std_basis R η (λi:η, unit) (λi:η, R) _ _ _ _ (λ _ _, (1 : R))
-      (assume i, @is_basis_singleton_one _ _ _ _),
-end
+@is_basis_std_basis R η (λi:η, unit) (λi:η, R) _ _ _ _ (λ _ _, (1 : R))
+  (assume i, @is_basis_singleton_one _ _ _ _)
 
 lemma is_basis_fun : is_basis R (λ i, std_basis R (λi:η, R) i 1) :=
 begin
-  apply is_basis.comp (is_basis_fun₀ R η) (λ i, ⟨i, punit.star⟩),
+  apply (is_basis_fun₀ R η).comp (λ i, ⟨i, punit.star⟩),
   apply bijective_iff_has_inverse.2,
-  use (λ x, x.1),
-  simp [function.left_inverse, function.right_inverse],
-  intros _ b,
-  rw [unique.eq_default b, unique.eq_default punit.star]
+  use sigma.fst,
+  suffices : ∀ (a : η) (b : unit), punit.star = b,
+  { simpa [function.left_inverse, function.right_inverse] },
+  exact λ _, punit_eq _
 end
 
 end