Mathlib.Algebra.CharP.Reduced

iterateFrobenius_inj theorem

: Function.Injective (iterateFrobenius R p n)

Full source

theorem iterateFrobenius_inj : Function.Injective (iterateFrobenius R p n) := fun x y H ↦ by
  rw [← sub_eq_zero] at H ⊢
  simp_rw [iterateFrobenius_def, ← sub_pow_expChar_pow] at H
  exact IsReduced.eq_zero _ ⟨_, H⟩

Injectivity of Iterated Frobenius Homomorphism on Reduced Commutative Rings

Informal description

Let $R$ be a commutative ring with exponential characteristic $p$ that is reduced (i.e., has no nonzero nilpotent elements). Then for any natural number $n$, the iterated Frobenius homomorphism $\text{Frob}_{p^n} : R \to R$ defined by $x \mapsto x^{p^n}$ is injective.

frobenius_inj theorem

: Function.Injective (frobenius R p)

Full source

theorem frobenius_inj : Function.Injective (frobenius R p) :=
  iterateFrobenius_one (R := R) p ▸ iterateFrobenius_inj R p 1

Injectivity of Frobenius Endomorphism on Reduced Commutative Rings

Informal description

Let $R$ be a reduced commutative ring with exponential characteristic $p$. Then the Frobenius endomorphism $\text{Frob}_p : R \to R$ defined by $x \mapsto x^p$ is injective.

isSquare_of_charTwo' theorem

{R : Type*} [Finite R] [CommRing R] [IsReduced R] [CharP R 2] (a : R) : IsSquare a

Full source

/-- If `ringChar R = 2`, where `R` is a finite reduced commutative ring,
then every `a : R` is a square. -/
theorem isSquare_of_charTwo' {R : Type*} [Finite R] [CommRing R] [IsReduced R] [CharP R 2]
    (a : R) : IsSquare a := by
  cases nonempty_fintype R
  exact
    Exists.imp (fun b h => pow_two b ▸ Eq.symm h)
      (((Fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a)

Every Element is a Square in Finite Reduced Commutative Rings of Characteristic 2

Informal description

Let $R$ be a finite reduced commutative ring of characteristic $2$. Then every element $a \in R$ is a square, i.e., there exists $r \in R$ such that $a = r^2$.

ExpChar.pow_prime_pow_mul_eq_one_iff theorem

(p k m : ℕ) [ExpChar R p] (x : R) : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1

Full source

@[simp]
theorem ExpChar.pow_prime_pow_mul_eq_one_iff (p k m : ℕ) [ExpChar R p] (x : R) :
    x ^ (p ^ k * m) = 1 ↔ x ^ m = 1 := by
  rw [pow_mul']
  convert ← (iterateFrobenius_inj R p k).eq_iff
  apply map_one

Exponential Characteristic Power Identity: $x^{p^k m} = 1 \leftrightarrow x^m = 1$

Informal description

Let $R$ be a commutative ring with exponential characteristic $p$. For any natural numbers $k$ and $m$, and any element $x \in R$, we have $x^{p^k m} = 1$ if and only if $x^m = 1$.