Truncated Witt vectors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The ring of truncated Witt vectors (of length n) is a quotient of the ring of Witt vectors. It retains the first n coefficients of each Witt vector. In this file, we set up the basic quotient API for this ring.

The ring of Witt vectors is the projective limit of all the rings of truncated Witt vectors.

Main declarations #

truncated_witt_vector: the underlying type of the ring of truncated Witt vectors
truncated_witt_vector.comm_ring: the ring structure on truncated Witt vectors
witt_vector.truncate: the quotient homomorphism that truncates a Witt vector, to obtain a truncated Witt vector
truncated_witt_vector.truncate: the homomorphism that truncates a truncated Witt vector of length n to one of length m (for some m ≤ n)
witt_vector.lift: the unique ring homomorphism into the ring of Witt vectors that is compatible with a family of ring homomorphisms to the truncated Witt vectors: this realizes the ring of Witt vectors as projective limit of the rings of truncated Witt vectors

References #

source

@[nolint]

def truncated_witt_vector (p n : ℕ) (R : Type u_1) :

Type u_1

A truncated Witt vector over R is a vector of elements of R, i.e., the first n coefficients of a Witt vector. We will define operations on this type that are compatible with the (untruncated) Witt vector operations.

truncated_witt_vector p n R takes a parameter p : ℕ that is not used in the definition. In practice, this number p is assumed to be a prime number, and under this assumption we construct a ring structure on truncated_witt_vector p n R. (truncated_witt_vector p₁ n R and truncated_witt_vector p₂ n R are definitionally equal as types but will have different ring operations.)

Equations

truncated_witt_vector p n R = (fin n → R)

Instances for truncated_witt_vector

source

@[protected, instance]

def truncated_witt_vector.inhabited (p n : ℕ) (R : Type u_1) [inhabited R] :

inhabited (truncated_witt_vector p n R)

Equations

truncated_witt_vector.inhabited p n R = {default := λ (_x : fin n), inhabited.default}

source

def truncated_witt_vector.mk (p : ℕ) {n : ℕ} {R : Type u_1} (x : fin n → R) :

truncated_witt_vector p n R

Create a truncated_witt_vector from a vector x.

Equations

truncated_witt_vector.mk p x = x

source

def truncated_witt_vector.coeff {p n : ℕ} {R : Type u_1} (i : fin n) (x : truncated_witt_vector p n R) :

x.coeff i is the ith entry of x.

Equations

truncated_witt_vector.coeff i x = x i

source

@[ext]

theorem truncated_witt_vector.ext {p n : ℕ} {R : Type u_1} {x y : truncated_witt_vector p n R} (h : ∀ (i : fin n), truncated_witt_vector.coeff i x = truncated_witt_vector.coeff i y) :

x = y

source

theorem truncated_witt_vector.ext_iff {p n : ℕ} {R : Type u_1} {x y : truncated_witt_vector p n R} :

x = y ↔ ∀ (i : fin n), truncated_witt_vector.coeff i x = truncated_witt_vector.coeff i y

source

@[simp]

theorem truncated_witt_vector.coeff_mk {p n : ℕ} {R : Type u_1} (x : fin n → R) (i : fin n) :

truncated_witt_vector.coeff i (truncated_witt_vector.mk p x) = x i

source

@[simp]

theorem truncated_witt_vector.mk_coeff {p n : ℕ} {R : Type u_1} (x : truncated_witt_vector p n R) :

truncated_witt_vector.mk p (λ (i : fin n), truncated_witt_vector.coeff i x) = x

source

def truncated_witt_vector.out {p n : ℕ} {R : Type u_1} [comm_ring R] (x : truncated_witt_vector p n R) :

witt_vector p R

We can turn a truncated Witt vector x into a Witt vector by setting all coefficients after x to be 0.

Equations

x.out = {coeff := λ (i : ℕ), dite (i < n) (λ (h : i < n), truncated_witt_vector.coeff ⟨i, h⟩ x) (λ (h : ¬i < n), 0)}

source

@[simp]

theorem truncated_witt_vector.coeff_out {p n : ℕ} {R : Type u_1} [comm_ring R] (x : truncated_witt_vector p n R) (i : fin n) :

x.out.coeff ↑i = truncated_witt_vector.coeff i x

source

theorem truncated_witt_vector.out_injective {p n : ℕ} {R : Type u_1} [comm_ring R] :

function.injective truncated_witt_vector.out

source

def witt_vector.truncate_fun {p : ℕ} (n : ℕ) {R : Type u_1} (x : witt_vector p R) :

truncated_witt_vector p n R

truncate_fun n x uses the first n entries of x to construct a truncated_witt_vector, which has the same base p as x. This function is bundled into a ring homomorphism in witt_vector.truncate

Equations

witt_vector.truncate_fun n x = truncated_witt_vector.mk p (λ (i : fin n), x.coeff ↑i)

source

@[simp]

theorem witt_vector.coeff_truncate_fun {p n : ℕ} {R : Type u_1} (x : witt_vector p R) (i : fin n) :

truncated_witt_vector.coeff i (witt_vector.truncate_fun n x) = x.coeff ↑i

source

@[simp]

theorem witt_vector.out_truncate_fun {p n : ℕ} {R : Type u_1} [comm_ring R] (x : witt_vector p R) :

(witt_vector.truncate_fun n x).out = witt_vector.init n x

source

@[simp]

theorem truncated_witt_vector.truncate_fun_out {p n : ℕ} {R : Type u_1} [comm_ring R] (x : truncated_witt_vector p n R) :

witt_vector.truncate_fun n x.out = x

source

@[protected, instance]

noncomputable def truncated_witt_vector.has_zero (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

has_zero (truncated_witt_vector p n R)

Equations

truncated_witt_vector.has_zero p n R = {zero := witt_vector.truncate_fun n 0}

source

@[protected, instance]

noncomputable def truncated_witt_vector.has_one (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

has_one (truncated_witt_vector p n R)

Equations

truncated_witt_vector.has_one p n R = {one := witt_vector.truncate_fun n 1}

source

@[protected, instance]

noncomputable def truncated_witt_vector.has_nat_cast (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

has_nat_cast (truncated_witt_vector p n R)

Equations

truncated_witt_vector.has_nat_cast p n R = {nat_cast := λ (i : ℕ), witt_vector.truncate_fun n ↑i}

source

@[protected, instance]

noncomputable def truncated_witt_vector.has_int_cast (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

has_int_cast (truncated_witt_vector p n R)

Equations

truncated_witt_vector.has_int_cast p n R = {int_cast := λ (i : ℤ), witt_vector.truncate_fun n ↑i}

source

@[protected, instance]

noncomputable def truncated_witt_vector.has_add (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

has_add (truncated_witt_vector p n R)

Equations

truncated_witt_vector.has_add p n R = {add := λ (x y : truncated_witt_vector p n R), witt_vector.truncate_fun n (x.out + y.out)}

source

@[protected, instance]

noncomputable def truncated_witt_vector.has_mul (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

has_mul (truncated_witt_vector p n R)

Equations

truncated_witt_vector.has_mul p n R = {mul := λ (x y : truncated_witt_vector p n R), witt_vector.truncate_fun n (x.out * y.out)}

source

@[protected, instance]

noncomputable def truncated_witt_vector.has_neg (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

has_neg (truncated_witt_vector p n R)

Equations

truncated_witt_vector.has_neg p n R = {neg := λ (x : truncated_witt_vector p n R), witt_vector.truncate_fun n (-x.out)}

source

@[protected, instance]

noncomputable def truncated_witt_vector.has_sub (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

has_sub (truncated_witt_vector p n R)

Equations

truncated_witt_vector.has_sub p n R = {sub := λ (x y : truncated_witt_vector p n R), witt_vector.truncate_fun n (x.out - y.out)}

source

@[protected, instance]

noncomputable def truncated_witt_vector.has_nat_scalar (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

has_smul ℕ (truncated_witt_vector p n R)

Equations

truncated_witt_vector.has_nat_scalar p n R = {smul := λ (m : ℕ) (x : truncated_witt_vector p n R), witt_vector.truncate_fun n (m • x.out)}

source

@[protected, instance]

noncomputable def truncated_witt_vector.has_int_scalar (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

has_smul ℤ (truncated_witt_vector p n R)

Equations

truncated_witt_vector.has_int_scalar p n R = {smul := λ (m : ℤ) (x : truncated_witt_vector p n R), witt_vector.truncate_fun n (m • x.out)}

source

@[protected, instance]

noncomputable def truncated_witt_vector.has_nat_pow (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

has_pow (truncated_witt_vector p n R) ℕ

Equations

truncated_witt_vector.has_nat_pow p n R = {pow := λ (x : truncated_witt_vector p n R) (m : ℕ), witt_vector.truncate_fun n (x.out ^ m)}

source

@[simp]

theorem truncated_witt_vector.coeff_zero (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] (i : fin n) :

truncated_witt_vector.coeff i 0 = 0

source

meta def tactic.interactive.witt_truncate_fun_tac :

tactic unit

A macro tactic used to prove that truncate_fun respects ring operations.

source

theorem witt_vector.truncate_fun_surjective (p n : ℕ) (R : Type u_1) [comm_ring R] :

function.surjective (witt_vector.truncate_fun n)

source

@[simp]

theorem witt_vector.truncate_fun_zero (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

witt_vector.truncate_fun n 0 = 0

source

@[simp]

theorem witt_vector.truncate_fun_one (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

witt_vector.truncate_fun n 1 = 1

source

@[simp]

theorem witt_vector.truncate_fun_add {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] (x y : witt_vector p R) :

witt_vector.truncate_fun n (x + y) = witt_vector.truncate_fun n x + witt_vector.truncate_fun n y

source

@[simp]

theorem witt_vector.truncate_fun_mul {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] (x y : witt_vector p R) :

witt_vector.truncate_fun n (x * y) = witt_vector.truncate_fun n x * witt_vector.truncate_fun n y

source

theorem witt_vector.truncate_fun_neg {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] (x : witt_vector p R) :

witt_vector.truncate_fun n (-x) = -witt_vector.truncate_fun n x

source

theorem witt_vector.truncate_fun_sub {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] (x y : witt_vector p R) :

witt_vector.truncate_fun n (x - y) = witt_vector.truncate_fun n x - witt_vector.truncate_fun n y

source

theorem witt_vector.truncate_fun_nsmul {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] (x : witt_vector p R) (m : ℕ) :

witt_vector.truncate_fun n (m • x) = m • witt_vector.truncate_fun n x

source

theorem witt_vector.truncate_fun_zsmul {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] (x : witt_vector p R) (m : ℤ) :

witt_vector.truncate_fun n (m • x) = m • witt_vector.truncate_fun n x

source

theorem witt_vector.truncate_fun_pow {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] (x : witt_vector p R) (m : ℕ) :

witt_vector.truncate_fun n (x ^ m) = witt_vector.truncate_fun n x ^ m

source

theorem witt_vector.truncate_fun_nat_cast {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] (m : ℕ) :

witt_vector.truncate_fun n ↑m = ↑m

source

theorem witt_vector.truncate_fun_int_cast {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] (m : ℤ) :

witt_vector.truncate_fun n ↑m = ↑m

source

@[protected, instance]

noncomputable def truncated_witt_vector.comm_ring (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

comm_ring (truncated_witt_vector p n R)

Equations

truncated_witt_vector.comm_ring p n R = function.surjective.comm_ring (witt_vector.truncate_fun n) _ _ _ _ _ _ _ _ _ _ _ _

source

def witt_vector.truncate {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] :

witt_vector p R →+* truncated_witt_vector p n R

truncate n is a ring homomorphism that truncates x to its first n entries to obtain a truncated_witt_vector, which has the same base p as x.

Equations

witt_vector.truncate n = {to_fun := witt_vector.truncate_fun n R, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

theorem witt_vector.truncate_surjective (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (R : Type u_1) [comm_ring R] :

function.surjective ⇑(witt_vector.truncate n)

source

@[simp]

theorem witt_vector.coeff_truncate {p : ℕ} [hp : fact (nat.prime p)] {n : ℕ} {R : Type u_1} [comm_ring R] (x : witt_vector p R) (i : fin n) :

truncated_witt_vector.coeff i (⇑(witt_vector.truncate n) x) = x.coeff ↑i

source

theorem witt_vector.mem_ker_truncate {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] (x : witt_vector p R) :

x ∈ ring_hom.ker (witt_vector.truncate n) ↔ ∀ (i : ℕ), i < n → x.coeff i = 0

source

@[simp]

theorem witt_vector.truncate_mk (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] (f : ℕ → R) :

⇑(witt_vector.truncate n) {coeff := f} = truncated_witt_vector.mk p (λ (k : fin n), f ↑k)

source

noncomputable def truncated_witt_vector.truncate {p : ℕ} [hp : fact (nat.prime p)] {n : ℕ} {R : Type u_1} [comm_ring R] {m : ℕ} (hm : n ≤ m) :

truncated_witt_vector p m R →+* truncated_witt_vector p n R

A ring homomorphism that truncates a truncated Witt vector of length m to a truncated Witt vector of length n, for n ≤ m.

Equations

truncated_witt_vector.truncate hm = ⇑((witt_vector.truncate m).lift_of_right_inverse truncated_witt_vector.out truncated_witt_vector.truncate_fun_out) ⟨witt_vector.truncate n _inst_1, _⟩

source

@[simp]

theorem truncated_witt_vector.truncate_comp_witt_vector_truncate {p : ℕ} [hp : fact (nat.prime p)] {n : ℕ} {R : Type u_1} [comm_ring R] {m : ℕ} (hm : n ≤ m) :

(truncated_witt_vector.truncate hm).comp (witt_vector.truncate m) = witt_vector.truncate n

source

@[simp]

theorem truncated_witt_vector.truncate_witt_vector_truncate {p : ℕ} [hp : fact (nat.prime p)] {n : ℕ} {R : Type u_1} [comm_ring R] {m : ℕ} (hm : n ≤ m) (x : witt_vector p R) :

⇑(truncated_witt_vector.truncate hm) (⇑(witt_vector.truncate m) x) = ⇑(witt_vector.truncate n) x

source

@[simp]

theorem truncated_witt_vector.truncate_truncate {p : ℕ} [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {n₁ n₂ n₃ : ℕ} (h1 : n₁ ≤ n₂) (h2 : n₂ ≤ n₃) (x : truncated_witt_vector p n₃ R) :

⇑(truncated_witt_vector.truncate h1) (⇑(truncated_witt_vector.truncate h2) x) = ⇑(truncated_witt_vector.truncate _) x

source

@[simp]

theorem truncated_witt_vector.truncate_comp {p : ℕ} [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {n₁ n₂ n₃ : ℕ} (h1 : n₁ ≤ n₂) (h2 : n₂ ≤ n₃) :

(truncated_witt_vector.truncate h1).comp (truncated_witt_vector.truncate h2) = truncated_witt_vector.truncate _

source

theorem truncated_witt_vector.truncate_surjective {p : ℕ} [hp : fact (nat.prime p)] {n : ℕ} {R : Type u_1} [comm_ring R] {m : ℕ} (hm : n ≤ m) :

function.surjective ⇑(truncated_witt_vector.truncate hm)

source

@[simp]

theorem truncated_witt_vector.coeff_truncate {p : ℕ} [hp : fact (nat.prime p)] {n : ℕ} {R : Type u_1} [comm_ring R] {m : ℕ} (hm : n ≤ m) (i : fin n) (x : truncated_witt_vector p m R) :

truncated_witt_vector.coeff i (⇑(truncated_witt_vector.truncate hm) x) = truncated_witt_vector.coeff (⇑(fin.cast_le hm) i) x

source

@[protected, instance]

def truncated_witt_vector.fintype {p n : ℕ} {R : Type u_1} [fintype R] :

fintype (truncated_witt_vector p n R)

Equations

truncated_witt_vector.fintype = pi.fintype

source

theorem truncated_witt_vector.card (p n : ℕ) {R : Type u_1} [fintype R] :

fintype.card (truncated_witt_vector p n R) = fintype.card R ^ n

source

theorem truncated_witt_vector.infi_ker_truncate {p : ℕ} [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] :

(⨅ (i : ℕ), ring_hom.ker (witt_vector.truncate i)) = ⊥

source

noncomputable def witt_vector.lift_fun {p : ℕ} [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {S : Type u_2} [semiring S] (f : Π (k : ℕ), S →+* truncated_witt_vector p k R) (s : S) :

witt_vector p R

Given a family fₖ : S → truncated_witt_vector p k R and s : S, we produce a Witt vector by defining the kth entry to be the final entry of fₖ s.

Equations

witt_vector.lift_fun f s = {coeff := λ (k : ℕ), truncated_witt_vector.coeff (fin.last k) (⇑(f (k + 1)) s)}

source

@[simp]

theorem witt_vector.truncate_lift_fun {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] {S : Type u_2} [semiring S] {f : Π (k : ℕ), S →+* truncated_witt_vector p k R} (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (truncated_witt_vector.truncate hk).comp (f k₂) = f k₁) (s : S) :

⇑(witt_vector.truncate n) (witt_vector.lift_fun f s) = ⇑(f n) s

source

noncomputable def witt_vector.lift {p : ℕ} [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {S : Type u_2} [semiring S] (f : Π (k : ℕ), S →+* truncated_witt_vector p k R) (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (truncated_witt_vector.truncate hk).comp (f k₂) = f k₁) :

S →+* witt_vector p R

Given compatible ring homs from S into truncated_witt_vector 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 truncated_witt_vector n.

Equations

witt_vector.lift f f_compat = {to_fun := witt_vector.lift_fun f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[simp]

theorem witt_vector.truncate_lift {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] {S : Type u_2} [semiring S] {f : Π (k : ℕ), S →+* truncated_witt_vector p k R} (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (truncated_witt_vector.truncate hk).comp (f k₂) = f k₁) (s : S) :

⇑(witt_vector.truncate n) (⇑(witt_vector.lift (λ (k₂ : ℕ), f k₂) f_compat) s) = ⇑(f n) s

source

@[simp]

theorem witt_vector.truncate_comp_lift {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) {R : Type u_1} [comm_ring R] {S : Type u_2} [semiring S] {f : Π (k : ℕ), S →+* truncated_witt_vector p k R} (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (truncated_witt_vector.truncate hk).comp (f k₂) = f k₁) :

(witt_vector.truncate n).comp (witt_vector.lift (λ (k₂ : ℕ), f k₂) f_compat) = f n

source

theorem witt_vector.lift_unique {p : ℕ} [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {S : Type u_2} [semiring S] {f : Π (k : ℕ), S →+* truncated_witt_vector p k R} (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (truncated_witt_vector.truncate hk).comp (f k₂) = f k₁) (g : S →+* witt_vector p R) (g_compat : ∀ (k : ℕ), (witt_vector.truncate k).comp g = f k) :

witt_vector.lift (λ (k₂ : ℕ), f k₂) f_compat = g

The uniqueness part of the universal property of 𝕎 R.

source

noncomputable def witt_vector.lift_equiv {p : ℕ} [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {S : Type u_2} [semiring S] :

{f // ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (truncated_witt_vector.truncate hk).comp (f k₂) = f k₁} ≃ (S →+* witt_vector p R)

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

Equations

witt_vector.lift_equiv = {to_fun := λ (f : {f // ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (truncated_witt_vector.truncate hk).comp (f k₂) = f k₁}), witt_vector.lift f.val _, inv_fun := λ (g : S →+* witt_vector p R), ⟨λ (k : ℕ), (witt_vector.truncate k).comp g, _⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem witt_vector.lift_equiv_symm_apply_coe {p : ℕ} [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {S : Type u_2} [semiring S] (g : S →+* witt_vector p R) (k : ℕ) :

↑(⇑(witt_vector.lift_equiv.symm) g) k = (witt_vector.truncate k).comp g

source

@[simp]

theorem witt_vector.lift_equiv_apply {p : ℕ} [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {S : Type u_2} [semiring S] (f : {f // ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (truncated_witt_vector.truncate hk).comp (f k₂) = f k₁}) :

⇑witt_vector.lift_equiv f = witt_vector.lift f.val _

source

theorem witt_vector.hom_ext {p : ℕ} [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {S : Type u_2} [semiring S] (g₁ g₂ : S →+* witt_vector p R) (h : ∀ (k : ℕ), (witt_vector.truncate k).comp g₁ = (witt_vector.truncate k).comp g₂) :

g₁ = g₂