IMO 2012 A5

Let $S$ be an integral domain. Find all functions $f : ℝ → S$ such that $f(-1) ≠ 0$ and for any $x, y ∈ ℝ$, $$ f(xy + 1) = f(x) f(y) + f(x + y). $$

Answer

$f(x) = φ(x) - 1$ for some ring homomorphism $φ : ℝ → S$.

Solution

We follow the official solution. We skip (4) and immediately prove that the function $g(x) = f(x) + 1$ is odd. The method essentially follows from the official solution as well.

Note that the only ring homomorphism from $ℝ$ to itself is the identity map. However, we have to add a step of showing that $S$ cannot have characteristic $2$. This is done when obtaining $g(1 + xy) = 1 + g(x) g(y)$, where again $g(x) = f(x) + 1$.

Generalization

Several AoPS users have also solved the problem without the assumption $f(-1) ≠ 0$. See this thread. In particular, the only extra functions are $f ≡ 0$ and $f(x) = x^2 - 1$.

It is even possible to find all functions $f : R → S$ satisfying the functional equation, where $R$ is a ring and $S$ is a domain; no commutativity is assumed. See IMOSLLean4/Generalization/IMO2012A5/IMO2012A5.lean for the implementation.

def IMOSL.IMO2012A5.good {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R → S) : Prop

A function f : R → S is called good if f(xy + 1) = f(x) f(y) + f(x + y) for all x, y ∈ R.

Equations

• IMOSL.IMO2012A5.good f = ∀ (x y : R), f (x * y + 1) = f x * f y + f (x + y)

def IMOSL.IMO2012A5.good' {R : Type u_1} {S : Type u_2} [Semiring R] [Ring S] (g : R → S) : Prop

A function g : R → S is called good' if g(xy + 1) = (g(x) - 1)(g(y) - 1) + g(x + y) for all x, y ∈ R.

Equations

• IMOSL.IMO2012A5.good' g = ∀ (x y : R), g (x * y + 1) = (g x - 1) * (g y - 1) + g (x + y)

theorem IMOSL.IMO2012A5.good_iff_good' {R : Type u_1} {S : Type u_2} [Semiring R] [Ring S] {f : R → S} : good f ↔ good' fun (x : R) => f x + 1

f is good if and only if f + 1 is good'.

theorem IMOSL.IMO2012A5.RingHom_is_good' {R : Type u_1} {S : Type u_2} [Semiring R] [Ring S] (φ : R →+* S) : good' ⇑φ

A ring homomorphism is always good'.

theorem IMOSL.IMO2012A5.good'.eq2_map_one_sub {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {g : R → S} (hg : good' g) (x : R) : g (1 - x) = (g (-1) - 1) * (g x - 1) + g (x - 1)

If g : R → S is good', then g(1 - x) = (g(-1) - 1)(g(x) - 1) + g(x - 1).

theorem IMOSL.IMO2012A5.good'.map_one_eq_one {R : Type u_2} {S : Type u_1} [Ring R] [Ring S] [IsDomain S] {g : R → S} (hg : good' g) (hg0 : g (-1) ≠ 1) : g 1 = 1

If g : R → S is good' and g(-1) ≠ 1, then g(1) = 1.

theorem IMOSL.IMO2012A5.good'.map_zero_eq_zero {R : Type u_2} {S : Type u_1} [Ring R] [Ring S] [IsDomain S] {g : R → S} (hg : good' g) (hg0 : g (-1) ≠ 1) : g 0 = 0

If g : R → S is good' and g(-1) ≠ 1, then g(0) = 0.

theorem IMOSL.IMO2012A5.good'.eq3_map_one_add_add_map_one_sub {R : Type u_2} {S : Type u_1} [Ring R] [Ring S] [IsDomain S] {g : R → S} (hg : good' g) (hg0 : g (-1) ≠ 1) (x : R) : g (1 + x) + g (1 - x) = 2

If g : R → S is good', then g(1 + x) + g(1 - x) = 2 for all x.

theorem IMOSL.IMO2012A5.good'.Real_odd {S : Type u_1} [Ring S] [IsDomain S] {g : ℝ → S} (hg : good' g) (hg0 : g (-1) ≠ 1) (x : ℝ) : g (-x) = -g x

If g : ℝ → S is good' and g(-1) ≠ 1, then g is odd.

theorem IMOSL.IMO2012A5.good'.Real_is_hom {S : Type u_1} [Ring S] [IsDomain S] {g : ℝ → S} (hg : good' g) (hg0 : g (-1) ≠ 1) : ∃ (φ : ℝ →+* S), g = ⇑φ

If g : ℝ → S is good' and g(-1) ≠ 1, then g is a ring homomorphism.

theorem IMOSL.IMO2012A5.good'_Real_iff {S : Type u_1} [Ring S] [IsDomain S] {g : ℝ → S} : good' g ∧ g (-1) ≠ 1 ↔ ∃ (φ : ℝ →+* S), g = ⇑φ

A function g : ℝ → S is good' with g(-1) ≠ 1 if and only if g is a ring homomorphism.

theorem IMOSL.IMO2012A5.final_solution {S : Type u_1} [Ring S] [IsDomain S] {f : ℝ → S} : good f ∧ f (-1) ≠ 0 ↔ ∃ (φ : ℝ →+* S), f = fun (x : ℝ) => φ x - 1

Final solution