import Mathlib
import Definitions.Def_Dieudonne_DatumAndHonda
import Definitions.Def_Dieudonne_WittVectorHom

set_option autoImplicit false

open Function

universe u v w

namespace Deformation

namespace TruncWitt

variable {p : ℕ} [hp : Fact p.Prime] {n m l : ℕ}
variable {R : Type u} {S : Type v} [CommRing R] [CommRing S]

noncomputable def verschiebungIter (k : ℕ) : WittVector p R →+ WittVector p R where
  toFun x := (WittVector.verschiebung (p := p) (R := R))^[k] x
  map_zero' := iterate_map_zero _ _
  map_add' := iterate_map_add _ _

@[simp] theorem verschiebungIter_apply (k : ℕ) (x : WittVector p R) :
    verschiebungIter k x = (WittVector.verschiebung (p := p) (R := R))^[k] x := rfl

noncomputable def shiftLE (h : n ≤ m) :
    TruncatedWittVector p n R →+ TruncatedWittVector p m R :=
  AddMonoidHom.liftOfRightInverse (WittVector.truncate n).toAddMonoidHom TruncatedWittVector.out
    (fun x => TruncatedWittVector.truncateFun_out x)
    ⟨(WittVector.truncate m).toAddMonoidHom.comp (verschiebungIter (m - n)),
      fun x hx => by
        change (WittVector.truncate n) x = 0 at hx
        rw [← RingHom.mem_ker, WittVector.mem_ker_truncate] at hx
        change (WittVector.truncate m) ((WittVector.verschiebung (p := p) (R := R))^[m - n] x) = 0
        ext ⟨i, hi⟩
        simp only [WittVector.coeff_truncate, TruncatedWittVector.coeff_zero]
        by_cases him : i < m - n
        · exact WittVector.iterate_verschiebung_coeff_eq_zero x him
        · obtain ⟨k, rfl⟩ : ∃ k, i = k + (m - n) := ⟨i - (m - n), by omega⟩
          rw [WittVector.iterate_verschiebung_coeff]
          exact hx k (by omega)⟩

@[simp] theorem shiftLE_truncate (h : n ≤ m) (x : WittVector p R) :
    shiftLE h (WittVector.truncate n x) =
      WittVector.truncate m ((WittVector.verschiebung (p := p) (R := R))^[m - n] x) :=
  AddMonoidHom.liftOfRightInverse_comp_apply _ _
    (fun x => TruncatedWittVector.truncateFun_out x) _ _

theorem coeff_shiftLE (h : n ≤ m) (x : TruncatedWittVector p n R) (i : Fin m) :
    (shiftLE h x).coeff i =
      if hi : m - n ≤ (i : ℕ) then x.coeff ⟨i - (m - n), by omega⟩ else 0 := by
  obtain ⟨x, rfl⟩ := WittVector.truncate_surjective p n R x
  rw [shiftLE_truncate, WittVector.coeff_truncate]
  split_ifs with hi
  · rw [WittVector.coeff_truncate]
    have hk : (i : ℕ) = (i - (m - n)) + (m - n) := by omega
    conv_lhs => rw [hk]
    exact WittVector.iterate_verschiebung_coeff x (m - n) _
  · exact WittVector.iterate_verschiebung_coeff_eq_zero x (by omega)

theorem coeff_shiftLE_of_lt (h : n ≤ m) (x : TruncatedWittVector p n R) (i : Fin m)
    (hi : (i : ℕ) < m - n) : (shiftLE h x).coeff i = 0 := by
  rw [coeff_shiftLE, dif_neg (by omega)]

theorem coeff_shiftLE_add (h : n ≤ m) (x : TruncatedWittVector p n R) (i : Fin n) :
    (shiftLE h x).coeff ⟨i + (m - n), by omega⟩ = x.coeff i := by
  rw [coeff_shiftLE, dif_pos (by simp)]
  congr 1
  ext
  simp

@[simp] theorem shiftLE_refl (x : TruncatedWittVector p n R) : shiftLE le_rfl x = x :=
  TruncatedWittVector.ext fun i => by
    rw [coeff_shiftLE, dif_pos (by simp)]
    congr 1
    exact Fin.ext (by simp)

theorem shiftLE_shiftLE (h₁ : n ≤ m) (h₂ : m ≤ l) (x : TruncatedWittVector p n R) :
    shiftLE h₂ (shiftLE h₁ x) = shiftLE (h₁.trans h₂) x := by
  obtain ⟨x, rfl⟩ := WittVector.truncate_surjective p n R x
  rw [shiftLE_truncate, shiftLE_truncate, shiftLE_truncate, ← Function.iterate_add_apply]
  congr 2
  omega

theorem shiftLE_succ (x : TruncatedWittVector p n R) :
    shiftLE (Nat.le_succ n) x = shift x := by
  obtain ⟨x, rfl⟩ := WittVector.truncate_surjective p n R x
  rw [shiftLE_truncate, shift_truncate, Nat.succ_sub (le_refl n), Nat.sub_self,
    Function.iterate_one]

theorem shiftLE_injective (h : n ≤ m) : Injective (shiftLE (p := p) (R := R) h) :=
  fun x y hxy => TruncatedWittVector.ext fun i => by
    rw [← coeff_shiftLE_add h x i, ← coeff_shiftLE_add h y i, hxy]

theorem map_shiftLE (f : R →+* S) (h : n ≤ m) (x : TruncatedWittVector p n R) :
    map f (shiftLE h x) = shiftLE h (map f x) :=
  TruncatedWittVector.ext fun i => by
    simp only [coeff_map, coeff_shiftLE]
    split_ifs
    · rfl
    · exact map_zero f

theorem frobeniusFun_shiftLE (h : n ≤ m) (x : TruncatedWittVector p n R) :
    frobeniusFun (shiftLE h x) = shiftLE h (frobeniusFun x) :=
  TruncatedWittVector.ext fun i => by
    simp only [coeff_frobeniusFun, coeff_shiftLE]
    split_ifs
    · rfl
    · exact zero_pow hp.out.ne_zero

theorem verschiebung_shiftLE (h : n ≤ m) (x : TruncatedWittVector p n R) :
    verschiebung (shiftLE h x) = shiftLE h (verschiebung x) := by
  obtain ⟨x, rfl⟩ := WittVector.truncate_surjective p n R x
  rw [shiftLE_truncate, verschiebung_truncate, verschiebung_truncate, shiftLE_truncate,
    ← Function.iterate_succ_apply' (f := WittVector.verschiebung),
    Function.iterate_succ_apply (f := WittVector.verschiebung)]

theorem verschiebung_iterate_eq_zero (x : TruncatedWittVector p n R) :
    (verschiebung (p := p) (R := R))^[n] x = 0 := by
  obtain ⟨x, rfl⟩ := WittVector.truncate_surjective p n R x
  have key : ∀ k : ℕ, (verschiebung (p := p) (n := n) (R := R))^[k] (WittVector.truncate n x) =
      WittVector.truncate n ((WittVector.verschiebung (p := p) (R := R))^[k] x) := by
    intro k
    induction k with
    | zero => rfl
    | succ k ih =>
      rw [Function.iterate_succ_apply', ih, verschiebung_truncate,
        ← Function.iterate_succ_apply' (f := WittVector.verschiebung)]
  rw [key]
  ext ⟨i, hi⟩
  rw [WittVector.coeff_truncate, TruncatedWittVector.coeff_zero]
  exact WittVector.iterate_verschiebung_coeff_eq_zero x hi

theorem pow_card_nsmul_eq_zero (hR : (p : R) = 0) (x : TruncatedWittVector p n R) :
    p ^ n • x = 0 := by
  rcases subsingleton_or_charP hR with h | h
  · exact Subsingleton.elim _ _
  · obtain ⟨x, rfl⟩ := WittVector.truncate_surjective p n R x
    rw [← map_nsmul, nsmul_eq_mul, Nat.cast_pow, mul_comm,
      ← WittVector.iterate_verschiebung_iterate_frobenius]
    ext ⟨i, hi⟩
    rw [WittVector.coeff_truncate, TruncatedWittVector.coeff_zero]
    exact WittVector.iterate_verschiebung_coeff_eq_zero _ hi

end TruncWitt

section WittHom

variable {R : Type u} [CommRing R] {p : ℕ} [hp : Fact p.Prime] {n m l : ℕ}
variable {A : Type v} [CommRing A] [Bialgebra R A]

open TruncWitt

theorem shiftLE_mem_wittHom (h : n ≤ m) {x : TruncatedWittVector p n A}
    (hx : x ∈ wittHom R p n A) : TruncWitt.shiftLE h x ∈ wittHom R p m A := by
  rw [mem_wittHom_iff] at hx ⊢
  rw [map_shiftLE, map_shiftLE, map_shiftLE, hx, map_add]

theorem shiftLE_mem_wittHom_iff (h : n ≤ m) (x : TruncatedWittVector p n A) :
    TruncWitt.shiftLE h x ∈ wittHom R p m A ↔ x ∈ wittHom R p n A := by
  refine ⟨fun hx => ?_, shiftLE_mem_wittHom h⟩
  rw [mem_wittHom_iff] at hx ⊢
  rw [map_shiftLE, map_shiftLE, map_shiftLE, ← map_add] at hx
  exact shiftLE_injective h hx

variable (R p A) in

noncomputable def wittHomShiftLE (h : n ≤ m) : wittHom R p n A →+ wittHom R p m A where
  toFun x := ⟨TruncWitt.shiftLE h x, shiftLE_mem_wittHom h x.2⟩
  map_zero' := Subtype.ext (by simp)
  map_add' _ _ := Subtype.ext (by simp)

@[simp] theorem coe_wittHomShiftLE (h : n ≤ m) (x : wittHom R p n A) :
    (wittHomShiftLE R p A h x : TruncatedWittVector p m A) = TruncWitt.shiftLE h x := rfl

@[simp] theorem wittHomShiftLE_refl (x : wittHom R p n A) : wittHomShiftLE R p A le_rfl x = x :=
  Subtype.ext (shiftLE_refl _)

theorem wittHomShiftLE_shiftLE (h₁ : n ≤ m) (h₂ : m ≤ l) (x : wittHom R p n A) :
    wittHomShiftLE R p A h₂ (wittHomShiftLE R p A h₁ x) = wittHomShiftLE R p A (h₁.trans h₂) x :=
  Subtype.ext (shiftLE_shiftLE h₁ h₂ _)

theorem wittHomShiftLE_succ (x : wittHom R p n A) :
    wittHomShiftLE R p A (Nat.le_succ n) x = wittHomShift R p n A x :=
  Subtype.ext (shiftLE_succ _)

theorem wittHomShiftLE_injective (h : n ≤ m) : Injective (wittHomShiftLE R p A h) :=
  fun _ _ hxy => Subtype.ext (shiftLE_injective h (congrArg Subtype.val hxy))

theorem wittHomShiftLE_verschiebung (h : n ≤ m) (x : wittHom R p n A) :
    wittHomShiftLE R p A h (wittHomVerschiebung R p n A x) =
      wittHomVerschiebung R p m A (wittHomShiftLE R p A h x) :=
  Subtype.ext (verschiebung_shiftLE h _).symm

theorem wittHomShiftLE_frobenius [CharP R p] (h : n ≤ m) (x : wittHom R p n A) :
    wittHomShiftLE R p A h (wittHomFrobenius R p n A x) =
      wittHomFrobenius R p m A (wittHomShiftLE R p A h x) :=
  Subtype.ext (frobeniusFun_shiftLE h _).symm

theorem wittHomMap_shiftLE {B : Type w} [CommRing B] [Bialgebra R B] (φ : A →ₐc[R] B)
    (h : n ≤ m) (x : wittHom R p n A) :
    wittHomMap p m φ (wittHomShiftLE R p A h x) = wittHomShiftLE R p B h (wittHomMap p n φ x) :=
  Subtype.ext (map_shiftLE _ h _)

theorem wittHomVerschiebung_iterate_eq_zero (x : wittHom R p n A) :
    (wittHomVerschiebung R p n A)^[n] x = 0 := by
  apply Subtype.ext
  have : ∀ k : ℕ, (((wittHomVerschiebung R p n A)^[k] x : wittHom R p n A) :
      TruncatedWittVector p n A) = (TruncWitt.verschiebung (p := p) (R := A))^[k] x := by
    intro k
    induction k with
    | zero => rfl
    | succ k ih => rw [Function.iterate_succ_apply', Function.iterate_succ_apply', ← ih]; rfl
  rw [this]
  exact verschiebung_iterate_eq_zero _

theorem pow_nsmul_wittHom_eq_zero [CharP R p] (x : wittHom R p n A) : p ^ n • x = 0 :=
  Subtype.ext (by
    rw [AddSubgroupClass.coe_nsmul, ZeroMemClass.coe_zero]
    exact pow_card_nsmul_eq_zero (natCast_eq_zero_of_algebra R p A) _)

instance wittHomShiftLE_directedSystem :
    DirectedSystem (fun n => ↥(wittHom R p n A)) fun _ _ h => wittHomShiftLE R p A h where
  map_self _ x := wittHomShiftLE_refl x
  map_map _ _ _ h₁ h₂ x := wittHomShiftLE_shiftLE h₁ h₂ x

end WittHom

section Colimit

variable (R : Type u) [CommRing R] (p : ℕ) [hp : Fact p.Prime]
variable (A : Type v) [CommRing A] [Bialgebra R A]

def DieudonneModule : Type v :=
  AddCommGroup.DirectLimit (fun n => ↥(wittHom R p n A)) fun _ _ h => wittHomShiftLE R p A h

namespace DieudonneModule

noncomputable instance instAddCommGroup : AddCommGroup (DieudonneModule R p A) :=
  inferInstanceAs (AddCommGroup
    (AddCommGroup.DirectLimit (fun n => ↥(wittHom R p n A)) fun _ _ h => wittHomShiftLE R p A h))

noncomputable instance instInhabited : Inhabited (DieudonneModule R p A) := ⟨0⟩

noncomputable def of (n : ℕ) : wittHom R p n A →+ DieudonneModule R p A :=
  AddCommGroup.DirectLimit.of (fun n => ↥(wittHom R p n A)) (fun _ _ h => wittHomShiftLE R p A h) n

variable {R p A}
variable {n m : ℕ}

@[simp] theorem of_shiftLE (h : n ≤ m) (x : wittHom R p n A) :
    of R p A m (wittHomShiftLE R p A h x) = of R p A n x :=
  AddCommGroup.DirectLimit.of_f _ _

@[simp] theorem of_shift (x : wittHom R p n A) :
    of R p A (n + 1) (wittHomShift R p n A x) = of R p A n x := by
  rw [← wittHomShiftLE_succ, of_shiftLE]

@[elab_as_elim]
protected theorem induction_on {C : DieudonneModule R p A → Prop} (z : DieudonneModule R p A)
    (ih : ∀ (n : ℕ) (x : wittHom R p n A), C (of R p A n x)) : C z :=
  AddCommGroup.DirectLimit.induction_on z ih

theorem exists_of (z : DieudonneModule R p A) : ∃ (n : ℕ) (x : wittHom R p n A), of R p A n x = z :=
  DieudonneModule.induction_on z fun n x => ⟨n, x, rfl⟩

theorem exists_shiftLE_eq_zero_of_of_eq_zero {x : wittHom R p n A} (hx : of R p A n x = 0) :
    ∃ (m : ℕ) (h : n ≤ m), wittHomShiftLE R p A h x = 0 :=
  AddCommGroup.DirectLimit.of.zero_exact (f := fun _ _ h => wittHomShiftLE R p A h) n x hx

theorem of_injective (n : ℕ) : Injective (of R p A n) := by
  refine (injective_iff_map_eq_zero _).2 fun x hx => ?_
  obtain ⟨m, h, hm⟩ := exists_shiftLE_eq_zero_of_of_eq_zero hx
  exact wittHomShiftLE_injective h (by rw [hm, map_zero])

theorem of_eq_of_iff (x : wittHom R p n A) (y : wittHom R p m A) :
    of R p A n x = of R p A m y ↔
      wittHomShiftLE R p A (le_max_left n m) x = wittHomShiftLE R p A (le_max_right n m) y := by
  constructor
  · intro h
    apply of_injective (max n m)
    rwa [of_shiftLE, of_shiftLE]
  · intro h
    rw [← of_shiftLE (le_max_left n m) x, h, of_shiftLE]

section Lift

variable {P : Type w} [AddCommGroup P]

theorem compat_shiftLE (g : ∀ n, wittHom R p n A →+ P)
    (hg : ∀ (n : ℕ) (x : wittHom R p n A), g (n + 1) (wittHomShift R p n A x) = g n x)
    (h : n ≤ m) (x : wittHom R p n A) : g m (wittHomShiftLE R p A h x) = g n x := by
  induction h with
  | refl => rw [wittHomShiftLE_refl]
  | @step m h ih =>
    rw [← wittHomShiftLE_shiftLE h (Nat.le_succ m), wittHomShiftLE_succ, hg, ih]

variable (R p A) in

noncomputable def lift (g : ∀ n, wittHom R p n A →+ P)
    (hg : ∀ (n : ℕ) (x : wittHom R p n A), g (n + 1) (wittHomShift R p n A x) = g n x) :
    DieudonneModule R p A →+ P :=
  AddCommGroup.DirectLimit.lift (fun n => ↥(wittHom R p n A)) (fun _ _ h => wittHomShiftLE R p A h)
    P g fun _ _ h x => compat_shiftLE g hg h x

@[simp] theorem lift_of (g : ∀ n, wittHom R p n A →+ P)
    (hg : ∀ (n : ℕ) (x : wittHom R p n A), g (n + 1) (wittHomShift R p n A x) = g n x)
    (x : wittHom R p n A) : lift R p A g hg (of R p A n x) = g n x :=
  AddCommGroup.DirectLimit.lift_of _ _ _ _ _

theorem hom_ext {f g : DieudonneModule R p A →+ P}
    (h : ∀ (n : ℕ) (x : wittHom R p n A), f (of R p A n x) = g (of R p A n x)) : f = g :=
  AddMonoidHom.ext fun z => DieudonneModule.induction_on z h

end Lift

variable (R p A) in

noncomputable def verschiebung : DieudonneModule R p A →+ DieudonneModule R p A :=
  lift R p A (fun n => (of R p A n).comp (wittHomVerschiebung R p n A)) fun n x => by
    rw [AddMonoidHom.comp_apply, AddMonoidHom.comp_apply, ← wittHomShift_verschiebung, of_shift]

@[simp] theorem verschiebung_of (x : wittHom R p n A) :
    verschiebung R p A (of R p A n x) = of R p A n (wittHomVerschiebung R p n A x) :=
  lift_of _ _ _

section CharP

variable [CharP R p]

variable (R p A) in

noncomputable def frobenius : DieudonneModule R p A →+ DieudonneModule R p A :=
  lift R p A (fun n => (of R p A n).comp (wittHomFrobenius R p n A)) fun n x => by
    rw [AddMonoidHom.comp_apply, AddMonoidHom.comp_apply, ← wittHomShift_frobenius, of_shift]

@[simp] theorem frobenius_of (x : wittHom R p n A) :
    frobenius R p A (of R p A n x) = of R p A n (wittHomFrobenius R p n A x) :=
  lift_of _ _ _

theorem frobenius_verschiebung (z : DieudonneModule R p A) :
    frobenius R p A (verschiebung R p A z) = (p : ℤ) • z := by
  induction z using DieudonneModule.induction_on with
  | ih n x => rw [verschiebung_of, frobenius_of, wittHomFrobenius_verschiebung, map_zsmul]

theorem verschiebung_frobenius (z : DieudonneModule R p A) :
    verschiebung R p A (frobenius R p A z) = (p : ℤ) • z := by
  induction z using DieudonneModule.induction_on with
  | ih n x => rw [frobenius_of, verschiebung_of, wittHomVerschiebung_frobenius, map_zsmul]

variable (R p A) in

noncomputable def dieudonneDatum : DieudonneDatum (p : ℤ) (DieudonneModule R p A) where
  F := (frobenius R p A).toIntLinearMap
  V := (verschiebung R p A).toIntLinearMap
  fv := LinearMap.ext fun z => frobenius_verschiebung z
  vf := LinearMap.ext fun z => verschiebung_frobenius z

@[simp] theorem dieudonneDatum_F_apply (z : DieudonneModule R p A) :
    (dieudonneDatum R p A).F z = frobenius R p A z := rfl

@[simp] theorem dieudonneDatum_V_apply (z : DieudonneModule R p A) :
    (dieudonneDatum R p A).V z = verschiebung R p A z := rfl

theorem pow_nsmul_of (x : wittHom R p n A) : p ^ n • of R p A n x = 0 := by
  rw [← map_nsmul, pow_nsmul_wittHom_eq_zero, map_zero]

theorem exists_pow_nsmul_eq_zero (z : DieudonneModule R p A) : ∃ n : ℕ, p ^ n • z = 0 := by
  obtain ⟨n, x, rfl⟩ := exists_of z
  exact ⟨n, pow_nsmul_of x⟩

end CharP

section Map

variable {B : Type w} [CommRing B] [Bialgebra R B]

variable (R p) in

noncomputable def map (φ : A →ₐc[R] B) : DieudonneModule R p A →+ DieudonneModule R p B :=
  lift R p A (fun n => (of R p B n).comp (wittHomMap p n φ)) fun n x => by
    rw [AddMonoidHom.comp_apply, AddMonoidHom.comp_apply, wittHomMap_shift, of_shift]

@[simp] theorem map_of (φ : A →ₐc[R] B) (x : wittHom R p n A) :
    map R p φ (of R p A n x) = of R p B n (wittHomMap p n φ x) :=
  lift_of _ _ _

theorem map_verschiebung (φ : A →ₐc[R] B) (z : DieudonneModule R p A) :
    map R p φ (verschiebung R p A z) = verschiebung R p B (map R p φ z) := by
  induction z using DieudonneModule.induction_on with
  | ih n x => rw [verschiebung_of, map_of, map_of, verschiebung_of, wittHomMap_verschiebung]

theorem map_frobenius [CharP R p] (φ : A →ₐc[R] B) (z : DieudonneModule R p A) :
    map R p φ (frobenius R p A z) = frobenius R p B (map R p φ z) := by
  induction z using DieudonneModule.induction_on with
  | ih n x => rw [frobenius_of, map_of, map_of, frobenius_of, wittHomMap_frobenius]

theorem map_id (z : DieudonneModule R p A) : map R p (BialgHom.id R A) z = z := by
  induction z using DieudonneModule.induction_on with
  | ih n x =>
    rw [map_of]
    congr 1
    exact Subtype.ext (TruncWitt.map_id _)

theorem map_comp {C : Type*} [CommRing C] [Bialgebra R C] (φ : A →ₐc[R] B) (ψ : B →ₐc[R] C)
    (z : DieudonneModule R p A) : map R p (ψ.comp φ) z = map R p ψ (map R p φ z) := by
  induction z using DieudonneModule.induction_on with
  | ih n x =>
    rw [map_of, map_of, map_of]
    congr 1
    refine Subtype.ext (TruncatedWittVector.ext fun i => ?_)
    simp only [coe_wittHomMap, TruncWitt.coeff_map]
    rfl

theorem map_injective {φ : A →ₐc[R] B} (hφ : Injective φ) : Injective (map R p φ) := by
  refine (injective_iff_map_eq_zero _).2 fun z hz => ?_
  obtain ⟨n, x, rfl⟩ := exists_of z
  rw [map_of] at hz
  have hx : wittHomMap p n φ x = 0 := of_injective n (by rw [hz, map_zero])
  rw [wittHomMap_injective hφ (hx.trans (map_zero _).symm), map_zero]

end Map

end DieudonneModule

end Colimit

namespace DieudonneModule.Examples

variable (R : Type u) [CommRing R] (p : ℕ) [hp : Fact p.Prime]

abbrev Ga : Type u := SymmetricAlgebra R R

noncomputable def coordinate : Ga R := SymmetricAlgebra.ι R R 1

theorem coordinate_ne_zero [Nontrivial R] : coordinate R ≠ 0 := by
  intro h
  have := congrArg (SymmetricAlgebra.lift (LinearMap.id : R →ₗ[R] R)) h
  rw [coordinate, SymmetricAlgebra.lift_ι_apply, map_zero, LinearMap.id_apply] at this
  exact one_ne_zero this

theorem coeff_zero_add_of_length_one {S : Type v} [CommRing S] (x y : TruncatedWittVector p 1 S) :
    (x + y).coeff 0 = x.coeff 0 + y.coeff 0 := by
  obtain ⟨x, rfl⟩ := WittVector.truncate_surjective p 1 S x
  obtain ⟨y, rfl⟩ := WittVector.truncate_surjective p 1 S y
  rw [← map_add, WittVector.coeff_truncate, WittVector.coeff_truncate, WittVector.coeff_truncate]
  exact WittVector.add_coeff_zero x y

theorem coordinate_mem_wittHom :
    TruncatedWittVector.mk p (fun _ : Fin 1 => coordinate R) ∈ wittHom R p 1 (Ga R) := by
  rw [mem_wittHom_iff]
  refine TruncatedWittVector.ext fun i => ?_
  obtain rfl : i = 0 := Subsingleton.elim _ _
  rw [coeff_zero_add_of_length_one, TruncWitt.coeff_map, TruncWitt.coeff_map,
    TruncWitt.coeff_map, TruncatedWittVector.coeff_mk]
  change Coalgebra.comul (R := R) (coordinate R) = _
  rw [coordinate, SymmetricAlgebra.comul_ι]
  rfl

theorem of_coordinate_ne_zero [Nontrivial R] :
    DieudonneModule.of R p (Ga R) 1
      ⟨TruncatedWittVector.mk p (fun _ : Fin 1 => coordinate R), coordinate_mem_wittHom R p⟩ ≠ 0 := by
  intro h
  have h1 := DieudonneModule.of_injective 1 (h.trans (map_zero _).symm)
  have h2 := congrArg (fun x : wittHom R p 1 (Ga R) => (x : TruncatedWittVector p 1 (Ga R)).coeff 0) h1
  simp only [TruncatedWittVector.coeff_mk, AddSubgroup.coe_zero,
    TruncatedWittVector.coeff_zero] at h2
  exact coordinate_ne_zero R h2

end DieudonneModule.Examples

end Deformation