The Artin–Schreier map t ↦ t² + t on a finite ring

On a finite nontrivial ring, the map t ↦ t² + t is not surjective: it sends both 0 and -1 to zero. This supplies residue-field witnesses for local square and norm arguments.

On a finite commutative local ring of characteristic two the map is additive with kernel {0, 1}, so its range has index two: the sum of two elements outside the range lies in the range. Over the residue field, this makes the unramified quadratic class of a dyadic local field unique.

theorem TauCeti.exists_not_mem_range_sq_add_self (R : Type u_1) [Ring R] [Finite R] [Nontrivial R] : ∃ (a : R), a ∉ Set.range fun (t : R) => t ^ 2 + t

The map t ↦ t² + t has a value outside its range on every finite nontrivial ring.

theorem TauCeti.index_range_frobenius_two_add_id (R : Type u_1) [CommRing R] [IsLocalRing R] [Finite R] [CharP R 2] : ((frobenius R 2).toAddMonoidHom + AddMonoidHom.id R).range.index = 2

On a finite commutative local ring of characteristic two, the Artin–Schreier map frobenius R 2 + id has range of index two.

theorem TauCeti.add_mem_range_sq_add_self {R : Type u_1} [CommRing R] [IsLocalRing R] [Finite R] [CharP R 2] {a b : R} (ha : a ∉ Set.range fun (t : R) => t ^ 2 + t) (hb : b ∉ Set.range fun (t : R) => t ^ 2 + t) : a + b ∈ Set.range fun (t : R) => t ^ 2 + t

On a finite commutative local ring of characteristic two, the sum of two elements outside the range of t ↦ t² + t lies in the range.