Two.lean

/-
Copyright (c) 2021 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser
-/
module

public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Ring.Parity

/-!
# Lemmas about rings of characteristic two

This file contains results about `CharP R 2`, in the `CharTwo` namespace.

The lemmas in this file with a `_sq` suffix are just special cases of the `_pow_char` lemmas
elsewhere, with a shorter name for ease of discovery, and no need for a `[Fact (Prime 2)]` argument.
-/

public section

-- TODO: `assert_not_exists Field` is added because of `Mathlib.GroupTheory.OrderOfElement`.
-- If you want to import fields here, please refactor the import hierarchy for
-- `Mathlib.GroupTheory.OrderOfElement`.
assert_not_exists Algebra LinearMap Field

variable {R ι : Type*}

namespace CharTwo

section AddMonoidWithOne

variable [AddMonoidWithOne R]

/-- The only hypotheses required to build a `CharP R 2` instance are `1 ≠ 0` and `2 = 0`. -/
theorem of_one_ne_zero_of_two_eq_zero (h₁ : (1 : R) ≠ 0) (h₂ : (2 : R) = 0) : CharP R 2 where
  cast_eq_zero_iff n := by
    obtain hn | hn := Nat.even_or_odd n
    · simp_rw [hn.two_dvd, iff_true]
      exact natCast_eq_zero_of_even_of_two_eq_zero hn h₂
    · simp_rw [hn.not_two_dvd_nat, iff_false]
      rwa [natCast_eq_one_of_odd_of_two_eq_zero hn h₂]

variable [CharP R 2]

@[scoped simp]
theorem two_eq_zero : (2 : R) = 0 := by
  rw [← Nat.cast_two, CharP.cast_eq_zero]

theorem natCast_eq_ite (n : ℕ) : (n : R) = if Even n then 0 else 1 := by
  induction n <;> aesop (add simp [one_add_one_eq_two])

@[simp]
theorem range_natCast : Set.range ((↑) : ℕ → R) = {0, 1} := by
  rw [funext natCast_eq_ite, Set.range_ite_const]
  · use 0; simp
  · use 1; simp

variable (R) in
theorem natCast_cases (n : ℕ) : (n : R) = 0 ∨ (n : R) = 1 :=
  range_natCast.le (Set.mem_range_self _)

theorem natCast_eq_mod (n : ℕ) : (n : R) = (n % 2 : ℕ) := by
  simp [natCast_eq_ite, Nat.even_iff]

set_option warning.simp.varHead false in
@[scoped simp]
theorem ofNat_eq_mod (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R) = (ofNat(n) % 2 : ℕ) :=
  natCast_eq_mod n

example : (37 : R) = 1 := by simp

end AddMonoidWithOne

section Semiring

variable [Semiring R] [CharP R 2]

@[scoped simp]
theorem add_self_eq_zero (x : R) : x + x = 0 := by rw [← two_mul x, two_eq_zero, zero_mul]

@[scoped simp]
protected theorem two_nsmul (x : R) : 2 • x = 0 := by rw [two_nsmul, add_self_eq_zero]

@[scoped simp]
protected theorem add_cancel_left (a b : R) : a + (a + b) = b := by
  rw [← add_assoc, add_self_eq_zero, zero_add]

@[scoped simp]
protected theorem add_cancel_right (a b : R) : a + b + b = a := by
  rw [add_assoc, add_self_eq_zero, add_zero]

end Semiring

section Ring

variable [Ring R] [CharP R 2]

@[scoped simp]
theorem neg_eq (x : R) : -x = x := by
  rw [neg_eq_iff_add_eq_zero, add_self_eq_zero]

theorem neg_eq' : Neg.neg = (id : R → R) :=
  funext neg_eq

@[scoped simp]
theorem sub_eq_add (x y : R) : x - y = x + y := by rw [sub_eq_add_neg, neg_eq]

theorem add_eq_iff_eq_add {a b c : R} : a + b = c ↔ a = c + b := by
  rw [← sub_eq_iff_eq_add, sub_eq_add]

theorem eq_add_iff_add_eq {a b c : R} : a = b + c ↔ a + c = b := by
  rw [← eq_sub_iff_add_eq, sub_eq_add]

@[scoped simp]
protected theorem two_zsmul (x : R) : (2 : ℤ) • x = 0 := by
  rw [two_zsmul, add_self_eq_zero]

protected theorem add_eq_zero {a b : R} : a + b = 0 ↔ a = b := by
  rw [← CharTwo.sub_eq_add, sub_eq_iff_eq_add, zero_add]

theorem intCast_eq_ite (n : ℤ) : (n : R) = if Even n then 0 else 1 := by
  obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg <;> simpa using natCast_eq_ite n

@[simp]
theorem range_intCast : Set.range ((↑) : ℤ → R) = {0, 1} := by
  rw [funext intCast_eq_ite, Set.range_ite_const]
  · use 0; simp
  · use 1; simp

variable (R) in
theorem intCast_cases (n : ℤ) : (n : R) = 0 ∨ (n : R) = 1 :=
  (Set.ext_iff.1 range_intCast _).1 (Set.mem_range_self _)

theorem intCast_eq_mod (n : ℤ) : (n : R) = (n % 2 : ℤ) := by
  simp [intCast_eq_ite, Int.even_iff]

end Ring

section CommSemiring

variable [CommSemiring R] [CharP R 2]

theorem add_sq (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 := by
  simp [add_pow_two]

theorem add_mul_self (x y : R) : (x + y) * (x + y) = x * x + y * y := by
  rw [← pow_two, ← pow_two, ← pow_two, add_sq]

/-- See `frobenius` for the Frobenius map. -/
private def sqAddMonoidHom : R →+ R where
  toFun := (· ^ 2)
  map_zero' := zero_pow two_ne_zero
  map_add' := add_sq

theorem list_sum_sq (l : List R) : l.sum ^ 2 = (l.map (· ^ 2)).sum :=
  map_list_sum sqAddMonoidHom _

theorem list_sum_mul_self (l : List R) : l.sum * l.sum = (List.map (fun x => x * x) l).sum := by
  simp_rw [← pow_two, list_sum_sq]

theorem multiset_sum_sq (l : Multiset R) : l.sum ^ 2 = (l.map (· ^ 2)).sum :=
  map_multiset_sum sqAddMonoidHom _

theorem multiset_sum_mul_self (l : Multiset R) :
    l.sum * l.sum = (Multiset.map (fun x => x * x) l).sum := by simp_rw [← pow_two, multiset_sum_sq]

theorem sum_sq (s : Finset ι) (f : ι → R) : (∑ i ∈ s, f i) ^ 2 = ∑ i ∈ s, f i ^ 2 :=
  map_sum sqAddMonoidHom _ _

theorem sum_mul_self (s : Finset ι) (f : ι → R) :
    ((∑ i ∈ s, f i) * ∑ i ∈ s, f i) = ∑ i ∈ s, f i * f i := by simp_rw [← pow_two, sum_sq]

end CommSemiring

section CommRing

variable [CommRing R] [CharP R 2] [NoZeroDivisors R]

theorem sq_injective : Function.Injective fun x : R ↦ x ^ 2 := by
  intro x y h
  rwa [← CharTwo.add_eq_zero, ← add_sq, pow_eq_zero_iff two_ne_zero, CharTwo.add_eq_zero] at h

@[scoped simp]
theorem sq_inj {x y : R} : x ^ 2 = y ^ 2 ↔ x = y :=
  sq_injective.eq_iff

end CommRing

@[deprecated (since := "2026-02-05")]
alias CommRing.sq_injective := sq_injective

@[deprecated (since := "2026-02-05")]
alias CommRing.sq_inj := sq_inj

end CharTwo

section ringChar

variable [Ring R]

theorem neg_one_eq_one_iff [Nontrivial R] : (-1 : R) = 1 ↔ ringChar R = 2 := by
  refine ⟨fun h => ?_, fun h => @CharTwo.neg_eq _ _ (ringChar.of_eq h) 1⟩
  rw [eq_comm, ← sub_eq_zero, sub_neg_eq_add, ← Nat.cast_one, ← Nat.cast_add] at h
  exact ((Nat.dvd_prime Nat.prime_two).mp (ringChar.dvd h)).resolve_left CharP.ringChar_ne_one

end ringChar