feat(ring_theory/finiteness): add add_monoid_algebra.ft_of_fg (#7265)

This is from `lean_liquid`. We prove `add_monoid_algebra.ft_of_fg`: if `M` is a finitely generated monoid then `add_monoid_algebra R M` if finitely generated as `R-alg`.

The converse is also true, but the proof is longer and I wanted to keep the PR small.

- [x] depends on: #7279

Author: riccardobrasca

src/algebra/module/submodule.lean

@@ -48,6 +48,9 @@ variables [semiring R] [add_comm_monoid M] [module R M]
 instance : set_like (submodule R M) M :=
 ⟨submodule.carrier, λ p q h, by cases p; cases q; congr'⟩
 
+@[simp] theorem mem_to_add_submonoid (p : submodule R M) (x : M) : x ∈ p.to_add_submonoid ↔ x ∈ p :=
+iff.rfl
+
 variables {p q : submodule R M}
 
 @[simp] lemma mk_coe (S : set M) (h₁ h₂ h₃) :

src/algebra/monoid_algebra.lean

@@ -434,6 +434,16 @@ lemma single_algebra_map_eq_algebra_map_mul_of {A : Type*} [comm_semiring k] [se
   single a (algebra_map k A b) = algebra_map k (monoid_algebra A G) b * of A G a :=
 by simp
 
+lemma induction_on [semiring k] [monoid G] {p : monoid_algebra k G → Prop} (f : monoid_algebra k G)
+  (hM : ∀ g, p (of k G g)) (hadd : ∀ f g : monoid_algebra k G, p f → p g → p (f + g))
+  (hsmul : ∀ (r : k) f, p f → p (r • f)) : p f :=
+begin
+  refine finsupp.induction_linear f _ (λ f g hf hg, hadd f g hf hg) (λ g r, _),
+  { simpa using hsmul 0 (of k G 1) (hM 1) },
+  { convert hsmul r (of k G g) (hM g),
+    simp only [mul_one, smul_single', of_apply] },
+end
+
 end algebra
 
 section lift
@@ -592,7 +602,6 @@ calc (f * g) x = sum f (λ a b, (single a b * g) x) :
   by rw [← finsupp.sum_apply, ← finsupp.sum_mul, f.sum_single]
 ... = _ : by simp only [single_mul_apply, finsupp.sum]
 
-
 -- If we'd assumed `comm_semiring`, we could deduce this from `mul_apply_left`.
 lemma mul_apply_right (f g : monoid_algebra k G) (x : G) :
   (f * g) x = (g.sum $ λa b, (f (x * a⁻¹)) * b) :=
@@ -901,6 +910,19 @@ lemma lift_nc_smul {R : Type*} [add_zero_class G] [semiring R] (f : k →+* R)
   lift_nc (f : k →+ R) g (c • φ) = f c * lift_nc (f : k →+ R) g φ :=
 @monoid_algebra.lift_nc_smul k (multiplicative G) _ _ _ _ f g c φ
 
+variables {k G}
+
+lemma induction_on [add_monoid G] {p : add_monoid_algebra k G → Prop} (f : add_monoid_algebra k G)
+  (hM : ∀ g, p (of k G (multiplicative.of_add g)))
+  (hadd : ∀ f g : add_monoid_algebra k G, p f → p g → p (f + g))
+  (hsmul : ∀ (r : k) f, p f → p (r • f)) : p f :=
+begin
+  refine finsupp.induction_linear f _ (λ f g hf hg, hadd f g hf hg) (λ g r, _),
+  { simpa using hsmul 0 (of k G (multiplicative.of_add 0)) (hM 0) },
+  { convert hsmul r (of k G (multiplicative.of_add g)) (hM g),
+    simp only [mul_one, to_add_of_add, smul_single', of_apply] },
+end
+
 end misc_theorems
 
 section span
@@ -1089,3 +1111,19 @@ finset.induction_on s rfl $ λ a s has ih, by rw [prod_insert has, ih,
 end
 
 end add_monoid_algebra
+
+variables {R : Type*} [comm_semiring R] (k G)
+
+/-- The algebra equivalence between `add_monoid_algebra` and `monoid_algebra` in terms of
+`multiplicative`. -/
+def add_monoid_algebra.to_multiplicative_alg_equiv [semiring k] [algebra R k] [add_monoid G] :
+  add_monoid_algebra k G ≃ₐ[R] monoid_algebra k (multiplicative G) :=
+{ commutes' := λ r, by simp [add_monoid_algebra.to_multiplicative],
+  ..add_monoid_algebra.to_multiplicative k G }
+
+/-- The algebra equivalence between `monoid_algebra` and `add_monoid_algebra` in terms of
+`additive`. -/
+def monoid_algebra.to_additive_alg_equiv [semiring k] [algebra R k] [monoid G] :
+  monoid_algebra k G ≃ₐ[R] add_monoid_algebra k (additive G) :=
+{ commutes' := λ r, by simp [monoid_algebra.to_additive],
+  ..monoid_algebra.to_additive k G }

src/ring_theory/finiteness.lean

@@ -7,6 +7,7 @@ Authors: Johan Commelin
 import ring_theory.noetherian
 import ring_theory.ideal.operations
 import ring_theory.algebra_tower
+import group_theory.finiteness
 
 /-!
 # Finiteness conditions in commutative algebra
@@ -558,3 +559,69 @@ ring_hom.finite_presentation.of_finite_type
 end finite_presentation
 
 end alg_hom
+
+section monoid_algebra
+
+namespace add_monoid_algebra
+
+open algebra add_submonoid
+
+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) :=
+begin
+  refine λ f, induction_on f (λ m, _) _ _,
+  { have : m ∈ closure S := hS.symm ▸ mem_top _,
+    refine closure_induction this (λ m hm, _) _ _,
+    { exact ⟨mv_polynomial.X ⟨m, hm⟩, mv_polynomial.aeval_X _ _⟩ },
+    { exact ⟨1, alg_hom.map_one _⟩ },
+    { rintro m₁ m₂ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩,
+      exact ⟨P₁ * P₂, by rw [alg_hom.map_mul, hP₁, hP₂, of_apply, of_apply, of_apply,
+        single_mul_single, one_mul]; refl⟩ } },
+  { rintro f g ⟨P, rfl⟩ ⟨Q, rfl⟩,
+    exact ⟨P + Q, alg_hom.map_add _ _ _⟩ },
+  { rintro r f ⟨P, rfl⟩,
+    exact ⟨r • P, alg_hom.map_smul _ _ _⟩ }
+end
+
+instance ft_of_fg [comm_ring R] [h : add_monoid.fg M] : finite_type R (add_monoid_algebra R M) :=
+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)
+end
+
+end add_monoid_algebra
+
+namespace monoid_algebra
+
+open algebra submonoid
+
+variables {R : Type*} {M : Type*} [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 ↑s) : mv_polynomial S R → monoid_algebra R M) :=
+begin
+  refine λ f, induction_on f (λ m, _) _ _,
+  { have : m ∈ closure S := hS.symm ▸ mem_top _,
+    refine closure_induction this (λ m hm, _) _ _,
+    { exact ⟨mv_polynomial.X ⟨m, hm⟩, mv_polynomial.aeval_X _ _⟩ },
+    { exact ⟨1, alg_hom.map_one _⟩ },
+    { rintro m₁ m₂ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩,
+      exact ⟨P₁ * P₂, by rw [alg_hom.map_mul, hP₁, hP₂, of_apply, of_apply, of_apply,
+        single_mul_single, one_mul]⟩ } },
+  { rintro f g ⟨P, rfl⟩ ⟨Q, rfl⟩,
+    exact ⟨P + Q, alg_hom.map_add _ _ _⟩ },
+  { rintro r f ⟨P, rfl⟩,
+    exact ⟨r • P, alg_hom.map_smul _ _ _⟩ }
+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
+
+end monoid_algebra
+
+end monoid_algebra