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

def Counterexample.IntWithEpsilon : Type

The integers with infinitesimals adjoined.

Equations

• Counterexample.IntWithEpsilon = Polynomial ℤ

instance Counterexample.instNontrivialIntWithEpsilon : Nontrivial IntWithEpsilon

Equations

• Counterexample.instNontrivialIntWithEpsilon = ⋯

instance Counterexample.instCommRingIntWithEpsilon : CommRing IntWithEpsilon

Equations

• Counterexample.instCommRingIntWithEpsilon = Polynomial.commRing

instance Counterexample.instInhabitedIntWithEpsilon : Inhabited IntWithEpsilon

Equations

• Counterexample.instInhabitedIntWithEpsilon = Polynomial.inhabited

instance Counterexample.IntWithEpsilon.linearOrder : LinearOrder IntWithEpsilon

Equations

• Counterexample.IntWithEpsilon.linearOrder = LinearOrder.lift' (⇑toLex ∘ Polynomial.coeff) ⋯

instance Counterexample.IntWithEpsilon.isOrderedAddMonoid : IsOrderedAddMonoid IntWithEpsilon

theorem Counterexample.IntWithEpsilon.pos_iff {p : IntWithEpsilon} : 0 < p ↔ 0 < Polynomial.trailingCoeff p

instance Counterexample.IntWithEpsilon.instZeroLEOneClass : ZeroLEOneClass IntWithEpsilon

instance Counterexample.IntWithEpsilon.instIsStrictOrderedRing : IsStrictOrderedRing IntWithEpsilon

instance Counterexample.IntWithEpsilon.instFloorRing : FloorRing IntWithEpsilon

Equations

• One or more equations did not get rendered due to their size.

def Counterexample.IntWithEpsilon.forgetEpsilons : IntWithEpsilon →+*o ℤ

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Counterexample.IntWithEpsilon.forgetEpsilons_apply (p : IntWithEpsilon) : forgetEpsilons p = Polynomial.coeff p 0

theorem Counterexample.IntWithEpsilon.forgetEpsilons_floor_lt (n : ℤ) : forgetEpsilons ↑⌊↑n - Polynomial.X⌋ < ⌊forgetEpsilons (↑n - Polynomial.X)⌋

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

theorem Counterexample.IntWithEpsilon.lt_forgetEpsilons_ceil (n : ℤ) : ⌈forgetEpsilons (↑n + Polynomial.X)⌉ < forgetEpsilons ↑⌈↑n + Polynomial.X⌉

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