feat(algebra/*,linear_algebra/basic,ring_theory/ideal): lemmas about …

…span of finite subsets and nontrivial maximal ideals (#5641)

Co-authored-by: laughinggas <58670661+laughinggas@users.noreply.github.com>
Co-authored-by: Ashvni <ashvni.n@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

src/algebra/algebra/operations.lean

@@ -162,7 +162,30 @@ calc map f.to_linear_map (M * N)
       rw f.to_linear_map_apply at fy_eq,
       ext,
       simp [fy_eq] }
-  end
+end
+
+section decidable_eq
+
+open_locale classical
+
+lemma mem_span_mul_finite_of_mem_span_mul {S : set A} {S' : set A} {x : A}
+  (hx : x ∈ span R (S * S')) :
+  ∃ (T T' : finset A), ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ span R (T * T' : set A) :=
+begin
+  obtain ⟨U, h, hU⟩ := mem_span_finite_of_mem_span hx,
+  obtain ⟨T, T', hS, hS', h⟩ := finset.subset_mul h,
+  use [T, T', hS, hS'],
+  have h' : (U : set A) ⊆ T * T', { assumption_mod_cast, },
+  have h'' := span_mono h' hU,
+  assumption,
+end
+
+end decidable_eq
+
+lemma mem_span_mul_finite_of_mem_mul {P Q : submodule R A} {x : A} (hx : x ∈ P * Q) :
+  ∃ (T T' : finset A), (T : set A) ⊆ P ∧ (T' : set A) ⊆ Q ∧ x ∈ span R (T * T' : set A) :=
+submodule.mem_span_mul_finite_of_mem_span_mul
+  (by rwa [← submodule.span_eq P, ← submodule.span_eq Q, submodule.span_mul_span] at hx)
 
 variables {M N P}
 

src/algebra/pointwise.lean

@@ -420,6 +420,33 @@ by { convert finset.card_image_le, rw [finset.card_product, mul_comm] }
 lemma mul_card_le [has_mul α] {s t : finset α} : (s * t).card ≤ s.card * t.card :=
 by { convert finset.card_image_le, rw [finset.card_product, mul_comm] }
 
+open_locale classical
+
+/-- A finite set `U` contained in the product of two sets `S * S'` is also contained in the product
+of two finite sets `T * T' ⊆ S * S'`. -/
+@[to_additive]
+lemma subset_mul {M : Type*} [monoid M] {S : set M} {S' : set M} {U : finset M} (f : ↑U ⊆ S * S') :
+  ∃ (T T' : finset M), ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ U ⊆ T * T' :=
+begin
+  apply finset.induction_on' U,
+  { use [∅, ∅], simp only [finset.empty_subset, finset.coe_empty, set.empty_subset, and_self], },
+  rintros a s haU hs has ⟨T, T', hS, hS', h⟩,
+  obtain ⟨x, y, hx, hy, ha⟩ := set.mem_mul.1 (f haU),
+  use [insert x T, insert y T'],
+  simp only [finset.coe_insert],
+  repeat { rw [set.insert_subset], },
+  use [hx, hS, hy, hS'],
+  refine finset.insert_subset.mpr ⟨_, _⟩,
+  { rw finset.mem_mul,
+    use [x,y],
+    simpa only [true_and, true_or, eq_self_iff_true, finset.mem_insert], },
+  { suffices g : (s : set M) ⊆ insert x T * insert y T', { norm_cast at g, assumption, },
+    transitivity ↑(T * T'),
+    apply h,
+    rw finset.coe_mul,
+    apply set.mul_subset_mul (set.subset_insert x T) (set.subset_insert y T'), },
+end
+
 end finset
 
 /-! Some lemmas about pointwise multiplication and submonoids. Ideally we put these in

src/linear_algebra/basic.lean

@@ -1030,6 +1030,33 @@ begin
   simp only [span_singleton_le_iff_mem],
 end
 
+section
+
+open_locale classical
+
+/-- For every element in the span of a set, there exists a finite subset of the set
+such that the element is contained in the span of the subset. -/
+lemma mem_span_finite_of_mem_span {S : set M} {x : M} (hx : x ∈ span R S) :
+  ∃ T : finset M, ↑T ⊆ S ∧ x ∈ span R (T : set M) :=
+begin
+  refine span_induction hx (λ x hx, _) _ _ _,
+  { refine ⟨{x}, _, _⟩,
+    { rwa [finset.coe_singleton, set.singleton_subset_iff] },
+    { rw finset.coe_singleton,
+      exact submodule.mem_span_singleton_self x } },
+  { use ∅, simp },
+  { rintros x y ⟨X, hX, hxX⟩ ⟨Y, hY, hyY⟩,
+    refine ⟨X ∪ Y, _, _⟩,
+    { rw finset.coe_union,
+      exact set.union_subset hX hY },
+    rw [finset.coe_union, span_union, mem_sup],
+    exact ⟨x, hxX, y, hyY, rfl⟩, },
+  { rintros a x ⟨T, hT, h2⟩,
+    exact ⟨T, hT, smul_mem _ _ h2⟩ }
+end
+
+end
+
 /-- The product of two submodules is a submodule. -/
 def prod : submodule R (M × M₂) :=
 { carrier   := set.prod p q,

src/ring_theory/ideal/basic.lean

@@ -598,6 +598,17 @@ not_is_field_iff_exists_ideal_bot_lt_and_lt_top.trans
     ⟨p, bot_lt_iff_ne_bot.mp (lt_of_lt_of_le bot_lt le_p), hp.is_prime⟩,
    λ ⟨p, ne_bot, prime⟩, ⟨p, bot_lt_iff_ne_bot.mpr ne_bot, lt_top_iff_ne_top.mpr prime.1⟩⟩
 
+/-- When a ring is not a field, the maximal ideals are nontrivial. -/
+lemma ne_bot_of_is_maximal_of_not_is_field [nontrivial R] {M : ideal R} (max : M.is_maximal)
+  (not_field : ¬ is_field R) : M ≠ ⊥ :=
+begin
+  rintros h,
+  rw h at max,
+  cases max with h1 h2,
+  obtain ⟨I, hIbot, hItop⟩ := not_is_field_iff_exists_ideal_bot_lt_and_lt_top.mp not_field,
+  exact ne_of_lt hItop (h2 I hIbot),
+end
+
 end ring
 
 namespace ideal