Additive cancellation in characteristic two

In a possibly nonassociative semiring of characteristic two, each element is its own additive inverse. Consequently addition is cancellative, even when the given semiring structure lacks additive cancellation. This supplies the cancellation needed by the grid commutation chain-map criterion. The same holds in any module over a semiring of characteristic two (TauCeti.add_self_eq_zero_of_charTwo), which is how terms appearing twice cancel in sign-free differentials.

Two consequences for quadratic equations follow. In a ring of characteristic two without zero divisors, two roots of X ^ 2 + t X - s are equal or differ by t (TauCeti.eq_or_eq_add_of_sq_add_mul_eq_of_charTwo). An algebra endomorphism over a ring of characteristic two that translates an element by a scalar is an involution on that element (AlgHom.apply_apply_of_apply_eq_add_algebraMap), as for the translations permuting these roots.

differentials, and there a + b = 0 exactly when a = b (TauCeti.add_eq_zero_iff_eq_of_charTwo).

theorem TauCeti.isCancelAdd_of_charTwo (R : Type u_1) [NonAssocSemiring R] [CharP R 2] : IsCancelAdd R

Addition in a possibly nonassociative semiring of characteristic two is cancellative.

theorem TauCeti.add_self_eq_zero_of_charTwo (R : Type u_1) {M : Type u_2} [Semiring R] [CharP R 2] [AddCommMonoid M] [Module R M] (x : M) : x + x = 0

In a module over a semiring of characteristic two, each element is its own additive inverse.

theorem TauCeti.eq_or_eq_add_of_sq_add_mul_eq_of_charTwo {S : Type u_1} [CommRing S] [NoZeroDivisors S] [CharP S 2] {t s a b : S} (ha : a ^ 2 + t * a = s) (hb : b ^ 2 + t * b = s) : b = a ∨ b = a + t

In a ring of characteristic two without zero divisors, two roots of X ^ 2 + t X - s are equal or differ by t.

theorem TauCeti.add_eq_zero_iff_eq_of_charTwo (R : Type u_1) {M : Type u_2} [Semiring R] [CharP R 2] [AddCommMonoid M] [Module R M] {a b : M} : a + b = 0 ↔ a = b

In a module over a semiring of characteristic two, a + b = 0 exactly when a = b.

theorem AlgHom.apply_apply_of_apply_eq_add_algebraMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [CharP R 2] [Semiring A] [Algebra R A] (f : A →ₐ[R] A) {x : A} {a : R} (h : f x = x + (algebraMap R A) a) : f (f x) = x

Over a ring of characteristic two, an algebra endomorphism translating x by a scalar sends x + a back to x, so applying it twice fixes x.