import Mathlib
import Definitions.Def_Dieudonne_DatumAndHonda
import Definitions.Def_Dieudonne_WittVectorHom
import Definitions.Def_Dieudonne_WittHomColimit
import Definitions.Def_Dieudonne_FontaineHodge
import Definitions.Def_Dieudonne_UnipotentWittCovector

set_option autoImplicit false

open Function

universe u v w u' v' w'

namespace Deformation

namespace PLoc

variable (p : ℕ) (ℛ : Type u) [CommRing ℛ]

theorem isUnit_algebraMap : IsUnit (algebraMap ℛ (Localization.Away (p : ℛ)) (p : ℛ)) :=
  IsLocalization.Away.algebraMap_isUnit (p : ℛ)

noncomputable def invPow (m : ℕ) : Localization.Away (p : ℛ) :=
  (((isUnit_algebraMap p ℛ).unit⁻¹ : (Localization.Away (p : ℛ))ˣ) : Localization.Away (p : ℛ)) ^ m

theorem invPow_zero : invPow p ℛ 0 = 1 := by
  rw [invPow, pow_zero]

theorem invPow_one_mul_algebraMap :
    invPow p ℛ 1 * algebraMap ℛ (Localization.Away (p : ℛ)) (p : ℛ) = 1 := by
  rw [invPow, pow_one, IsUnit.val_inv_mul]

theorem invPow_succ_mul (m : ℕ) :
    invPow p ℛ (m + 1) * algebraMap ℛ (Localization.Away (p : ℛ)) (p : ℛ) = invPow p ℛ m := by
  have h1 := invPow_one_mul_algebraMap p ℛ
  rw [invPow, pow_one] at h1
  rw [invPow, invPow, pow_succ, mul_assoc, h1, mul_one]

theorem algebraMap_pow_mul_invPow (m : ℕ) :
    algebraMap ℛ (Localization.Away (p : ℛ)) ((p : ℛ) ^ m) * invPow p ℛ m = 1 := by
  rw [map_pow, invPow, ← mul_pow, IsUnit.mul_val_inv, one_pow]

theorem invPow_mul_algebraMap_pow (m : ℕ) :
    invPow p ℛ m * algebraMap ℛ (Localization.Away (p : ℛ)) ((p : ℛ) ^ m) = 1 := by
  rw [mul_comm, algebraMap_pow_mul_invPow]

theorem invPow_add (m n : ℕ) : invPow p ℛ (m + n) = invPow p ℛ m * invPow p ℛ n := by
  rw [invPow, invPow, invPow, pow_add]

theorem invPow_mul_algebraMap_pow_add (m s : ℕ) :
    invPow p ℛ m * algebraMap ℛ (Localization.Away (p : ℛ)) ((p : ℛ) ^ (m + s)) =
      algebraMap ℛ (Localization.Away (p : ℛ)) ((p : ℛ) ^ s) := by
  rw [pow_add, map_mul, ← mul_assoc, invPow_mul_algebraMap_pow, one_mul]

noncomputable def powSub (s : ℕ) : Submodule ℛ (Localization.Away (p : ℛ)) :=
  Submodule.span ℛ {algebraMap ℛ (Localization.Away (p : ℛ)) ((p : ℛ) ^ s)}

noncomputable def pSub : Submodule ℛ (Localization.Away (p : ℛ)) := powSub p ℛ 1

variable {ℛ}

theorem mem_powSub_iff {s : ℕ} {z : Localization.Away (p : ℛ)} :
    z ∈ powSub p ℛ s ↔ ∃ r : ℛ, algebraMap ℛ (Localization.Away (p : ℛ)) ((p : ℛ) ^ s * r) = z := by
  rw [powSub, Submodule.mem_span_singleton]
  constructor
  · rintro ⟨r, rfl⟩
    exact ⟨r, by rw [map_mul, Algebra.smul_def, mul_comm]⟩
  · rintro ⟨r, rfl⟩
    exact ⟨r, by rw [map_mul, Algebra.smul_def, mul_comm]⟩

theorem mem_pSub_iff {z : Localization.Away (p : ℛ)} :
    z ∈ pSub p ℛ ↔ ∃ r : ℛ, algebraMap ℛ (Localization.Away (p : ℛ)) ((p : ℛ) * r) = z := by
  rw [pSub, mem_powSub_iff, pow_one]

theorem algebraMap_pow_mul_mem_powSub (s : ℕ) (r : ℛ) :
    algebraMap ℛ (Localization.Away (p : ℛ)) ((p : ℛ) ^ s * r) ∈ powSub p ℛ s :=
  (mem_powSub_iff p).2 ⟨r, rfl⟩

theorem algebraMap_mul_mem_pSub (r : ℛ) :
    algebraMap ℛ (Localization.Away (p : ℛ)) ((p : ℛ) * r) ∈ pSub p ℛ :=
  (mem_pSub_iff p).2 ⟨r, rfl⟩

theorem algebraMap_mem_powSub_of_mem {s : ℕ} {a : ℛ} (ha : a ∈ Ideal.span {(p : ℛ) ^ s}) :
    algebraMap ℛ (Localization.Away (p : ℛ)) a ∈ powSub p ℛ s := by
  obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.1 ha
  rw [mul_comm]
  exact algebraMap_pow_mul_mem_powSub p s c

theorem powSub_le_powSub_of_le {s t : ℕ} (h : s ≤ t) : powSub p ℛ t ≤ powSub p ℛ s := by
  intro z hz
  obtain ⟨r, rfl⟩ := (mem_powSub_iff p).1 hz
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
  rw [pow_add, mul_assoc]
  exact algebraMap_pow_mul_mem_powSub p s _

theorem invPow_mul_algebraMap_mem_powSub {m s : ℕ} {a : ℛ} (ha : a ∈ Ideal.span {(p : ℛ) ^ (m + s)}) :
    invPow p ℛ m * algebraMap ℛ (Localization.Away (p : ℛ)) a ∈ powSub p ℛ s := by
  obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.1 ha
  rw [map_mul, mul_comm (algebraMap ℛ _ c), ← mul_assoc, invPow_mul_algebraMap_pow_add, ← map_mul]
  exact algebraMap_pow_mul_mem_powSub p s c

theorem invPow_mul_algebraMap_mem_pSub {m : ℕ} {a : ℛ} (ha : a ∈ Ideal.span {(p : ℛ) ^ (m + 1)}) :
    invPow p ℛ m * algebraMap ℛ (Localization.Away (p : ℛ)) a ∈ pSub p ℛ :=
  invPow_mul_algebraMap_mem_powSub p ha

theorem algebraMap_injective (hp' : (p : ℛ) ∈ nonZeroDivisors ℛ) :
    Injective (algebraMap ℛ (Localization.Away (p : ℛ))) :=
  IsLocalization.injective (M := Submonoid.powers (p : ℛ)) _ (Submonoid.powers_le.2 hp')

theorem mem_span_pow_of_invPow_mul_algebraMap_mem_powSub (hp' : (p : ℛ) ∈ nonZeroDivisors ℛ)
    {m s : ℕ} {a : ℛ} (h : invPow p ℛ m * algebraMap ℛ (Localization.Away (p : ℛ)) a ∈ powSub p ℛ s) :
    a ∈ Ideal.span {(p : ℛ) ^ (m + s)} := by
  obtain ⟨r, hr⟩ := (mem_powSub_iff p).1 h
  have key : algebraMap ℛ (Localization.Away (p : ℛ)) ((p : ℛ) ^ (m + s) * r) =
      algebraMap ℛ (Localization.Away (p : ℛ)) a := by
    rw [pow_add, mul_assoc, map_mul, hr, ← mul_assoc, algebraMap_pow_mul_invPow, one_mul]
  rw [← algebraMap_injective p hp' key]
  exact Ideal.mem_span_singleton'.2 ⟨r, mul_comm _ _⟩

theorem mem_span_pow_of_invPow_mul_algebraMap_mem_pSub (hp' : (p : ℛ) ∈ nonZeroDivisors ℛ)
    {m : ℕ} {a : ℛ} (h : invPow p ℛ m * algebraMap ℛ (Localization.Away (p : ℛ)) a ∈ pSub p ℛ) :
    a ∈ Ideal.span {(p : ℛ) ^ (m + 1)} :=
  mem_span_pow_of_invPow_mul_algebraMap_mem_powSub p hp' h

theorem exists_eq_invPow_mul_algebraMap (z : Localization.Away (p : ℛ)) :
    ∃ (k : ℕ) (a : ℛ), z = invPow p ℛ k * algebraMap ℛ (Localization.Away (p : ℛ)) a := by
  obtain ⟨⟨a, ⟨_, k, rfl⟩⟩, h⟩ := IsLocalization.surj (Submonoid.powers (p : ℛ)) z
  refine ⟨k, a, ?_⟩
  calc z = z * (algebraMap ℛ (Localization.Away (p : ℛ)) ((p : ℛ) ^ k) * invPow p ℛ k) := by
          rw [algebraMap_pow_mul_invPow, mul_one]
    _ = invPow p ℛ k * algebraMap ℛ (Localization.Away (p : ℛ)) a := by
          rw [← mul_assoc, h, mul_comm]

theorem eq_zero_of_forall_mem_powSub (hp' : (p : ℛ) ∈ nonZeroDivisors ℛ)
    [IsHausdorff (Ideal.span {(p : ℛ)}) ℛ] {z : Localization.Away (p : ℛ)}
    (hz : ∀ s, z ∈ powSub p ℛ s) : z = 0 := by

  obtain ⟨k, a, rfl⟩ := exists_eq_invPow_mul_algebraMap p z
  have ha : ∀ s, a ∈ Ideal.span {(p : ℛ) ^ (k + s)} := fun s =>
    mem_span_pow_of_invPow_mul_algebraMap_mem_powSub p hp' (hz s)
  have ha0 : a = 0 := by
    refine IsHausdorff.haus (I := Ideal.span {(p : ℛ)}) (M := ℛ) ‹_› a fun n => ?_
    rw [SModEq.zero, Ideal.span_singleton_pow, smul_eq_mul, Ideal.mul_top]
    exact Ideal.span_singleton_le_span_singleton.2 (pow_dvd_pow _ (Nat.le_add_left n k)) (ha n)
  rw [ha0, map_zero, mul_zero]

section Map

variable {ℛ' : Type v} [CommRing ℛ'] {ℛ'' : Type w} [CommRing ℛ'']

noncomputable def map (f : ℛ →+* ℛ') : Localization.Away (p : ℛ) →+* Localization.Away (p : ℛ') :=
  IsLocalization.Away.lift (p : ℛ) (g := (algebraMap ℛ' (Localization.Away (p : ℛ'))).comp f)
    (by rw [RingHom.comp_apply, map_natCast]; exact isUnit_algebraMap p ℛ')

@[simp] theorem map_algebraMap (f : ℛ →+* ℛ') (r : ℛ) :
    map p f (algebraMap ℛ _ r) = algebraMap ℛ' _ (f r) :=
  IsLocalization.Away.lift_eq _ _ r

@[simp] theorem map_invPow (f : ℛ →+* ℛ') (m : ℕ) : map p f (invPow p ℛ m) = invPow p ℛ' m := by

  have h1 : map p f (invPow p ℛ m) * algebraMap ℛ' _ ((p : ℛ') ^ m) = 1 := by
    have hpm : ((p : ℛ') ^ m) = f ((p : ℛ) ^ m) := by rw [map_pow, map_natCast]
    rw [hpm, ← map_algebraMap p f, ← map_mul, invPow_mul_algebraMap_pow, map_one]
  calc map p f (invPow p ℛ m)
      = map p f (invPow p ℛ m) * (algebraMap ℛ' _ ((p : ℛ') ^ m) * invPow p ℛ' m) := by
          rw [algebraMap_pow_mul_invPow, mul_one]
    _ = invPow p ℛ' m := by rw [← mul_assoc, h1, one_mul]

theorem map_mem_powSub (f : ℛ →+* ℛ') {s : ℕ} {z : Localization.Away (p : ℛ)}
    (hz : z ∈ powSub p ℛ s) : map p f z ∈ powSub p ℛ' s := by
  obtain ⟨r, rfl⟩ := (mem_powSub_iff p).1 hz
  rw [map_algebraMap, map_mul, map_pow, map_natCast]
  exact algebraMap_pow_mul_mem_powSub p s (f r)

theorem map_mem_pSub (f : ℛ →+* ℛ') {z : Localization.Away (p : ℛ)} (hz : z ∈ pSub p ℛ) :
    map p f z ∈ pSub p ℛ' :=
  map_mem_powSub p f hz

theorem map_id (z : Localization.Away (p : ℛ)) : map p (RingHom.id ℛ) z = z := by
  obtain ⟨k, a, rfl⟩ := exists_eq_invPow_mul_algebraMap p z
  rw [map_mul, map_invPow, map_algebraMap, RingHom.id_apply]

theorem map_map (f : ℛ →+* ℛ') (f' : ℛ' →+* ℛ'') (z : Localization.Away (p : ℛ)) :
    map p f' (map p f z) = map p (f'.comp f) z := by
  obtain ⟨k, a, rfl⟩ := exists_eq_invPow_mul_algebraMap p z
  rw [map_mul, map_mul, map_mul, map_invPow, map_invPow, map_invPow, map_algebraMap,
    map_algebraMap, map_algebraMap, RingHom.comp_apply]

noncomputable def mapLinear {𝓞 : Type u'} [CommRing 𝓞] [Algebra 𝓞 ℛ] [Algebra 𝓞 ℛ'] (f : ℛ →ₐ[𝓞] ℛ') :
    Localization.Away (p : ℛ) →ₗ[𝓞] Localization.Away (p : ℛ') where
  toFun := map p f.toRingHom
  map_add' := map_add _
  map_smul' o z := by
    rw [RingHom.id_apply, Algebra.smul_def, Algebra.smul_def, map_mul,
      IsScalarTower.algebraMap_apply 𝓞 ℛ (Localization.Away (p : ℛ)), map_algebraMap,
      IsScalarTower.algebraMap_apply 𝓞 ℛ' (Localization.Away (p : ℛ')), AlgHom.toRingHom_eq_coe,
      RingHom.coe_coe, AlgHom.commutes]

@[simp] theorem mapLinear_apply {𝓞 : Type u'} [CommRing 𝓞] [Algebra 𝓞 ℛ] [Algebra 𝓞 ℛ']
    (f : ℛ →ₐ[𝓞] ℛ') (z : Localization.Away (p : ℛ)) : mapLinear p f z = map p f.toRingHom z := rfl

end Map

def IsPadicLimit (u : ℕ → Localization.Away (p : ℛ)) (α : Localization.Away (p : ℛ)) : Prop :=
  ∀ s : ℕ, ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → u n - α ∈ powSub p ℛ s

theorem IsPadicLimit.const (α : Localization.Away (p : ℛ)) : IsPadicLimit p (fun _ => α) α :=
  fun s => ⟨0, fun n _ => by rw [sub_self]; exact zero_mem _⟩

theorem IsPadicLimit.unique (hp' : (p : ℛ) ∈ nonZeroDivisors ℛ) [IsHausdorff (Ideal.span {(p : ℛ)}) ℛ]
    {u : ℕ → Localization.Away (p : ℛ)} {α β : Localization.Away (p : ℛ)}
    (hα : IsPadicLimit p u α) (hβ : IsPadicLimit p u β) : α = β := by
  rw [← sub_eq_zero]
  refine eq_zero_of_forall_mem_powSub p hp' fun s => ?_
  obtain ⟨n₁, h₁⟩ := hα s
  obtain ⟨n₂, h₂⟩ := hβ s
  have := sub_mem (h₂ (max n₁ n₂) (le_max_right _ _)) (h₁ (max n₁ n₂) (le_max_left _ _))
  rwa [sub_sub_sub_cancel_left] at this

noncomputable def wPartialSum (a : ℕ → ℛ) (N : ℕ) : Localization.Away (p : ℛ) :=
  ∑ n ∈ Finset.range N, invPow p ℛ n * algebraMap ℛ (Localization.Away (p : ℛ)) (a n ^ p ^ n)

theorem wPartialSum_zero (a : ℕ → ℛ) : wPartialSum p a 0 = 0 := by
  rw [wPartialSum, Finset.sum_range_zero]

theorem wPartialSum_succ (a : ℕ → ℛ) (N : ℕ) :
    wPartialSum p a (N + 1) =
      wPartialSum p a N + invPow p ℛ N * algebraMap ℛ (Localization.Away (p : ℛ)) (a N ^ p ^ N) := by
  rw [wPartialSum, wPartialSum, Finset.sum_range_succ]

open Classical in

noncomputable def wSeries (a : ℕ → ℛ) : Localization.Away (p : ℛ) :=
  if h : ∃ α, IsPadicLimit p (wPartialSum p a) α then Classical.choose h else 0

theorem isPadicLimit_wSeries {a : ℕ → ℛ} (h : ∃ α, IsPadicLimit p (wPartialSum p a) α) :
    IsPadicLimit p (wPartialSum p a) (wSeries p a) := by
  rw [wSeries, dif_pos h]
  exact Classical.choose_spec h

theorem wSeries_eq_of_isPadicLimit (hp' : (p : ℛ) ∈ nonZeroDivisors ℛ)
    [IsHausdorff (Ideal.span {(p : ℛ)}) ℛ] {a : ℕ → ℛ} {α : Localization.Away (p : ℛ)}
    (hα : IsPadicLimit p (wPartialSum p a) α) : wSeries p a = α :=
  (isPadicLimit_wSeries p ⟨α, hα⟩).unique p hp' hα

theorem wSeries_eq_wPartialSum_of_forall_eq_zero [hp : Fact p.Prime] (hp' : (p : ℛ) ∈ nonZeroDivisors ℛ)
    [IsHausdorff (Ideal.span {(p : ℛ)}) ℛ] {a : ℕ → ℛ} {N : ℕ} (hN : ∀ n, N ≤ n → a n = 0) :
    wSeries p a = wPartialSum p a N := by
  refine wSeries_eq_of_isPadicLimit p hp' fun s => ⟨N, fun n hn => ?_⟩
  suffices h : wPartialSum p a n = wPartialSum p a N by rw [h, sub_self]; exact zero_mem _
  induction hn with
  | refl => rfl
  | @step m hm ih =>
    rw [wPartialSum_succ, ih, hN m hm, zero_pow (pow_ne_zero _ hp.out.ne_zero), map_zero, mul_zero,
      add_zero]

end PLoc

namespace WittGhost

variable (p : ℕ) [hp : Fact p.Prime] {ℛ : Type u} [CommRing ℛ]

noncomputable def divGhost (m : ℕ) : WittVector p ℛ →+ Localization.Away (p : ℛ) where
  toFun X := PLoc.invPow p ℛ m * algebraMap ℛ (Localization.Away (p : ℛ)) (WittVector.ghostComponent m X)
  map_zero' := by rw [map_zero, map_zero, mul_zero]
  map_add' X Y := by rw [map_add, map_add, mul_add]

theorem divGhost_apply (m : ℕ) (X : WittVector p ℛ) :
    divGhost p m X =
      PLoc.invPow p ℛ m * algebraMap ℛ (Localization.Away (p : ℛ)) (WittVector.ghostComponent m X) :=
  rfl

theorem divGhost_zero_apply (X : WittVector p ℛ) :
    divGhost p 0 X = algebraMap ℛ (Localization.Away (p : ℛ)) (X.coeff 0) := by
  rw [divGhost_apply, PLoc.invPow_zero, one_mul, WittVector.ghostComponent_apply, wittPolynomial_zero,
    MvPolynomial.aeval_X]

theorem divGhost_verschiebung (m : ℕ) (X : WittVector p ℛ) :
    divGhost p (m + 1) (WittVector.verschiebung X) = divGhost p m X := by
  rw [divGhost_apply, divGhost_apply, WittVector.ghostComponent_verschiebung, map_mul, map_natCast,
    ← mul_assoc, ← map_natCast (algebraMap ℛ (Localization.Away (p : ℛ))) p, PLoc.invPow_succ_mul]

theorem divGhost_zero_verschiebung (X : WittVector p ℛ) :
    divGhost p 0 (WittVector.verschiebung X) = 0 := by
  rw [divGhost_apply, WittVector.ghostComponent_zero_verschiebung, map_zero, mul_zero]

theorem divGhost_eq_of_truncate_eq {m : ℕ} {X Y : WittVector p ℛ}
    (h : WittVector.truncate (m + 1) X = WittVector.truncate (m + 1) Y) :
    divGhost p m X = divGhost p m Y := by
  have hc : ∀ i ≤ m, X.coeff i = Y.coeff i := fun i hi => by
    have := congrArg (TruncatedWittVector.coeff (⟨i, Nat.lt_succ_of_le hi⟩ : Fin (m + 1))) h
    simpa only [WittVector.coeff_truncate] using this
  rw [divGhost_apply, divGhost_apply, ghostComponent_eq_sum, ghostComponent_eq_sum]
  congr 2
  exact Finset.sum_congr rfl fun i hi => by
    rw [hc i (Nat.le_of_lt_succ (Finset.mem_range.1 hi))]

theorem divGhost_mem_pSub_of_forall_coeff_mem {m : ℕ} {X : WittVector p ℛ}
    (hX : ∀ i ≤ m, X.coeff i ∈ Ideal.span {(p : ℛ)}) : divGhost p m X ∈ PLoc.pSub p ℛ :=
  PLoc.invPow_mul_algebraMap_mem_pSub p (ghostComponent_mem_span_pow_of_forall_coeff_mem hX)

theorem divGhost_sub_mem_pSub_of_truncate_map_eq {A : Type v} [CommRing A] (π : ℛ →+* A)
    (hπ : RingHom.ker π ≤ Ideal.span {(p : ℛ)}) {m : ℕ} {X Y : WittVector p ℛ}
    (h : WittVector.truncate (m + 1) (WittVector.map π X) =
      WittVector.truncate (m + 1) (WittVector.map π Y)) :
    divGhost p m X - divGhost p m Y ∈ PLoc.pSub p ℛ := by
  rw [← map_sub]
  refine divGhost_mem_pSub_of_forall_coeff_mem p fun i hi => hπ ?_
  refine TruncWitt.coeff_mem_ker_of_truncate_map_eq_zero (n := m + 1) ?_ i (Nat.lt_succ_of_le hi)
  rw [map_sub, map_sub, h, sub_self]

theorem divGhost_mem_pSub_iff (hp' : (p : ℛ) ∈ nonZeroDivisors ℛ) {m : ℕ} (X : WittVector p ℛ) :
    divGhost p m X ∈ PLoc.pSub p ℛ ↔
      WittVector.ghostComponent m X ∈ Ideal.span {(p : ℛ) ^ (m + 1)} :=
  ⟨PLoc.mem_span_pow_of_invPow_mul_algebraMap_mem_pSub p hp', PLoc.invPow_mul_algebraMap_mem_pSub p⟩

theorem divGhost_map {ℛ' : Type v} [CommRing ℛ'] (f : ℛ →+* ℛ') (m : ℕ) (X : WittVector p ℛ) :
    divGhost p m (WittVector.map f X) = PLoc.map p f (divGhost p m X) := by
  rw [divGhost_apply, divGhost_apply, ghostComponent_map, map_mul, PLoc.map_invPow, PLoc.map_algebraMap]

end WittGhost

namespace UnipotentWittCovector

section WUp

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

noncomputable def wLevel : ∀ n : ℕ, TruncatedWittVector p n ℛ →+ Localization.Away (p : ℛ)
  | 0 => 0
  | m + 1 =>
    AddMonoidHom.liftOfRightInverse (WittVector.truncate (m + 1)).toAddMonoidHom TruncatedWittVector.out
      (fun x => TruncatedWittVector.truncateFun_out x)
      ⟨WittGhost.divGhost p m, fun X hX => by
        change (WittVector.truncate (m + 1)) X = 0 at hX
        change WittGhost.divGhost p m X = 0
        rw [WittGhost.divGhost_eq_of_truncate_eq p (hX.trans (map_zero _).symm), map_zero]⟩

theorem wLevel_zero_apply (x : TruncatedWittVector p 0 ℛ) : wLevel p ℛ 0 x = 0 := rfl

@[simp] theorem wLevel_succ_truncate (m : ℕ) (X : WittVector p ℛ) :
    wLevel p ℛ (m + 1) (WittVector.truncate (m + 1) X) = WittGhost.divGhost p m X :=
  AddMonoidHom.liftOfRightInverse_comp_apply _ _ (fun x => TruncatedWittVector.truncateFun_out x) _ _

theorem wLevel_shift (n : ℕ) (x : TruncatedWittVector p n ℛ) :
    wLevel p ℛ (n + 1) (TruncWitt.shift x) = wLevel p ℛ n x := by
  obtain ⟨X, rfl⟩ := WittVector.truncate_surjective p n ℛ x
  cases n with
  | zero =>
    rw [TruncWitt.shift_truncate, wLevel_succ_truncate, WittGhost.divGhost_zero_verschiebung,
      wLevel_zero_apply]
  | succ m =>
    rw [TruncWitt.shift_truncate, wLevel_succ_truncate, wLevel_succ_truncate,
      WittGhost.divGhost_verschiebung]

noncomputable def wUp : UnipotentWittCovector p ℛ →+ Localization.Away (p : ℛ) :=
  lift p ℛ (wLevel p ℛ) fun n x => wLevel_shift p ℛ n x

variable {ℛ}
variable {n : ℕ}

@[simp] theorem wUp_of (x : TruncatedWittVector p n ℛ) : wUp p ℛ (of p ℛ n x) = wLevel p ℛ n x :=
  lift_of _ _ _

theorem wUp_of_truncate (m : ℕ) (X : WittVector p ℛ) :
    wUp p ℛ (of p ℛ (m + 1) (WittVector.truncate (m + 1) X)) = WittGhost.divGhost p m X := by
  rw [wUp_of, wLevel_succ_truncate]

theorem wUp_of_zero (x : TruncatedWittVector p 0 ℛ) : wUp p ℛ (of p ℛ 0 x) = 0 := by
  rw [wUp_of, wLevel_zero_apply]

theorem wUp_map {ℛ' : Type v} [CommRing ℛ'] (f : ℛ →+* ℛ') (z : UnipotentWittCovector p ℛ) :
    wUp p ℛ' (map p f z) = PLoc.map p f (wUp p ℛ z) := by
  induction z using UnipotentWittCovector.induction_on with
  | ih n x =>
    obtain ⟨X, rfl⟩ := WittVector.truncate_surjective p n ℛ x
    rw [map_of, TruncWitt.map_truncate]
    cases n with
    | zero => rw [wUp_of_zero, wUp_of_zero, map_zero]
    | succ m => rw [wUp_of_truncate, wUp_of_truncate, WittGhost.divGhost_map]

end WUp

section WRel

variable (p : ℕ) [hp : Fact p.Prime] {ℛ : Type u} [CommRing ℛ] {A : Type v} [CommRing A] (π : ℛ →+* A)

theorem map_surjective (hπs : Surjective π) : Surjective (map p π) := by
  intro z
  induction z using UnipotentWittCovector.induction_on with
  | ih n x =>
    obtain ⟨X, rfl⟩ := TruncWitt.exists_truncate_map_eq (p := p) (n := n) hπs x
    exact ⟨of p ℛ n (WittVector.truncate n X), by rw [map_of, TruncWitt.map_truncate]⟩

theorem wUp_of_sub_wUp_of_mem_pSub (hπ : RingHom.ker π ≤ Ideal.span {(p : ℛ)}) {N : ℕ}
    {y y' : TruncatedWittVector p N ℛ} (h : TruncWitt.map π y = TruncWitt.map π y') :
    wUp p ℛ (of p ℛ N y) - wUp p ℛ (of p ℛ N y') ∈ PLoc.pSub p ℛ := by
  obtain ⟨Y, rfl⟩ := WittVector.truncate_surjective p N ℛ y
  obtain ⟨Y', rfl⟩ := WittVector.truncate_surjective p N ℛ y'
  rw [TruncWitt.map_truncate, TruncWitt.map_truncate] at h
  cases N with
  | zero => rw [wUp_of_zero, wUp_of_zero, sub_zero]; exact zero_mem _
  | succ m =>
    rw [wUp_of_truncate, wUp_of_truncate]
    exact WittGhost.divGhost_sub_mem_pSub_of_truncate_map_eq p π hπ h

theorem wUp_sub_wUp_mem_pSub (hπ : RingHom.ker π ≤ Ideal.span {(p : ℛ)})
    {Z Z' : UnipotentWittCovector p ℛ} (h : map p π Z = map p π Z') :
    wUp p ℛ Z - wUp p ℛ Z' ∈ PLoc.pSub p ℛ := by
  obtain ⟨n, x, rfl⟩ := exists_of Z
  obtain ⟨n', x', rfl⟩ := exists_of Z'

  rw [← of_shiftLE (le_max_left n n') x, ← of_shiftLE (le_max_right n n') x'] at h ⊢
  rw [map_of, map_of] at h
  exact wUp_of_sub_wUp_of_mem_pSub p π hπ (of_injective _ h)

open Classical in

noncomputable def w (z : UnipotentWittCovector p A) : Localization.Away (p : ℛ) ⧸ PLoc.pSub p ℛ :=
  if h : ∃ Z : UnipotentWittCovector p ℛ, map p π Z = z then
    Submodule.Quotient.mk (wUp p ℛ (Classical.choose h)) else 0

theorem w_map (hπ : RingHom.ker π ≤ Ideal.span {(p : ℛ)}) (Z : UnipotentWittCovector p ℛ) :
    w p π (map p π Z) = Submodule.Quotient.mk (wUp p ℛ Z) := by
  have h : ∃ Z' : UnipotentWittCovector p ℛ, map p π Z' = map p π Z := ⟨Z, rfl⟩
  rw [w, dif_pos h, Submodule.Quotient.eq]
  exact wUp_sub_wUp_mem_pSub p π hπ (Classical.choose_spec h)

theorem w_of_truncate_map (hπ : RingHom.ker π ≤ Ideal.span {(p : ℛ)}) (m : ℕ) (X : WittVector p ℛ) :
    w p π (of p A (m + 1) (WittVector.truncate (m + 1) (WittVector.map π X))) =
      Submodule.Quotient.mk (WittGhost.divGhost p m X) := by
  rw [← TruncWitt.map_truncate, ← map_of, w_map p π hπ, wUp_of_truncate]

theorem w_zero (hπ : RingHom.ker π ≤ Ideal.span {(p : ℛ)}) : w p π (0 : UnipotentWittCovector p A) = 0 := by
  rw [← map_zero (map p π), w_map p π hπ, map_zero, Submodule.Quotient.mk_zero]

noncomputable def wHom (hπ : RingHom.ker π ≤ Ideal.span {(p : ℛ)}) (hπs : Surjective π) :
    UnipotentWittCovector p A →+ Localization.Away (p : ℛ) ⧸ PLoc.pSub p ℛ where
  toFun := w p π
  map_zero' := w_zero p π hπ
  map_add' z z' := by
    obtain ⟨Z, rfl⟩ := map_surjective p π hπs z
    obtain ⟨Z', rfl⟩ := map_surjective p π hπs z'
    rw [← map_add, w_map p π hπ, w_map p π hπ, w_map p π hπ, map_add, Submodule.Quotient.mk_add]

@[simp] theorem wHom_apply (hπ : RingHom.ker π ≤ Ideal.span {(p : ℛ)}) (hπs : Surjective π)
    (z : UnipotentWittCovector p A) : wHom p π hπ hπs z = w p π z := rfl

theorem w_eq_zero_iff_mem_wKer (hp' : (p : ℛ) ∈ nonZeroDivisors ℛ)
    (hπ : RingHom.ker π ≤ Ideal.span {(p : ℛ)}) (hπs : Surjective π) (z : UnipotentWittCovector p A) :
    w p π z = 0 ↔ z ∈ wKer p π := by
  obtain ⟨n, x, rfl⟩ := exists_of z
  obtain ⟨X, rfl⟩ := TruncWitt.exists_truncate_map_eq (p := p) (n := n) hπs x
  cases n with
  | zero =>
    rw [of_zero_eq_zero, w_zero p π hπ]
    exact ⟨fun _ => zero_mem _, fun _ => rfl⟩
  | succ m =>
    rw [w_of_truncate_map p π hπ, Submodule.Quotient.mk_eq_zero, WittGhost.divGhost_mem_pSub_iff p hp',
      of_mem_wKer_iff hp' hπ hπs, TruncWitt.truncate_map_mem_fontaineKer_iff hπ, Nat.add_sub_cancel]

theorem w_map_map {ℛ' : Type w} [CommRing ℛ'] {A' : Type u'} [CommRing A'] (f : ℛ →+* ℛ')
    (φ : A →+* A') (π' : ℛ' →+* A') (hcomm : π'.comp f = φ.comp π)
    (hπ' : RingHom.ker π' ≤ Ideal.span {(p : ℛ')}) (Z : UnipotentWittCovector p ℛ) :
    w p π' (map p φ (map p π Z)) = Submodule.Quotient.mk (PLoc.map p f (wUp p ℛ Z)) := by
  rw [map_map, ← hcomm, ← map_map, w_map p π' hπ', wUp_map]

end WRel

end UnipotentWittCovector

namespace HondaSystem

variable {𝓞 : Type u} [CommRing 𝓞] (p : ℕ) [hp : Fact p.Prime]
variable {M : Type v} [AddCommGroup M] [Module 𝓞 M] (H : HondaSystem (p : 𝓞) M)
variable (k : Type w) [CommRing k] [CharP k p]
variable {g : Type u'} [CommRing g] [Algebra 𝓞 g] {S : Type v'} [CommRing S] [Algebra k S] (π : g →+* S)

noncomputable def fontaineFunctor :
    AddSubgroup ((H.L →ₗ[𝓞] Localization.Away (p : g)) × (M →+ UnipotentWittCovector p S)) where
  carrier := {x |
    (∀ m, x.2 (H.F m) = UnipotentWittCovector.frobenius k p S (x.2 m)) ∧
    (∀ m, x.2 (H.V m) = UnipotentWittCovector.verschiebung p S (x.2 m)) ∧
    ∀ l : H.L, ∃ Z : UnipotentWittCovector p g, UnipotentWittCovector.map p π Z = x.2 l ∧
      (Submodule.Quotient.mk (x.1 l) : Localization.Away (p : g) ⧸ PLoc.pSub p g) =
        Submodule.Quotient.mk (UnipotentWittCovector.wUp p g Z)}
  zero_mem' := ⟨fun m => by simp, fun m => by simp, fun l => ⟨0, by simp, by simp⟩⟩
  add_mem' := by
    rintro x y ⟨hxF, hxV, hxL⟩ ⟨hyF, hyV, hyL⟩
    refine ⟨fun m => ?_, fun m => ?_, fun l => ?_⟩
    · rw [Prod.snd_add, AddMonoidHom.add_apply, AddMonoidHom.add_apply, hxF, hyF, map_add]
    · rw [Prod.snd_add, AddMonoidHom.add_apply, AddMonoidHom.add_apply, hxV, hyV, map_add]
    · obtain ⟨Z, hZ, hx⟩ := hxL l
      obtain ⟨Z', hZ', hy⟩ := hyL l
      refine ⟨Z + Z', by rw [map_add, hZ, hZ', Prod.snd_add, AddMonoidHom.add_apply], ?_⟩
      rw [Prod.fst_add, LinearMap.add_apply, map_add, Submodule.Quotient.mk_add,
        Submodule.Quotient.mk_add, hx, hy]
  neg_mem' := by
    rintro x ⟨hxF, hxV, hxL⟩
    refine ⟨fun m => ?_, fun m => ?_, fun l => ?_⟩
    · rw [Prod.snd_neg, AddMonoidHom.neg_apply, AddMonoidHom.neg_apply, hxF, map_neg]
    · rw [Prod.snd_neg, AddMonoidHom.neg_apply, AddMonoidHom.neg_apply, hxV, map_neg]
    · obtain ⟨Z, hZ, hx⟩ := hxL l
      refine ⟨-Z, by rw [map_neg, hZ, Prod.snd_neg, AddMonoidHom.neg_apply], ?_⟩
      rw [Prod.fst_neg, LinearMap.neg_apply, map_neg, Submodule.Quotient.mk_neg,
        Submodule.Quotient.mk_neg, hx]

variable {p H k π}

theorem mem_fontaineFunctor_iff
    (x : (H.L →ₗ[𝓞] Localization.Away (p : g)) × (M →+ UnipotentWittCovector p S)) :
    x ∈ fontaineFunctor p H k π ↔
      (∀ m, x.2 (H.F m) = UnipotentWittCovector.frobenius k p S (x.2 m)) ∧
      (∀ m, x.2 (H.V m) = UnipotentWittCovector.verschiebung p S (x.2 m)) ∧
      ∀ l : H.L, ∃ Z : UnipotentWittCovector p g, UnipotentWittCovector.map p π Z = x.2 l ∧
        (Submodule.Quotient.mk (x.1 l) : Localization.Away (p : g) ⧸ PLoc.pSub p g) =
          Submodule.Quotient.mk (UnipotentWittCovector.wUp p g Z) :=
  Iff.rfl

theorem fst_sub_wUp_mem_pSub (hπ : RingHom.ker π ≤ Ideal.span {(p : g)})
    {x : (H.L →ₗ[𝓞] Localization.Away (p : g)) × (M →+ UnipotentWittCovector p S)}
    (hx : x ∈ fontaineFunctor p H k π) (l : H.L) {Z : UnipotentWittCovector p g}
    (hZ : UnipotentWittCovector.map p π Z = x.2 l) :
    x.1 l - UnipotentWittCovector.wUp p g Z ∈ PLoc.pSub p g := by
  obtain ⟨Z', hZ', h⟩ := hx.2.2 l
  rw [Submodule.Quotient.eq] at h
  have h2 := UnipotentWittCovector.wUp_sub_wUp_mem_pSub p π hπ (hZ'.trans hZ.symm)
  have := add_mem h h2
  rwa [sub_add_sub_cancel] at this

theorem mk_fst_eq_w_snd (hπ : RingHom.ker π ≤ Ideal.span {(p : g)})
    {x : (H.L →ₗ[𝓞] Localization.Away (p : g)) × (M →+ UnipotentWittCovector p S)}
    (hx : x ∈ fontaineFunctor p H k π) (l : H.L) :
    (Submodule.Quotient.mk (x.1 l) : Localization.Away (p : g) ⧸ PLoc.pSub p g) =
      UnipotentWittCovector.w p π (x.2 l) := by
  obtain ⟨Z, hZ, h⟩ := hx.2.2 l
  rw [← hZ, UnipotentWittCovector.w_map p π hπ, h]

theorem zero_prod_mem_fontaineFunctor_iff (hp' : (p : g) ∈ nonZeroDivisors g)
    (hπ : RingHom.ker π ≤ Ideal.span {(p : g)}) (hπs : Surjective π)
    (η : M →+ UnipotentWittCovector p S) :
    ((0, η) : (H.L →ₗ[𝓞] Localization.Away (p : g)) × (M →+ UnipotentWittCovector p S)) ∈
        fontaineFunctor p H k π ↔
      (∀ m, η (H.F m) = UnipotentWittCovector.frobenius k p S (η m)) ∧
      (∀ m, η (H.V m) = UnipotentWittCovector.verschiebung p S (η m)) ∧
      ∀ l : H.L, η l ∈ UnipotentWittCovector.wKer p π := by
  refine ⟨fun ⟨hF, hV, hL⟩ => ⟨hF, hV, fun l => ?_⟩, fun ⟨hF, hV, hL⟩ => ⟨hF, hV, fun l => ?_⟩⟩
  · obtain ⟨Z, hZ, h⟩ := hL l
    rw [← UnipotentWittCovector.w_eq_zero_iff_mem_wKer p π hp' hπ hπs, ← hZ,
      UnipotentWittCovector.w_map p π hπ, ← h, LinearMap.zero_apply, Submodule.Quotient.mk_zero]
  · obtain ⟨Z, hZ⟩ := UnipotentWittCovector.map_surjective p π hπs (η l)
    refine ⟨Z, hZ, ?_⟩
    have := (UnipotentWittCovector.w_eq_zero_iff_mem_wKer p π hp' hπ hπs (η l)).2 (hL l)
    rw [← hZ, UnipotentWittCovector.w_map p π hπ] at this
    rw [LinearMap.zero_apply, Submodule.Quotient.mk_zero, this]

theorem map_mem_fontaineFunctor {g' : Type w'} [CommRing g'] [Algebra 𝓞 g'] {S' : Type v}
    [CommRing S'] [Algebra k S'] (π' : g' →+* S') (f : g →ₐ[𝓞] g') (φ : S →ₐ[k] S')
    (hcomm : π'.comp f.toRingHom = φ.toRingHom.comp π)
    {x : (H.L →ₗ[𝓞] Localization.Away (p : g)) × (M →+ UnipotentWittCovector p S)}
    (hx : x ∈ fontaineFunctor p H k π) :
    ((PLoc.mapLinear p f).comp x.1, (UnipotentWittCovector.map p φ.toRingHom).comp x.2) ∈
      fontaineFunctor p H k π' := by
  obtain ⟨hF, hV, hL⟩ := hx
  refine ⟨fun m => ?_, fun m => ?_, fun l => ?_⟩
  · rw [AddMonoidHom.comp_apply, AddMonoidHom.comp_apply, hF, UnipotentWittCovector.map_frobenius k k]
  · rw [AddMonoidHom.comp_apply, AddMonoidHom.comp_apply, hV, UnipotentWittCovector.map_verschiebung]
  · obtain ⟨Z, hZ, h⟩ := hL l
    refine ⟨UnipotentWittCovector.map p f.toRingHom Z, ?_, ?_⟩
    · rw [AddMonoidHom.comp_apply, ← hZ, UnipotentWittCovector.map_map,
        UnipotentWittCovector.map_map, hcomm]
    · rw [Submodule.Quotient.eq] at h ⊢
      rw [LinearMap.comp_apply, PLoc.mapLinear_apply, UnipotentWittCovector.wUp_map, ← map_sub]
      exact PLoc.map_mem_pSub p f.toRingHom h

end HondaSystem

namespace UnipotentWittCovector.Examples

variable (p : ℕ) [hp : Fact p.Prime] (S : Type v) [CommRing S]

theorem wUp_one : wUp p S (one p S) = 1 := by
  have h1 : (TruncatedWittVector.mk p fun _ : Fin 1 => (1 : S)) = WittVector.truncate 1 1 := by
    ext i
    rw [TruncatedWittVector.coeff_mk, WittVector.coeff_truncate, Fin.val_eq_zero i,
      WittVector.one_coeff_zero]
  rw [one, h1, wUp_of_truncate, WittGhost.divGhost_zero_apply, WittVector.one_coeff_zero, map_one]

end UnipotentWittCovector.Examples

namespace HondaSystem.Examples

variable {𝓞 : Type u} [CommRing 𝓞] (p : ℕ) [hp : Fact p.Prime]

noncomputable def mult : HondaSystem (p : 𝓞) 𝓞 where
  toDieudonneDatum := DieudonneDatum.multOne (p : 𝓞)
  L := ⊤
  sh1_le x _ hx := by
    obtain ⟨y, rfl⟩ := hx
    exact ⟨y, Submodule.mem_top, rfl⟩
  sh1_ge y _ := ⟨y, rfl⟩
  sh2' := sup_top_eq _
  sh3 x _ hx := hx

variable (k : Type w) [CommRing k] [CharP k p]
variable {g : Type u'} [CommRing g] [Algebra 𝓞 g] {S : Type v'} [CommRing S] [Algebra k S] (π : g →+* S)

noncomputable def unitMap : (mult (𝓞 := 𝓞) p).L →ₗ[𝓞] Localization.Away (p : g) :=
  (Algebra.linearMap 𝓞 (Localization.Away (p : g))).comp (Submodule.subtype _)

omit hp in
theorem unitMap_apply (l : (mult (𝓞 := 𝓞) p).L) :
    unitMap (𝓞 := 𝓞) p (g := g) l = algebraMap 𝓞 (Localization.Away (p : g)) l := rfl

theorem not_mem_fontaineFunctor (hπ : RingHom.ker π ≤ Ideal.span {(p : g)})
    (h1 : (1 : Localization.Away (p : g)) ∉ PLoc.pSub p g) :
    ((unitMap (𝓞 := 𝓞) p, 0) :
        ((mult (𝓞 := 𝓞) p).L →ₗ[𝓞] Localization.Away (p : g)) × (𝓞 →+ UnipotentWittCovector p S)) ∉
      fontaineFunctor p (mult (𝓞 := 𝓞) p) k π := by
  intro hmem
  have := fst_sub_wUp_mem_pSub (k := k) hπ hmem ⟨1, Submodule.mem_top⟩ (Z := 0)
    (by rw [map_zero]; rfl)
  rw [unitMap_apply, map_zero, sub_zero] at this
  exact h1 (by simpa using this)

theorem smul_unitMap_mem_fontaineFunctor :
    (((p : 𝓞) • unitMap (𝓞 := 𝓞) p, 0) :
        ((mult (𝓞 := 𝓞) p).L →ₗ[𝓞] Localization.Away (p : g)) × (𝓞 →+ UnipotentWittCovector p S)) ∈
      fontaineFunctor p (mult (𝓞 := 𝓞) p) k π := by
  refine ⟨fun m => by simp, fun m => by simp, fun l => ⟨0, by rw [map_zero]; rfl, ?_⟩⟩
  rw [map_zero, LinearMap.smul_apply, unitMap_apply, Submodule.Quotient.eq, sub_zero, Algebra.smul_def,
    IsScalarTower.algebraMap_apply 𝓞 g (Localization.Away (p : g)),
    IsScalarTower.algebraMap_apply 𝓞 g (Localization.Away (p : g)), map_natCast, ← map_mul]
  exact PLoc.algebraMap_mul_mem_pSub p _

end HondaSystem.Examples

end Deformation