## Stream: maths

### Topic: floor_ring

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

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

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


#### Mario Carneiro (Feb 04 2019 at 10:58):

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

#### Kevin Buzzard (Feb 04 2019 at 10:58):

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

#### Kevin Buzzard (Feb 04 2019 at 10:58):

You mean we don't have the instance?

#### Mario Carneiro (Feb 04 2019 at 10:59):

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

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

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

#### Kevin Buzzard (Feb 04 2019 at 11:02):

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

#### Kevin Buzzard (Feb 04 2019 at 11:03):

A weaker question is: is every floor_ring commutative.

#### Sebastien Gouezel (Feb 04 2019 at 11:04):

Is every floor_ring a subring of the reals?.

What about reals with an infinitesimal t?

#### Kevin Buzzard (Feb 04 2019 at 11:04):

Right -- this is what I thought originally.

#### Kevin Buzzard (Feb 04 2019 at 11:04):

But what is the floor of 1/t?

#### Mario Carneiro (Feb 04 2019 at 11:04):

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

#### Mario Carneiro (Feb 04 2019 at 11:05):

where t is infinitesimal

#### Kevin Buzzard (Feb 04 2019 at 11:05):

Now there's a good candidate.

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

#### Kevin Buzzard (Feb 04 2019 at 11:05):

So maybe the question is whether every floor_division_ring is commutative.

#### Kevin Buzzard (Feb 04 2019 at 11:06):

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

#### Mario Carneiro (Feb 04 2019 at 11:06):

that should be enough to get archimedean, at least

#### Kevin Buzzard (Feb 04 2019 at 11:07):

Does archimedean imply "embeds in the reals"??

#### Mario Carneiro (Feb 04 2019 at 11:07):

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

#### Mario Carneiro (Feb 04 2019 at 11:07):

just keep multiplying by 10 and floor

#### Kevin Buzzard (Feb 04 2019 at 11:08):

right! But are we assuming commutative here?

#### Mario Carneiro (Feb 04 2019 at 11:08):

and you get a decimal expansion for a real

wait

#### Kevin Buzzard (Feb 04 2019 at 11:08):

Z[t] is archimedean, I guess?

#### Mario Carneiro (Feb 04 2019 at 11:09):

not by mathlib definition

#### Mario Carneiro (Feb 04 2019 at 11:09):

that's what the two variables are for

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

#### Mario Carneiro (Feb 04 2019 at 11:10):

how do they compare?

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

#### Kevin Buzzard (Feb 04 2019 at 11:10):

One is bigger than the other one.

Much bigger.

#### Mario Carneiro (Feb 04 2019 at 11:10):

and s * t < t * s?

#### Kevin Buzzard (Feb 04 2019 at 11:10):

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

#### Kevin Buzzard (Feb 04 2019 at 11:11):

Maybe you order monomials lexicographically.

#### Kevin Buzzard (Feb 04 2019 at 11:11):

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

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

#### Mario Carneiro (Feb 04 2019 at 11:13):

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

#### Mario Carneiro (Feb 04 2019 at 11:14):

aha you might want decidable_linear_ordered_comm_ring

#### Mario Carneiro (Feb 04 2019 at 11:14):

oh wait linear_ordered_comm_ring is there too

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

#### Kevin Buzzard (Feb 04 2019 at 11:15):

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

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

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

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

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

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

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

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

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