chore(linear_algebra/dimension): remove a nontriviality assumption (#18715)

`dim_pos` does not need `nontrivial R`.

Also adds a new lemma that demonstrates why the assumption is still needed on some later results.

Author: eric-wieser

src/linear_algebra/dimension.lean

@@ -463,23 +463,53 @@ end
 section rank_zero
 
 variables {R : Type u} {M : Type v}
-variables [ring R] [nontrivial R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M]
+variables [ring R] [add_comm_group M] [module R M]
+
+@[simp] lemma dim_subsingleton [subsingleton R] : module.rank R M = 1 :=
+begin
+  haveI := module.subsingleton R M,
+  haveI : nonempty {s : set M // linear_independent R (coe : s → M)},
+  { exact ⟨⟨∅, linear_independent_empty _ _⟩⟩ },
+  rw [module.rank, csupr_eq_of_forall_le_of_forall_lt_exists_gt],
+  { rintros ⟨s, hs⟩,
+    rw cardinal.mk_le_one_iff_set_subsingleton,
+    apply subsingleton_of_subsingleton },
+  intros w hw,
+  refine ⟨⟨{0}, _⟩, _⟩,
+  { rw linear_independent_iff',
+    intros,
+    exact subsingleton.elim _ _ },
+  { exact hw.trans_eq (cardinal.mk_singleton _).symm },
+end
+
+variables [no_zero_smul_divisors R M]
+
+lemma dim_pos [nontrivial M] : 0 < module.rank R M :=
+begin
+  obtain ⟨x, hx⟩ := exists_ne (0 : M),
+  suffices : 1 ≤ module.rank R M,
+  { exact zero_lt_one.trans_le this },
+  letI := module.nontrivial R M,
+  suffices : linear_independent R (λ (y : ({x} : set M)), ↑y),
+  { simpa using (cardinal_le_dim_of_linear_independent this), },
+  exact linear_independent_singleton hx
+end
+
+variables [nontrivial R]
 
 lemma dim_zero_iff_forall_zero : module.rank R M = 0 ↔ ∀ x : M, x = 0 :=
 begin
   refine ⟨λ h, _, λ h, _⟩,
   { contrapose! h,
     obtain ⟨x, hx⟩ := h,
-    suffices : 1 ≤ module.rank R M,
-    { intro h, exact this.not_lt (h.symm ▸ zero_lt_one) },
-    suffices : linear_independent R (λ (y : ({x} : set M)), ↑y),
-    { simpa using (cardinal_le_dim_of_linear_independent this), },
-    exact linear_independent_singleton hx },
+    letI : nontrivial M := nontrivial_of_ne _ _ hx,
+    exact dim_pos.ne' },
   { have : (⊤ : submodule R M) = ⊥,
     { ext x, simp [h x] },
     rw [←dim_top, this, dim_bot] }
 end
 
+/-- See `dim_subsingleton` for the reason that `nontrivial R` is needed. -/
 lemma dim_zero_iff : module.rank R M = 0 ↔ subsingleton M :=
 dim_zero_iff_forall_zero.trans (subsingleton_iff_forall_eq 0).symm
 
@@ -492,9 +522,6 @@ end
 lemma dim_pos_iff_nontrivial : 0 < module.rank R M ↔ nontrivial M :=
 dim_pos_iff_exists_ne_zero.trans (nontrivial_iff_exists_ne 0).symm
 
-lemma dim_pos [h : nontrivial M] : 0 < module.rank R M :=
-dim_pos_iff_nontrivial.2 h
-
 end rank_zero
 
 section invariant_basis_number