feat(linear_algebra/finite_dimensional): characterizations of finrank = 1 and ≤ 1 (#7354)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/linear_algebra/affine_space/independent.lean

@@ -398,7 +398,7 @@ begin
     intro he,
     rw vsub_eq_zero_iff_eq at he,
     exact h he.symm },
-  exact linear_independent_unique hz
+  exact linear_independent_unique _ hz
 end
 
 end field

src/linear_algebra/basic.lean

@@ -948,6 +948,12 @@ lemma le_span_singleton_iff {s : submodule R M} {v₀ : M} :
   s ≤ (R ∙ v₀) ↔ ∀ v ∈ s, ∃ r : R, r • v₀ = v :=
 by simp_rw [set_like.le_def, mem_span_singleton]
 
+lemma span_singleton_eq_top_iff (x : M) : (R ∙ x) = ⊤ ↔ ∀ v, ∃ r : R, r • x = v :=
+begin
+  rw [eq_top_iff, le_span_singleton_iff],
+  finish,
+end
+
 @[simp] lemma span_zero_singleton : (R ∙ (0:M)) = ⊥ :=
 by { ext, simp [mem_span_singleton, eq_comm] }
 

src/linear_algebra/basis.lean

@@ -343,6 +343,22 @@ end
 
 end is_basis
 
+lemma is_basis_singleton_iff
+  {R : Type*} [ring R] [nontrivial R] [module R M] [no_zero_smul_divisors R M]
+  (ι : Type*) [unique ι] (x : M) :
+  is_basis R (λ (_ : ι), x) ↔ x ≠ 0 ∧ ∀ y : M, ∃ r : R, r • x = y :=
+begin
+  fsplit,
+  rintro ⟨li, sp⟩,
+  fsplit,
+  apply linear_independent.ne_zero (default ι) li,
+  simpa [span_singleton_eq_top_iff] using sp,
+  rintro ⟨nz, w⟩,
+  fsplit,
+  simpa [linear_independent_unique_iff] using nz,
+  simpa [span_singleton_eq_top_iff] using w,
+end
+
 lemma is_basis_singleton_one (R : Type*) [unique ι] [ring R] :
   is_basis R (λ (_ : ι), (1 : R)) :=
 begin

src/linear_algebra/finite_dimensional.lean

@@ -283,6 +283,17 @@ let ⟨B, hB, B_fin⟩ := exists_is_basis_finite K V, ⟨g, hg⟩ := finite_dime
 
 variables {K V}
 
+/-- A module with dimension 1 has a basis of the form `{v}` for some `v : V`. -/
+lemma exists_is_basis_singleton (h : finrank K V = 1) :
+  ∃ (v : V), is_basis K (coe : ({v} : set V) → V) :=
+begin
+  haveI := finite_dimensional_of_finrank (_root_.zero_lt_one.trans_le h.symm.le),
+  obtain ⟨s, b⟩ := exists_is_basis_finset K V,
+  obtain ⟨v, rfl⟩ := finset.card_eq_one.mp ((finrank_eq_card_finset_basis b).symm.trans h),
+  use v,
+  convert b; simp,
+end
+
 lemma cardinal_mk_le_finrank_of_linear_independent
   [finite_dimensional K V] {ι : Type w} {b : ι → V} (h : linear_independent K b) :
   cardinal.mk ι ≤ finrank K V :=
@@ -344,7 +355,7 @@ lemma finrank_zero_iff [finite_dimensional K V] :
 iff.trans (by { rw ← finrank_eq_dim, norm_cast }) (@dim_zero_iff K V _ _ _)
 
 /-- A finite dimensional space that is a subsingleton has zero `finrank`. -/
-lemma finrank_zero_of_subsingleton [finite_dimensional K V] [h : subsingleton V] :
+lemma finrank_zero_of_subsingleton [h : subsingleton V] :
   finrank K V = 0 :=
 finrank_zero_iff.2 h
 
@@ -1197,8 +1208,99 @@ lemma set_is_basis_of_linear_independent_of_card_eq_finrank
   is_basis K (coe : s → V) :=
 is_basis_of_linear_independent_of_card_eq_finrank lin_ind (trans s.to_finset_card.symm card_eq)
 
+lemma singleton_is_basis (v : V) (nz : v ≠ 0) (h : finrank K V = 1) :
+  is_basis K (coe : ({v} : set V) → V) :=
+set_is_basis_of_linear_independent_of_card_eq_finrank
+  (linear_independent_singleton nz) (by simp [h])
+
 end is_basis
 
+/-!
+We now give characterisations of `finrank K V = 1` and `finrank K V ≤ 1`.
+-/
+section finrank_eq_one
+
+/-- If there is a nonzero vector and every other vector is a multiple of it,
+then the module has dimension one. -/
+lemma finrank_eq_one (v : V) (n : v ≠ 0) (h : ∀ w : V, ∃ c : K, c • v = w) :
+  finrank K V = 1 :=
+begin
+  convert finrank_eq_card_basis ((is_basis_singleton_iff punit v).mpr _),
+  apply_instance, apply_instance, -- Not sure why these aren't found automatically.
+  exact ⟨n, h⟩,
+end
+
+/--
+If every vector is a multiple of some `v : V`, then `V` has dimension at most one.
+-/
+lemma finrank_le_one (v : V) (h : ∀ w : V, ∃ c : K, c • v = w) :
+  finrank K V ≤ 1 :=
+begin
+  by_cases n : v = 0,
+  { subst n,
+    convert zero_le_one,
+    haveI := subsingleton_of_forall_eq (0 : V) (λ w, by { obtain ⟨c, rfl⟩ := h w, simp, }),
+    exact finrank_zero_of_subsingleton, },
+  { exact (finrank_eq_one v n h).le, }
+end
+
+/--
+A module with a nonzero vector `v` has dimension 1 iff `v` spans.
+-/
+lemma finrank_eq_one_iff_of_nonzero (v : V) (nz : v ≠ 0) :
+  finrank K V = 1 ↔ span K ({v} : set V) = ⊤ :=
+⟨λ h, by { convert (singleton_is_basis v nz h).2, simp },
+  λ s, finrank_eq_card_basis ⟨linear_independent_singleton nz, by { convert s, simp }⟩⟩
+
+/--
+A module has dimension 1 iff there is some `v : V` so `{v}` is a basis.
+-/
+lemma finrank_eq_one_iff :
+  finrank K V = 1 ↔ ∃ (v : V), is_basis K (λ x : ({v} : set V), (x : V)) :=
+begin
+  fsplit,
+  { intro h,
+    haveI := finite_dimensional_of_finrank (_root_.zero_lt_one.trans_le h.symm.le),
+    exact exists_is_basis_singleton h, },
+  { rintro ⟨v, b⟩,
+    convert finrank_eq_card_basis b, }
+end
+
+/--
+A module has dimension 1 iff there is some nonzero `v : V` so every vector is a multiple of `v`.
+-/
+lemma finrank_eq_one_iff' :
+  finrank K V = 1 ↔ ∃ (v : V) (n : v ≠ 0), ∀ w : V, ∃ c : K, c • v = w :=
+begin
+  convert finrank_eq_one_iff,
+  funext v,
+  simp only [exists_prop, eq_iff_iff, ne.def],
+  convert (is_basis_singleton_iff ({v} : set V) v).symm,
+  ext ⟨x, ⟨⟩⟩,
+  refl,
+  apply_instance, apply_instance, -- Not sure why this aren't found automatically.
+end
+
+/--
+A finite dimensional module has dimension at most 1 iff
+there is some `v : V` so every vector is a multiple of `v`.
+-/
+lemma finrank_le_one_iff [finite_dimensional K V] :
+  finrank K V ≤ 1 ↔ ∃ (v : V), ∀ w : V, ∃ c : K, c • v = w :=
+begin
+  fsplit,
+  { intro h,
+    by_cases h' : finrank K V = 0,
+    { use 0, intro w, use 0, haveI := finrank_zero_iff.mp h', apply subsingleton.elim, },
+    { replace h' := zero_lt_iff.mpr h', have : finrank K V = 1, { linarith },
+      obtain ⟨v, -, p⟩ := finrank_eq_one_iff'.mp this,
+      use ⟨v, p⟩, }, },
+  { rintro ⟨v, p⟩,
+    exact finrank_le_one v p, }
+end
+
+end finrank_eq_one
+
 section subalgebra_dim
 open module
 variables {F E : Type*} [field F] [field E] [algebra F E]

src/linear_algebra/linear_independent.lean

@@ -900,8 +900,10 @@ begin
     exact false.elim (h _ ((smul_mem_iff _ ha').1 ha)) }
 end
 
-lemma linear_independent_unique_iff [unique ι] :
-  linear_independent K v ↔ v (default ι) ≠ 0 :=
+lemma linear_independent_unique_iff [ring R] [nontrivial R] [add_comm_monoid M] [module R M]
+  [no_zero_smul_divisors R M]
+  (v : ι → M) [unique ι] :
+  linear_independent R v ↔ v (default ι) ≠ 0 :=
 begin
   simp only [linear_independent_iff, finsupp.total_unique, smul_eq_zero],
   refine ⟨λ h hv, _, λ hv l hl, finsupp.unique_ext $ hl.resolve_right hv⟩,
@@ -913,7 +915,7 @@ alias linear_independent_unique_iff ↔ _ linear_independent_unique
 
 lemma linear_independent_singleton {x : V} (hx : x ≠ 0) :
   linear_independent K (λ x, x : ({x} : set V) → V) :=
-@linear_independent_unique _ _ _ _ _ _ _ (set.unique_singleton _) ‹_›
+linear_independent_unique coe hx
 
 lemma linear_independent_option' :
   linear_independent K (λ o, option.cases_on' o x v : option ι → V) ↔