IMO 2012 A5 (Case 3: char(R) ∣ 2)

We solve the case where f is reduced good and char(R) ∣ 2.

TODO: Optimize/clean up the proofs if possible, starting from R_elts_claim1.

General lemmas

theorem IMOSL.IMO2012A5.Generalization.Case3.Eq1 {R : Type u_2} {S : Type u_1} [Semiring R] [Extra.CharTwo R] [Ring S] {f : R → S} (hf : NontrivialGood f) (x : R) : f (x * (x + 1) + 1) = f x * f (x + 1)

(3.1)

theorem IMOSL.IMO2012A5.Generalization.Case3.Eq2 {R : Type u_2} {S : Type u_1} [Semiring R] [Extra.CharTwo R] [Ring S] {f : R → S} (hf : NontrivialGood f) (x : R) : f (x * x + 1) = f x ^ 2 - 1

(3.2)

theorem IMOSL.IMO2012A5.Generalization.Case3.Eq2_v2 {R : Type u_2} {S : Type u_1} [Semiring R] [Extra.CharTwo R] [Ring S] {f : R → S} (hf : NontrivialGood f) (x : R) : f (x * x) = f (x + 1) ^ 2 - 1

theorem IMOSL.IMO2012A5.Generalization.Case3.Eq3 {R : Type u_2} {S : Type u_1} [Semiring R] [Extra.CharTwo R] [Ring S] {f : R → S} (hf : NontrivialGood f) (x : R) : f x * f (x * x + x) = (f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)

(3.3)

theorem IMOSL.IMO2012A5.Generalization.Case3.Eq3_v2 {R : Type u_2} {S : Type u_1} [Semiring R] [Extra.CharTwo R] [Ring S] {f : R → S} (hf : NontrivialGood f) (x : R) : f (x + 1) * f (x * x + x) = (f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x

Lemmas in commutative case

theorem IMOSL.IMO2012A5.Generalization.Case3.CommCase.Thm1_ring_id1 {S : Type u_1} [CommRing S] (a b : S) : a * ((a ^ 2 - 1) * (a - 1) + b * a) - b * ((b ^ 2 - 1) * (b - 1) + a * b) = (a ^ 2 + b ^ 2 - 1) * (a + b - 1) * (a - b)

Big ring identity 1 used in Thm1

theorem IMOSL.IMO2012A5.Generalization.Case3.CommCase.Thm1_ring_id2 {S : Type u_1} [CommRing S] (a : S) : a ^ 2 * ((a ^ 2 - 1) ^ 2 + 1) - ((a ^ 2 - 1) * (a - 1) + a * a) ^ 2 = (1 - 2 * a) * (a ^ 2 - 1)

Big ring identity 2 used in Thm1

theorem IMOSL.IMO2012A5.Generalization.Case3.CommCase.Thm1 {R : Type u_2} {S : Type u_1} [CommSemiring R] [Extra.CharTwo R] [CommRing S] [NoZeroDivisors S] {f : R → S} (hf : NontrivialGood f) (x : R) : f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1

(3.4)

theorem IMOSL.IMO2012A5.Generalization.Case3.CommCase.SCharTwo_map_add_one {R : Type u_2} {S : Type u_1} [CommSemiring R] [Extra.CharTwo R] [CommRing S] [NoZeroDivisors S] {f : R → S} (hf : NontrivialGood f) [Extra.CharTwo S] (x : R) : f (x + 1) = f x + 1

Main theorem 1: We are (almost!) done if char(S) ∣ 2

theorem IMOSL.IMO2012A5.Generalization.Case3.CommCase.pow_four_Eq1 {R : Type u_2} {S : Type u_1} [CommSemiring R] [Extra.CharTwo R] [CommRing S] {f : R → S} (hf : NontrivialGood f) (x : R) : f ((x ^ 2) ^ 2) = (f x ^ 2 - 1) ^ 2 - 1

theorem IMOSL.IMO2012A5.Generalization.Case3.CommCase.pow_four_Eq2 {R : Type u_2} {S : Type u_1} [CommSemiring R] [Extra.CharTwo R] [CommRing S] {f : R → S} (hf : NontrivialGood f) (x : R) : f ((x ^ 2) ^ 2 + 1) = (f (x + 1) ^ 2 - 1) ^ 2 - 1

theorem IMOSL.IMO2012A5.Generalization.Case3.CommCase.SCharNeTwo_main_ring_id {S : Type u_1} [CommRing S] (a b : S) : ((a - 1) ^ 2 - 1) * ((b - 1) ^ 2 - 1) - ((a * b - 1) ^ 2 - 1) = 2 * (a * b * (2 + 1 - (a + b)))

Big ring identity used in SCharNeTwo_main

theorem IMOSL.IMO2012A5.Generalization.Case3.CommCase.SCharNeTwo_cases {R : Type u_2} {S : Type u_1} [CommSemiring R] [Extra.CharTwo R] [CommRing S] [NoZeroDivisors S] {f : R → S} (hf : NontrivialGood f) (h : 2 ≠ 0) (x : R) : (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1

Main theorem 2: Case division when char(S) ∤ 2

Transferring results from commutative case

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharTwo.solution {R : Type u_2} {S : Type u_1} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] [Extra.CharTwo S] {f : R → S} (hf : NontrivialGood f) : ∃ (φ : R →+* S), ∀ (x : R), f x = φ (x - 1)

Solution for char(S) ∣ 2

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.main_cases {R : Type u_2} {S : Type u_1} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : NontrivialGood f) (x : R) : (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1

(3.5)

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq {R : Type u_2} {S : Type u_1} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : NontrivialGood f) {x : R} : f (x + 1) = 0 ↔ f x ^ 2 = 1

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.map_eq_neg_one_imp_map_add_one {R : Type u_2} {S : Type u_1} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : NontrivialGood f) {x : R} (h : f x = -1) : f (x + 1) = 0

Reduction lemmas for 𝔽₂-zeroes

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.ReductionLemmas.Lem1 {R : Type u_2} {S : Type u_1} {r : R} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : NontrivialGood f) (h : f r = -1) : f (r * r) = -1

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.ReductionLemmas.Lem2 {R : Type u_2} {S : Type u_1} {r : R} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : NontrivialGood f) (h : f r = -1) : f (r * r + r) = -1

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.ReductionLemmas.Lem3 {R : Type u_2} {S : Type u_1} {r : R} [Ring R] [Ring S] {f : R → S} (hf : NontrivialGood f) (h : f r = -1) (x : R) : f (r * x + 1) = f (r + x) - f x

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.ReductionLemmas.Lem4 {R : Type u_1} {S : Type u_2} {r : R} [Ring R] [Extra.CharTwo R] [Ring S] {f : R → S} (hf : NontrivialGood f) (h : f r = -1) {x : R} (h0 : ∃ (y : R), x = r * y + 1) : f (r * r + x) = -f x

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.ReductionLemmas.Lem5 {R : Type u_1} {S : Type u_2} {r : R} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : NontrivialGood f) (h : f r = -1) {x : R} (h0 : ∃ (y : R), x = r * r * y + 1) : f ((r * r + r) * (r * r + r) + x) = f x

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.ReductionLemmas.Lem6 {R : Type u_1} {S : Type u_2} {r : R} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : NontrivialGood f) (h : f r = -1) : QuasiPeriodic f (r * r * (r + 1))

Characterization of elements of R

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.map_eq_neg_one_reduced_imp {R : Type u_2} {S : Type u_1} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : ReducedGood f) {r : R} (h : f r = -1) : r = 0

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.map_add_one_eq_zero_imp {R : Type u_2} {S : Type u_1} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : ReducedGood f) {x : R} (h : f (x + 1) = 0) : x * x = 0

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.reduced_eq_zero_iff {R : Type u_1} {S : Type u_2} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : ReducedGood f) {r : R} : r = 0 ↔ f r = -1

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.reduced_𝔽₂ε_iff {R : Type u_1} {S : Type u_2} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : ReducedGood f) {r : R} : r * r = 0 ↔ f (r + 1) = 0

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.reduced_𝔽₄_iff {R : Type u_1} {S : Type u_2} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : ReducedGood f) {r : R} : r * (r + 1) + 1 = 0 ↔ f r + f (r + 1) = 1 ∧ f r * f (r + 1) = -1

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.R_elts_cases {R : Type u_1} {S : Type u_2} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : ReducedGood f) (r : R) : ((r + 1) * (r + 1) = 0 ∨ r * r = 0) ∨ r * (r + 1) + 1 = 0

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.R_elts_claim1 {R : Type u_1} {S : Type u_2} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : ReducedGood f) {r s : R} (hr : r * r = 0) (hs : s * s = 0) : r = 0 ∨ s = 0 ∨ r = s

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.R_elts_claim2 {R : Type u_1} {S : Type u_2} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : ReducedGood f) {r s : R} (hr : r * r = 0) (hs : s * (s + 1) + 1 = 0) : r = 0

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.𝔽₂_solution {R : Type u_1} {S : Type u_2} [Ring R] [Extra.CharTwo R] [Ring S] (hS : 2 ≠ 0) {f : R → S} (hf : ReducedGood f) (hR : ∀ (r : R), r = 0 ∨ r = 1) : ∃ (φ : R →+* 𝔽₂), ∀ (x : R), f x = ↑(𝔽₂Map (φ x))

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.𝔽₂ε_solution {R : Type u_1} {S : Type u_2} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : ReducedGood f) {r : R} (hr : r ≠ 0) (hr0 : r * r = 0) : ∃ (φ : R →+* 𝔽₂ε), ∀ (x : R), f x = ↑(𝔽₂εMap (φ x))

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.𝔽₄_solution {R : Type u_1} {S : Type u_2} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : ReducedGood f) {r : R} (hr : r * (r + 1) + 1 = 0) : ∃ (φ : R →+* 𝔽₄) (ι : ℤφ →+* S), ∀ (x : R), f x = ι (𝔽₄Map (φ x))

theorem IMOSL.IMO2012A5.Generalization.Case3.SCharNeTwo.solution {R : Type u_1} {S : Type u_2} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] (hS : 2 ≠ 0) {f : R → S} (hf : ReducedGood f) : (∃ (φ : R →+* 𝔽₂ε), ∀ (x : R), f x = ↑(𝔽₂εMap (φ x))) ∨ (∃ (φ : R →+* 𝔽₄) (ι : ℤφ →+* S), ∀ (x : R), f x = ι (𝔽₄Map (φ x))) ∨ ∃ (φ : R →+* 𝔽₂), ∀ (x : R), f x = ↑(𝔽₂Map (φ x))

Summary

theorem IMOSL.IMO2012A5.Generalization.Case3.solution {R : Type u_1} {S : Type u_2} [Ring R] [Extra.CharTwo R] [Ring S] [NoZeroDivisors S] {f : R → S} (hf : ReducedGood f) : (∃ (φ : R →+* S), ∀ (x : R), f x = φ (x - 1)) ∨ (∃ (φ : R →+* 𝔽₂ε), ∀ (x : R), f x = ↑(𝔽₂εMap (φ x))) ∨ (∃ (φ : R →+* 𝔽₄) (ι : ℤφ →+* S), ∀ (x : R), f x = ι (𝔽₄Map (φ x))) ∨ ∃ (φ : R →+* 𝔽₂), ∀ (x : R), f x = ↑(𝔽₂Map (φ x))