IMO 2010 A1 (P1)

A ring with floor is a totally ordered ring $R$ with a floor function $⌊⬝⌋ : R → ℤ$ such that for any $x ∈ R$ and $n ∈ ℤ$, we have $⌊x⌋ ≤ n$ if and only if $x ≤ n_R$. (See FloorRing for the formal definition.)

Let $R$ and $S$ be totally ordered rings with floor. Suppose that there exists $α ∈ R$ such that $0 < α < 1$. Find all functions $f : R → S$ such that for any $x, y ∈ R$, $$ f(⌊x⌋ y) = ⌊f(y)⌋ f(x). $$

Answer

$f ≡ 0$ and $f ≡ C$ for some constant $C ∈ S$ with $⌊C⌋ = 1$.

Solution

Plugging $(x, y) = (0, 0)$ yields either $f(0) = 0$ or $⌊f(0)⌋ = 1$. In the case $⌊f(0)⌋ = 1$, plugging $y = 0$ yields that $f ≡ C$ for some constant $C$. Note that $C = f(0)$, so $⌊C⌋ = ⌊f(0)⌋ = 1$.

Now assume that $f(0) = 0$. Fix some $α ∈ R$ such that $0 < α < 1$. Plugging $x = y = α$ yields $⌊f(α)⌋ f(α) = f(0) = 0$ and so $⌊f(α)⌋ = 0$. Plugging $(x, y) = (-1, α)$ then yields $f(-α) = 0$. Finally, since $⌊-α⌋ = -1$, plugging $x = -α$ gives $f ≡ 0$.

Extra

It can be shown that there exists $α ∈ R$ such that $0 < α < 1$ as long as $R$ is not isomorphic to either $ℤ$ or the trivial ring.

def IMOSL.IMO2010A1.good {R : Type u_1} {S : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [Ring S] [LinearOrder S] [FloorRing S] (f : R → S) : Prop

A function f : R → S is called good if f(⌊x⌋ y) = ⌊f(y)⌋ f(x) for all x, y : R.

Equations

• IMOSL.IMO2010A1.good f = ∀ (x y : R), f (⌊x⌋ • y) = ⌊f y⌋ • f x

theorem IMOSL.IMO2010A1.zero_is_good {R : Type u_1} {S : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [Ring S] [LinearOrder S] [FloorRing S] : good 0

The zero function is good.

theorem IMOSL.IMO2010A1.const_is_good_of_floor_eq_one {R : Type u_2} {S : Type u_1} [Ring R] [LinearOrder R] [FloorRing R] [Ring S] [LinearOrder S] [FloorRing S] {C : S} (hC : ⌊C⌋ = 1) : good fun (x : R) => C

The constant function f ≡ C is good if ⌊C⌋ = 1.

theorem IMOSL.IMO2010A1.good.floor_eq_one_or_eq_zero {R : Type u_2} {S : Type u_1} [Ring R] [LinearOrder R] [FloorRing R] [Ring S] [LinearOrder S] [FloorRing S] [IsOrderedAddMonoid S] {f : R → S} (hf : good f) : ⌊f 0⌋ = 1 ∨ f 0 = 0

We have either ⌊f(0)⌋ = 1 or f(0) = 0.

theorem IMOSL.IMO2010A1.good.eq_const_of_floor_map_zero_eq_one {R : Type u_1} {S : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [Ring S] [LinearOrder S] [FloorRing S] {f : R → S} (hf : good f) (hf0 : ⌊f 0⌋ = 1) : ∃ (C : S), ⌊C⌋ = 1 ∧ f = fun (x : R) => C

If ⌊f(0)⌋ = 1, then f is constant.

theorem IMOSL.IMO2010A1.good.eq_zero_of_map_zero_eq_zero {R : Type u_1} {S : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [Ring S] [LinearOrder S] [FloorRing S] [IsStrictOrderedRing R] (hR : ∃ (α : R), 0 < α ∧ α < 1) [IsStrictOrderedRing S] {f : R → S} (hf : good f) (hf0 : f 0 = 0) : f = 0

Suppose there exists α : R such that 0 < α < 1. Then f(0) = 0 implies f ≡ 0.

theorem IMOSL.IMO2010A1.final_solution {R : Type u_1} {S : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [Ring S] [LinearOrder S] [FloorRing S] [IsStrictOrderedRing R] (hR : ∃ (α : R), 0 < α ∧ α < 1) [IsStrictOrderedRing S] {f : R → S} : good f ↔ (∃ (C : S), ⌊C⌋ = 1 ∧ f = fun (x : R) => C) ∨ f = 0

Final solution