Theorems · Definition · commutative algebra

WittVector.lift

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

Given compatible ring homs from S into TruncatedWittVector n for each n, we can lift these to a ring hom S → 𝕎 R. lift defines the universal property of 𝕎 R as the inverse limit of TruncatedWittVector n.

Defined in

Mathlib.RingTheory.WittVector.Truncated

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingFactSemiring