Stream: maths

Topic: algebra problem

Heather Macbeth (Jan 01 2021 at 21:46):

True or false: the mathlib definition docs#nondiscrete_normed_field implies characteristic zero?

Adam Topaz (Jan 01 2021 at 21:52):

I hope it's false so that $\mathbb{F}_p((t))$ can have the $t$-adic norm...

Heather Macbeth (Jan 01 2021 at 21:53):

I have no idea what that is :) Does it satisfy our definition?

Mario Carneiro (Jan 01 2021 at 21:57):

I think zmod 2 is a normed_field, where the distance between 0 and 1 is 1

Adam Topaz (Jan 01 2021 at 21:57):

Yeah I think so. The name "non discrete" is unfortunate, because the norm on the field I mentioned comes from a discrete valuation

Heather Macbeth (Jan 01 2021 at 21:57):

Mario Carneiro said:

I think zmod 2 is a normed_field, where the distance between 0 and 1 is 1

Yes, but the nondiscrete hypothesis excludes that example.

Adam Topaz (Jan 01 2021 at 21:59):

"non-discrete" should really be called "non-trivial"

Mario Carneiro (Jan 01 2021 at 21:59):

oh, that assumption implies that it is at least infinite

Adam Topaz (Jan 01 2021 at 21:59):

Or "non-trivially-normed" field

Heather Macbeth (Jan 01 2021 at 21:59):

Adam, your example is $\mathbb{F}_p$-coefficient rational functions in $t$? What is the norm?

Adam Topaz (Jan 01 2021 at 22:00):

It's Laurent series. The norm sends t to 1/2 (for example)

Mario Carneiro (Jan 01 2021 at 22:00):

what happens with the padic norm on Qp?

Adam Topaz (Jan 01 2021 at 22:00):

Same. But that char 0

Adam Topaz (Jan 01 2021 at 22:01):

The same norm works for rational functions

Mario Carneiro (Jan 01 2021 at 22:03):

aha, now I'm on board with adam's example

Mario Carneiro (Jan 01 2021 at 22:03):

does it work with rational functions?

Yeah

Adam Topaz (Jan 01 2021 at 22:04):

For example you can embed rational functions in Laurent series and restrict the norm

Mario Carneiro (Jan 01 2021 at 22:04):

what's the norm exactly? Is it the degree?

Adam Topaz (Jan 01 2021 at 22:04):

Explicitly the norm of a power series in t is (1/2)^n where n is the index of the first coefficient of the series which is nonzero

Adam Topaz (Jan 01 2021 at 22:05):

(1/2 is of course a choice, and you can choose any positive real less than 1)

or greater

Adam Topaz (Jan 01 2021 at 22:05):

No, it needs to be less than 1

Adam Topaz (Jan 01 2021 at 22:05):

The triangle inequality won't work otherwise

Adam Topaz (Jan 01 2021 at 22:11):

Well, if you want to work with rational functions then it doesn't matter, since you can always replace t with 1/t, but for Laurent series one should be careful

Last updated: May 14 2021 at 19:21 UTC