floor_ring

Stream: maths

[Kevin Buzzard]

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]

class floor_ring (α) [linear_ordered_ring α] :=
(floor : α → ℤ)
(le_floor : ∀ (z : ℤ) (x : α), z ≤ floor x ↔ (z : α) ≤ x)

From algebra/archimedean.lean

[Kevin Buzzard]

One can prove

lemma eq_floor_iff_bounds (r : α) (z : ℤ) :
  ⌊r⌋ = z ↔ ↑z ≤ r ∧ r < (z + 1) := ...

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

You mean we don't have the instance?

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

A weaker question is: is every floor_ring commutative.

[Sebastien Gouezel]

Is every floor_ring a subring of the reals?.

What about reals with an infinitesimal t?

[Kevin Buzzard]

Right -- this is what I thought originally.

[Kevin Buzzard]

But what is the floor of 1/t?

[Mario Carneiro]

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

[Mario Carneiro]

where t is infinitesimal

[Kevin Buzzard]

Now there's a good candidate.

[Sebastien Gouezel]

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

[Kevin Buzzard]

So maybe the question is whether every floor_division_ring is commutative.

[Kevin Buzzard]

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

[Mario Carneiro]

that should be enough to get archimedean, at least

[Kevin Buzzard]

Does archimedean imply "embeds in the reals"??

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

just keep multiplying by 10 and floor

[Kevin Buzzard]

right! But are we assuming commutative here?

[Mario Carneiro]

and you get a decimal expansion for a real

[Kevin Buzzard]

wait

[Kevin Buzzard]

Z[t] is archimedean, I guess?

[Mario Carneiro]

not by mathlib definition

[Mario Carneiro]

that's what the two variables are for

[Kevin Buzzard]

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

[Mario Carneiro]

how do they compare?

[Kevin Buzzard]

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

[Kevin Buzzard]

One is bigger than the other one.

[Kevin Buzzard]

Much bigger.

[Mario Carneiro]

and s * t < t * s?

[Kevin Buzzard]

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

[Kevin Buzzard]

Maybe you order monomials lexicographically.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

aha you might want decidable_linear_ordered_comm_ring

[Mario Carneiro]

oh wait linear_ordered_comm_ring is there too

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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