feat(ring_theory/finiteness): add monoid_algebra.ft_iff_fg (#7445)

We prove here `add monoid_algebra.ft_iff_fg`: the monoid algebra is of finite type if and only if the monoid is finitely generated.

- [x] depends on: #7409

Author: riccardobrasca

src/algebra/monoid_algebra.lean

@@ -615,6 +615,7 @@ section span
 
 variables [semiring k] [mul_one_class G]
 
+/-- An element of `monoid_algebra R M` is in the subalgebra generated by its support. -/
 lemma mem_span_support (f : 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]
@@ -888,6 +889,8 @@ rfl
 
 @[simp] lemma of'_apply (a : G) : of' k G a = single a 1 := rfl
 
+lemma of'_eq_of [add_zero_class G] (a : G) : of' k G a = of k G a := 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
 
@@ -933,10 +936,13 @@ section span
 
 variables [semiring k]
 
+/-- An element of `add_monoid_algebra R M` is in the submodule generated by its support. -/
 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]
 
+/-- An element of `add_monoid_algebra R M` is in the subalgebra generated by its support, using
+unbundled inclusion. -/
 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]

src/ring_theory/finiteness.lean

@@ -565,37 +565,44 @@ end alg_hom
 
 section monoid_algebra
 
+variables {R : Type*} {M : Type*}
+
 namespace add_monoid_algebra
 
 open algebra add_submonoid submodule
 
 section span
 
-variables {R : Type*} {M : Type*} [comm_semiring R] [add_monoid M]
+section semiring
+
+variables [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)) :=
+/-- An element of `add_monoid_algebra R M` is in the subalgebra generated by its support. -/
+lemma mem_adjoin_support (f : add_monoid_algebra R M) : f ∈ adjoin R (of' R M '' f.support) :=
 begin
-  suffices : span R (of R M '' (f.support : set M)) ≤
-    (adjoin R (of R M '' (f.support : set M))).to_submodule,
+  suffices : span R (of' R M '' f.support) ≤ (adjoin R (of' R M '' f.support)).to_submodule,
   { exact this (mem_span_support f) },
   rw submodule.span_le,
   exact subset_adjoin
 end
 
+/-- If a set `S` generates, as algebra, `add_monoid_algebra R M`, then the set of supports of
+elements of `S` generates `add_monoid_algebra R M`. -/
 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),
+  have hincl : of' R M '' f.support ⊆
+    ⋃ (g : add_monoid_algebra R M) (H : g ∈ S), of' R M '' g.support,
   { intros s hs,
     exact set.mem_bUnion_iff.2 ⟨f, ⟨hf, hs⟩⟩ },
-  exact adjoin_mono hincl (mem_adjoint_support f)
+  exact adjoin_mono hincl (mem_adjoin_support f)
 end
 
+/-- If a set `S` generates, as algebra, `add_monoid_algebra R M`, then the image of the union of
+the supports of elements of `S` generates `add_monoid_algebra R M`. -/
 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
@@ -605,10 +612,58 @@ begin
   simp only [set.image_Union]
 end
 
+end semiring
+
+section ring
+
+variables [comm_ring R] [add_comm_monoid M]
+
+/-- If `add_monoid_algebra R M` is of finite type, there there is a `G : finset M` such that its
+image generates, as algera, `add_monoid_algebra R M`. -/
+lemma exists_finset_adjoin_eq_top [h : finite_type R (add_monoid_algebra R M)] :
+  ∃ G : finset M, algebra.adjoin R (of' R M '' G) = ⊤ :=
+begin
+  unfreezingI { obtain ⟨S, hS⟩ := h },
+  letI : decidable_eq M := classical.dec_eq M,
+  use finset.bUnion S (λ f, f.support),
+  have : (finset.bUnion S (λ f, f.support) : set M) = ⋃ f ∈ S, (f.support : set M),
+  { simp only [finset.set_bUnion_coe, finset.coe_bUnion] },
+  rw [this],
+  exact support_gen_of_gen' hS
+end
+
+/-- The image of an element `m : M` in `add_monoid_algebra R M` belongs the submodule generated by
+`S : set M` if and only if `m ∈ S`. -/
+lemma of'_mem_span [nontrivial R] {m : M} {S : set M} :
+  of' R M m ∈ span R (of' R M '' S) ↔ m ∈ S :=
+begin
+  refine ⟨λ h, _, λ h, submodule.subset_span $ set.mem_image_of_mem (of R M) h⟩,
+  rw [of', ← finsupp.supported_eq_span_single, finsupp.mem_supported,
+    finsupp.support_single_ne_zero (@one_ne_zero R _ (by apply_instance))] at h,
+  simpa using h
+end
+
+/--If the image of an element `m : M` in `add_monoid_algebra R M` belongs the submodule generated by
+the closure of some `S : set M` then `m ∈ closure S`. -/
+lemma mem_closure_of_mem_span_closure [nontrivial R] {m : M} {S : set M}
+  (h : of' R M m ∈ span R (submonoid.closure (of' R M '' S) : set (add_monoid_algebra R M))) :
+  m ∈ closure S :=
+begin
+  suffices : multiplicative.of_add m ∈ submonoid.closure (multiplicative.to_add ⁻¹' S),
+  { simpa [← to_submonoid_closure] },
+  rw [set.image_congr' (show ∀ x, of' R M x = of R M x, from λ x, of'_eq_of x),
+    ← monoid_hom.map_mclosure] at h,
+  simpa using of'_mem_span.1 h
+end
+
+end ring
+
 end span
 
-variables {R : Type*} {M : Type*} [add_comm_monoid M]
+variables [add_comm_monoid M]
 
+/-- If a set `S` generates an additive monoid `M`, then the image of `M` generates, as algebra,
+`add_monoid_algebra R 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 → add_monoid_algebra R M) :=
@@ -627,13 +682,35 @@ begin
     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) :=
+/-- If an additive monoid `M` is finitely generated then `add_monoid_algebra R M` is of finite
+type. -/
+instance finite_type_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)) (mv_polynomial_aeval_of_surjective_of_closure hS)
 end
 
+/-- An additive monoid `M` is finitely generated if and only if `add_monoid_algebra R M` is of
+finite type. -/
+lemma finite_type_iff_fg [comm_ring R] [nontrivial R] :
+  add_monoid.fg M ↔ finite_type R (add_monoid_algebra R M) :=
+begin
+  refine ⟨λ h, @add_monoid_algebra.finite_type_of_fg _ _ _ _ h, λ h, _⟩,
+  obtain ⟨S, hS⟩ := @exists_finset_adjoin_eq_top R M _ _ h,
+  refine add_monoid.fg_def.2 ⟨S, (eq_top_iff' _).2 (λ m, _)⟩,
+  have hm : of' R M m ∈ (adjoin R (of' R M '' ↑S)).to_submodule,
+  { simp only [hS, top_to_submodule, submodule.mem_top], },
+  rw [adjoin_eq_span] at hm,
+  exact mem_closure_of_mem_span_closure hm
+end
+
+/-- If `add_monoid_algebra R M` is of finite type then `M` is finitely generated. -/
+lemma fg_of_finite_type [comm_ring R] [nontrivial R] [h : finite_type R (add_monoid_algebra R M)] :
+  add_monoid.fg M :=
+finite_type_iff_fg.2 h
+
 end add_monoid_algebra
 
 namespace monoid_algebra
@@ -642,31 +719,36 @@ open algebra submonoid submodule
 
 section span
 
-variables {R : Type*} {M : Type*} [comm_semiring R] [monoid M]
+section semiring
+
+variables [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)) :=
+/-- An element of `monoid_algebra R M` is in the subalgebra generated by its support. -/
+lemma mem_adjoint_support (f : monoid_algebra R M) : f ∈ adjoin R (of R M '' f.support) :=
 begin
-  suffices : span R (of R M '' (f.support : set M)) ≤
-    (adjoin R (of R M '' (f.support : set M))).to_submodule,
+  suffices : span R (of R M '' f.support) ≤ (adjoin R (of R M '' f.support)).to_submodule,
   { exact this (mem_span_support f) },
   rw submodule.span_le,
   exact subset_adjoin
 end
 
+/-- If a set `S` generates, as algebra, `monoid_algebra R M`, then the set of supports of elements
+of `S` generates `monoid_algebra R M`. -/
 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))) = ⊤ :=
+  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),
+  have hincl : (of R M) '' f.support ⊆
+    ⋃ (g : monoid_algebra R M) (H : g ∈ S), of R M '' g.support,
   { intros s hs,
     exact set.mem_bUnion_iff.2 ⟨f, ⟨hf, hs⟩⟩ },
   exact adjoin_mono hincl (mem_adjoint_support f)
 end
 
+/-- If a set `S` generates, as algebra, `monoid_algebra R M`, then the image of the union of the
+supports of elements of `S` generates `monoid_algebra R M`. -/
 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
@@ -676,10 +758,55 @@ begin
   simp only [set.image_Union]
 end
 
+end semiring
+
+section ring
+
+variables [comm_ring R] [comm_monoid M]
+
+/-- If `monoid_algebra R M` is of finite type, there there is a `G : finset M` such that its image
+generates, as algera, `monoid_algebra R M`. -/
+lemma exists_finset_adjoin_eq_top [h :finite_type R (monoid_algebra R M)] :
+  ∃ G : finset M, algebra.adjoin R (of R M '' G) = ⊤ :=
+begin
+  unfreezingI { obtain ⟨S, hS⟩ := h },
+  letI : decidable_eq M := classical.dec_eq M,
+  use finset.bUnion S (λ f, f.support),
+  have : (finset.bUnion S (λ f, f.support) : set M) = ⋃ f ∈ S, (f.support : set M),
+  { simp only [finset.set_bUnion_coe, finset.coe_bUnion] },
+  rw [this],
+  exact support_gen_of_gen' hS
+end
+
+/-- The image of an element `m : M` in `monoid_algebra R M` belongs the submodule generated by
+`S : set M` if and only if `m ∈ S`. -/
+lemma of_mem_span_of_iff [nontrivial R] {m : M} {S : set M} :
+  of R M m ∈ span R (of R M '' S) ↔ m ∈ S :=
+begin
+  refine ⟨λ h, _, λ h, submodule.subset_span $ set.mem_image_of_mem (of R M) h⟩,
+  rw [of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single, finsupp.mem_supported,
+    finsupp.support_single_ne_zero (@one_ne_zero R _ (by apply_instance))] at h,
+  simpa using h
+end
+
+/--If the image of an element `m : M` in `monoid_algebra R M` belongs the submodule generated by the
+closure of some `S : set M` then `m ∈ closure S`. -/
+lemma mem_closure_of_mem_span_closure [nontrivial R] {m : M} {S : set M}
+  (h : of R M m ∈ span R (submonoid.closure (of R M '' S) : set (monoid_algebra R M))) :
+  m ∈ closure S :=
+begin
+  rw ← monoid_hom.map_mclosure at h,
+  simpa using of_mem_span_of_iff.1 h
+end
+
+end ring
+
 end span
 
-variables {R : Type*} {M : Type*} [comm_monoid M]
+variables [comm_monoid M]
 
+/-- If a set `S` generates a monoid `M`, then the image of `M` generates, as algebra,
+`monoid_algebra R 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) :=
@@ -698,8 +825,20 @@ begin
     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 (to_additive_alg_equiv R M).symm
+/-- If a monoid `M` is finitely generated then `monoid_algebra R M` is of finite type. -/
+instance finite_type_of_fg [comm_ring R] [monoid.fg M] : finite_type R (monoid_algebra R M) :=
+add_monoid_algebra.finite_type_of_fg.equiv (to_additive_alg_equiv R M).symm
+
+/-- A monoid `M` is finitely generated if and only if `monoid_algebra R M` is of finite type. -/
+lemma finite_type_iff_fg [comm_ring R] [nontrivial R] :
+  monoid.fg M ↔ finite_type R (monoid_algebra R M) :=
+⟨λ h, @monoid_algebra.finite_type_of_fg _ _ _ _ h, λ h, monoid.fg_iff_add_fg.2 $
+  add_monoid_algebra.finite_type_iff_fg.2 $ h.equiv $ to_additive_alg_equiv R M⟩
+
+/-- If `monoid_algebra R M` is of finite type then `M` is finitely generated. -/
+lemma fg_of_finite_type [comm_ring R] [nontrivial R] [h : finite_type R (monoid_algebra R M)] :
+  monoid.fg M :=
+finite_type_iff_fg.2 h
 
 end monoid_algebra