Power series Inclusion Function

Stream: new members

[Coleton Kotch]

Hello, I am relatively new to lean and could use some help. Currently I am trying to write prove that the (incl_fun) function defined, mapping a power series in a set of variables to a power series in variables corresponding to the disjoint union of the first set with another set in the natural way, gives a morphism of rings.

import tactic
import ring_theory.ideal.quotient
import ring_theory.power_series.basic

noncomputable theory
open_locale classical
open_locale big_operators

variables (σ τ R : Type*) [comm_ring R]

namespace mv_power_series

open finset

variables {σ τ R}

def incl_fun : mv_power_series σ R → mv_power_series (σ ⊕ τ) R :=
  show ((σ →₀ ℕ) → R) → ((σ ⊕ τ →₀ ℕ) → R), from λ f m,
  let n := finsupp.sum_finsupp_equiv_prod_finsupp m in
  if n.2 = 0 then f n.1 else 0


def incl : mv_power_series σ R →+* mv_power_series (σ ⊕ τ) R :=
{ to_fun := incl_fun,
  map_one' :=  begin
  ext n,
  unfold incl_fun,
  rw coeff_one,
  simp,
  split_ifs,
  end,
  map_mul' := sorry,
  map_zero' := begin
  ext,
  unfold incl_fun,
  simp,
  refl,
  end,
  map_add' := sorry }

Above is what I have so far. Below is the tactic state after the split_ifs tactic in map_one'.

σ: Type u_1
τ: Type u_2
R: Type u_4
_inst_1: comm_ring R
n: σ ⊕ τ →₀ ℕ
h: n = 0
⊢ ⇑(coeff R n) (λ (m : σ ⊕ τ →₀ ℕ), ite (finsupp.comap_domain sum.inr m _ = 0) (1 (finsupp.comap_domain sum.inl m _)) 0) = 1

σ: Type u_1
τ: Type u_2
R: Type u_4
_inst_1: comm_ring R
n: σ ⊕ τ →₀ ℕ
h: ¬n = 0
⊢ ⇑(coeff R n) (λ (m : σ ⊕ τ →₀ ℕ), ite (finsupp.comap_domain sum.inr m _ = 0) (1 (finsupp.comap_domain sum.inl m _)) 0) = 0

It seems as though the way to proceed would be to "evaluate" the lambda at our n and then split_ifs again to deal with all possibilities, however, I have not been able to figure out how I should go about doing this.

[Yakov Pechersky]

Am I correct that your definition would be the same as mv_polynomial.eval₂_hom mv_polynomial.C or.inl?

[Coleton Kotch]

I believe that my definition would be the same as that yes, other than for power series of course and using sum.inl instead of or.inl.

[Yakov Pechersky]

Ah, yes, I meant sum.inl

[Kevin Buzzard]

So you could prove it by using extensionality to verify that your map is the same as the ring homomorphism which already exists, and then deducing that your map is also a ring homomorphism :-)

[Kevin Buzzard]

These internal definitions of things like polynomial multiplication are very delicate. If you're doing this as a learning exercise then you've certainly jumped in at the deep end and you might want to look at how things like eval2hom are constructed. If you're doing it because you need it for something else then just breathe a sigh of relief because it's done already. Even single variable polynomials are quite messy when dealing with multiplication.

[Coleton Kotch]

My goal is to use it in defining formal group laws so I don't need to do everything from scratch. However, though I do now know how to get the morphism for polynomials thanks to Yakov Pechersky's help, I don't see how to construct the analogous morphism for power series.

[Kevin Buzzard]

The power series API might be less complete than the polynomial API -- probably power series have had less love than polynomials. So what's the set-up: a power series ring in finitely many variables over a commutative base ring? My feeling is that the correct way to set this up is to first show that power series rings are uniform space completions of polynomial rings and then use the polynomial API and argue by continuity to develop the corresponding power series API. The first step (although it would be worth checking to see nobody did it already) would be to put the uniform space structure on a polynomial ring coming from the ideal generated by the coefficients and prove that the inclusion to the power series ring identifies the power series ring with the completion (at least in the case of finitely many variables; I'd have to think a little more to be sure it worked in the case of infinite variables)