Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Dieudonne_FontaineFunctor.lean

definition module

Fontaine's map on unipotent Witt covectors; Fontaine functor

Let p be a prime and \mathcal R a commutative ring, and write \mathcal R[1/p] for Localization.Away (p : ℛ). The namespace PLoc sets up the p-adic geometry of this localisation: invPow p ℛ m is the m-th power of the inverse of the (invertible) image of p, powSub p ℛ s is the \mathcal R-submodule of \mathcal R[1/p] generated by p^s, with pSub the case s=1, and the membership criteria characterise powSub p ℛ s as the set of images of p^s\mathcal R; for p a non-zero-divisor and \mathcal R p-adically Hausdorff the submodules p^s\mathcal R intersect in 0. IsPadicLimit p u α asserts that for each s the terms u_n-\alpha eventually lie in powSub p ℛ s; wPartialSum p a N = \sum_{n<N} p^{-n} a_n^{p^n}, and wSeries p a is a choice of p-adic limit of these partial sums when one exists, and 0 otherwise.

WittGhost.divGhost p m is the additive map W(\mathcal R)\to\mathcal R[1/p], X\mapsto p^{-m}\,\mathrm{ghost}_m(X). It depends only on the truncation of X at level m+1, satisfies \mathrm{divGhost}_{m+1}(VX)=\mathrm{divGhost}_m(X) (and vanishes at m=0 on VX), lands in pSub exactly when \mathrm{ghost}_m(X)\in p^{m+1}\mathcal R (for p a non-zero-divisor), and is compatible with ring maps. These compatibilities let wLevel p ℛ n be defined on W_n(\mathcal R) (0 for n=0, induced by \mathrm{divGhost}_{m} for n=m+1) and assemble, via the shift-compatibility wLevel_shift, into the additive map wUp p ℛ : UnipotentWittCovector p ℛ → ℛ[1/p], Fontaine's w; it commutes with the functoriality maps and sends the covector one to 1.

For \pi:\mathcal R\to A, w p π z is the class in \mathcal R[1/p]/p\mathcal R of \mathrm{wUp}(Z) for a chosen Z with map p π Z = z, and 0 if no such Z exists; when \ker\pi\subseteq p\mathcal R the class is independent of the lift, and with \pi surjective wHom packages it as an additive map, whose vanishing locus is the predicate wKer p π provided p is a non-zero-divisor.

Finally, given a Honda system H with parameter p on an \mathcal O-module M (so F,V with FV=VF=p, together with the submodule L and its three conditions), a commutative ring k of characteristic p, an \mathcal O-algebra g, a k-algebra S and \pi: g\to S, fontaineFunctor p H k π is the subgroup of pairs x=(x_1,x_2) with x_1: L\to g[1/p] an \mathcal O-linear map and x_2: M\to CW^u(S) additive, cut out by: x_2\circ F=\mathrm{Frob}\circ x_2, x_2\circ V=V\circ x_2, and for every l\in L the existence of Z\in CW^u(g) with map p π Z = x₂ l whose \mathrm{wUp}(Z) is congruent to x_1(l) modulo p\,g[1/p]. The accompanying lemmas record that x_1(l)-\mathrm{wUp}(Z)\in p\,g[1/p] for any such lift, that the class of x_1(l) equals w(x_2 l), that (0,\eta) belongs to the subgroup precisely when \eta is F,V-equivariant and carries L into wKer p π, and functoriality along a commuting square (f,\varphi). Examples: the multiplicative Honda system on \mathcal O with F=p, V=\mathrm{id}, L=\top; the map unitMap induced by \mathcal O\to g[1/p], which does not belong to the functor (paired with 0) when 1\notin p\,g[1/p], whereas p\cdot\mathrm{unitMap} does.

Relation to Mathlib

Mathlib supplies Witt vectors, their truncations, ghost components, Verschiebung and Frobenius, and localisation away from an element; the divided ghost components, the p-adic limit predicate, Fontaine's map on unipotent Witt covectors and the Fontaine functor attached to a Honda system are the project's own.

Where it is used

This is the functor whose representability by a smooth formal group over W(k) realises the lifting of a formal group over k singled out by the L-part of a Honda system, the input to the Fontaine–Laffaille style control of finite flat group schemes used in the local deformation-theoretic conditions of the modularity lifting argument.

References

  1. J.-M. Fontaine, Groupes p-divisibles sur les corps locaux, Astérisque 47–48, Société Mathématique de France, 1977, Chap. IV
  2. T. Honda, On the theory of commutative formal groups, J. Math. Soc. Japan 22 (1970), 213–246

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_Dieudonne_FontaineFunctor.lean

Imports

Imported by

  • no other definition module

Declarations

Source

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

Statements phrased using this module (14)