Zulip Chat Archive

Stream: maths

Topic: floor_ring


view this post on Zulip Kevin Buzzard (Feb 04 2019 at 10:55):

Is every floor_ring a subring of the reals? Note that a floor_ring is not assumed commutative! But for a general floor_ring it is proved in the library that floor x <= x < (floor x) + 1.

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 10:56):

class floor_ring (α) [linear_ordered_ring α] :=
(floor : α  )
(le_floor :  (z : ) (x : α), z  floor x  (z : α)  x)

From algebra/archimedean.lean

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 10:57):

One can prove

lemma eq_floor_iff_bounds (r : α) (z : ) :
  r = z  z  r  r < (z + 1) := ...

view this post on Zulip Mario Carneiro (Feb 04 2019 at 10:58):

I just noticed we don't even have that floor_ring implies archimedean

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 10:58):

it's part of the definition in some sense, right?

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 10:58):

You mean we don't have the instance?

view this post on Zulip Mario Carneiro (Feb 04 2019 at 10:59):

not exactly... the definition of archimedean uses two variables from the ring

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 10:59):

Sorry I'm talking nonsense. It's linear_ordered_ring which is part of the definition. I was going to delete my comments but then you replied too quickly :-)

view this post on Zulip Mario Carneiro (Feb 04 2019 at 10:59):

only when you have a field does it reduce to the one variable version i.e. archimedean_iff_nat_le which is obviously implied by a floor ring

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:02):

So this is another maths question, right? Are all floor_rings archimedean?

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:03):

A weaker question is: is every floor_ring commutative.

view this post on Zulip Sebastien Gouezel (Feb 04 2019 at 11:04):

Is every floor_ring a subring of the reals?.

What about reals with an infinitesimal t?

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:04):

Right -- this is what I thought originally.

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:04):

But what is the floor of 1/t?

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:04):

Also isn't Z[t] a floor ring?

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:05):

where t is infinitesimal

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:05):

Now there's a good candidate.

view this post on Zulip Sebastien Gouezel (Feb 04 2019 at 11:05):

t is not invertible in this example, so 1/t is zero, so the floor of 1/t is zero.

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:05):

So maybe the question is whether every floor_division_ring is commutative.

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:06):

OK but this is great, not every floor_ring is a subring of the reals.

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:06):

that should be enough to get archimedean, at least

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:07):

Does archimedean imply "embeds in the reals"??

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:07):

I realise I know nothing about this stuff. I have been non-archimedean all my life.

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:07):

there's a floor function, seems like a good start

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:07):

just keep multiplying by 10 and floor

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:08):

right! But are we assuming commutative here?

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:08):

and you get a decimal expansion for a real

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:08):

wait

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:08):

Z[t] is archimedean, I guess?

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:09):

not by mathlib definition

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:09):

that's what the two variables are for

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:09):

Hey, can we have non-commuting infinitesimals, to give me a non-commuting floor_ring? I bet we can.

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:10):

how do they compare?

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:10):

I had ruled out infinitesimals because of my 1/t error so my thoughts on this are all out of whack.

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:10):

One is bigger than the other one.

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:10):

Much bigger.

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:10):

and s * t < t * s?

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:10):

This is the heart of the matter isn't it.

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:11):

Maybe you order monomials lexicographically.

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:11):

I could imagine this being preserved under pre and post multiplication by infinitesimals.

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:13):

OK I think the thing to do in my decimal expansion thing is just to allow non-commutative rings until it starts becoming painful and then just add in the commutativity assumption.

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:13):

requires a bit more formalization, but I think it checks out

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:14):

aha you might want decidable_linear_ordered_comm_ring

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:14):

oh wait linear_ordered_comm_ring is there too

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:14):

Yes, I discovered it when I was trying to debug why linarith couldn't prove s >= 0 -> r - s <= r in the other thread!

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:15):

[answer: default ring discharger wouldn't run because underlying ring was not commutative]

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:16):

I think linarith isn't really designed for noncomm rings, since it uses ring as part of completeness

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:17):

Right, so when things start getting hairy to the extent that simp won't discharge things, I'll give in and switch to commutative rings.

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:17):

We could extend ring to noncomm rings, but I'm not sure how useful that is. It seems like it would just be a combination of abel and cc on the monomials

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 11:19):

I meant to get all this done over the weekend so I could work on the perfectoid project today, but I didn't quite finish, and I really want to do it because modulo decimal expansions we have the entire questions and solutions for my final exam, and this is too cool to go unignored. When I started here we had no sine and cosine so we couldn't even formalise the questions. Ever since my birthday I've been desperate to formalise this final exam but I've been in teaching / admin hell which I am now finally out of.

view this post on Zulip Sebastien Gouezel (Feb 07 2019 at 10:33):

I just noticed that floor is defined on rings, but the definition does not involve the multiplication at all. Shouldn't it be defined on linear_order_add_comm_group or something like that instead?

view this post on Zulip Kevin Buzzard (Feb 07 2019 at 10:37):

floor takes values in Z so we need a group with a 1, but I am not sure we need the ring structure.

view this post on Zulip Sebastien Gouezel (Feb 07 2019 at 10:46):

Anyway, the only interesting examples are rationals and reals, so defining it on rings does no harm. We could even define it directly on decidable_linear_ordered_comm_ring.

view this post on Zulip Kevin Buzzard (Feb 07 2019 at 12:06):

Because Mario (I think) had already made the decision on what a floor_ring was, I just went with that when it came to fractional parts. The fact that I later on discovered that the rings were not necessarily commutative just meant that I had to be slightly more careful and could use slightly fewer tactics (i.e. no ring).


Last updated: May 06 2021 at 18:20 UTC