# Zulip Chat Archive

## 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?

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

Edited, added them.

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

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

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

There's the `rfl`

s 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

#### Eric Wieser (Feb 15 2021 at 14:00):

(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,
map_add' := coe_add }
```

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

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

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