chore(algebra/module/submodule_lattice): lemmas about the trivial sub…

…module (#10022)

Lemmas about the trivial submodule.  Also move an existing lemma `exists_mem_ne_zero_of_ne_bot` about the trivial submodule from `linear_algebra/dimension` to `algebra/module/submodule_lattice`, since it doesn't use any facts about dimension.

src/algebra/module/submodule_lattice.lean

@@ -51,12 +51,6 @@ end
 instance unique_bot : unique (⊥ : submodule R M) :=
 ⟨infer_instance, λ x, subtype.ext $ (mem_bot R).1 x.mem⟩
 
-lemma nonzero_mem_of_bot_lt {I : submodule R M} (bot_lt : ⊥ < I) : ∃ a : I, a ≠ 0 :=
-begin
-  have h := (set_like.lt_iff_le_and_exists.1 bot_lt).2,
-  tidy,
-end
-
 instance : order_bot (submodule R M) :=
 { bot := ⊥,
   bot_le := λ p x, by simp {contextual := tt},
@@ -76,6 +70,12 @@ end
 protected lemma ne_bot_iff (p : submodule R M) : p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ (0 : M) :=
 by { haveI := classical.prop_decidable, simp_rw [ne.def, p.eq_bot_iff, not_forall] }
 
+lemma nonzero_mem_of_bot_lt {p : submodule R M} (bot_lt : ⊥ < p) : ∃ a : p, a ≠ 0 :=
+let ⟨b, hb₁, hb₂⟩ := p.ne_bot_iff.mp bot_lt.ne' in ⟨⟨b, hb₁⟩, hb₂ ∘ (congr_arg coe)⟩
+
+lemma exists_mem_ne_zero_of_ne_bot {p : submodule R M} (h : p ≠ ⊥) : ∃ b : M, b ∈ p ∧ b ≠ 0 :=
+let ⟨b, hb₁, hb₂⟩ := p.ne_bot_iff.mp h in ⟨b, hb₁, hb₂⟩
+
 /-- The bottom submodule is linearly equivalent to punit as an `R`-module. -/
 @[simps] def bot_equiv_punit : (⊥ : submodule R M) ≃ₗ[R] punit :=
 { to_fun := λ x, punit.star,
@@ -85,6 +85,13 @@ by { haveI := classical.prop_decidable, simp_rw [ne.def, p.eq_bot_iff, not_foral
   left_inv := by { intro x, ext, },
   right_inv := by { intro x, ext, }, }
 
+lemma eq_bot_of_subsingleton (p : submodule R M) [subsingleton p] : p = ⊥ :=
+begin
+  rw eq_bot_iff,
+  intros v hv,
+  exact congr_arg coe (subsingleton.elim (⟨v, hv⟩ : p) 0)
+end
+
 /-- The universal set is the top element of the lattice of submodules. -/
 instance : has_top (submodule R M) :=
 ⟨{ carrier := set.univ, smul_mem' := λ _ _ _, trivial, .. (⊤ : add_submonoid M)}⟩

src/linear_algebra/dimension.lean

@@ -1124,14 +1124,6 @@ by { rw [← dim_sup_add_dim_inf_eq], exact self_le_add_right _ _ }
 
 end
 
-lemma exists_mem_ne_zero_of_ne_bot {s : submodule K V} (h : s ≠ ⊥) : ∃ b : V, b ∈ s ∧ b ≠ 0 :=
-begin
-  classical,
-  by_contradiction hex,
-  have : ∀x∈s, (x:V) = 0, { simpa only [not_exists, not_and, not_not, ne.def] using hex },
-  exact (h $ bot_unique $ assume s hs, (submodule.mem_bot K).2 $ this s hs)
-end
-
 lemma exists_mem_ne_zero_of_dim_pos {s : submodule K V} (h : 0 < module.rank K s) :
   ∃ b : V, b ∈ s ∧ b ≠ 0 :=
 exists_mem_ne_zero_of_ne_bot $ assume eq, by rw [eq, dim_bot] at h; exact lt_irrefl _ h

src/linear_algebra/eigenspace.lean

@@ -168,7 +168,7 @@ begin
   obtain ⟨c, nu⟩ := exists_spectrum_of_is_alg_closed_of_finite_dimensional K f,
   use c,
   rw linear_map.is_unit_iff at nu,
-  exact has_eigenvalue_of_has_eigenvector (exists_mem_ne_zero_of_ne_bot nu).some_spec,
+  exact has_eigenvalue_of_has_eigenvector (submodule.exists_mem_ne_zero_of_ne_bot nu).some_spec,
 end
 
 /-- Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly