algebra problem

Stream: maths

[Heather Macbeth]

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

[Adam Topaz]

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

[Heather Macbeth]

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

[Mario Carneiro]

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

[Adam Topaz]

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]

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]

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

[Mario Carneiro]

oh, that assumption implies that it is at least infinite

[Adam Topaz]

Or "non-trivially-normed" field

[Heather Macbeth]

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

[Adam Topaz]

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

[Mario Carneiro]

what happens with the padic norm on Qp?

[Adam Topaz]

Same. But that char 0

[Adam Topaz]

The same norm works for rational functions

[Mario Carneiro]

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

[Mario Carneiro]

does it work with rational functions?

[Adam Topaz]

Yeah

[Adam Topaz]

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

[Mario Carneiro]

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

[Adam Topaz]

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]

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

[Mario Carneiro]

or greater

[Adam Topaz]

No, it needs to be less than 1

[Adam Topaz]

The triangle inequality won't work otherwise

[Adam Topaz]

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