# Documentation

Counterexamples.MapFloor

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

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 ℤ[ε] (IntWithEpsilon), the integers with infinitesimals adjoined. This is a linearly ordered commutative floor ring (IntWithEpsilon.linearOrderedCommRing, IntWithEpsilon.floorRing).

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

But it does not preserve floors (nor ceils) as ⌊-ε⌋ = -1 while ⌊f (-ε)⌋ = ⌊0⌋ = 0 (IntWithEpsilon.forgetEpsilons_floor_lt, IntWithEpsilon.lt_forgetEpsilons_ceil).

The ordered ring homomorphisms from ℤ[ε] to ℤ that "forgets" the εs.
The floor of n - ε is n - 1 but its image under forgetEpsilons is n, whose floor is itself.
The ceil of n + ε is n + 1 but its image under forgetEpsilons is n, whose ceil is itself.