mathlib3 documentation

mathlib-counterexamples / map_floor

Floors and ceils aren't preserved under ordered ring homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Intuitively, if f : α → β is an ordered ring homomorphism, then floors and ceils should be preserved by f because:

However, there is a catch. Potentially something whose floor was n could get mapped to n + 1, and this has floor n + 1, not n. Note that this is at most an off by one error.

This pathology disappears if you require f to be strictly monotone or α to be archimedean.

The counterexample #

Consider ℤ[ε] (int_with_epsilons), the integers with infinitesimals adjoined. This is a linearly ordered commutative floor ring (int_with_epsilons.linear_ordered_comm_ring, int_with_epsilons.floor_ring).

The map f : ℤ[ε] → ℤ that forgets about the epsilons (int_with_epsilons.forget_epsilons) is an ordered ring homomorphism.

But it does not preserve floors (nor ceils) as ⌊-ε⌋ = -1 while ⌊f (-ε)⌋ = ⌊0⌋ = 0 (int_with_epsilons.forget_epsilons_floor_lt, int_with_epsilons.lt_forget_epsilons_ceil).

@[protected, instance]
Equations
@[protected, instance]
Equations

The ordered ring homomorphisms from ℤ[ε] to that "forgets" the εs.

Equations