feat(ring_theory/finiteness): add lemmas (#7409)

I add here some preliminary lemmas to prove that a monoid is finitely generated iff the monoid algebra is.

src/algebra/monoid_algebra.lean

@@ -616,9 +616,8 @@ section span
 variables [semiring k] [mul_one_class G]
 
 lemma mem_span_support (f : monoid_algebra k G) :
-  f ∈ submodule.span k (monoid_algebra.of k G '' (f.support : set G)) :=
-by rw [monoid_algebra.of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single,
-  finsupp.mem_supported]
+  f ∈ submodule.span k (of k G '' (f.support : set G)) :=
+by rw [of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single, finsupp.mem_supported]
 
 end span
 
@@ -879,11 +878,16 @@ def of [add_zero_class G] : multiplicative G →* add_monoid_algebra k G :=
   map_one' := rfl,
   map_mul' := λ a b, by { rw [single_mul_single, one_mul], refl } }
 
+/-- Embedding of a monoid into its monoid algebra, having `G` as source. -/
+def of' : G → add_monoid_algebra k G := λ a, single a 1
+
 end
 
 @[simp] lemma of_apply [add_zero_class G] (a : multiplicative G) : of k G a = single a.to_add 1 :=
 rfl
 
+@[simp] lemma of'_apply (a : G) : of' k G a = single a 1 := rfl
+
 lemma of_injective [nontrivial k] [add_zero_class G] : function.injective (of k G) :=
 λ a b h, by simpa using (single_eq_single_iff _ _ _ _).mp h
 
@@ -927,12 +931,15 @@ end misc_theorems
 
 section span
 
-variables [semiring k] [add_zero_class G]
+variables [semiring k]
+
+lemma mem_span_support [add_zero_class G] (f : add_monoid_algebra k G) :
+  f ∈ submodule.span k (of k G '' (f.support : set G)) :=
+by rw [of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single, finsupp.mem_supported]
 
-lemma mem_span_support (f : add_monoid_algebra k G) :
-  f ∈ submodule.span k (add_monoid_algebra.of k G '' (f.support : set G)) :=
-by rw [add_monoid_algebra.of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single,
-  finsupp.mem_supported]
+lemma mem_span_support' (f : add_monoid_algebra k G) :
+  f ∈ submodule.span k (of' k G '' (f.support : set G)) :=
+by rw [of', ← finsupp.supported_eq_span_single, finsupp.mem_supported]
 
 end span
 

src/ring_theory/finiteness.lean

@@ -567,13 +567,51 @@ section monoid_algebra
 
 namespace add_monoid_algebra
 
-open algebra add_submonoid
+open algebra add_submonoid submodule
+
+section span
+
+variables {R : Type*} {M : Type*} [comm_semiring R] [add_monoid M]
+
+lemma mem_adjoint_support (f : add_monoid_algebra R M) :
+  f ∈ adjoin R (of' R M '' (f.support : set M)) :=
+begin
+  suffices : span R (of R M '' (f.support : set M)) ≤
+    (adjoin R (of R M '' (f.support : set M))).to_submodule,
+  { exact this (mem_span_support f) },
+  rw submodule.span_le,
+  exact subset_adjoin
+end
+
+lemma support_gen_of_gen {S : set (add_monoid_algebra R M)} (hS : algebra.adjoin R S = ⊤) :
+  algebra.adjoin R (⋃ f ∈ S, (of' R M '' (f.support : set M))) = ⊤ :=
+begin
+  refine le_antisymm le_top _,
+  rw [← hS, adjoin_le_iff],
+  intros f hf,
+  have hincl : of' R M '' (f.support : set M) ⊆
+    ⋃ (g : add_monoid_algebra R M) (H : g ∈ S), of' R M '' (g.support : set M),
+  { intros s hs,
+    exact set.mem_bUnion_iff.2 ⟨f, ⟨hf, hs⟩⟩ },
+  exact adjoin_mono hincl (mem_adjoint_support f)
+end
+
+lemma support_gen_of_gen' {S : set (add_monoid_algebra R M)} (hS : algebra.adjoin R S = ⊤) :
+  algebra.adjoin R (of' R M '' (⋃ f ∈ S, (f.support : set M))) = ⊤ :=
+begin
+  suffices : of' R M '' (⋃ f ∈ S, (f.support : set M)) = ⋃ f ∈ S, (of' R M '' (f.support : set M)),
+  { rw this,
+    exact support_gen_of_gen hS },
+  simp only [set.image_Union]
+end
+
+end span
 
 variables {R : Type*} {M : Type*} [add_comm_monoid M]
 
 lemma mv_polynomial_aeval_of_surjective_of_closure [comm_semiring R] {S : set M}
   (hS : closure S = ⊤) : function.surjective (mv_polynomial.aeval
-  (λ (s : S), of R M (multiplicative.of_add ↑s)) : mv_polynomial S R → add_monoid_algebra R M) :=
+  (λ (s : S), of' R M ↑s) : mv_polynomial S R → add_monoid_algebra R M) :=
 begin
   refine λ f, induction_on f (λ m, _) _ _,
   { have : m ∈ closure S := hS.symm ▸ mem_top _,
@@ -593,14 +631,52 @@ instance ft_of_fg [comm_ring R] [h : add_monoid.fg M] : finite_type R (add_monoi
 begin
   obtain ⟨S, hS⟩ := h.out,
   exact (finite_type.mv_polynomial R (S : set M)).of_surjective (mv_polynomial.aeval
-    (λ (s : (S : set M)), of R M s.1)) (mv_polynomial_aeval_of_surjective_of_closure hS)
+    (λ (s : (S : set M)), of' R M ↑s)) (mv_polynomial_aeval_of_surjective_of_closure hS)
 end
 
 end add_monoid_algebra
 
 namespace monoid_algebra
 
-open algebra submonoid
+open algebra submonoid submodule
+
+section span
+
+variables {R : Type*} {M : Type*} [comm_semiring R] [monoid M]
+
+lemma mem_adjoint_support (f : monoid_algebra R M) :
+  f ∈ adjoin R (monoid_algebra.of R M '' (f.support : set M)) :=
+begin
+  suffices : span R (of R M '' (f.support : set M)) ≤
+    (adjoin R (of R M '' (f.support : set M))).to_submodule,
+  { exact this (mem_span_support f) },
+  rw submodule.span_le,
+  exact subset_adjoin
+end
+
+lemma support_gen_of_gen {S : set (monoid_algebra R M)} (hS : algebra.adjoin R S = ⊤) :
+  algebra.adjoin R (⋃ f ∈ S, ((of R M) '' (f.support : set M))) = ⊤ :=
+begin
+  refine le_antisymm le_top _,
+  rw [← hS, adjoin_le_iff],
+  intros f hf,
+  have hincl : (of R M) '' (f.support : set M) ⊆
+    ⋃ (g : monoid_algebra R M) (H : g ∈ S), of R M '' (g.support : set M),
+  { intros s hs,
+    exact set.mem_bUnion_iff.2 ⟨f, ⟨hf, hs⟩⟩ },
+  exact adjoin_mono hincl (mem_adjoint_support f)
+end
+
+lemma support_gen_of_gen' {S : set (monoid_algebra R M)} (hS : algebra.adjoin R S = ⊤) :
+  algebra.adjoin R (of R M '' (⋃ f ∈ S, (f.support : set M))) = ⊤ :=
+begin
+  suffices : of R M '' (⋃ f ∈ S, (f.support : set M)) = ⋃ f ∈ S, (of R M '' (f.support : set M)),
+  { rw this,
+    exact support_gen_of_gen hS },
+  simp only [set.image_Union]
+end
+
+end span
 
 variables {R : Type*} {M : Type*} [comm_monoid M]
 
@@ -623,7 +699,7 @@ begin
 end
 
 instance ft_of_fg [comm_ring R] [monoid.fg M] : finite_type R (monoid_algebra R M) :=
-add_monoid_algebra.ft_of_fg.equiv (monoid_algebra.to_additive_alg_equiv R M).symm
+add_monoid_algebra.ft_of_fg.equiv (to_additive_alg_equiv R M).symm
 
 end monoid_algebra