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.instIntWithEpsilonNontrivial : Nontrivial Counterexample.IntWithEpsilon

Equations

• Counterexample.instIntWithEpsilonNontrivial = ⋯

instance Counterexample.IntWithEpsilon.nontrivial : Nontrivial Counterexample.IntWithEpsilon

Equations

• Counterexample.IntWithEpsilon.nontrivial = ⋯

instance Counterexample.IntWithEpsilon.commRing : CommRing Counterexample.IntWithEpsilon

Equations

• Counterexample.IntWithEpsilon.commRing = Polynomial.commRing

instance Counterexample.IntWithEpsilon.inhabited : Inhabited Counterexample.IntWithEpsilon

Equations

• Counterexample.IntWithEpsilon.inhabited = { default := 69 }

instance Counterexample.IntWithEpsilon.linearOrder : LinearOrder Counterexample.IntWithEpsilon

Equations

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

instance Counterexample.IntWithEpsilon.orderedAddCommGroup : OrderedAddCommGroup Counterexample.IntWithEpsilon

Equations

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

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

instance Counterexample.IntWithEpsilon.instLinearOrderedCommRing : LinearOrderedCommRing Counterexample.IntWithEpsilon

Equations

• Counterexample.IntWithEpsilon.instLinearOrderedCommRing = LinearOrderedCommRing.mk ⋯

instance Counterexample.IntWithEpsilon.instFloorRing : FloorRing Counterexample.IntWithEpsilon

Equations

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

def Counterexample.IntWithEpsilon.forgetEpsilons : Counterexample.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 : Counterexample.IntWithEpsilon) : Counterexample.IntWithEpsilon.forgetEpsilons p = Polynomial.coeff p 0

theorem Counterexample.IntWithEpsilon.forgetEpsilons_floor_lt (n : ℤ) : Counterexample.IntWithEpsilon.forgetEpsilons ↑⌊↑n - Polynomial.X⌋ < ⌊Counterexample.IntWithEpsilon.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 : ℤ) : ⌈Counterexample.IntWithEpsilon.forgetEpsilons (↑n + Polynomial.X)⌉ < Counterexample.IntWithEpsilon.forgetEpsilons ↑⌈↑n + Polynomial.X⌉

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