subtypes

Stream: new members

[Ashwin Iyengar]

I'm a bit confused about how subtypes work. This simp [h] doesn't close the subgoal:

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

open filter

def mv_restricted_power_series (σ R : Type*) [normed_ring R] :=
{f : mv_power_series σ R // tendsto f cofinite (nhds 0)}

namespace mv_restricted_power_series

variables (σ R : Type*) [normed_ring R]

instance : has_zero (mv_restricted_power_series σ R) := {zero := ⟨mv_power_series.has_zero.zero, tendsto_const_nhds⟩}

theorem exists_max (f : mv_restricted_power_series σ R) : ∃ x, ∀ y, norm (f.val x) ≥ norm (f.val y) :=
begin
  cases em (f = 0),
  {
    simp [h],
  },
  {}
end

But if I change cases em (f = 0) to cases em (f.val = 0) it does close the goal. I don't get why this makes such a big difference; wouldn't it be more natural to write f = 0?

[Kevin Buzzard]

what imports do I need to make this a #mwe?

[Ashwin Iyengar]

Edited, added them.

[Kevin Buzzard]

I think there are some simp lemmas missing.

[Ashwin Iyengar]

Some simp lemmas that need to be written for mv_restricted_power_series? Or things missing from one of the imports?

[Kevin Buzzard]

If h : f = 0 then simp [h] takes you to 0.val x and then to ↑0 x and then it gets stuck

[Ashwin Iyengar]

If h : f.val = 0 then the simp does a pi.zero_apply, which I guess it doesn't want to do if h : f = 0

[Kevin Buzzard]

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

@[simp, norm_cast] lemma coe_zero :
  ((0 : mv_restricted_power_series σ R) : mv_power_series σ R) = 0 := rfl

theorem exists_max (f : mv_restricted_power_series σ R) : ∃ x, ∀ y, norm (f.val x) ≥ norm (f.val y) :=
begin
  cases em (f = 0),
  { simp [h] }, -- works now
  { sorry }
end

[Ashwin Iyengar]

ahh amazing, thanks!

[Kevin Buzzard]

simp changes f.val into ↑f it seems, so you need a simp lemma saying that the coerced 0 is still 0.

[Ashwin Iyengar]

Right ok that makes sense

[Kevin Buzzard]

The trick with these things is to look at the goal left by simp (in this case one involving ↑0) and to ask "why did it not get any further than this?" and the answer is that the lemma you want to apply next (namely ↑0 = 0) is not there.

[Kevin Buzzard]

Making definitions is much harder than proving theorems, but after a while you just pick up the tricks of what needs to be done.

[Kevin Buzzard]

-- don't want them to be explicit for this next function
variables {σ R}

open mv_power_series

def coeff (f : mv_restricted_power_series σ R) (c : σ →₀ ℕ) : R :=
coeff R c (f : mv_power_series σ R)

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

lemma ext_iff (f g : mv_restricted_power_series σ R) :
  f = g ↔ ∀ (c : σ →₀ ℕ), coeff f c = coeff g c :=
⟨λ h _, h ▸ rfl, ext f g⟩

theorem exists_max (f : mv_restricted_power_series σ R) : ∃ x, ∀ y, norm (f.val x) ≥ norm (f.val y) :=
begin
  cases em (f = 0),
  { simp [h] }, -- works now
  { rw ext_iff at h,
    push_neg at h,
    sorry }
end

@Ashwin Iyengar that's how I'd start. Any new type needs an extensionality lemma.

[Ashwin Iyengar]

Nice, thanks

[Kevin Buzzard]

In fact looking at mv_power_series the coeff function should be an R-module hom really.

[Kevin Buzzard]

so another thing you might want to do is to make mv_restricted_power_series σ R into an R-module and then beef up the definition of coeff

[Kevin Buzzard]

Of course it's entirely up to you how you do this. If you're thinking about a PR (and you perhaps should be) then you might want to look at the beginning of the power series file in mathlib, where they do exactly what I decided was the best idea -- give it an R-module structure and then define coeff and ext. They also defined monomial. These things will ultimately make your life easier in the end.

[Ashwin Iyengar]

Cool yeah that's basically what I was planning to do after getting to grips with the library a bit more

[Kevin Buzzard]

I know several cases of beginners who have started exactly this way -- made a PR to mathlib generalising something which was already there.

[Kevin Buzzard]

Ashvni (who you know), Amelia and Jason (both IC UGs) all started like this.

[Kevin Buzzard]

If you do nothing more than to make it a ring under the assumption of the ultrametric inequality then this is already really useful. Then you come back to look at it 3 months later and other random people have built on top of it. It's the way the library grows.

[Ashwin Iyengar]

I would expect that in my instantiation of an add_comm_group, I should just be able to do rfl for add_assoc because I added a coe_add but it doesn't work. Is there a simple way to prove add_assoc which essentially just says "it's true because it's true for the supertype"?

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

open filter

noncomputable theory

def mv_restricted_power_series (σ R : Type*) [normed_field R] :=
{f : mv_power_series σ R // tendsto f cofinite (nhds 0)}

namespace mv_restricted_power_series

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

instance : has_coe (mv_restricted_power_series σ R) (mv_power_series σ R) :=
⟨subtype.val⟩
instance : has_zero (mv_restricted_power_series σ R) := {zero := ⟨mv_power_series.has_zero.zero, tendsto_const_nhds⟩}

@[simp, norm_cast] lemma coe_zero :
  ((0 : mv_restricted_power_series σ R) : mv_power_series σ R) = 0 := rfl

def add (f g : mv_restricted_power_series σ R) : mv_restricted_power_series σ R :=
  ⟨f.val + g.val, by simpa using tendsto.add f.2 g.2⟩

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

def neg (f : mv_restricted_power_series σ R) : mv_restricted_power_series σ R :=
⟨-f.val,
begin
  have f_conv := metric.tendsto_nhds.1 f.2,
  simp at f_conv,
  rw metric.tendsto_nhds,
  simp,
  exact f_conv,
end⟩

instance : add_comm_group (mv_restricted_power_series σ R) :=
{
  add := add,
  add_assoc := rfl,
  zero := 0,
  zero_add := sorry,
  add_zero := sorry,
  neg := neg,
  add_left_neg := sorry,
  add_comm := sorry,
}

[Ruben Van de Velde]

One thing that seems to work is

  add_assoc := by { rintros ⟨a, _⟩ ⟨b, _⟩ ⟨c, _⟩, simp only [add, subtype.mk_eq_mk], apply add_assoc,  },

[Eric Wieser]

ext ought to help here too, after those rintros

[Kevin Buzzard]

add_assoc := λ _ _ _, by {ext, simp only [add_assoc, coe_add]}, would be the way I would prove it. by {ext, simp [add_assoc]} works too, but is slower. Note that add_assoc is not a simp` lemma so needs to be added explicitly.

[Kevin Buzzard]

rfl means "this is true by definition, if you unfold all the definitions", so it won't work here, because if you unfold all the definitions you are reduced to associativity of addition for multivariable power series, which is true, but not true by definition -- it's true because of a theorem (in fact an axiom, namely associativity of addition on R).

[Ashwin Iyengar]

Thanks all! ext was the key that I wasn't aware existed.

[Kevin Buzzard]

The ext lemma we proved earlier was tagged with @[ext], which means that the ext tactic will use it. But actually I guess the reason it's working without that ext lemma is that the ext tactic is using subtype.ext and then the ext lemma for mv_power_series.

Here's a proof of neg which just says "f.2 says some filter tends to 0, so the corresponding filter for -f tends to -0".

def neg (f : mv_restricted_power_series σ R) : mv_restricted_power_series σ R :=
⟨-f.val,
begin
  convert tendsto.comp continuous_at_neg f.2,
  exact neg_zero.symm,
end⟩

[Eric Wieser]

The implementation for something like src#submonoid.to_monoid ought to show how ext is normally used here

[Kevin Buzzard]

  add_assoc := λ _ _ _, by {show_term{ext}, simp only [add_assoc, coe_add]},

shows that it's using subtype.ext and then the ext lemma for mv power series

[Eric Wieser]

Actually it seems like ext isn't used at all, and the proofs are just transferred across the injectivity of coe, using docs#function.injective.add_comm_monoid

[Eric Wieser]

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

instance : has_add (mv_restricted_power_series σ R) := ⟨add⟩
instance : has_neg (mv_restricted_power_series σ R) := ⟨neg⟩

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

[Eric Wieser]

There's the rfls you were hoping to see

[Kevin Buzzard]

How can this work? One has to check that the subtype condition is preserved by addition and negation.

[Eric Wieser]

That's why you have to define add and neg yourself

[Kevin Buzzard]

Oh I see, you use the contructions of add and neg

[Eric Wieser]

(deleted)

[Kevin Buzzard]

def neg (f : mv_restricted_power_series σ R) : mv_restricted_power_series σ R :=
⟨-f.val, by simpa using tendsto.comp continuous_at_neg f.2⟩

[Kevin Buzzard]

def neg (f : mv_restricted_power_series σ R) : mv_restricted_power_series σ R :=
⟨-f.val, by simpa using tendsto.neg f.2⟩

[Kevin Buzzard]

No need to ever translate into epsilons.

[Ashwin Iyengar]

Thanks. This code works:

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

but now I want to use docs#function.injective.semimodule to show that restricted power series are an R-module. The problem is that it's not clear that coe is an additive monoid homomorphism. My understanding is that morphisms should be bundled. So what's the best way of stating that coe is a homomorphism? Then I can do something like

instance : semimodule R (mv_restricted_power_series σ R) :=
  coe_injective.semimodule _ ???

[Kevin Buzzard]

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

[Ashwin Iyengar]

Ah ok so treat it as a separate thing. Thanks!

[Kevin Buzzard]

yeah it's kind of annoying. In Lean 4 we might be able to go back to the instance : is_add_monoid_hom coe approach but in Lean 3 the separate thing approach turned out to be nicer.

[Kevin Buzzard]

instance : semimodule R (mv_restricted_power_series σ R) :=
function.injective.semimodule R coe_hom coe_hom_injective (λ c x, rfl)

works but I can't get coe_hom_injective.semimodule ... to work.

[Ashwin Iyengar]

Yeah I guess coe_injective doesn't know that coe is a hom

[Eric Wieser]

Can you post an updated #mwe?

[Ashwin Iyengar]

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

open filter

noncomputable theory

def mv_restricted_power_series (σ R : Type*) [normed_ring R] :=
{f : mv_power_series σ R // tendsto f cofinite (nhds 0)}

namespace mv_restricted_power_series

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

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_add (mv_restricted_power_series σ R) :=
  ⟨λ f g, ⟨f.val + g.val, by simpa using tendsto.add f.2 g.2⟩⟩
instance : has_zero (mv_restricted_power_series σ R) := ⟨⟨0, tendsto_const_nhds⟩⟩
instance : has_neg (mv_restricted_power_series σ R) :=
  ⟨λ f, ⟨-f.val, by simpa using tendsto.neg f.2⟩⟩
instance : has_scalar R (mv_restricted_power_series σ R) :=
  {smul := λ r f, ⟨r • f.val, by simpa using tendsto.comp ((mul_left_continuous r).tendsto 0) f.property⟩}

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

def coe_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_hom coe_injective (λ _ _, rfl)

[Kevin Buzzard]

Hey, nice has_scalar.smul proof :-) You can use f.2 for f.property if you want (and f.1 for f.val) -- but I'm not sure that there is any particular preference for one over the other, I'm just noting this general trick of X.1 and X.2 which works in large generality. Note that X.3 doesn't work :-( (in situations where it's meaningful, e.g. if X is a proof of P and Q and R) -- it's X.2.2.

[Ashwin Iyengar]

Ok, yeah either way I should probably pick a convention and stick to it

[Ashwin Iyengar]

I sort of like f.val and f.property because they're less ambiguous, but maybe that hasn't been the design principle?

[Kevin Buzzard]

No, I agree about the lack of ambiguity, stick with them, I was just pointing out a trick.

[Kevin Buzzard]

Honestly, the only reason I said it was that

  {smul := λ r f, ⟨r • f.val, by simpa using tendsto.comp ((mul_left_continuous r).tendsto 0) f.property⟩}

is over 100 characters long, and there's a 100 character limit per line in mathlib, and this trick got it back down to under 100 characters :-)

[Ashwin Iyengar]

Ah good to know

[Eric Wieser]

Usually coercion is used as the simp-normal form in place of .val or .1

[Eric Wieser]

That is,

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⟩}

[Mario Carneiro]

Note that X.3 doesn't work :-( (in situations where it's meaningful, e.g. if X is a proof of P and Q and R) -- it's X.2.2.

By the way, while I would be all for such an abbreviation, it makes X.2 ambiguous

[Ashwin Iyengar]

Also @Kevin Buzzard I would think that

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

is more natural than

@[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}

but maybe I'm missing something? Is the idea that using coeff is more elegant because it doesn't rely on the precise definition of mv_power_series or mv_restricted_power_series?

[Kevin Buzzard]

I am always a bit edgy about abuse of definitional equality. What you say is exactly what worries me -- but I know that some computer scientists would find your suggestion more elegant. Your code breaks if someone refactors mv_power_series to be e.g. a completion of k[sigma]/I^n with I the ideal generated by the sigma, whereas mine uses the interface so doesn't break. I've seen definitions change in the past in mathlib. On the other hand the current definition of power series seems to be one which makes everyone happy right now so maybe it's unlikely to change in future. Abuse of definitional equality is really handy when you're writing slick term mode proofs at the beginning of your API. After a while it basically becomes irrelevant though, because e.g. if you're trying to prove that Tate algebras in finitely many variables over a complete nonarchimedean normed field are Noetherian then these issues are not really the important ones -- you're going to write a long tactic proof there so who cares what the definition is under the hood.

[Ashwin Iyengar]

I see. Yeah it's the little things like this I get perplexed by, like e.g. right now I'm stuck trying to convert hd: ¬⇑(coeff R d) f = 0 to hd: ¬∥f.val d∥ = 0

[Kevin Buzzard]

You can probably change ¬(f.val d = 0) at hd because these will be definitional.

[Kevin Buzzard]

But one thing you should definitely do is to decide once and for all whether you're going to refer to to the d'th coefficient of f via f.val d or coeff R d f or whatever, and then stick to your convention, and write simp lemmas changing every other convention to your convention.

[Ashwin Iyengar]

A tactic a day...