# mathlib3documentation

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:

• f preserves the naturals/integers in α and β because it's a ring hom.
• f preserves what's between n and n + 1 because it's monotone.

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]
@[protected, instance]

Equations
Instances for counterexample.int_with_epsilon
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
The ordered ring homomorphisms from ℤ[ε] to ℤ that "forgets" the εs.
The floor of n - ε is n - 1 but its image under forget_epsilons is n, whose floor is itself.
The ceil of n + ε is n + 1 but its image under forget_epsilons is n, whose ceil is itself.