Definitions/Def_CerednikDrinfeld_StandardFormalODModule.lean

import Mathlib
import Definitions.Def_MvFormalGroup_NegV2
import Definitions.Def_CerednikDrinfeld_SpecialFormalModule
import Definitions.Def_CerednikDrinfeld_LubinTateModule

section BoxBasisLemmaAppendix

set_option autoImplicit false
set_option linter.unusedSectionVars false

universe u

noncomputable section

open MvPowerSeries

namespace CerednikDrinfeld.BoxBasisLemma

variable {R : Type*} [CommRing R] {g : ℕ} {N : Fin g → ℕ}

abbrev powIdeal (R : Type*) [CommRing R] (g : ℕ) (N : Fin g → ℕ) : Ideal (MvPowerSeries (Fin g) R) :=
  Ideal.span (Set.range fun i : Fin g => (X i : MvPowerSeries (Fin g) R) ^ N i)

def InBox (N : Fin g → ℕ) (d : Fin g →₀ ℕ) : Prop := ∀ i, d i < N i

instance instDecidableInBox (N : Fin g → ℕ) (d : Fin g →₀ ℕ) : Decidable (InBox N d) := by
  unfold InBox; infer_instance

def boxKer (R : Type*) [CommRing R] (g : ℕ) (N : Fin g → ℕ) : Ideal (MvPowerSeries (Fin g) R) where
  carrier := {θ | ∀ d : Fin g →₀ ℕ, InBox N d → coeff d θ = 0}
  zero_mem' := fun d _ => map_zero _
  add_mem' := by
    intro a b ha hb d hd
    rw [map_add, ha d hd, hb d hd, add_zero]
  smul_mem' := by
    intro c θ hθ d hd
    rw [smul_eq_mul, coeff_mul]
    refine Finset.sum_eq_zero fun x hx => ?_
    rw [Finset.HasAntidiagonal.mem_antidiagonal] at hx
    have hx2 : InBox N x.2 := fun i => lt_of_le_of_lt (by rw [← hx]; simp) (hd i)
    rw [hθ x.2 hx2, mul_zero]

theorem mem_boxKer {θ : MvPowerSeries (Fin g) R} :
    θ ∈ boxKer R g N ↔ ∀ d : Fin g →₀ ℕ, InBox N d → coeff d θ = 0 := Iff.rfl

theorem X_pow_mem_boxKer (i : Fin g) :
    (X i : MvPowerSeries (Fin g) R) ^ N i ∈ boxKer R g N := by
  classical
  intro d hd
  rw [coeff_X_pow, if_neg]
  rintro rfl
  have := hd i
  rw [Finsupp.single_eq_same] at this
  exact lt_irrefl _ this

theorem powIdeal_le_boxKer : powIdeal R g N ≤ boxKer R g N :=
  Ideal.span_le.mpr (by
    rintro _ ⟨i, rfl⟩
    exact X_pow_mem_boxKer i)

def part (N : Fin g → ℕ) (θ : MvPowerSeries (Fin g) R) (i : Fin g) : MvPowerSeries (Fin g) R :=
  fun e => if (∀ j, j < i → e j < N j) then coeff (e + Finsupp.single i (N i)) θ else 0

theorem coeff_part (θ : MvPowerSeries (Fin g) R) (i : Fin g) (e : Fin g →₀ ℕ) :
    coeff e (part N θ i)
      = if (∀ j, j < i → e j < N j) then coeff (e + Finsupp.single i (N i)) θ else 0 :=
  rfl

theorem coeff_X_pow_mul_part (θ : MvPowerSeries (Fin g) R) (i : Fin g) (d : Fin g →₀ ℕ) :
    coeff d ((X i : MvPowerSeries (Fin g) R) ^ N i * part N θ i)
      = if (N i ≤ d i ∧ ∀ j, j < i → d j < N j) then coeff d θ else 0 := by
  classical
  rw [X_pow_eq, coeff_monomial_mul, one_mul]
  by_cases hi : N i ≤ d i
  · have hle : Finsupp.single i (N i) ≤ d := Finsupp.single_le_iff.mpr hi
    rw [if_pos hle, coeff_part]
    have hsub : ∀ j, j < i → (d - Finsupp.single i (N i)) j = d j := by
      intro j hj
      rw [Finsupp.coe_tsub, Pi.sub_apply, Finsupp.single_eq_of_ne (ne_of_lt hj), Nat.sub_zero]
    by_cases hj : ∀ j, j < i → d j < N j
    · rw [if_pos (fun j hj' => by rw [hsub j hj']; exact hj j hj'), if_pos ⟨hi, hj⟩,
        tsub_add_cancel_of_le hle]
    · rw [if_neg (fun h => hj fun j hj' => by rw [← hsub j hj']; exact h j hj'), if_neg]
      exact fun h => hj h.2
  · rw [if_neg (fun h => hi (Finsupp.single_le_iff.mp h)), if_neg]
    exact fun h => hi h.1

theorem eq_sum_X_pow_mul_part {θ : MvPowerSeries (Fin g) R} (hθ : θ ∈ boxKer R g N) :
    θ = ∑ i, (X i : MvPowerSeries (Fin g) R) ^ N i * part N θ i := by
  classical
  refine MvPowerSeries.ext fun d => ?_
  rw [map_sum]
  simp_rw [coeff_X_pow_mul_part]
  by_cases hd : InBox N d
  · rw [hθ d hd, Finset.sum_eq_zero]
    intro i _
    rw [if_neg]
    exact fun h => absurd (hd i) (not_lt.mpr h.1)
  ·
    have hne : (Finset.univ.filter fun i : Fin g => N i ≤ d i).Nonempty := by
      by_contra hc
      rw [Finset.not_nonempty_iff_eq_empty, Finset.filter_eq_empty_iff] at hc
      exact hd fun i => not_le.mp (hc (Finset.mem_univ i))
    set i₀ := (Finset.univ.filter fun i : Fin g => N i ≤ d i).min' hne with hi₀
    have hi₀mem : N i₀ ≤ d i₀ := by
      have := Finset.min'_mem _ hne
      rw [Finset.mem_filter] at this
      exact this.2
    have hi₀min : ∀ j, j < i₀ → d j < N j := by
      intro j hj
      by_contra hc
      have hjmem : j ∈ Finset.univ.filter fun i : Fin g => N i ≤ d i :=
        Finset.mem_filter.mpr ⟨Finset.mem_univ j, not_lt.mp hc⟩
      exact absurd (Finset.min'_le _ j hjmem) (not_le.mpr hj)
    rw [Finset.sum_eq_single i₀]
    · rw [if_pos ⟨hi₀mem, hi₀min⟩]
    · intro j _ hj
      rw [if_neg]
      rintro ⟨hj1, hj2⟩
      rcases lt_trichotomy j i₀ with hlt | heq | hgt
      · exact absurd (hi₀min j hlt) (not_lt.mpr hj1)
      · exact hj heq
      · exact absurd (hj2 i₀ hgt) (not_lt.mpr hi₀mem)
    · intro h
      exact absurd (Finset.mem_univ i₀) h

theorem boxKer_le_powIdeal : boxKer R g N ≤ powIdeal R g N := by
  intro θ hθ
  rw [eq_sum_X_pow_mul_part hθ]
  exact Ideal.sum_mem _ fun i _ => Ideal.mul_mem_right _ _ (Ideal.subset_span ⟨i, rfl⟩)

theorem powIdeal_eq_boxKer : powIdeal R g N = boxKer R g N :=
  le_antisymm powIdeal_le_boxKer boxKer_le_powIdeal

def toFinsupp (u : (i : Fin g) → Fin (N i)) : Fin g →₀ ℕ :=
  Finsupp.equivFunOnFinite.symm fun i => (u i : ℕ)

@[simp] theorem toFinsupp_apply (u : (i : Fin g) → Fin (N i)) (i : Fin g) : toFinsupp u i = u i := rfl

theorem inBox_toFinsupp (u : (i : Fin g) → Fin (N i)) : InBox N (toFinsupp u) := fun i => (u i).isLt

def extend (v : ((i : Fin g) → Fin (N i)) → R) : MvPowerSeries (Fin g) R :=
  fun d => if h : InBox N d then v (fun i => ⟨d i, h i⟩) else 0

theorem coeff_extend (v : ((i : Fin g) → Fin (N i)) → R) (d : Fin g →₀ ℕ) :
    coeff d (extend v) = if h : InBox N d then v (fun i => ⟨d i, h i⟩) else 0 :=
  rfl

theorem coeff_extend_toFinsupp (v : ((i : Fin g) → Fin (N i)) → R) (u : (i : Fin g) → Fin (N i)) :
    coeff (toFinsupp u) (extend v) = v u := by
  rw [coeff_extend, dif_pos (inBox_toFinsupp u)]
  rfl

theorem coeff_extend_of_not (v : ((i : Fin g) → Fin (N i)) → R) {d : Fin g →₀ ℕ}
    (hd : ¬ InBox N d) : coeff d (extend v) = 0 := by
  rw [coeff_extend, dif_neg hd]

theorem toFinsupp_mk {d : Fin g →₀ ℕ} (h : InBox N d) :
    toFinsupp (fun i => (⟨d i, h i⟩ : Fin (N i))) = d := by
  ext i
  rfl

def extendLin (R : Type*) [CommRing R] (g : ℕ) (N : Fin g → ℕ) :
    (((i : Fin g) → Fin (N i)) → R) →ₗ[R] (MvPowerSeries (Fin g) R ⧸ powIdeal R g N) :=
  (Ideal.Quotient.mkₐ R (powIdeal R g N)).toLinearMap ∘ₗ
    { toFun := extend
      map_add' := fun v w => by
        refine MvPowerSeries.ext fun d => ?_
        rw [map_add, coeff_extend, coeff_extend, coeff_extend]
        split_ifs <;> simp
      map_smul' := fun c v => by
        refine MvPowerSeries.ext fun d => ?_
        rw [map_smul, coeff_extend, coeff_extend, RingHom.id_apply, smul_eq_mul]
        split_ifs <;> simp }

theorem extendLin_apply (v : ((i : Fin g) → Fin (N i)) → R) :
    extendLin R g N v = Ideal.Quotient.mk (powIdeal R g N) (extend v) := rfl

theorem extendLin_injective : Function.Injective (extendLin R g N) := by
  rw [injective_iff_map_eq_zero]
  intro v hv
  rw [extendLin_apply, Ideal.Quotient.eq_zero_iff_mem, powIdeal_eq_boxKer] at hv
  funext u
  rw [← coeff_extend_toFinsupp v u]
  exact hv _ (inBox_toFinsupp u)

theorem extendLin_surjective : Function.Surjective (extendLin R g N) := by
  intro x
  obtain ⟨θ, rfl⟩ := Ideal.Quotient.mk_surjective x
  refine ⟨fun u => coeff (toFinsupp u) θ, ?_⟩
  rw [extendLin_apply, Ideal.Quotient.eq, powIdeal_eq_boxKer]
  intro d hd
  rw [map_sub, coeff_extend, dif_pos hd, toFinsupp_mk hd, sub_self]

def boxEquiv (R : Type*) [CommRing R] (g : ℕ) (N : Fin g → ℕ) :
    (((i : Fin g) → Fin (N i)) → R) ≃ₗ[R] (MvPowerSeries (Fin g) R ⧸ powIdeal R g N) :=
  LinearEquiv.ofBijective (extendLin R g N) ⟨extendLin_injective, extendLin_surjective⟩

end CerednikDrinfeld.BoxBasisLemma

end

open CerednikDrinfeld.BoxBasisLemma in
theorem CerednikDrinfeld.BoxBasisLemma.free_and_finite_and_finrank_quotient_span_range_X_pow (R : Type u) [CommRing R] [Nontrivial R] (g : ℕ) (N : Fin g → ℕ) :
    Module.Free R (MvPowerSeries (Fin g) R ⧸
        Ideal.span (Set.range fun i : Fin g => (MvPowerSeries.X i : MvPowerSeries (Fin g) R) ^ N i)) ∧
      Module.Finite R (MvPowerSeries (Fin g) R ⧸
        Ideal.span (Set.range fun i : Fin g => (MvPowerSeries.X i : MvPowerSeries (Fin g) R) ^ N i)) ∧
      Module.finrank R (MvPowerSeries (Fin g) R ⧸
        Ideal.span (Set.range fun i : Fin g => (MvPowerSeries.X i : MvPowerSeries (Fin g) R) ^ N i))
          = ∏ i, N i := by
  refine ⟨Module.Free.of_equiv (boxEquiv R g N), Module.Finite.equiv (boxEquiv R g N), ?_⟩
  rw [← (boxEquiv R g N).finrank_eq, Module.finrank_fintype_fun_eq_card, Fintype.card_pi]
  simp only [Fintype.card_fin]

end BoxBasisLemmaAppendix

set_option autoImplicit false
set_option linter.unusedSectionVars false

noncomputable section

open MvPowerSeries CerednikDrinfeld CerednikDrinfeld.SpecialFormal CerednikDrinfeld.LubinTate

namespace CerednikDrinfeld.Standard

universe u v

variable {p : ℕ} [Fact p.Prime]

local notation "𝕆" => Zp2 p
local notation "𝔮" => Fintype.card (GaloisField p 2)

section Standard

def lawLin (i : Fin 2) : Fin 2 ⊕ Fin 2 → 𝕆 :=
  Sum.elim (fun j => if j = i then 1 else 0) (fun j => if j = i then 1 else 0)

theorem sum_lawLin_mul (i : Fin 2) (g : Fin 2 ⊕ Fin 2 → 𝕆) :
    ∑ v, lawLin (p := p) i v * g v = g (Sum.inl i) + g (Sum.inr i) := by
  rw [Fintype.sum_sum_type]
  simp only [lawLin, Sum.elim_inl, Sum.elim_inr, ite_mul, one_mul, zero_mul,
    Finset.sum_ite_eq', Finset.mem_univ, if_true]

theorem lawLin_eq (i : Fin 2) (v : Fin 2 ⊕ Fin 2) :
    lawLin (p := p) i v = (if v = Sum.inl i then 1 else 0) + (if v = Sum.inr i then 1 else 0) := by
  rcases v with j | j <;> by_cases h : j = i <;> simp [lawLin, h]

variable (p)

def lawSeries (i : Fin 2) : MvPowerSeries (Fin 2 ⊕ Fin 2) 𝕆 := lt p (Fin 2 ⊕ Fin 2) (lawLin i)

variable {p}

theorem constantCoeff_lawSeries (i : Fin 2) : constantCoeff (lawSeries p i) = 0 := constantCoeff_lt _

theorem comm_lawSeries (i : Fin 2) : Comm p (lawSeries p i) := comm_lt _

theorem coeff_single_lawSeries (i : Fin 2) (v : Fin 2 ⊕ Fin 2) :
    coeff (Finsupp.single v 1) (lawSeries p i)
      = (if v = Sum.inl i then 1 else 0) + (if v = Sum.inr i then 1 else 0) := by
  rw [lawSeries, coeff_single_lt, lawLin_eq]

theorem coeff_single_subst_lawSeries {τ : Type*} [Fintype τ] (i : Fin 2)
    {a : Fin 2 ⊕ Fin 2 → MvPowerSeries τ 𝕆} (ha0 : ∀ v, constantCoeff (a v) = 0) (t : τ) :
    coeff (Finsupp.single t 1) (subst a (lawSeries p i))
      = coeff (Finsupp.single t 1) (a (Sum.inl i)) + coeff (Finsupp.single t 1) (a (Sum.inr i)) := by
  rw [lawSeries, coeff_single_subst_lt _ ha0, sum_lawLin_mul]

def law : MvFormalGroup 2 𝕆 where
  toPowerSeries := lawSeries p
  constantCoeff_eq_zero := constantCoeff_lawSeries
  coeff_single_inl i j := by
    rw [coeff_single_lawSeries]
    by_cases h : i = j
    · subst h; simp
    · simp [h, Ne.symm h]
  coeff_single_inr i j := by
    rw [coeff_single_lawSeries]
    by_cases h : i = j
    · subst h; simp
    · simp [h, Ne.symm h]
  assoc i := by
    classical

    have hB : ∀ s : Fin 2 ⊕ Fin 2, constantCoeff ((Sum.elim
        (fun l => (X (Sum.inl l) : MvPowerSeries (Fin 2 ⊕ (Fin 2 ⊕ Fin 2)) 𝕆))
        fun l => X (Sum.inr (Sum.inl l))) s) = 0 := by
      rintro (l | l) <;> exact constantCoeff_X _
    have hC : ∀ s : Fin 2 ⊕ Fin 2, constantCoeff ((Sum.elim
        (fun l => (X (Sum.inr (Sum.inl l)) : MvPowerSeries (Fin 2 ⊕ (Fin 2 ⊕ Fin 2)) 𝕆))
        fun l => X (Sum.inr (Sum.inr l))) s) = 0 := by
      rintro (l | l) <;> exact constantCoeff_X _
    have hBv : (Sum.elim (fun l => (X (Sum.inl l) : MvPowerSeries (Fin 2 ⊕ (Fin 2 ⊕ Fin 2)) 𝕆))
        fun l => X (Sum.inr (Sum.inl l))) = fun s => X (Sum.elim (fun l => Sum.inl l)
          (fun l => Sum.inr (Sum.inl l)) s) := by
      funext s; rcases s with l | l <;> rfl
    have hCv : (Sum.elim
        (fun l => (X (Sum.inr (Sum.inl l)) : MvPowerSeries (Fin 2 ⊕ (Fin 2 ⊕ Fin 2)) 𝕆))
        fun l => X (Sum.inr (Sum.inr l))) = fun s => X (Sum.elim (fun l => Sum.inr (Sum.inl l))
          (fun l => Sum.inr (Sum.inr l)) s) := by
      funext s; rcases s with l | l <;> rfl
    have hA : ∀ s : Fin 2 ⊕ Fin 2, constantCoeff ((Sum.elim
        (fun j => subst (Sum.elim
          (fun l => (X (Sum.inl l) : MvPowerSeries (Fin 2 ⊕ (Fin 2 ⊕ Fin 2)) 𝕆))
          fun l => X (Sum.inr (Sum.inl l))) (lawSeries p j))
        fun j => X (Sum.inr (Sum.inr j))) s) = 0 := by
      rintro (j | j)
      · exact constantCoeff_subst_of (constantCoeff_lawSeries j) hB
      · exact constantCoeff_X _
    have hA' : ∀ s : Fin 2 ⊕ Fin 2, constantCoeff ((Sum.elim
        (fun j => (X (Sum.inl j) : MvPowerSeries (Fin 2 ⊕ (Fin 2 ⊕ Fin 2)) 𝕆))
        fun j => subst (Sum.elim
          (fun l => (X (Sum.inr (Sum.inl l)) : MvPowerSeries (Fin 2 ⊕ (Fin 2 ⊕ Fin 2)) 𝕆))
          fun l => X (Sum.inr (Sum.inr l))) (lawSeries p j)) s) = 0 := by
      rintro (j | j)
      · exact constantCoeff_X _
      · exact constantCoeff_subst_of (constantCoeff_lawSeries j) hC
    refine eq_of_comm (constantCoeff_subst_of (constantCoeff_lawSeries i) hA)
      (constantCoeff_subst_of (constantCoeff_lawSeries i) hA') ?_ ?_ ?_
    · refine comm_subst (comm_lawSeries i) hA ?_
      rintro (j | j)
      · show Comm p (subst _ (lawSeries p j))
        rw [hBv]
        exact comm_subst_X (comm_lawSeries j) _
      · exact comm_X _
    · refine comm_subst (comm_lawSeries i) hA' ?_
      rintro (j | j)
      · exact comm_X _
      · show Comm p (subst _ (lawSeries p j))
        rw [hCv]
        exact comm_subst_X (comm_lawSeries j) _
    · intro t
      rw [coeff_single_subst_lawSeries i hA, coeff_single_subst_lawSeries i hA']
      simp only [Sum.elim_inl, Sum.elim_inr]
      rw [coeff_single_subst_lawSeries i hB, coeff_single_subst_lawSeries i hC]
      simp only [Sum.elim_inl, Sum.elim_inr]
      exact add_assoc _ _ _

instance law_isComm : (law (p := p)).IsComm where
  comm i := by
    classical
    have hS : ∀ s : Fin 2 ⊕ Fin 2, constantCoeff ((Sum.elim
        (fun j => (X (Sum.inr j) : MvPowerSeries (Fin 2 ⊕ Fin 2) 𝕆))
        fun j => X (Sum.inl j)) s) = 0 := by
      rintro (j | j) <;> exact constantCoeff_X _
    have hSv : (Sum.elim (fun j => (X (Sum.inr j) : MvPowerSeries (Fin 2 ⊕ Fin 2) 𝕆))
        fun j => X (Sum.inl j)) = fun s => X (Sum.swap s) := by
      funext s; rcases s with l | l <;> rfl
    show subst _ (lawSeries p i) = lawSeries p i
    refine eq_of_comm (constantCoeff_subst_of (constantCoeff_lawSeries i) hS)
      (constantCoeff_lawSeries i) ?_ (comm_lawSeries i) ?_
    · rw [hSv]
      exact comm_subst_X (comm_lawSeries i) _
    · intro t
      rw [coeff_single_subst_lawSeries i hS, coeff_single_lawSeries]
      simp only [Sum.elim_inl, Sum.elim_inr, coeff_index_single_X]
      exact add_comm _ _

def chi (i : Fin 2) : 𝕆 →+* 𝕆 := if i = 0 then RingHom.id _ else WittVector.frobenius

@[simp] theorem chi_zero : chi (p := p) 0 = RingHom.id _ := rfl

@[simp] theorem chi_one : chi (p := p) 1 = WittVector.frobenius := rfl

theorem chi_frobenius (i : Fin 2) (a : 𝕆) :
    chi i (WittVector.frobenius a) = WittVector.frobenius (chi i a) := by
  fin_cases i <;> simp

theorem chi_natCast (i : Fin 2) : chi i (p : 𝕆) = p := map_natCast _ _

variable (p)

def actSeries (a : 𝕆) : Series 𝕆 := fun i => lt p (Fin 2) fun s => if s = i then chi i a else 0

def varpiLin (i s : Fin 2) : 𝕆 := if i = 0 then (if s = 1 then p else 0) else (if s = 0 then 1 else 0)

def varpiSeries : Series 𝕆 := fun i => lt p (Fin 2) (varpiLin p i)

variable {p}

theorem constantCoeff_actSeries (a : 𝕆) (i : Fin 2) : constantCoeff (actSeries p a i) = 0 :=
  constantCoeff_lt _

theorem comm_actSeries (a : 𝕆) (i : Fin 2) : Comm p (actSeries p a i) := comm_lt _

theorem coeff_single_actSeries (a : 𝕆) (i s : Fin 2) :
    coeff (Finsupp.single s 1) (actSeries p a i) = if s = i then chi i a else 0 := by
  rw [actSeries, coeff_single_lt]

theorem coeff_single_subst_actSeries {τ : Type*} [Fintype τ] (a : 𝕆) (i : Fin 2)
    {b : Fin 2 → MvPowerSeries τ 𝕆} (hb0 : ∀ s, constantCoeff (b s) = 0) (t : τ) :
    coeff (Finsupp.single t 1) (subst b (actSeries p a i))
      = chi i a * coeff (Finsupp.single t 1) (b i) := by
  rw [actSeries, coeff_single_subst_lt _ hb0]
  simp only [ite_mul, zero_mul, Finset.sum_ite_eq', Finset.mem_univ, if_true]

theorem constantCoeff_varpiSeries (i : Fin 2) : constantCoeff (varpiSeries p i) = 0 :=
  constantCoeff_lt _

theorem comm_varpiSeries (i : Fin 2) : Comm p (varpiSeries p i) := comm_lt _

theorem coeff_single_varpiSeries (i s : Fin 2) :
    coeff (Finsupp.single s 1) (varpiSeries p i) = varpiLin p i s := by
  rw [varpiSeries, coeff_single_lt]

theorem sum_varpiLin_mul (i : Fin 2) (g : Fin 2 → 𝕆) :
    ∑ s, varpiLin p i s * g s = if i = 0 then (p : 𝕆) * g 1 else g 0 := by
  rw [Fin.sum_univ_two]
  fin_cases i <;> simp [varpiLin]

theorem coeff_single_subst_varpiSeries {τ : Type*} [Fintype τ] (i : Fin 2)
    {b : Fin 2 → MvPowerSeries τ 𝕆} (hb0 : ∀ s, constantCoeff (b s) = 0) (t : τ) :
    coeff (Finsupp.single t 1) (subst b (varpiSeries p i))
      = if i = 0 then (p : 𝕆) * coeff (Finsupp.single t 1) (b 1)
        else coeff (Finsupp.single t 1) (b 0) := by
  rw [varpiSeries, coeff_single_subst_lt _ hb0, sum_varpiLin_mul]

theorem constantCoeff_homFamily {φ : Series 𝕆} (hφ : ∀ i, constantCoeff (φ i) = 0) :
    ∀ s : Fin 2 ⊕ Fin 2, constantCoeff ((Sum.elim
      (fun j => subst (fun l => (X (Sum.inl l) : MvPowerSeries (Fin 2 ⊕ Fin 2) 𝕆)) (φ j))
      fun j => subst (fun l => (X (Sum.inr l) : MvPowerSeries (Fin 2 ⊕ Fin 2) 𝕆)) (φ j)) s) = 0 := by
  rintro (j | j) <;> exact constantCoeff_subst_of (hφ j) (fun l => constantCoeff_X _)

theorem isLawHom_of_comm {φ : Series 𝕆} (h0 : ∀ i, constantCoeff (φ i) = 0)
    (hc : ∀ i, Comm p (φ i)) : IsLawHom (law (p := p)) law φ := by
  classical
  refine ⟨h0, fun i => ?_⟩
  have hF : ∀ j, constantCoeff (lawSeries p j) = 0 := constantCoeff_lawSeries
  have hA := constantCoeff_homFamily h0
  refine eq_of_comm (constantCoeff_subst_of (h0 i) hF)
    (constantCoeff_subst_of (constantCoeff_lawSeries i) hA)
    (comm_subst (hc i) hF comm_lawSeries) (comm_subst (comm_lawSeries i) hA ?_) ?_
  · rintro (j | j) <;> exact comm_subst_X (hc j) _
  · intro t
    show coeff _ (subst (lawSeries p) (φ i)) = coeff _ (subst _ (lawSeries p i))
    rw [coeff_single_subst_lawSeries i hA, MvFormalGroup.coeff_single_subst hF]
    simp only [Sum.elim_inl, Sum.elim_inr, coeff_single_lawSeries]
    rw [MvFormalGroup.coeff_single_subst (fun l => constantCoeff_X _),
      MvFormalGroup.coeff_single_subst (fun l => constantCoeff_X _)]
    simp only [coeff_index_single_X, mul_add, Finset.sum_add_distrib, mul_ite, mul_one, mul_zero]

def standard : FormalODModule p 𝕆 where
  F := law
  isComm := law_isComm
  act := actSeries p
  varpi := varpiSeries p
  isLawHom_act a := isLawHom_of_comm (constantCoeff_actSeries a) (comm_actSeries a)
  isLawHom_varpi := isLawHom_of_comm constantCoeff_varpiSeries comm_varpiSeries
  act_one := by
    classical
    funext i
    refine eq_of_comm (constantCoeff_actSeries 1 i) (constantCoeff_X i) (comm_actSeries 1 i)
      (comm_X i) fun s => ?_
    rw [coeff_single_actSeries, map_one]
    exact (coeff_index_single_X i s).symm
  act_mul a b := by
    classical
    funext i
    refine eq_of_comm (constantCoeff_actSeries _ i)
      (constantCoeff_subst_of (constantCoeff_actSeries a i) (constantCoeff_actSeries b))
      (comm_actSeries _ i) (comm_subst (comm_actSeries a i) (constantCoeff_actSeries b)
        (comm_actSeries b)) fun s => ?_
    show _ = coeff _ (subst (actSeries p b) (actSeries p a i))
    rw [coeff_single_actSeries, coeff_single_subst_actSeries a i (constantCoeff_actSeries b),
      coeff_single_actSeries, map_mul]
    split_ifs <;> ring
  act_add a b := by
    classical
    funext i
    have hab : ∀ s : Fin 2 ⊕ Fin 2, constantCoeff ((Sum.elim (actSeries p a) (actSeries p b)) s) = 0 := by
      rintro (j | j) <;> exact constantCoeff_actSeries _ j
    refine eq_of_comm (constantCoeff_actSeries _ i)
      (constantCoeff_subst_of (constantCoeff_lawSeries i) hab)
      (comm_actSeries _ i) (comm_subst (comm_lawSeries i) hab ?_) fun s => ?_
    · rintro (j | j) <;> exact comm_actSeries _ j
    · show _ = coeff _ (subst _ (lawSeries p i))
      rw [coeff_single_actSeries, coeff_single_subst_lawSeries i hab]
      simp only [Sum.elim_inl, Sum.elim_inr, coeff_single_actSeries, map_add]
      split_ifs <;> ring
  varpi_comp_varpi := by
    classical
    funext i
    refine eq_of_comm
      (constantCoeff_subst_of (constantCoeff_varpiSeries i) constantCoeff_varpiSeries)
      (constantCoeff_actSeries _ i)
      (comm_subst (comm_varpiSeries i) constantCoeff_varpiSeries comm_varpiSeries)
      (comm_actSeries _ i) fun s => ?_
    show coeff _ (subst (varpiSeries p) (varpiSeries p i)) = _
    rw [coeff_single_subst_varpiSeries i constantCoeff_varpiSeries, coeff_single_varpiSeries,
      coeff_single_varpiSeries, coeff_single_actSeries, chi_natCast]
    fin_cases i <;> fin_cases s <;> simp [varpiLin]
  varpi_comp_act a := by
    classical
    funext i
    refine eq_of_comm
      (constantCoeff_subst_of (constantCoeff_varpiSeries i) (constantCoeff_actSeries a))
      (constantCoeff_subst_of (constantCoeff_actSeries _ i) constantCoeff_varpiSeries)
      (comm_subst (comm_varpiSeries i) (constantCoeff_actSeries a) (comm_actSeries a))
      (comm_subst (comm_actSeries _ i) constantCoeff_varpiSeries comm_varpiSeries) fun s => ?_
    show coeff _ (subst (actSeries p a) (varpiSeries p i))
      = coeff _ (subst (varpiSeries p) (actSeries p _ i))
    rw [coeff_single_subst_varpiSeries i (constantCoeff_actSeries a), coeff_single_actSeries,
      coeff_single_actSeries, coeff_single_subst_actSeries _ i constantCoeff_varpiSeries,
      coeff_single_varpiSeries]
    fin_cases i <;> fin_cases s <;> simp [varpiLin, frobenius_frobenius, mul_comm]

theorem standard_act_p : (standard (p := p)).act (p : 𝕆) = fvec p (Fin 2) := by
  classical
  funext i
  refine eq_of_comm (constantCoeff_actSeries _ i) (constantCoeff_fvec i) (comm_actSeries _ i)
    (comm_fvec i) fun s => ?_
  show coeff _ (actSeries p _ i) = _
  rw [coeff_single_actSeries, coeff_single_fvec, chi_natCast]

theorem coeff_single_standard_act (a : 𝕆) (i s : Fin 2) :
    coeff (Finsupp.single s 1) ((standard (p := p)).act a i) = if s = i then chi i a else 0 :=
  coeff_single_actSeries a i s

end Standard

section Identities

def emb (i : Fin 2) : Fin 1 ⊕ Fin 1 → Fin 2 ⊕ Fin 2 := Sum.map (fun _ => i) fun _ => i

@[simp] theorem emb_inl (i : Fin 2) (l : Fin 1) : emb i (Sum.inl l) = Sum.inl i := rfl
@[simp] theorem emb_inr (i : Fin 2) (l : Fin 1) : emb i (Sum.inr l) = Sum.inr i := rfl

theorem lawSeries_eq (i : Fin 2) :
    lawSeries p i = subst (fun s => (X (emb i s) : MvPowerSeries (Fin 2 ⊕ Fin 2) 𝕆))
      (sigmaSeries p) := by
  classical
  have h0 : ∀ s : Fin 1 ⊕ Fin 1, constantCoeff ((X (emb i s) : MvPowerSeries (Fin 2 ⊕ Fin 2) 𝕆)) = 0 :=
    fun s => constantCoeff_X _
  refine eq_of_comm (constantCoeff_lawSeries i) (constantCoeff_subst_of constantCoeff_sigmaSeries h0)
    (comm_lawSeries i) (comm_subst_X comm_sigmaSeries _) fun v => ?_
  rw [coeff_single_lawSeries, coeff_single_subst_sigmaSeries h0]
  simp only [emb_inl, emb_inr, coeff_index_single_X]

theorem actSeries_eq (a : 𝕆) (i : Fin 2) :
    actSeries p a i = subst (fun _ : Fin 1 => (X i : MvPowerSeries (Fin 2) 𝕆)) (act₁ p (chi i a)) := by
  classical
  refine eq_of_comm (constantCoeff_actSeries a i)
    (constantCoeff_subst_of (constantCoeff_act₁ _) fun _ => constantCoeff_X _)
    (comm_actSeries a i) (comm_subst_X (comm_act₁ _) _) fun s => ?_
  rw [coeff_single_actSeries, coeff_single_subst_act₁ _ (fun _ => constantCoeff_X _),
    coeff_index_single_X, mul_ite, mul_one, mul_zero]

theorem varpiSeries_zero :
    varpiSeries p 0 = subst (fun _ : Fin 1 => (X 1 : MvPowerSeries (Fin 2) 𝕆)) (act₁ p (p : 𝕆)) := by
  classical
  refine eq_of_comm (constantCoeff_varpiSeries 0)
    (constantCoeff_subst_of (constantCoeff_act₁ _) fun _ => constantCoeff_X _)
    (comm_varpiSeries 0) (comm_subst_X (comm_act₁ _) _) fun s => ?_
  rw [coeff_single_varpiSeries, coeff_single_subst_act₁ _ (fun _ => constantCoeff_X _),
    coeff_index_single_X, mul_ite, mul_one, mul_zero]
  simp [varpiLin]

theorem varpiSeries_one : varpiSeries p 1 = X 0 := by
  classical
  refine eq_of_comm (constantCoeff_varpiSeries 1) (constantCoeff_X 0) (comm_varpiSeries 1) (comm_X 0)
    fun s => ?_
  rw [coeff_single_varpiSeries, coeff_index_single_X]
  simp [varpiLin]

end Identities

section OverB

variable {B : Type*} [CommRing B] [CharP B p] (j : Zp2 p →+* B)

def modB : FormalODModule p B := (standard (p := p)).map j

theorem lieAct_apply (a : 𝕆) (m : (modB j).Lie) (i : Fin 2) :
    (modB j).lieAct a m i = j (chi i a) * m i := by
  classical
  show (Matrix.mulVecLin (MvFormalGroup.linearPart ((modB j).act a))) m i = _
  rw [Matrix.mulVecLin_apply, Matrix.mulVec, dotProduct]
  simp only [MvFormalGroup.linearPart, Matrix.of_apply]
  show ∑ s, coeff (Finsupp.single s 1) (MvPowerSeries.map j ((standard (p := p)).act a i)) * m s = _
  simp only [MvPowerSeries.coeff_map, coeff_single_standard_act, apply_ite j, map_zero, ite_mul,
    zero_mul, Finset.sum_ite_eq', Finset.mem_univ, if_true]

theorem sub_smul_apply (a : 𝕆) (m : (modB j).Lie) (i : Fin 2) :
    (((modB j).lieAct a - j a • (LinearMap.id : (modB j).Lie →ₗ[B] (modB j).Lie)) m) i
      = (j (chi i a) - j a) * m i := by
  rw [LinearMap.sub_apply, LinearMap.smul_apply, LinearMap.id_apply, Pi.sub_apply,
    Pi.smul_apply, lieAct_apply, smul_eq_mul, sub_mul]

theorem sub_smul_apply' (a : 𝕆) (m : (modB j).Lie) (i : Fin 2) :
    (((modB j).lieAct a - j (WittVector.frobenius a) •
        (LinearMap.id : (modB j).Lie →ₗ[B] (modB j).Lie)) m) i
      = (j (chi i a) - j (WittVector.frobenius a)) * m i := by
  rw [LinearMap.sub_apply, LinearMap.smul_apply, LinearMap.id_apply, Pi.sub_apply,
    Pi.smul_apply, lieAct_apply, smul_eq_mul, sub_mul]

theorem mem_lieZero_iff (m : (modB j).Lie) : m ∈ (modB j).lieZero j ↔ m 1 = 0 := by
  rw [FormalODModule.lieZero, Submodule.mem_iInf]
  constructor
  · intro h
    obtain ⟨a₀, ha₀⟩ := exists_isUnit_frobenius_sub (p := p)
    have h1 := congrFun (LinearMap.mem_ker.mp (h a₀)) 1
    rw [sub_smul_apply, Pi.zero_apply, chi_one, ← map_sub] at h1
    exact (ha₀.map j).mul_right_eq_zero.mp h1
  · intro hm a
    rw [LinearMap.mem_ker]
    funext i
    rw [sub_smul_apply, Pi.zero_apply]
    fin_cases i
    · simp
    · simp [hm]

theorem mem_lieOne_iff (m : (modB j).Lie) : m ∈ (modB j).lieOne j ↔ m 0 = 0 := by
  rw [FormalODModule.lieOne, Submodule.mem_iInf]
  constructor
  · intro h
    obtain ⟨a₀, ha₀⟩ := exists_isUnit_frobenius_sub (p := p)
    have h1 := congrFun (LinearMap.mem_ker.mp (h a₀)) 0
    rw [sub_smul_apply', Pi.zero_apply, chi_zero, RingHom.id_apply, ← map_sub] at h1
    have hu : IsUnit (a₀ - WittVector.frobenius a₀) := by
      rw [← neg_sub]
      exact ha₀.neg
    exact (hu.map j).mul_right_eq_zero.mp h1
  · intro hm a
    rw [LinearMap.mem_ker]
    funext i
    rw [sub_smul_apply', Pi.zero_apply]
    fin_cases i
    · simp [hm]
    · simp

theorem isCompl_lie : IsCompl ((modB j).lieZero j) ((modB j).lieOne j) := by
  refine IsCompl.of_eq ?_ ?_
  · rw [Submodule.eq_bot_iff]
    intro m hm
    rw [Submodule.mem_inf, mem_lieZero_iff, mem_lieOne_iff] at hm
    funext i
    fin_cases i
    · exact hm.2
    · exact hm.1
  · rw [Submodule.eq_top_iff']
    intro m
    rw [Submodule.mem_sup]
    refine ⟨Pi.single 0 (m 0), (mem_lieZero_iff j _).mpr (by simp), Pi.single 1 (m 1),
      (mem_lieOne_iff j _).mpr (by simp), ?_⟩
    funext i
    fin_cases i <;> simp

def lieZeroEquiv : ↥((modB j).lieZero j) ≃ₗ[B] B where
  toFun m := (m : Fin 2 → B) 0
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun b := ⟨Pi.single 0 b, (mem_lieZero_iff j _).mpr (by simp)⟩
  left_inv m := by
    apply Subtype.ext
    funext i
    fin_cases i
    · simp
    · simpa using ((mem_lieZero_iff j _).mp m.2).symm
  right_inv b := by simp

def lieOneEquiv : ↥((modB j).lieOne j) ≃ₗ[B] B where
  toFun m := (m : Fin 2 → B) 1
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun b := ⟨Pi.single 1 b, (mem_lieOne_iff j _).mpr (by simp)⟩
  left_inv m := by
    apply Subtype.ext
    funext i
    fin_cases i
    · simpa using ((mem_lieOne_iff j _).mp m.2).symm
    · simp
  right_inv b := by simp

theorem isSpecial : (modB j).IsSpecial j :=
  ⟨isCompl_lie j, Module.Invertible.congr (lieZeroEquiv j).symm,
    Module.Invertible.congr (lieOneEquiv j).symm⟩

theorem modB_act_p : (modB j).act (p : 𝕆) = fun i => (X i : MvPowerSeries (Fin 2) B) ^ 𝔮 := by
  show ((standard (p := p)).act (p : 𝕆)).map j = _
  rw [standard_act_p]
  funext i
  show MvPowerSeries.map j (C (p : 𝕆) * X i + X i ^ 𝔮) = X i ^ 𝔮
  rw [map_add, map_mul, map_C, map_natCast, CharP.cast_eq_zero, map_zero, zero_mul, zero_add,
    map_pow, map_X]

theorem hasKernelOfDegree_X_pow :
    FormalODModule.HasKernelOfDegree (fun i => (X i : MvPowerSeries (Fin 2) B) ^ 𝔮) (p ^ 4) := by
  haveI : Nontrivial B := CharP.nontrivial_of_char_ne_one (Fact.out : p.Prime).ne_one
  obtain ⟨hfree, hfin, -⟩ :=
    CerednikDrinfeld.BoxBasisLemma.free_and_finite_and_finrank_quotient_span_range_X_pow B 2 (fun _ => 𝔮)
  refine ⟨hfin, Module.Projective.of_free, fun κ _ f => ?_⟩
  have hφ : (fun i : Fin 2 => MvPowerSeries.map f ((X i : MvPowerSeries (Fin 2) B) ^ 𝔮))
      = fun i => (X i : MvPowerSeries (Fin 2) κ) ^ 𝔮 := by
    funext i
    rw [map_pow, map_X]
  show Module.finrank κ (MvPowerSeries (Fin 2) κ ⧸ Ideal.span (Set.range
    fun i : Fin 2 => MvPowerSeries.map f ((X i : MvPowerSeries (Fin 2) B) ^ 𝔮))) = p ^ 4
  rw [hφ, (CerednikDrinfeld.BoxBasisLemma.free_and_finite_and_finrank_quotient_span_range_X_pow κ 2 fun _ => 𝔮).2.2,
    Finset.prod_const, Finset.card_univ, Fintype.card_fin, card_GF, ← pow_mul]

theorem hasHeight : (modB j).HasHeight 4 := by
  show FormalODModule.HasKernelOfDegree ((modB j).act (p : 𝕆)) (p ^ 4)
  rw [modB_act_p]
  exact hasKernelOfDegree_X_pow

end OverB

def _root_.CerednikDrinfeld.SpecialFormalODModule.standard {B : Type u} [CommRing B] [CharP B p]
    (j : Zp2 p →+* B) : SpecialFormalODModule p j where
  toFormalODModule := modB j
  isSpecial := isSpecial j
  hasHeight := hasHeight j

theorem _root_.CerednikDrinfeld.SpecialFormalODModule.standard_toFormalODModule {B : Type u}
    [CommRing B] [CharP B p] (j : Zp2 p →+* B) :
    (SpecialFormalODModule.standard j).toFormalODModule = modB j := rfl

section HomAlgebra

variable {R : Type*} [CommRing R] {g h k m : ℕ}

theorem _root_.MvFormalGroup.Hom.comp_assoc {F : MvFormalGroup g R} {G : MvFormalGroup h R}
    {H : MvFormalGroup k R} {K : MvFormalGroup m R} (χ : MvFormalGroup.Hom H K)
    (ψ : MvFormalGroup.Hom G H) (φ : MvFormalGroup.Hom F G) :
    (χ.comp ψ).comp φ = χ.comp (ψ.comp φ) := by
  apply MvFormalGroup.Hom.ext
  funext i
  exact subst_comp_subst_apply ψ.hasSubst_toPowerSeries φ.hasSubst_toPowerSeries _

theorem _root_.MvFormalGroup.Hom.comp_id' {F : MvFormalGroup g R} {G : MvFormalGroup h R}
    (φ : MvFormalGroup.Hom F G) : φ.comp (MvFormalGroup.Hom.id F) = φ := by
  apply MvFormalGroup.Hom.ext
  funext i
  exact congrFun MvPowerSeries.subst_self _

theorem _root_.MvFormalGroup.Hom.comp_one' {F : MvFormalGroup g R} {G : MvFormalGroup h R}
    (φ : MvFormalGroup.Hom F G) : φ.comp (1 : MvFormalGroup.End F) = φ :=
  MvFormalGroup.Hom.comp_id' φ

theorem _root_.MvFormalGroup.Hom.id_comp' {F : MvFormalGroup g R} {G : MvFormalGroup h R}
    (φ : MvFormalGroup.Hom F G) : (MvFormalGroup.Hom.id G).comp φ = φ := by
  apply MvFormalGroup.Hom.ext
  funext i
  exact subst_X φ.hasSubst_toPowerSeries i

end HomAlgebra

section Biproduct

variable {B : Type u} [CommRing B] [CharP B p] (j : Zp2 p →+* B)

theorem modB_F_toPowerSeries (l : Fin 2) :
    (modB j).F.toPowerSeries l =
      subst (fun s => (X (emb l s) : MvPowerSeries (Fin 2 ⊕ Fin 2) B))
        (MvPowerSeries.map j (sigmaSeries p)) := by
  show MvPowerSeries.map j (lawSeries p l) = _
  rw [lawSeries_eq, map_subst (hasSubst_of_constantCoeff_zero fun _ => constantCoeff_X _)]
  congr 1
  funext s
  exact MvPowerSeries.map_X j _

theorem modB_act (a : 𝕆) (i : Fin 2) :
    (modB j).act a i =
      subst (fun _ : Fin 1 => (X i : MvPowerSeries (Fin 2) B)) (MvPowerSeries.map j (act₁ p (chi i a))) := by
  show MvPowerSeries.map j (actSeries p a i) = _
  rw [actSeries_eq, map_subst (hasSubst_of_constantCoeff_zero fun _ => constantCoeff_X _)]
  congr 1
  funext s
  exact MvPowerSeries.map_X j _

theorem modB_varpi_zero :
    (modB j).varpi 0 =
      subst (fun _ : Fin 1 => (X 1 : MvPowerSeries (Fin 2) B)) (MvPowerSeries.map j (act₁ p (p : 𝕆))) := by
  show MvPowerSeries.map j (varpiSeries p 0) = _
  rw [varpiSeries_zero, map_subst (hasSubst_of_constantCoeff_zero fun _ => constantCoeff_X _)]
  congr 1
  funext s
  exact MvPowerSeries.map_X j _

theorem modB_varpi_one : (modB j).varpi 1 = X 0 := by
  show MvPowerSeries.map j (varpiSeries p 1) = _
  rw [varpiSeries_one, MvPowerSeries.map_X]

theorem subst_elim_modB_F {τ : Type*} {a b : Fin 2 → MvPowerSeries τ B}
    (ha : ∀ i, constantCoeff (a i) = 0) (hb : ∀ i, constantCoeff (b i) = 0) (l : Fin 2) :
    subst (Sum.elim a b) ((modB j).F.toPowerSeries l) =
      subst (Sum.elim (fun _ : Fin 1 => a l) fun _ : Fin 1 => b l) (MvPowerSeries.map j (sigmaSeries p)) := by
  have hab : HasSubst (Sum.elim a b) := MvFormalGroup.hasSubst_elim ha hb
  rw [modB_F_toPowerSeries, subst_comp_subst_apply
    (hasSubst_of_constantCoeff_zero fun _ => constantCoeff_X _) hab]
  congr 1
  funext s
  rcases s with m | m
  · rw [subst_X hab]; rfl
  · rw [subst_X hab]; rfl

theorem constantCoeff_sigmaBarSeries :
    constantCoeff (MvPowerSeries.map j (sigmaSeries p)) = 0 := by
  rw [constantCoeff_map, constantCoeff_sigmaSeries, map_zero]

theorem subst_elim_sigmaBar_zero_right {τ : Type*} {x : MvPowerSeries τ B} (hx : constantCoeff x = 0) :
    subst (Sum.elim (fun _ : Fin 1 => x) fun _ : Fin 1 => (0 : MvPowerSeries τ B))
      (MvPowerSeries.map j (sigmaSeries p)) = x :=
  MvFormalGroup.subst_elim_zero_right (sigmaBar j) (a := fun _ : Fin 1 => x) (fun _ => hx) 0

theorem subst_elim_sigmaBar_zero_left {τ : Type*} {x : MvPowerSeries τ B} (hx : constantCoeff x = 0) :
    subst (Sum.elim (fun _ : Fin 1 => (0 : MvPowerSeries τ B)) fun _ : Fin 1 => x)
      (MvPowerSeries.map j (sigmaSeries p)) = x :=
  MvFormalGroup.subst_elim_zero_left (sigmaBar j) (a := fun _ : Fin 1 => x) (fun _ => hx) 0

def single₂ {τ : Type*} (i : Fin 2) (x : MvPowerSeries τ B) : Fin 2 → MvPowerSeries τ B :=
  fun l => if l = i then x else 0

theorem single₂_apply {τ : Type*} (i : Fin 2) (x : MvPowerSeries τ B) (l : Fin 2) :
    single₂ i x l = if l = i then x else 0 := rfl

theorem constantCoeff_single₂ {τ : Type*} (i : Fin 2) {x : MvPowerSeries τ B} (hx : constantCoeff x = 0)
    (l : Fin 2) : constantCoeff (single₂ i x l) = 0 := by
  rw [single₂_apply]; split_ifs; exacts [hx, map_zero _]

theorem subst_single₂ {τ τ' : Type*} (i : Fin 2) {x : MvPowerSeries τ B} {c : τ → MvPowerSeries τ' B}
    (hc : HasSubst c) : (fun l => subst c (single₂ i x l)) = single₂ i (subst c x) := by
  funext l
  rw [single₂_apply, single₂_apply]
  split_ifs
  · rfl
  · rw [← coe_substAlgHom hc, map_zero]

def incl (i : Fin 2) : MvFormalGroup.Hom (sigmaBar j) (modB j).F where
  toPowerSeries := single₂ i (X 0 : MvPowerSeries (Fin 1) B)
  constantCoeff_eq_zero := constantCoeff_single₂ i (constantCoeff_X 0)
  subst_eq l := by
    have hXl : HasSubst (fun l' : Fin 1 => (X (Sum.inl l') : MvPowerSeries (Fin 1 ⊕ Fin 1) B)) :=
      hasSubst_of_constantCoeff_zero fun _ => constantCoeff_X _
    have hXr : HasSubst (fun l' : Fin 1 => (X (Sum.inr l') : MvPowerSeries (Fin 1 ⊕ Fin 1) B)) :=
      hasSubst_of_constantCoeff_zero fun _ => constantCoeff_X _
    rw [subst_single₂ i hXl, subst_single₂ i hXr, subst_X hXl, subst_X hXr,
      subst_elim_modB_F j (constantCoeff_single₂ i (constantCoeff_X _))
        (constantCoeff_single₂ i (constantCoeff_X _)), single₂_apply, single₂_apply, single₂_apply]
    split_ifs with h
    · rw [subst_X (sigmaBar j).hasSubst_toPowerSeries, sigmaBar_toPowerSeries]
      have hid : (Sum.elim (fun _ : Fin 1 => (X (Sum.inl 0) : MvPowerSeries (Fin 1 ⊕ Fin 1) B))
          fun _ : Fin 1 => (X (Sum.inr 0) : MvPowerSeries (Fin 1 ⊕ Fin 1) B))
          = fun s => X s := by
        funext s; rcases s with m | m <;> rw [Fin.fin_one_eq_zero m] <;> rfl
      rw [hid]
      exact (congrFun MvPowerSeries.subst_self _).symm
    · rw [← coe_substAlgHom (sigmaBar j).hasSubst_toPowerSeries, map_zero]
      have h00 : (Sum.elim (fun _ : Fin 1 => (0 : MvPowerSeries (Fin 1 ⊕ Fin 1) B))
          fun _ : Fin 1 => (0 : MvPowerSeries (Fin 1 ⊕ Fin 1) B)) = fun _ => 0 := by
        funext s; rcases s with m | m <;> rfl
      rw [h00]
      exact (MvFormalGroup.subst_zero_of_constantCoeff_eq_zero (constantCoeff_sigmaBarSeries j)).symm

theorem incl_toPowerSeries (i : Fin 2) :
    (incl j i).toPowerSeries = single₂ i (X 0 : MvPowerSeries (Fin 1) B) := rfl

def proj (i : Fin 2) : MvFormalGroup.Hom (modB j).F (sigmaBar j) where
  toPowerSeries := fun _ => (X i : MvPowerSeries (Fin 2) B)
  constantCoeff_eq_zero := fun _ => constantCoeff_X i
  subst_eq l := by
    have hXl : HasSubst (fun l' : Fin 2 => (X (Sum.inl l') : MvPowerSeries (Fin 2 ⊕ Fin 2) B)) :=
      hasSubst_of_constantCoeff_zero fun _ => constantCoeff_X _
    have hXr : HasSubst (fun l' : Fin 2 => (X (Sum.inr l') : MvPowerSeries (Fin 2 ⊕ Fin 2) B)) :=
      hasSubst_of_constantCoeff_zero fun _ => constantCoeff_X _
    rw [subst_X (modB j).F.hasSubst_toPowerSeries, Fin.fin_one_eq_zero l, sigmaBar_toPowerSeries,
      modB_F_toPowerSeries]
    congr 1
    funext s
    rcases s with m | m
    · rw [Sum.elim_inl, subst_X hXl]; rfl
    · rw [Sum.elim_inr, subst_X hXr]; rfl

theorem proj_toPowerSeries (i : Fin 2) (l : Fin 1) :
    (proj j i).toPowerSeries l = (X i : MvPowerSeries (Fin 2) B) := rfl

theorem proj_comp_incl (i i' : Fin 2) :
    (proj j i).comp (incl j i') =
      if i = i' then (1 : MvFormalGroup.End (sigmaBar j)) else (0 : MvFormalGroup.End (sigmaBar j)) := by
  apply MvFormalGroup.Hom.ext
  funext l
  show subst (incl j i').toPowerSeries (X i) = _
  rw [subst_X (incl j i').hasSubst_toPowerSeries, incl_toPowerSeries, single₂_apply]
  split_ifs
  · rw [Fin.fin_one_eq_zero l]; rfl
  · rfl

def cell (i i' : Fin 2) (e : MvFormalGroup.End (sigmaBar j)) : MvFormalGroup.End (modB j).F :=
  ((incl j i).comp e).comp (proj j i')

def entry (i i' : Fin 2) (E : MvFormalGroup.End (modB j).F) : MvFormalGroup.End (sigmaBar j) :=
  ((proj j i).comp E).comp (incl j i')

theorem cell_def (i i' : Fin 2) (e : MvFormalGroup.End (sigmaBar j)) :
    cell j i i' e = ((incl j i).comp e).comp (proj j i') := rfl

theorem entry_def (i i' : Fin 2) (E : MvFormalGroup.End (modB j).F) :
    entry j i i' E = ((proj j i).comp E).comp (incl j i') := rfl

theorem toPowerSeries_cell (i i' : Fin 2) (e : MvFormalGroup.End (sigmaBar j)) :
    (cell j i i' e).toPowerSeries =
      single₂ i (subst (fun _ : Fin 1 => (X i' : MvPowerSeries (Fin 2) B)) (e.toPowerSeries 0)) := by
  funext l
  show subst (proj j i').toPowerSeries (subst e.toPowerSeries ((incl j i).toPowerSeries l)) = _
  rw [incl_toPowerSeries, single₂_apply, single₂_apply]
  split_ifs
  · rw [subst_X e.hasSubst_toPowerSeries]
    rfl
  · rw [← coe_substAlgHom e.hasSubst_toPowerSeries, map_zero,
      ← coe_substAlgHom (proj j i').hasSubst_toPowerSeries, map_zero]

theorem mul_eq_comp {g : ℕ} {F : MvFormalGroup g B} (φ ψ : MvFormalGroup.End F) : φ * ψ = φ.comp ψ := rfl

theorem hasSubst_fin1' {τ : Type*} {x : MvPowerSeries τ B} (hx : constantCoeff x = 0) :
    HasSubst (fun _ : Fin 1 => x) :=
  hasSubst_of_constantCoeff_zero fun _ => hx

theorem hasSubst_single₂ {τ : Type*} (i : Fin 2) {x : MvPowerSeries τ B} (hx : constantCoeff x = 0) :
    HasSubst (single₂ i x) :=
  hasSubst_of_constantCoeff_zero (constantCoeff_single₂ i hx)

theorem constantCoeff_subst_X_toPowerSeries (i : Fin 2) (e : MvFormalGroup.End (sigmaBar j)) :
    constantCoeff (subst (fun _ : Fin 1 => (X i : MvPowerSeries (Fin 2) B)) (e.toPowerSeries 0)) = 0 :=
  constantCoeff_subst_eq_zero (hasSubst_of_constantCoeff_zero fun _ => constantCoeff_X _)
    (fun _ => constantCoeff_X _) (e.constantCoeff_eq_zero 0)

theorem toPowerSeries_fin1 (e : MvFormalGroup.End (sigmaBar j)) :
    e.toPowerSeries = fun _ => e.toPowerSeries 0 := by
  funext l; rw [Fin.fin_one_eq_zero l]

theorem subst_fin1_X (f : MvPowerSeries (Fin 1) B) :
    subst (fun _ : Fin 1 => (X 0 : MvPowerSeries (Fin 1) B)) f = f := by
  have h := congrFun (MvPowerSeries.subst_self (σ := Fin 1) (R := B)) f
  have hX : (X : Fin 1 → MvPowerSeries (Fin 1) B) = fun _ => X 0 := by
    funext l; rw [Fin.fin_one_eq_zero l]
  rw [hX] at h
  exact h

theorem subst_single₂_subst_X {τ : Type*} (k i' : Fin 2) {y : MvPowerSeries τ B} (hy : constantCoeff y = 0)
    (e : MvFormalGroup.End (sigmaBar j)) :
    subst (single₂ k y) (subst (fun _ : Fin 1 => (X i' : MvPowerSeries (Fin 2) B)) (e.toPowerSeries 0)) =
      if i' = k then subst (fun _ : Fin 1 => y) (e.toPowerSeries 0) else 0 := by
  rw [subst_comp_subst_apply (hasSubst_fin1' (constantCoeff_X _)) (hasSubst_single₂ k hy)]
  simp only [subst_X (hasSubst_single₂ k hy), single₂_apply]
  split_ifs
  · rfl
  · exact MvFormalGroup.subst_zero_of_constantCoeff_eq_zero (e.constantCoeff_eq_zero 0)

theorem cell_mul_cell (i i' k k' : Fin 2) (e e' : MvFormalGroup.End (sigmaBar j)) :
    cell j i i' e * cell j k k' e' = if i' = k then cell j i k' (e * e') else 0 := by
  apply MvFormalGroup.Hom.ext
  rw [MvFormalGroup.End.toPowerSeries_mul, toPowerSeries_cell, toPowerSeries_cell,
    subst_single₂ i (hasSubst_single₂ k (constantCoeff_subst_X_toPowerSeries j k' e')),
    subst_single₂_subst_X j k i' (constantCoeff_subst_X_toPowerSeries j k' e')]
  split_ifs with h
  · rw [toPowerSeries_cell, MvFormalGroup.End.toPowerSeries_mul, toPowerSeries_fin1 j e',
      subst_comp_subst_apply (hasSubst_fin1' (e'.constantCoeff_eq_zero 0)) (hasSubst_fin1' (constantCoeff_X _))]
  · funext l
    rw [single₂_apply, MvFormalGroup.End.toPowerSeries_zero]
    split_ifs <;> rfl

theorem cell_add (i i' : Fin 2) (e e' : MvFormalGroup.End (sigmaBar j)) :
    cell j i i' (e + e') = cell j i i' e + cell j i i' e' := by
  apply MvFormalGroup.Hom.ext
  funext l
  rw [toPowerSeries_cell, MvFormalGroup.End.toPowerSeries_add, MvFormalGroup.End.toPowerSeries_add,
    toPowerSeries_cell, toPowerSeries_cell]
  dsimp only
  rw [subst_elim_modB_F j (constantCoeff_single₂ i (constantCoeff_subst_X_toPowerSeries j i' e))
      (constantCoeff_single₂ i (constantCoeff_subst_X_toPowerSeries j i' e')), single₂_apply, single₂_apply,
    single₂_apply, sigmaBar_toPowerSeries,
    subst_comp_subst_apply (MvFormalGroup.hasSubst_elim e.constantCoeff_eq_zero e'.constantCoeff_eq_zero)
      (hasSubst_fin1' (constantCoeff_X _))]
  split_ifs
  · congr 1
    funext s
    rcases s with m | m <;> rw [Fin.fin_one_eq_zero m] <;> rfl
  · have h00 : (Sum.elim (fun _ : Fin 1 => (0 : MvPowerSeries (Fin 2) B))
        fun _ : Fin 1 => (0 : MvPowerSeries (Fin 2) B)) = fun _ => 0 := by
      funext s; rcases s with m | m <;> rfl
    rw [h00, MvFormalGroup.subst_zero_of_constantCoeff_eq_zero (constantCoeff_sigmaBarSeries j)]

theorem cell_zero (i i' : Fin 2) : cell j i i' 0 = 0 := by
  apply MvFormalGroup.Hom.ext
  funext l
  rw [toPowerSeries_cell, MvFormalGroup.End.toPowerSeries_zero, MvFormalGroup.End.toPowerSeries_zero,
    single₂_apply]
  dsimp only
  rw [← coe_substAlgHom (hasSubst_fin1' (constantCoeff_X _)), map_zero]
  split_ifs <;> rfl

theorem cell_neg (i i' : Fin 2) (e : MvFormalGroup.End (sigmaBar j)) : cell j i i' (-e) = -cell j i i' e := by
  rw [eq_neg_iff_add_eq_zero, ← cell_add, neg_add_cancel, cell_zero]

theorem cell_sub (i i' : Fin 2) (e e' : MvFormalGroup.End (sigmaBar j)) :
    cell j i i' (e - e') = cell j i i' e - cell j i i' e' := by
  rw [sub_eq_add_neg, cell_add, cell_neg, ← sub_eq_add_neg]

theorem entry_cell (i i' k k' : Fin 2) (e : MvFormalGroup.End (sigmaBar j)) :
    entry j i i' (cell j k k' e) = if i = k then (if k' = i' then e else 0) else 0 := by
  apply MvFormalGroup.Hom.ext
  funext l
  show subst (incl j i').toPowerSeries (subst (cell j k k' e).toPowerSeries (X i)) = _
  rw [toPowerSeries_cell, subst_X (hasSubst_single₂ k (constantCoeff_subst_X_toPowerSeries j k' e)),
    single₂_apply, incl_toPowerSeries]
  split_ifs with h1 h2
  · rw [subst_single₂_subst_X j i' k' (constantCoeff_X _), if_pos h2, Fin.fin_one_eq_zero l, subst_fin1_X]
  · rw [subst_single₂_subst_X j i' k' (constantCoeff_X _), if_neg h2]; rfl
  · rw [← coe_substAlgHom (hasSubst_single₂ i' (constantCoeff_X _)), map_zero]; rfl

theorem entry_add (i i' : Fin 2) (E E' : MvFormalGroup.End (modB j).F) :
    entry j i i' (E + E') = entry j i i' E + entry j i i' E' := by
  apply MvFormalGroup.Hom.ext
  funext l
  rw [MvFormalGroup.End.toPowerSeries_add]
  show subst (incl j i').toPowerSeries (subst (E + E').toPowerSeries (X i)) =
    subst (Sum.elim (fun _ => subst (incl j i').toPowerSeries (subst E.toPowerSeries (X i)))
      fun _ => subst (incl j i').toPowerSeries (subst E'.toPowerSeries (X i))) ((sigmaBar j).toPowerSeries l)
  rw [subst_X E.hasSubst_toPowerSeries, subst_X E'.hasSubst_toPowerSeries,
    subst_X (E + E').hasSubst_toPowerSeries, MvFormalGroup.End.toPowerSeries_add]
  dsimp only
  rw [subst_comp_subst_apply (MvFormalGroup.hasSubst_elim E.constantCoeff_eq_zero E'.constantCoeff_eq_zero)
      (incl j i').hasSubst_toPowerSeries, Fin.fin_one_eq_zero l, sigmaBar_toPowerSeries]
  have hfam : (fun s => subst (incl j i').toPowerSeries (Sum.elim E.toPowerSeries E'.toPowerSeries s)) =
      Sum.elim (fun m => subst (incl j i').toPowerSeries (E.toPowerSeries m))
        fun m => subst (incl j i').toPowerSeries (E'.toPowerSeries m) := by
    funext s; rcases s with m | m <;> rfl
  rw [hfam, subst_elim_modB_F j]
  · intro m
    exact constantCoeff_subst_eq_zero (incl j i').hasSubst_toPowerSeries (incl j i').constantCoeff_eq_zero
      (E.constantCoeff_eq_zero m)
  · intro m
    exact constantCoeff_subst_eq_zero (incl j i').hasSubst_toPowerSeries (incl j i').constantCoeff_eq_zero
      (E'.constantCoeff_eq_zero m)

theorem one_eq_cell_add_cell : (1 : MvFormalGroup.End (modB j).F) = cell j 0 0 1 + cell j 1 1 1 := by
  apply MvFormalGroup.Hom.ext
  funext l
  rw [MvFormalGroup.End.toPowerSeries_one, MvFormalGroup.End.toPowerSeries_add, toPowerSeries_cell,
    toPowerSeries_cell, MvFormalGroup.End.toPowerSeries_one, subst_X (hasSubst_fin1' (B := B) (constantCoeff_X _)),
    subst_X (hasSubst_fin1' (B := B) (constantCoeff_X _))]
  dsimp only
  rw [subst_elim_modB_F j (constantCoeff_single₂ 0 (constantCoeff_X _)) (constantCoeff_single₂ 1 (constantCoeff_X _)),
    single₂_apply, single₂_apply]
  revert l
  refine Fin.forall_fin_two.mpr ⟨?_, ?_⟩
  · rw [if_pos rfl, if_neg zero_ne_one]
    exact (subst_elim_sigmaBar_zero_right j (constantCoeff_X _)).symm
  · rw [if_neg one_ne_zero, if_pos rfl]
    exact (subst_elim_sigmaBar_zero_left j (constantCoeff_X _)).symm

theorem eq_sum_cell_entry (E : MvFormalGroup.End (modB j).F) :
    E = cell j 0 0 (entry j 0 0 E) + cell j 0 1 (entry j 0 1 E) +
      (cell j 1 0 (entry j 1 0 E) + cell j 1 1 (entry j 1 1 E)) := by
  have key : ∀ i i' : Fin 2, cell j i i 1 * E * cell j i' i' 1 = cell j i i' (entry j i i' E) := by
    intro i i'
    rw [mul_eq_comp, mul_eq_comp, cell_def, cell_def, cell_def, entry_def, MvFormalGroup.Hom.comp_one',
      MvFormalGroup.Hom.comp_one', MvFormalGroup.Hom.comp_assoc, MvFormalGroup.Hom.comp_assoc,
      MvFormalGroup.Hom.comp_assoc, MvFormalGroup.Hom.comp_assoc, MvFormalGroup.Hom.comp_assoc]
  calc E = 1 * E * 1 := by rw [one_mul, mul_one]
    _ = (cell j 0 0 1 + cell j 1 1 1) * E * (cell j 0 0 1 + cell j 1 1 1) := by rw [← one_eq_cell_add_cell]
    _ = _ := by rw [add_mul, add_mul, mul_add, mul_add, key, key, key, key]

theorem actEnd_eq (a : 𝕆) :
    (modB j).actEnd a = cell j 0 0 (rho j a) + cell j 1 1 (rho j (WittVector.frobenius a)) := by
  apply MvFormalGroup.Hom.ext
  funext l
  rw [MvFormalGroup.End.toPowerSeries_add, FormalODModule.actEnd_toPowerSeries, toPowerSeries_cell,
    toPowerSeries_cell]
  dsimp only
  rw [subst_elim_modB_F j (constantCoeff_single₂ 0 (constantCoeff_subst_X_toPowerSeries j _ _))
      (constantCoeff_single₂ 1 (constantCoeff_subst_X_toPowerSeries j _ _)),
    single₂_apply, single₂_apply, modB_act]
  revert l
  refine Fin.forall_fin_two.mpr ⟨?_, ?_⟩
  · rw [if_pos rfl, if_neg zero_ne_one, chi_zero, RingHom.id_apply]
    exact (subst_elim_sigmaBar_zero_right j (constantCoeff_subst_X_toPowerSeries j 0 (rho j a))).symm
  · rw [if_neg one_ne_zero, if_pos rfl, chi_one]
    exact (subst_elim_sigmaBar_zero_left j
      (constantCoeff_subst_X_toPowerSeries j 1 (rho j (WittVector.frobenius a)))).symm

theorem varpiEnd_eq : (modB j).varpiEnd = cell j 0 1 (rho j (p : 𝕆)) + cell j 1 0 1 := by
  apply MvFormalGroup.Hom.ext
  funext l
  rw [MvFormalGroup.End.toPowerSeries_add, FormalODModule.varpiEnd_toPowerSeries, toPowerSeries_cell,
    toPowerSeries_cell]
  dsimp only
  rw [subst_elim_modB_F j (constantCoeff_single₂ 0 (constantCoeff_subst_X_toPowerSeries j _ _))
      (constantCoeff_single₂ 1 (constantCoeff_subst_X_toPowerSeries j _ _)),
    single₂_apply, single₂_apply]
  revert l
  refine Fin.forall_fin_two.mpr ⟨?_, ?_⟩
  · rw [if_pos rfl, if_neg zero_ne_one, modB_varpi_zero]
    exact (subst_elim_sigmaBar_zero_right j (constantCoeff_subst_X_toPowerSeries j 1 (rho j (p : 𝕆)))).symm
  · rw [if_neg one_ne_zero, if_pos rfl, modB_varpi_one, MvFormalGroup.End.toPowerSeries_one,
      subst_X (hasSubst_of_constantCoeff_zero fun _ => constantCoeff_X _)]
    exact (subst_elim_sigmaBar_zero_left j (constantCoeff_X _)).symm

end Biproduct

end CerednikDrinfeld.Standard

end