Theorems · Definition · number theory

WittVector.FractionRing.frobeniusRingHom

(p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (k : Type u_1) →
      [inst_1 : CommRing k] →
        [CharP k p] → [PerfectRing k p] → FractionRing (WittVector p k) →+* FractionRing (WittVector p k)

The Frobenius automorphism of k induces an endomorphism of K. For notation purposes. Notation φ(p, k) in the Isocrystal namespace.

Defined in

Mathlib.RingTheory.WittVector.Isocrystal

Cited by

11 results in Mathlib

Foundations

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

Assumes

FactCommRingCharPPerfectRing