Theorems · Definition · commutative algebra

WittVector.frobenius

{p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [inst : CommRing R] → WittVector p R →+* WittVector p R

If R has characteristic p, then there is a ring endomorphism that raises r : R to the power p. By applying WittVector.map to this endomorphism, we obtain a ring endomorphism frobenius R p : 𝕎 R →+* 𝕎 R. The underlying function of this morphism is WittVector.frobeniusFun.

Defined in

Mathlib.RingTheory.WittVector.Frobenius

Cited by

22 results in Mathlib

Foundations

Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FactCommRing