Zulip Chat Archive

Stream: maths

Topic: algebra problem


view this post on Zulip Heather Macbeth (Jan 01 2021 at 21:46):

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

view this post on Zulip Adam Topaz (Jan 01 2021 at 21:52):

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

view this post on Zulip Heather Macbeth (Jan 01 2021 at 21:53):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jan 01 2021 at 21:59):

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

view this post on Zulip Mario Carneiro (Jan 01 2021 at 21:59):

oh, that assumption implies that it is at least infinite

view this post on Zulip Adam Topaz (Jan 01 2021 at 21:59):

Or "non-trivially-normed" field

view this post on Zulip Heather Macbeth (Jan 01 2021 at 21:59):

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

view this post on Zulip Adam Topaz (Jan 01 2021 at 22:00):

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

view this post on Zulip Mario Carneiro (Jan 01 2021 at 22:00):

what happens with the padic norm on Qp?

view this post on Zulip Adam Topaz (Jan 01 2021 at 22:00):

Same. But that char 0

view this post on Zulip Adam Topaz (Jan 01 2021 at 22:01):

The same norm works for rational functions

view this post on Zulip Mario Carneiro (Jan 01 2021 at 22:03):

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

view this post on Zulip Mario Carneiro (Jan 01 2021 at 22:03):

does it work with rational functions?

view this post on Zulip Adam Topaz (Jan 01 2021 at 22:03):

Yeah

view this post on Zulip Adam Topaz (Jan 01 2021 at 22:04):

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

view this post on Zulip Mario Carneiro (Jan 01 2021 at 22:04):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Jan 01 2021 at 22:05):

or greater

view this post on Zulip Adam Topaz (Jan 01 2021 at 22:05):

No, it needs to be less than 1

view this post on Zulip Adam Topaz (Jan 01 2021 at 22:05):

The triangle inequality won't work otherwise

view this post on Zulip 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