Theorems · Definition · commutative algebra

WittVector.liftEquiv

{p : ℕ} →
  {R : Type u_1} →
    [inst : CommRing R] →
      [inst_1 : Fact (Nat.Prime p)] →
        {S : Type u_2} →
          [inst_2 : Semiring S] →
            { f // ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁ } ≃
              (S →+* WittVector p R)

The universal property of 𝕎 R as projective limit of truncated Witt vector rings.

Defined in

Mathlib.RingTheory.WittVector.Truncated

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingFactSemiring