## Stream: new members

### Topic: subtypes

#### Ashwin Iyengar (Feb 13 2021 at 16:00):

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 (Feb 13 2021 at 16:06):

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

#### Kevin Buzzard (Feb 13 2021 at 16:09):

I think there are some simp lemmas missing.

#### Ashwin Iyengar (Feb 13 2021 at 16:10):

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

#### Kevin Buzzard (Feb 13 2021 at 16:11):

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 (Feb 13 2021 at 16:13):

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 (Feb 13 2021 at 16:17):

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 (Feb 13 2021 at 16:18):

ahh amazing, thanks!

#### Kevin Buzzard (Feb 13 2021 at 16:18):

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

#### Ashwin Iyengar (Feb 13 2021 at 16:19):

Right ok that makes sense

#### Kevin Buzzard (Feb 13 2021 at 16:19):

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 (Feb 13 2021 at 16:20):

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 (Feb 13 2021 at 16:32):

-- 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.

Nice, thanks

#### Kevin Buzzard (Feb 13 2021 at 16:36):

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

#### Kevin Buzzard (Feb 13 2021 at 16:37):

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 (Feb 13 2021 at 16:41):

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 (Feb 13 2021 at 16:43):

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

#### Kevin Buzzard (Feb 13 2021 at 16:44):

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 (Feb 13 2021 at 16:44):

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

#### Kevin Buzzard (Feb 13 2021 at 16:45):

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 (Feb 15 2021 at 12:38):

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) :=
{
zero := 0,
neg := neg,
}


#### Ruben Van de Velde (Feb 15 2021 at 13:05):

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 (Feb 15 2021 at 13:28):

ext ought to help here too, after those rintros

#### Kevin Buzzard (Feb 15 2021 at 13:32):

 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 (Feb 15 2021 at 13:33):

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 (Feb 15 2021 at 13:37):

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

#### Kevin Buzzard (Feb 15 2021 at 13:48):

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 (Feb 15 2021 at 13:50):

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

#### Kevin Buzzard (Feb 15 2021 at 13:50):

  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 (Feb 15 2021 at 13:51):

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 (Feb 15 2021 at 13:57):

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

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 (Feb 15 2021 at 13:58):

There's the rfls you were hoping to see

#### Kevin Buzzard (Feb 15 2021 at 13:58):

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

#### Eric Wieser (Feb 15 2021 at 13:59):

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

#### Kevin Buzzard (Feb 15 2021 at 13:59):

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

(deleted)

#### Kevin Buzzard (Feb 15 2021 at 14:02):

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 (Feb 15 2021 at 14:03):

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


#### Kevin Buzzard (Feb 15 2021 at 14:04):

No need to ever translate into epsilons.

#### Ashwin Iyengar (Feb 15 2021 at 18:09):

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 (Feb 15 2021 at 18:14):

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


#### Ashwin Iyengar (Feb 15 2021 at 18:15):

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

#### Kevin Buzzard (Feb 15 2021 at 18:15):

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 (Feb 15 2021 at 18:21):

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 (Feb 15 2021 at 18:23):

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

#### Eric Wieser (Feb 15 2021 at 18:24):

Can you post an updated #mwe?

#### Ashwin Iyengar (Feb 15 2021 at 18:24):

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 (Feb 15 2021 at 18:28):

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 (Feb 15 2021 at 18:32):

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

#### Ashwin Iyengar (Feb 15 2021 at 18:32):

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 (Feb 15 2021 at 18:33):

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

#### Kevin Buzzard (Feb 15 2021 at 18:34):

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 :-)

Ah good to know

#### Eric Wieser (Feb 15 2021 at 18:42):

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

#### Eric Wieser (Feb 15 2021 at 18:43):

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 (Feb 15 2021 at 18:46):

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 (Feb 15 2021 at 19:44):

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 (Feb 15 2021 at 19:52):

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 (Feb 15 2021 at 19:55):

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 (Feb 15 2021 at 19:57):

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

#### Kevin Buzzard (Feb 15 2021 at 19:58):

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 (Feb 15 2021 at 20:01):

A tactic a day...

Last updated: May 08 2021 at 18:17 UTC