feat(ring_theory/hahn_series): add a map to power series and dickson'…

…s lemma (#11836)

Add a ring equivalence between `hahn_series` and `mv_power_series` as discussed in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/induction.20on.20an.20index.20type/near/269463528.
This required adding some partially well ordered lemmas that it seems go under the name Dickson's lemma.
This may be independently useful, a constructive version of this has been used in other provers, especially in connection to Grobner basis and commutative algebra type material.

src/data/finsupp/pwo.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2022 Alex J. Best. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex J. Best
+-/
+import data.finsupp.order
+import order.well_founded_set
+
+
+/-!
+# Partial well ordering on finsupps
+
+This file contains the fact that finitely supported functions from a fintype are
+partially well ordered when the codomain is a linear order that is well ordered.
+It is in a separate file for now so as to not add imports to the file `order.well_founded_set`.
+
+## Main statements
+
+* `finsupp.is_pwo` - finitely supported functions from a fintype are partially well ordered when
+  the codomain is a linear order that is well ordered
+
+## Tags
+
+Dickson, order, partial well order
+-/
+
+
+/-- A version of **Dickson's lemma** any subset of functions `σ →₀ α` is partially well
+ordered, when `σ` is a `fintype` and `α` is a linear well order.
+This version uses finsupps on a fintype as it is intended for use with `mv_power_series`.
+-/
+lemma finsupp.is_pwo {α σ : Type*} [has_zero α] [linear_order α] [is_well_order α (<)] [fintype σ]
+  (S : set (σ →₀ α)) : S.is_pwo :=
+begin
+  rw ← finsupp.equiv_fun_on_fintype.symm.image_preimage S,
+  refine set.partially_well_ordered_on.image_of_monotone_on (pi.is_pwo _) (λ a b ha hb, id),
+end

src/order/well_founded_set.lean

@@ -190,6 +190,11 @@ theorem partially_well_ordered_on.mono {s t : set α} {r : α → α → Prop}
   s.partially_well_ordered_on r :=
 λ f hf, ht f (set.subset.trans hf hsub)
 
+theorem is_pwo.mono [preorder α] {s t : set α}
+  (ht : t.is_pwo) (hsub : s ⊆ t) :
+  s.is_pwo :=
+partially_well_ordered_on.mono ht hsub
+
 theorem partially_well_ordered_on.image_of_monotone_on {s : set α}
   {r : α → α → Prop} {β : Type*} {r' : β → β → Prop}
   (hs : s.partially_well_ordered_on r) {f : α → β}
@@ -894,3 +899,31 @@ end finset
 lemma well_founded.is_wf [has_lt α] (h : well_founded ((<) : α → α → Prop)) (s : set α) :
   s.is_wf :=
 (set.is_wf_univ_iff.2 h).mono (set.subset_univ s)
+
+/-- A version of **Dickson's lemma** any subset of functions `Π s : σ, α s` is partially well
+ordered, when `σ` is a `fintype` and each `α s` is a linear well order.
+This includes the classical case of Dickson's lemma that `ℕ ^ n` is a well partial order.
+Some generalizations would be possible based on this proof, to include cases where the target
+is partially well ordered, and also to consider the case of `partially_well_ordered_on` instead of
+`is_pwo`. -/
+lemma pi.is_pwo {σ : Type*} {α : σ → Type*} [∀ s, linear_order (α s)] [∀ s, is_well_order (α s) (<)]
+  [fintype σ] (S : set (Π s : σ, α s)) : S.is_pwo :=
+begin
+  classical,
+  refine set.is_pwo.mono _ (set.subset_univ _),
+  rw set.is_pwo_iff_exists_monotone_subseq,
+  simp_rw [monotone, pi.le_def],
+  suffices : ∀ s : finset σ, ∀ (f : ℕ → (Π s, α s)), set.range f ⊆ set.univ → ∃ (g : ℕ ↪o ℕ),
+    ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : σ) (hs : x ∈ s), (f ∘ g) a x ≤ (f ∘ g) b x,
+  { simpa only [forall_true_left, finset.mem_univ] using this finset.univ, },
+  apply' finset.induction,
+  { intros f hf, existsi rel_embedding.refl (≤),
+    simp only [forall_false_left, implies_true_iff, forall_const, finset.not_mem_empty], },
+  { intros x s hx ih f hf,
+    obtain ⟨g, hg⟩ := (is_well_order.wf.is_wf (set.univ : set _)).is_pwo.exists_monotone_subseq
+      ((λ mo : Π s : σ, α s, mo x) ∘ f) (set.subset_univ _),
+    obtain ⟨g', hg'⟩ := ih (f ∘ g) (set.subset_univ _),
+    refine ⟨g'.trans g, λ a b hab, _⟩,
+    simp only [finset.mem_insert, rel_embedding.coe_trans, function.comp_app, forall_eq_or_imp],
+    exact ⟨hg (order_hom_class.mono g' hab), hg' hab⟩, },
+end

src/ring_theory/hahn_series.lean

@@ -8,6 +8,7 @@ import algebra.big_operators.finprod
 import ring_theory.valuation.basic
 import algebra.module.pi
 import ring_theory.power_series.basic
+import data.finsupp.pwo
 
 /-!
 # Hahn Series
@@ -1073,6 +1074,44 @@ begin
   rw [pow_succ, ih, of_power_series_X, mul_comm, single_mul_single, one_mul, nat.cast_succ]
 end
 
+-- Lemmas about converting hahn_series over fintype to and from mv_power_series
+
+/-- The ring `hahn_series (σ →₀ ℕ) R` is isomorphic to `mv_power_series σ R` for a `fintype` `σ`.
+We take the index set of the hahn series to be `finsupp` rather than `pi`,
+even though we assume `fintype σ` as this is more natural for alignment with `mv_power_series`.
+After importing `algebra.order.pi` the ring `hahn_series (σ → ℕ) R` could be constructed instead.
+ -/
+@[simps] def to_mv_power_series {σ : Type*} [fintype σ] :
+  hahn_series (σ →₀ ℕ) R ≃+* mv_power_series σ R :=
+{ to_fun := λ f, f.coeff,
+  inv_fun := λ f, ⟨(f : (σ →₀ ℕ) → R), finsupp.is_pwo _⟩,
+  left_inv := λ f, by { ext, simp },
+  right_inv := λ f, by { ext, simp },
+  map_add' := λ f g, by { ext, simp },
+  map_mul' := λ f g, begin
+    ext n,
+    simp only [mv_power_series.coeff_mul],
+    classical,
+    change (f * g).coeff n = _,
+    simp_rw [mul_coeff],
+    refine sum_filter_ne_zero.symm.trans ((sum_congr _ (λ _ _, rfl)).trans sum_filter_ne_zero),
+    ext m,
+    simp only [and.congr_left_iff, mem_add_antidiagonal, ne.def, and_iff_left_iff_imp, mem_filter,
+      mem_support, finsupp.mem_antidiagonal],
+    intros h1 h2,
+    contrapose h1,
+    rw ← decidable.or_iff_not_and_not at h1,
+    cases h1; simp [h1],
+  end }
+
+variables {σ : Type*} [fintype σ]
+lemma coeff_to_mv_power_series {f : hahn_series (σ →₀ ℕ) R} {n : σ →₀ ℕ} :
+  mv_power_series.coeff R n f.to_mv_power_series = f.coeff n :=
+rfl
+
+lemma coeff_to_mv_power_series_symm {f : mv_power_series σ R} {n : σ →₀ ℕ} :
+  (hahn_series.to_mv_power_series.symm f).coeff n = mv_power_series.coeff R n f := rfl
+
 end semiring
 
 section algebra