Mathlib.Algebra.CharP.Frobenius

The Frobenius endomorphism #

Tags #

Frobenius endomorphism

Implementation notes #

The definitions of frobenius and iterateFrobenius ring homomorphisms are in Mathlib/Algebra/CharP/Lemmas.lean as they are needed for some results that in turn are used in files forbidding to import algebra-related definitions (see Mathlib/Algebra/CharP/Two.lean).

source

📐 coverage

theorem frobenius_def {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] (x : R) :

(frobenius R p) x = x ^ p

source

📐 coverage

theorem iterateFrobenius_def {R : Type u_1} [CommSemiring R] (p n : ℕ) [ExpChar R p] (x : R) :

(iterateFrobenius R p n) x = x ^ p ^ n

source

📐 coverage

theorem iterate_frobenius {R : Type u_1} [CommSemiring R] (p n : ℕ) [ExpChar R p] (x : R) :

(⇑(frobenius R p))^[n] x = x ^ p ^ n

source

📐 coverage

theorem iterateFrobenius_eq_pow (R : Type u_1) [CommSemiring R] (p n : ℕ) [ExpChar R p] :

iterateFrobenius R p n = frobenius R p ^ n

source

📐 coverage

theorem coe_iterateFrobenius (R : Type u_1) [CommSemiring R] (p n : ℕ) [ExpChar R p] :

⇑(iterateFrobenius R p n) = (⇑(frobenius R p))^[n]

source

📐 coverage

theorem iterateFrobenius_one_apply (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] (x : R) :

(iterateFrobenius R p 1) x = x ^ p

source

📐 coverage

@[simp]

theorem iterateFrobenius_one (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] :

iterateFrobenius R p 1 = frobenius R p

source

📐 coverage

theorem iterateFrobenius_zero_apply (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] (x : R) :

(iterateFrobenius R p 0) x = x

source

📐 coverage

@[simp]

theorem iterateFrobenius_zero (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] :

iterateFrobenius R p 0 = RingHom.id R

source

📐 coverage

theorem iterateFrobenius_add_apply (R : Type u_1) [CommSemiring R] (p m n : ℕ) [ExpChar R p] (x : R) :

(iterateFrobenius R p (m + n)) x = (iterateFrobenius R p m) ((iterateFrobenius R p n) x)

source

📐 coverage

theorem iterateFrobenius_add (R : Type u_1) [CommSemiring R] (p m n : ℕ) [ExpChar R p] :

iterateFrobenius R p (m + n) = (iterateFrobenius R p m).comp (iterateFrobenius R p n)

source

📐 coverage

theorem iterateFrobenius_mul_apply (R : Type u_1) [CommSemiring R] (p m n : ℕ) [ExpChar R p] (x : R) :

(iterateFrobenius R p (m * n)) x = (⇑(iterateFrobenius R p m))^[n] x

source

📐 coverage

theorem coe_iterateFrobenius_mul (R : Type u_1) [CommSemiring R] (p m n : ℕ) [ExpChar R p] :

⇑(iterateFrobenius R p (m * n)) = (⇑(iterateFrobenius R p m))^[n]

source

📐 coverage

@[deprecated map_mul (since := "2025-10-28")]

theorem frobenius_mul {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] (x y : R) :

(frobenius R p) (x * y) = (frobenius R p) x * (frobenius R p) y

source

📐 coverage

@[deprecated map_one (since := "2025-10-28")]

theorem frobenius_one {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] :

(frobenius R p) 1 = 1

source

📐 coverage

theorem MonoidHom.map_frobenius {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] (f : R →* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) :

f ((frobenius R p) x) = (frobenius S p) (f x)

source

📐 coverage

theorem RingHom.map_frobenius {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] (g : R →+* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) :

g ((frobenius R p) x) = (frobenius S p) (g x)

source

📐 coverage

theorem MonoidHom.map_iterate_frobenius {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] (f : R →* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) (n : ℕ) :

f ((⇑(frobenius R p))^[n] x) = (⇑(frobenius S p))^[n] (f x)

source

📐 coverage

theorem MonoidHom.map_iterateFrobenius {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] (f : R →* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) (n : ℕ) :

f ((iterateFrobenius R p n) x) = (iterateFrobenius S p n) (f x)

source

📐 coverage

theorem RingHom.map_iterate_frobenius {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] (g : R →+* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) (n : ℕ) :

g ((⇑(frobenius R p))^[n] x) = (⇑(frobenius S p))^[n] (g x)

source

📐 coverage

theorem RingHom.map_iterateFrobenius {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] (g : R →+* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) (n : ℕ) :

g ((iterateFrobenius R p n) x) = (iterateFrobenius S p n) (g x)

source

📐 coverage

theorem MonoidHom.iterate_map_frobenius {R : Type u_1} [CommSemiring R] (x : R) (f : R →* R) (p : ℕ) [ExpChar R p] (n : ℕ) :

(⇑f)^[n] ((frobenius R p) x) = (frobenius R p) ((⇑f)^[n] x)

source

📐 coverage

theorem RingHom.iterate_map_frobenius {R : Type u_1} [CommSemiring R] (x : R) (f : R →+* R) (p : ℕ) [ExpChar R p] (n : ℕ) :

(⇑f)^[n] ((frobenius R p) x) = (frobenius R p) ((⇑f)^[n] x)

source

📐 coverage

theorem RingHom.frobenius_comm {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] (g : R →+* S) (p : ℕ) [ExpChar R p] [ExpChar S p] :

g.comp (frobenius R p) = (frobenius S p).comp g

The Frobenius endomorphism commutes with any ring homomorphism.

source

📐 coverage

theorem RingHom.iterateFrobenius_comm {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] (g : R →+* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (n : ℕ) :

g.comp (iterateFrobenius R p n) = (iterateFrobenius S p n).comp g

The iterated Frobenius endomorphism commutes with any ring homomorphism.

source

🔸 coverage

def LinearMap.frobenius (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] (p : ℕ) [ExpChar R p] [ExpChar S p] [Algebra R S] :

S →ₛₗ[_root_.frobenius R p] S

The Frobenius map of an algebra as a Frobenius-semilinear map.

Instances For

source

🔸 coverage

def LinearMap.iterateFrobenius (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] (p n : ℕ) [ExpChar R p] [ExpChar S p] [Algebra R S] :

S →ₛₗ[_root_.iterateFrobenius R p n] S

The iterated Frobenius map of an algebra as an iterated-Frobenius-semilinear map.

Instances For

source

📐 coverage

theorem LinearMap.frobenius_def (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] (p : ℕ) [ExpChar R p] [ExpChar S p] [Algebra R S] (x : S) :

(frobenius R S p) x = x ^ p

source

📐 coverage

theorem LinearMap.iterateFrobenius_def (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] (p : ℕ) [ExpChar R p] [ExpChar S p] [Algebra R S] (n : ℕ) (x : S) :

(iterateFrobenius R S p n) x = x ^ p ^ n

source

📐 coverage

@[deprecated map_zero (since := "2025-10-28")]

theorem frobenius_zero (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] :

(frobenius R p) 0 = 0

source

📐 coverage

@[deprecated map_add (since := "2025-10-28")]

theorem frobenius_add (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] (x y : R) :

(frobenius R p) (x + y) = (frobenius R p) x + (frobenius R p) y

source

📐 coverage

@[deprecated map_natCast (since := "2025-10-28")]

theorem frobenius_natCast (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] (n : ℕ) :

(frobenius R p) ↑n = ↑n

source

📐 coverage

@[deprecated map_neg (since := "2025-10-28")]

theorem frobenius_neg {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (x : R) :

(frobenius R p) (-x) = -(frobenius R p) x

source

📐 coverage

@[deprecated map_sub (since := "2025-10-28")]

theorem frobenius_sub {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (x y : R) :

(frobenius R p) (x - y) = (frobenius R p) x - (frobenius R p) y