induction on an index type

Stream: Is there code for X?

[Yakov Pechersky]

I am trying to show [is_domain (mv_power_series I R)], generalizing from [is_domain (power_series R)]. I am hoping to "induct" on the index type, proving the R[X] case first, using the proof we have already. Do we have code that helps facilitate this? I was thinking of something like:

import ring_theory.power_series.basic

universes u v w
noncomputable theory

namespace mv_power_series
variables {σ : Type v} {τ : Type w} {R : Type u}

/-- The contravariant map between multivariate formal power series
induced by a map on the indeterminates. -/
def map_indeterminate (φ : τ → σ) : mv_power_series σ R → mv_power_series τ R :=
λ f x, f (x.map_domain φ)

lemma indeterminate_induction (P : Π σ, mv_power_series σ R → Prop)
  (h_empty : ∀ (E : Type*) [subsingleton E] (f : mv_power_series E R), P _ f)
  (h_sum : ∀ (σₗ σᵣ : Type*) (hl : ∀ f : mv_power_series σₗ R, P _ f)
    (hr : ∀ g : mv_power_series σᵣ R, P _ g) (fg : mv_power_series (σₗ ⊕ σᵣ) R), P _ fg)
  (h_iso : ∀ (τ : Type*) (e : σ ≃ τ) (f : mv_power_series τ R) (hf : P _ f),
    P σ (f.map_indeterminate e))
  (f : mv_power_series σ R) : P _ f :=
begin
  sorry
end

end mv_power_series

[Alex J. Best]

You already showed this fact for hahn_series right? So it seems a bit of a shame to have to give a separate proof here, I couldn't find the equivalence between hahn series on \sigma \to \N and mv_power_series \sigma (hopefully I'm not mathematically wrong and it doesnt exist xD) but there is the single variable case already docs#hahn_series.to_power_series. Do you think it'll be easier to just transfer this fact from a ring equivalence to hahn_series?

[Yakov Pechersky]

Maybe -- I did want it in ring_theory.power_series.basic so I could generalize inv from field to division_ring though.

[Alex J. Best]

You could always split the file? Mathematically if a fact about power series is a special case of one about hahn series I'd say there is a dependency there and we shouldn't reprove things

[Yakov Pechersky]

Alex, can you clarify something for me please? Do you mean we should prove it via the hahn_series sigma X and a compatible \sigma to nat? (First showing that those are ring isomorphic?)

[Yakov Pechersky]

And in general refactor to make power_series/basic import hahn_series?

[Alex J. Best]

I was thinking of the following def, sans sorries + API

@[simps] def to_mv_power_series {σ : Type*} : (hahn_series (σ →₀ ℕ) R) ≃+* mv_power_series σ R :=
{ to_fun := λ f, f.coeff,
  inv_fun := λ f, ⟨(f : (σ →₀ ℕ) → R), sorry⟩,
  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 [mv_power_series.coeff_mul, power_series.coeff_mk, mul_coeff, is_pwo_support],
    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 [nat.mem_antidiagonal, and.congr_left_iff, mem_add_antidiagonal, ne.def,
      and_iff_left_iff_imp, mem_filter, mem_support],
    intros h1 h2,
    contrapose h1,
    rw ← decidable.or_iff_not_and_not at h1,
    cases h1; simp [h1],
  end }

[Alex J. Best]

Refactoring power_series/basic completely to depend on hahn_series would be quite a job right now (but might be worth it eventually), however its almost 2000 lines so it definitely needs a haircut or two. (One obvious thing is that docs#power_series is only defined on line 800 so could be split off but thats slightly orthogonal).
Domain for power_series is on line ~1300 of that file, so maybe stuff after that is more commutative algebra than just basic facts about power series, that could be a good point to split perhaps and have that part import hahn_series

[Yakov Pechersky]

Is this even true though? What if \sigma is complex? It's not ordered, but one can still have a completely valid mv_power_series complex R

[Alex J. Best]

Maybe you need fintype sigma yeah? That certainly was the case for the inductive proof you proposed too I guess

[Yakov Pechersky]

If my sigma was nat or even nat \o+ nat I think my proof would still work?

[Alex J. Best]

The induction you asked about above is summing subsingleton sigmas only so I don't think you can get nat from that

[Yakov Pechersky]

Or is it really only true for fintype in general?

[Yakov Pechersky]

I thought the summing singletons would be enough for any encodable type

[Alex J. Best]

I don't think thats possible, your induction principle can prove things about arbitrarily large fintypes but not infinite types. I think the statement that mv_power_series are a domain when R is is true in complete generality, but I cant think of a good way to approach proving it

[Reid Barton]

It seems to me that if you have countably many variables $X_1$, $X_2$, ... then $X_1 + X_2 + \cdots$ is not a Hahn series. (I checked the referenced paper by van der Hoeven and it seems to agree with this.) On the other hand it is an mv_power_series. I'm not sure whether this is a good thing or a bad thing--apparently SGA3 has an opinion about this which I'm trying to look up

[Alex J. Best]

Yeah my sorry above is unprovable (as they often are :grinning:) except in the fintype sigma case

[Reid Barton]

I didn't find whatever I was supposed to be looking for in SGA3, but Wikipedia agrees with mathlib's definition of the power series ring at least.

[Reid Barton]

How about this argument to reduce to the case of finitely many variables. Suppose $ab = 0$ but $a \ne 0$ and $b \ne 0$ in $R[[S]]$. Pick a nonzero monomial of each of $a$ and $b$. Together they contain only finitely many variables. Send the rest of the variables to 0. Then we get nonzero elements of a power series ring in finitely many variables, which multiply to zero

[Alex J. Best]

I just got back to this and finally proved the fintype version. Some lemmas need breaking out but I'll try and PR it today

@[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), begin
    refine set.partially_well_ordered_on.mono _ (set.subset_univ _),
    change set.is_pwo (set.univ), -- mono for is_pwo?
    rw set.is_pwo_iff_exists_monotone_subseq,
    simp_rw [monotone, finsupp.le_def],
    suffices : ∀ s : finset σ, ∀ (f : ℕ → σ →₀ ℕ), set.range f ⊆ set.univ → ∃ (g : ℕ ↪o ℕ),
      ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : σ) (hs : x ∈ s), (f ∘ g) a x ≤ (f ∘ g) b x,
    { simpa using this univ, },
    apply' finset.induction,
    { intros f hf, existsi rel_embedding.refl (≤),
      simp, },
    { 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 : σ →₀ ℕ, mo x) ∘ f) (set.subset_univ _),
      obtain ⟨g', hg'⟩ := ih (f ∘ g) (set.subset_univ _),
      refine ⟨g'.trans g, _⟩,
      simp only [mem_insert, forall_eq_or_imp, comp_app, rel_embedding.coe_trans],
      intros a b hab,
      split,
      { simpa using hg (order_hom_class.mono g' hab), },
      { exact hg' hab, }, },
  end⟩,
  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 [mv_power_series.coeff_mul, power_series.coeff_mk, mul_coeff, is_pwo_support],
    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 [nat.mem_antidiagonal, and.congr_left_iff, mem_add_antidiagonal, ne.def,
      and_iff_left_iff_imp, mem_filter, mem_support],
    intros h1 h2,
    contrapose h1,
    rw ← decidable.or_iff_not_and_not at h1,
    cases h1; simp [h1],
  end }