flatness of MvPowerSeries

Stream: PR reviews

[Bingyu Xia]

Hi everyone, I've been working on connecting multivariate power series with the completion of polynomials. I have a work-in-progress that constructs the isomorphism between MvPowerSeries σ R and the adic-completion of MvPolynomial σ R with respect to the ideal generated by all variables (assuming [Fintype σ]). The construction uses a truncTotal map (truncation by total degree). As a corollary, MvPowerSeries σ R is a flat MvPolynomial σ R-module when R is noetherian.

I've opened a preliminary PR #33539 which proves some necessary helper lemmas about powers of the ideal generated by all variables. The main ismorphism PR will follow later. Any feedback or suggestions would be greatly appreciated, thanks!

[Violeta Hernández]

Just left a small review with a suggestion.

[Bingyu Xia]

I generalized the arguments in pow_idealOfVars_eq_span to the following lemma, which is useful for MvPowerSeries and other contexts

variable {α β : Type*}

open Pointwise Finsupp in
lemma Set.image_pow_eq_image_finsupp_prod [CommMonoid β] {f : α → β} {n} {s : Set α} :
    (f '' s) ^ n = (fun a : α →₀ ℕ => a.prod fun n e => f n ^ e) ''
      {x | x.sum (fun _ => id) = n ∧ ↑x.support ⊆ s} := by
  classical
  ext p
  simp only [mem_pow_iff_prod, mem_image, mem_setOf_eq]
  refine ⟨fun ⟨g, h, hg⟩ => ?_, fun ⟨x, ⟨x_sum, x_supp⟩, hx⟩ => ?_⟩
  · choose i i_in hi using h
    use ∑ j, single (i j) 1; split_ands
    · simp [← sum_finset_sum_index]
    · simpa [Set.subset_def, single_apply]
    rw [← prod_finset_sum_index (by simp) (by simp [pow_add]), ← hg]
    simp [← hi]
  let l := x.toMultiset.toList
  have hl : n = l.length := by
    rw [Multiset.length_toList, card_toMultiset, x_sum]
  use fun i => f (l.get (Fin.cast hl i))
  simp only [List.get_eq_getElem, Fin.val_cast]
  refine ⟨fun _ ↦ ⟨_, x_supp ?_, rfl⟩, ?_⟩
  · rw [Finset.mem_coe, ← mem_toMultiset, ← Multiset.mem_toList]
    exact List.getElem_mem ..
  rw [← Fintype.prod_equiv (finCongr (Eq.symm hl)) (fun i ↦ f l[i]) _ (by simp)]
  simp only [Fin.getElem_fin, Fin.prod_univ_fun_getElem, Multiset.prod_map_toList, toMultiset_map,
    prod_toMultiset, l]
  rw [← hx, prod_mapDomain_index (by simp) (by simp [pow_add])]

Where would be the appropriate home for this? I suspect Set/Basic.lean might be too low in the hierarchy if it involves Finsupp. Any suggestions?

[Violeta Hernández]

What does #find_home say?

[Bingyu Xia]

#find_home only pointed to my local file. I also tried running #min_imports, it suggested me to find where the following three files are imported: Mathlib.Algebra.BigOperators.Fin
Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Mathlib.Data.Finsupp.Multiset

[Damiano Testa]

Does #find_home! report something more reasonable?

[Bingyu Xia]

I tried #find_home! and got a long list. The results don't seem to be the right place since my lemma is about powers of Set and products of Finsupp
screenshot-1768088756858.png

[Ruben Van de Velde]

Probably a new file then

[Bingyu Xia]

I updated what is done so far in PR #33539:

• Added a new file Mathlib/Algebra/Group/Pointwise/Set/Finsupp.lean for results about pointwise operations on sets and finitely supported functions
• Provided more APIs on MvPolynomial.restrictSupport and defined restrictSupportIdeal for the ideal determined by restrictSupport R s when s is an upper set
• Defined MvPolynomial.idealOfVars to be the ideal spanned by all variables in MvPolynomial and provided results about its powers
• Provided some helper results while golfing

There are still two helper results from the reviewer's suggestion left to be added, as I'm still unsure where to put them (I couldn't find a suitable home). I've included the two results and #find_home output below for reference.

open Pointwise

@[simp]
lemma Multiplicative.ofAdd_image_setAdd {M : Type*} [AddMonoid M] (s t : Set M) :
    Multiplicative.ofAdd '' (s + t) = Multiplicative.ofAdd '' s * Multiplicative.ofAdd '' t := by
  rw [← Set.image2_add, Set.image_image2_distrib ofAdd_add, Set.image2_mul]

@[simp]
lemma Multiplicative.ofAdd_image_nsmul {M : Type*} [AddMonoid M] (n : ℕ) (s : Set M) :
    Multiplicative.ofAdd '' (n • s) = (Multiplicative.ofAdd '' s) ^ n := by
  induction n with
  | zero => simp; rfl
  | succ n IH => simp [succ_nsmul, pow_succ, IH]

screenshot-1768347515189.png

[Violeta Hernández]

Is there an Algebra.Monoid.Pointwise file? If not then Algebra.Group.Pointwise probably works.

[Bingyu Xia]

Violeta Hernández 发言道：

Is there an Algebra.Monoid.Pointwise file? If not then Algebra.Group.Pointwise probably works.

How about adding a new file like Algebra/Group/TypeTags/Pointwise.lean since Multiplicative.toAdd is defined there?

[Violeta Hernández]

That works, I guess.

[Bingyu Xia]

Thanks for the review of the previous PR! The next PR is #35118, which resolves the TODO in MvPowerSeries/Trunc.lean by implementing a general truncation map truncFinset. This paves the way for unifying strict and non-strict truncations and defining other truncations.