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

source
@[protected, instance]
noncomputable def counterexample.int_with_epsilon.inhabited  :
inhabited counterexample.int_with_epsilon
source
@[protected, instance]
noncomputable def counterexample.int_with_epsilon.comm_ring  :
comm_ring counterexample.int_with_epsilon
source
def counterexample.int_with_epsilon  :
Type

The integers with infinitesimals adjoined.

Equations
Instances for counterexample.int_with_epsilon
source
@[protected, instance]
def counterexample.int_with_epsilon.nontrivial  :
nontrivial counterexample.int_with_epsilon
source
@[protected, instance]
noncomputable def counterexample.int_with_epsilon.linear_order  :
linear_order counterexample.int_with_epsilon
Equations
source
@[protected, instance]
noncomputable def counterexample.int_with_epsilon.ordered_add_comm_group  :
ordered_add_comm_group counterexample.int_with_epsilon
Equations
source
theorem counterexample.int_with_epsilon.pos_iff {p : counterexample.int_with_epsilon} :
0 < p ↔ 0 < polynomial.trailing_coeff p
source
@[protected, instance]
noncomputable def counterexample.int_with_epsilon.linear_ordered_comm_ring  :
linear_ordered_comm_ring counterexample.int_with_epsilon
Equations
source
@[protected, instance]
noncomputable def counterexample.int_with_epsilon.floor_ring  :
floor_ring counterexample.int_with_epsilon
Equations
source
def counterexample.int_with_epsilon.forget_epsilons  :
counterexample.int_with_epsilon →+*o ℤ

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

Equations
source
@[simp]
theorem counterexample.int_with_epsilon.forget_epsilons_apply (p : counterexample.int_with_epsilon) :
⇑counterexample.int_with_epsilon.forget_epsilons p = polynomial.coeff p 0
source
theorem counterexample.int_with_epsilon.forget_epsilons_floor_lt (n : ℤ) :
⇑counterexample.int_with_epsilon.forget_epsilons ↑⌊↑n - polynomial.X⌋ < ⌊⇑counterexample.int_with_epsilon.forget_epsilons (↑n - polynomial.X)⌋

The floor of n - ε is n - 1 but its image under forget_epsilons is n, whose floor is itself.

source
theorem counterexample.int_with_epsilon.lt_forget_epsilons_ceil (n : ℤ) :
⌈⇑counterexample.int_with_epsilon.forget_epsilons (↑n + polynomial.X)⌉ < ⇑counterexample.int_with_epsilon.forget_epsilons ↑⌈↑n + polynomial.X⌉

The ceil of n + ε is n + 1 but its image under forget_epsilons is n, whose ceil is itself.