feat(ring_theory/algebra_operations): submodules form a semiring

src/algebra/pointwise.lean

@@ -1,6 +1,7 @@
 import data.set.lattice
 import algebra.group
 import group_theory.subgroup
+import data.set.finite
 
 namespace set
 open function
@@ -38,6 +39,11 @@ set.ext $ λ a,
 ⟨ by { rintros ⟨_, _, _, _, rfl⟩, exact ⟨(_, _), mem_prod.mpr ⟨‹_›, ‹_›⟩, rfl⟩ },
   by { rintros ⟨_, _, rfl⟩, exact ⟨_, (mem_prod.mp ‹_›).1, _, (mem_prod.mp ‹_›).2, rfl⟩ }⟩
 
+@[to_additive set.pointwise_add_finite]
+lemma pointwise_mul_finite [has_mul α] {s t : set α} (hs : finite s) (ht : finite t) :
+  finite (s * t) :=
+by { rw pointwise_mul_eq_image, apply set.finite_image, exact set.finite_prod hs ht }
+
 def pointwise_mul_semigroup [semigroup α] : semigroup (set α) :=
 { mul_assoc := λ _ _ _, set.ext $ λ _,
   begin

src/ring_theory/algebra_operations.lean

@@ -6,27 +6,48 @@ Authors: Kenny Lau
 Multiplication of submodules of an algebra.
 -/
 
-import ring_theory.algebra ring_theory.noetherian
+import ring_theory.algebra algebra.pointwise ring_theory.ideals
+import tactic.chain
 
 universes u v
 
-open lattice submodule
+open lattice algebra
 
-namespace algebra
+local attribute [instance] set.pointwise_mul_semiring
+
+namespace submodule
 
 variables {R : Type u} [comm_ring R]
 
 section ring
 
 variables {A : Type v} [ring A] [algebra R A]
+variables (S T : set A) {M N P Q : submodule R A} {m n : A}
+
+instance : has_one (submodule R A) :=
+⟨submodule.map (of_id R A).to_linear_map (⊤ : ideal R)⟩
+
+theorem one_eq_map_top :
+  (1 : submodule R A) = submodule.map (of_id R A).to_linear_map (⊤ : ideal R) := rfl
+
+theorem one_eq_span : (1 : submodule R A) = span R {1} :=
+begin
+  apply submodule.ext,
+  intro a,
+  erw [mem_map, mem_span_singleton],
+  apply exists_congr,
+  intro r,
+  simpa [smul_def],
+end
+
+theorem one_le : (1 : submodule R A) ≤ P ↔ (1 : A) ∈ P :=
+by simpa only [one_eq_span, span_le, set.singleton_subset_iff]
 
 set_option class.instance_max_depth 50
 instance : has_mul (submodule R A) :=
 ⟨λ M N, ⨆ s : M, N.map $ algebra.lmul R A s.1⟩
 set_option class.instance_max_depth 32
 
-variables (S T : set A) {M N P Q : submodule R A} {m n : A}
-
 theorem mul_mem_mul (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N :=
 (le_supr _ ⟨m, hm⟩ : _ ≤ M * N) ⟨n, hn, rfl⟩
 
@@ -42,27 +63,21 @@ theorem mul_le : M * N ≤ P ↔ ∀ (m ∈ M) (n ∈ N), m * n ∈ P :=
 (@mul_le _ _ _ _ _ _ _ ⟨C, h0, ha, hs⟩).2 hm hr
 
 variables R
-theorem span_mul_span : span R S * span R T = span R ((S.prod T).image (λ p, p.1 * p.2)) :=
-le_antisymm
-  (mul_le.2 $ λ x1 hx1 x2 hx2, span_induction hx1
-    (λ y1 hy1, span_induction hx2
-      (λ y2 hy2, subset_span ⟨(y1, y2), ⟨hy1, hy2⟩, rfl⟩)
-      ((mul_zero y1).symm ▸ zero_mem _)
-      (λ r1 r2, (mul_add y1 r1 r2).symm ▸ add_mem _)
-      (λ s r, (algebra.mul_smul_comm s y1 r).symm ▸ smul_mem _ _))
-    ((zero_mul x2).symm ▸ zero_mem _)
-    (λ r1 r2, (add_mul r1 r2 x2).symm ▸ add_mem _)
-    (λ s r, (algebra.smul_mul_assoc s r x2).symm ▸ smul_mem _ _))
-  (span_le.2 (set.image_subset_iff.2 $ λ ⟨x1, x2⟩ ⟨hx1, hx2⟩,
-    mul_mem_mul (subset_span hx1) (subset_span hx2)))
+theorem span_mul_span : span R S * span R T = span R (S * T) :=
+begin
+  apply le_antisymm,
+  { rw mul_le, intros a ha b hb,
+    apply span_induction ha,
+    work_on_goal 0 { intros, apply span_induction hb,
+      work_on_goal 0 { intros, exact subset_span ⟨_, ‹_›, _, ‹_›, rfl⟩ } },
+    all_goals { intros, simp only [mul_zero, zero_mul, zero_mem,
+        left_distrib, right_distrib, mul_smul_comm, smul_mul_assoc],
+      try {apply add_mem _ _ _}, try {apply smul_mem _ _ _} }, assumption' },
+  { rw span_le, rintros _ ⟨a, ha, b, hb, rfl⟩,
+    exact mul_mem_mul (subset_span ha) (subset_span hb) }
+end
 variables {R}
 
-theorem fg_mul (hm : M.fg) (hn : N.fg) : (M * N).fg :=
-let ⟨m, hf1, hm⟩ := fg_def.1 hm, ⟨n, hf2, hn⟩ := fg_def.1 hn in
-fg_def.2 ⟨(m.prod n).image (λ p, p.1 * p.2),
-set.finite_image _ (set.finite_prod hf1 hf2),
-span_mul_span R m n ▸ hm ▸ hn ▸ rfl⟩
-
 variables (M N P Q)
 set_option class.instance_max_depth 50
 protected theorem mul_assoc : (M * N) * P = M * (N * P) :=
@@ -79,6 +94,13 @@ eq_bot_iff.2 $ mul_le.2 $ λ m hm n hn, by rw [submodule.mem_bot] at hn ⊢; rw
 
 @[simp] theorem bot_mul : ⊥ * M = ⊥ :=
 eq_bot_iff.2 $ mul_le.2 $ λ m hm n hn, by rw [submodule.mem_bot] at hm ⊢; rw [hm, zero_mul]
+
+@[simp] protected theorem one_mul : (1 : submodule R A) * M = M :=
+by { conv_lhs { rw [one_eq_span, ← span_eq M] }, erw [span_mul_span, one_mul, span_eq] }
+
+@[simp] protected theorem mul_one : M * 1 = M :=
+by { conv_lhs { rw [one_eq_span, ← span_eq M] }, erw [span_mul_span, mul_one, span_eq] }
+
 variables {M N P Q}
 
 @[mono] theorem mul_le_mul (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q :=
@@ -102,19 +124,17 @@ le_antisymm (mul_le.2 $ λ mn hmn p hp, let ⟨m, hm, n, hn, hmn⟩ := mem_sup.1
 (sup_le (mul_le_mul_left le_sup_left) (mul_le_mul_left le_sup_right))
 variables {M N P}
 
-instance : semigroup (submodule R A) :=
-{ mul := (*),
-  mul_assoc := algebra.mul_assoc }
-
-instance : mul_zero_class (submodule R A) :=
-{ zero_mul := bot_mul,
-  mul_zero := mul_bot,
-  .. submodule.add_comm_monoid, .. algebra.semigroup  }
-
-instance : distrib (submodule R A) :=
-{ left_distrib := mul_sup,
+instance : semiring (submodule R A) :=
+{ one_mul       := submodule.one_mul,
+  mul_one       := submodule.mul_one,
+  mul_assoc     := submodule.mul_assoc,
+  zero_mul      := bot_mul,
+  mul_zero      := mul_bot,
+  left_distrib  := mul_sup,
   right_distrib := sup_mul,
-  .. submodule.add_comm_monoid, .. algebra.semigroup }
+  ..submodule.add_comm_monoid,
+  ..submodule.has_one,
+  ..submodule.has_mul }
 
 end ring
 
@@ -131,10 +151,10 @@ protected theorem mul_comm : M * N = N * M :=
 le_antisymm (mul_le.2 $ λ r hrm s hsn, mul_mem_mul_rev hsn hrm)
 (mul_le.2 $ λ r hrn s hsm, mul_mem_mul_rev hsm hrn)
 
-instance : comm_semigroup (submodule R A) :=
-{ mul_comm := algebra.mul_comm,
-  .. algebra.semigroup }
+instance : comm_semiring (submodule R A) :=
+{ mul_comm := submodule.mul_comm,
+  .. submodule.semiring }
 
 end comm_ring
 
-end algebra
+end submodule

src/ring_theory/ideal_operations.lean

@@ -9,6 +9,7 @@ More operations on modules and ideals.
 import ring_theory.ideals data.nat.choose order.zorn
 import linear_algebra.tensor_product
 import data.equiv.algebra
+import ring_theory.algebra_operations
 
 universes u v w x
 
@@ -107,15 +108,15 @@ theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P :=
 smul_mono (le_refl I) h
 
 variables (I J N P)
-theorem smul_bot : I • (⊥ : submodule R M) = ⊥ :=
+@[simp] theorem smul_bot : I • (⊥ : submodule R M) = ⊥ :=
 eq_bot_iff.2 $ smul_le.2 $ λ r hri s hsb,
 (submodule.mem_bot R).2 $ ((submodule.mem_bot R).1 hsb).symm ▸ smul_zero r
 
-theorem bot_smul : (⊥ : ideal R) • N = ⊥ :=
+@[simp] theorem bot_smul : (⊥ : ideal R) • N = ⊥ :=
 eq_bot_iff.2 $ smul_le.2 $ λ r hrb s hsi,
 (submodule.mem_bot R).2 $ ((submodule.mem_bot R).1 hrb).symm ▸ zero_smul _ s
 
-theorem top_smul : (⊤ : ideal R) • N = N :=
+@[simp] theorem top_smul : (⊤ : ideal R) • N = N :=
 le_antisymm smul_le_right $ λ r hri, one_smul R r ▸ smul_mem_smul mem_top hri
 
 theorem smul_sup : I • (N ⊔ P) = I • N ⊔ I • P :=
@@ -379,22 +380,12 @@ have is_prime m, from ⟨by rintro rfl; rw radical_top at hrm; exact hrm trivial
     refine m.add_mem (m.mul_mem_right hpm) (m.add_mem (m.mul_mem_left hfm) (m.mul_mem_left hxym))⟩⟩,
 hrm $ this.radical.symm ▸ (Inf_le ⟨him, this⟩ : Inf {J : ideal R | I ≤ J ∧ is_prime J} ≤ m) hr
 
-instance : comm_semiring (ideal R) :=
-{ mul := (*),
-  mul_assoc := ideal.mul_assoc,
-  zero_mul := bot_mul,
-  mul_zero := mul_bot,
-  one := ⊤,
-  one_mul := top_mul,
-  mul_one := mul_top,
-  left_distrib := mul_sup,
-  right_distrib := sup_mul,
-  mul_comm := ideal.mul_comm,
-  .. submodule.add_comm_monoid }
+instance : comm_semiring (ideal R) := submodule.comm_semiring
 
 @[simp] lemma add_eq_sup : I + J = I ⊔ J := rfl
 @[simp] lemma zero_eq_bot : (0 : ideal R) = ⊥ := rfl
-@[simp] lemma one_eq_top : (1 : ideal R) = ⊤ := rfl
+@[simp] lemma one_eq_top : (1 : ideal R) = ⊤ :=
+by erw [submodule.one_eq_map_top, submodule.map_id]
 
 variables (I)
 theorem radical_pow (n : ℕ) (H : n > 0) : radical (I^n) = radical I :=
@@ -551,13 +542,14 @@ namespace submodule
 
 variables {R : Type u} {M : Type v}
 variables [comm_ring R] [add_comm_group M] [module R M]
-variables (I J : ideal R) (N P : submodule R M)
+
+-- It is even a semialgebra. But those aren't in mathlib yet.
 
 instance : semimodule (ideal R) (submodule R M) :=
 { smul_add := smul_sup,
   add_smul := sup_smul,
   mul_smul := smul_assoc,
-  one_smul := top_smul,
+  one_smul := by simp,
   zero_smul := bot_smul,
   smul_zero := smul_bot }
 

src/ring_theory/noetherian.lean

@@ -418,3 +418,15 @@ is_noetherian_ring.irreducible_induction_on a
         exact associated_mul_mul (by refl) hs.2⟩⟩)
 
 end is_noetherian_ring
+
+namespace submodule
+variables {R : Type*} {A : Type*} [comm_ring R] [ring A] [algebra R A]
+variables (M N : submodule R A)
+
+local attribute [instance] set.pointwise_mul_semiring
+
+theorem fg_mul (hm : M.fg) (hn : N.fg) : (M * N).fg :=
+let ⟨m, hfm, hm⟩ := fg_def.1 hm, ⟨n, hfn, hn⟩ := fg_def.1 hn in
+fg_def.2 ⟨m * n, set.pointwise_mul_finite hfm hfn, span_mul_span R m n ▸ hm ▸ hn ▸ rfl⟩
+
+end submodule