smul not coercing

Stream: general

[Ashwin Iyengar]

Sorry for the long code block but lean isn't using the definition ofsmul on a subtype and I really can't see why (the error happens on the third to last line). If anyone could lend some insight that would be amazing.

import analysis.normed_space.basic
import ring_theory.power_series.basic

open filter

noncomputable theory
open_locale big_operators

variables {σ R : Type*} [normed_ring R]

open mv_power_series

/-- Multivariate restricted power series, where `σ` is the index set of the
variables and `R` is the coefficient ring. This is a formal power series such
that the coefficients tend to 0 with respect to the cofinite filter on `σ → ℕ`. -/
def mv_restricted_power_series (σ R : Type*) [normed_ring R] :=
{f : mv_power_series σ R // tendsto (λ n, coeff R n f) cofinite (nhds 0)}

namespace mv_restricted_power_series

instance : has_coe (mv_restricted_power_series σ R) (mv_power_series σ R) :=
  ⟨subtype.val⟩

lemma coe_injective :
  function.injective (coe : mv_restricted_power_series σ R → mv_power_series σ R) :=
    subtype.coe_injective

instance : has_zero (mv_restricted_power_series σ R) := ⟨⟨0, tendsto_const_nhds⟩⟩
@[simp, norm_cast] lemma coe_zero :
  ((0 : mv_restricted_power_series σ R) : mv_power_series σ R) = 0 := rfl

instance : has_add (mv_restricted_power_series σ R) :=
  ⟨λ f g, ⟨f + g, by simpa using tendsto.add f.prop g.prop⟩⟩
instance : has_neg (mv_restricted_power_series σ R) :=
  ⟨λ f, ⟨-f, by simpa using tendsto.neg f.prop⟩⟩
instance : has_scalar R (mv_restricted_power_series σ R) :=
  { smul :=
      λ r f,
        ⟨r • f, by simpa using tendsto.comp ((mul_left_continuous r).tendsto 0) f.prop⟩}

instance : add_comm_group (mv_restricted_power_series σ R) :=
  coe_injective.add_comm_group _ rfl (λ x y, rfl) (λ x, rfl)

def coe_add_monoid_hom : mv_restricted_power_series σ R →+ mv_power_series σ R :=
  { to_fun := coe,
    map_zero' := rfl,
    map_add' := λ _ _, rfl}

instance : semimodule R (mv_restricted_power_series σ R) :=
  function.injective.semimodule R coe_add_monoid_hom coe_injective (λ _ _, rfl)

def coe_semimodule_hom : mv_restricted_power_series σ R →ₗ[R] mv_power_series σ R :=
  { to_fun := coe,
    map_add' := coe_add_monoid_hom.map_add,
    map_smul' := λ _ _, rfl}

variables (R)

/-- The `n`th coefficient of a multivariate formal power series.-/
def coeff (n : σ →₀ ℕ) : (mv_restricted_power_series σ R) →ₗ[R] R :=
  (coeff R n).comp coe_semimodule_hom

example (f : mv_power_series σ R) (g : tendsto f cofinite (nhds 0)) (r : R) :
  (r • (⟨f, g⟩ : mv_restricted_power_series σ R) : mv_power_series σ R) = r • f := rfl

/-- The `n`th monomial with coefficient `a` as multivariate formal power series.-/
def monomial (n : σ →₀ ℕ) : R →ₗ[R] mv_restricted_power_series σ R :=
{ to_fun := λ r, ⟨mv_power_series.monomial R n r,
  begin
    refine tendsto.congr' _ (0 : mv_restricted_power_series σ R).prop,
    refine eventually_eq_of_mem (set.finite.compl_mem_cofinite (set.finite_singleton n)) _,
    intros x hx,
    simp [coeff_monomial_ne hx]
  end⟩,
  map_add' := λ _ _, by simpa only [subtype.ext_iff, subtype.coe_mk, linear_map.map_add],
  map_smul' := λ r s, by { simp [subtype.ext_iff], } }

end mv_restricted_power_series

[Eric Wieser]

You're missing some simp lemmas to go with your coe_zero lemma - in particular, you should add lemmas about coe_smul, coe_add, coe_sub, and coe_neg

[Eric Wieser]

@[simp, norm_cast] lemma coe_add (a b : mv_restricted_power_series σ R):
  (↑(a + b) : mv_power_series σ R) = a + b := rfl

@[simp, norm_cast] lemma coe_sub (a b : mv_restricted_power_series σ R):
  (↑(a + b) : mv_power_series σ R) = a + b := rfl

@[simp, norm_cast] lemma coe_neg (a b : mv_restricted_power_series σ R):
  (↑(-a) : mv_power_series σ R) = -a := rfl

@[simp, norm_cast] lemma coe_smul (r : R) (a : mv_restricted_power_series σ R):
  (↑(r • a) : mv_power_series σ R) = r • a := rfl

[Ashwin Iyengar]

Ah wow thanks, I guess I thought that these were somehow implicitly constructed.

[Eric Wieser]

Adding ←smul_eq_mul to your failing simp call then closes the goal

[Eric Wieser]

It would be nice if they were, but only attributes (@[...]) can do that kind of thing, calling functions like function.injective.semimodule obviously can't have side-effects like that.

[Ashwin Iyengar]

Continuing on this thread, I've got a bizarre error that I can't interpret again. When I try to declare a comm_ring (mv_restricted_power_series σ R) assuming comm_ring R, it doesn't seem to want to use the fact that there's a comm_ring (mv_power_series σ R) (which is declared in the power series file) which should let me use mul_comm.

import analysis.normed_space.basic
import ring_theory.power_series.basic

open filter
open mv_power_series

noncomputable theory
open_locale big_operators

class nonarchimedean_normed_ring (R : Type*) extends normed_ring R :=
(ultrametric_inequality : ∀ x y : R, ∥x + y∥ ≤ (max ∥x∥ ∥y∥))

variables {σ R : Type*} [nonarchimedean_normed_ring R]

/-- Multivariate restricted power series, where `σ` is the index set of the
variables and `R` is the coefficient ring. This is a formal power series such
that the coefficients tend to 0 with respect to the cofinite filter on `σ → ℕ`. -/
def mv_restricted_power_series (σ R : Type*) [normed_ring R] :=
{f : mv_power_series σ R // tendsto (λ n, coeff R n f) cofinite (nhds 0)}

namespace mv_restricted_power_series

instance : has_coe (mv_restricted_power_series σ R) (mv_power_series σ R) :=
  ⟨subtype.val⟩

lemma coe_injective :
  function.injective (coe : mv_restricted_power_series σ R → mv_power_series σ R) :=
    subtype.coe_injective

instance : has_zero (mv_restricted_power_series σ R) := ⟨⟨0, tendsto_const_nhds⟩⟩
@[simp, norm_cast] lemma coe_zero :
  (↑(0 : mv_restricted_power_series σ R) : mv_power_series σ R) = 0 := rfl

instance : has_add (mv_restricted_power_series σ R) :=
  ⟨λ f g, ⟨f + g, by simpa using tendsto.add f.prop g.prop⟩⟩
@[simp, norm_cast] lemma coe_add (a b : mv_restricted_power_series σ R):
  (↑(a + b) : mv_power_series σ R) = a + b := rfl
@[simp, norm_cast] lemma coe_sub (a b : mv_restricted_power_series σ R):
  (↑(a + b) : mv_power_series σ R) = a + b := rfl

instance : has_neg (mv_restricted_power_series σ R) :=
  ⟨λ f, ⟨-f, by simpa using tendsto.neg f.prop⟩⟩
@[simp, norm_cast] lemma coe_neg (a : mv_restricted_power_series σ R):
  (↑(-a) : mv_power_series σ R) = -a := rfl

instance : has_scalar R (mv_restricted_power_series σ R) :=
  { smul :=
      λ r f,
        ⟨r • f, by simpa using tendsto.comp ((mul_left_continuous r).tendsto 0) f.prop⟩}

instance : add_comm_group (mv_restricted_power_series σ R) :=
  coe_injective.add_comm_group _ rfl coe_add coe_neg

def coe_add_monoid_hom : mv_restricted_power_series σ R →+ mv_power_series σ R :=
  { to_fun := coe,
    map_zero' := coe_zero,
    map_add' := coe_add}

instance : semimodule R (mv_restricted_power_series σ R) :=
  function.injective.semimodule R coe_add_monoid_hom coe_injective (λ _ _, rfl)

@[simp, norm_cast] lemma coe_smul (r : R) (a : mv_restricted_power_series σ R):
  (↑(r • a) : mv_power_series σ R) = r • a := rfl

def coe_semimodule_hom : mv_restricted_power_series σ R →ₗ[R] mv_power_series σ R :=
  { to_fun := coe,
    map_add' := coe_add,
    map_smul' := coe_smul}

variables (R)

/-- The `n`th coefficient of a multivariate restricted power series.-/
def coeff (n : σ →₀ ℕ) : (mv_restricted_power_series σ R) →ₗ[R] R :=
  (coeff R n).comp coe_semimodule_hom

example (f : mv_power_series σ R) (g : tendsto f cofinite (nhds 0)) (r : R) :
  (r • (⟨f, g⟩ : mv_restricted_power_series σ R) : mv_power_series σ R) = r • f := rfl

/-- The `n`th monomial with coefficient `a` as multivariate restricted power series.-/
def monomial (n : σ →₀ ℕ) : R →ₗ[R] mv_restricted_power_series σ R :=
{ to_fun := λ r, ⟨mv_power_series.monomial R n r,
  begin
    refine tendsto.congr' _ (0 : mv_restricted_power_series σ R).prop,
    refine eventually_eq_of_mem (set.finite.compl_mem_cofinite (set.finite_singleton n)) _,
    intros x hx,
    simp [coeff_monomial_ne hx]
  end⟩,
  map_add' := λ _ _, by simpa only [subtype.ext_iff, subtype.coe_mk, linear_map.map_add],
  map_smul' := λ m r, by simp only [subtype.ext_iff, coe_smul, subtype.coe_mk, linear_map.map_smul], }

variables {R}

instance : has_one (mv_restricted_power_series σ R) := ⟨monomial R 0 1⟩
@[simp, norm_cast] lemma coe_one :
  (↑(1 : mv_restricted_power_series σ R) : mv_power_series σ R) = 1 := rfl

@[simp] lemma apply_coeff (n : σ →₀ ℕ) (f : mv_restricted_power_series σ R) :
   f.val n = coeff R n f
     := rfl

@[ext] lemma ext (f g : mv_restricted_power_series σ R)
  (h : ∀ (n : σ →₀ ℕ), coeff R n f = coeff R n g) : f = g := by {ext, exact h n}

lemma ext_iff (f g : mv_restricted_power_series σ R) :
  f = g ↔ ∀ n : σ →₀ ℕ, coeff R n f = coeff R n g :=
    ⟨λ h _, by {rwa h}, ext f g⟩

lemma nonzero_coeff_of_nonzero (f : mv_restricted_power_series σ R) (h : f ≠ 0) :
  ∃ n, 0 < ∥coeff R n f∥ :=
begin
  rw [ne.def, ext_iff, not_forall] at h,
  cases h with n hn,
  rw [linear_map.map_zero, push_neg.not_eq, ← norm_pos_iff] at hn,
  use n,
  assumption
end

instance : has_mul (mv_restricted_power_series σ R) :=
  ⟨λ f g, ⟨f * g, sorry⟩⟩
@[simp, norm_cast] lemma coe_mul (a b : mv_restricted_power_series σ R):
  (↑(a * b) : mv_power_series σ R) = a * b := rfl

instance : ring (mv_restricted_power_series σ R) :=
  function.injective.ring (coe : mv_restricted_power_series σ R → mv_power_series σ R) coe_injective coe_zero coe_one coe_add coe_mul coe_neg

--instance [comm_ring R] : comm_ring (mv_restricted_power_series σ R) :=
--  function.injective.comm_ring (coe : mv_restricted_power_series σ R → mv_power_series σ R) coe_injective coe_zero coe_one coe_add coe_mul coe_neg

instance [comm_ring R] : comm_ring (mv_restricted_power_series σ R) :=
{ mul_comm := λ a b, begin simp [subtype.ext_iff, coe_mul], exact mul_comm (a : mv_power_series σ R) (b : mv_power_series σ R) end,
  .. mv_restricted_power_series.ring }

end mv_restricted_power_series

[Eric Wieser]

You have two ring instances, one via nonarchimedean_normed_ring R and one from comm_ring R

[Eric Wieser]

You need to add a nonarchimedean_normed_comm_ring R typeclass that extends both nonarchimedean_normed_ring and normed_comm_ring

[Ashwin Iyengar]

Ahh ok I see, that makes sense

[Eric Wieser]

Using convert instead of exact makes that difference easier to spot