CartierFixedness.lean

def kw_cfx_G : Polynomial (MvPolynomial (Fin ℓ) ℤ)

def kw_cfx_Gpow : Polynomial (MvPolynomial (Fin ℓ) ℤ)

theorem kw_cfx_z1_map_eq :
    (kw_cfx_G ℓ ^ ℓ - kw_cfx_Gpow ℓ).map
      (MvPolynomial.map (Int.castRingHom (ZMod ℓ))) = 0

theorem kw_cfx_z1 (k : ℕ) :
    MvPolynomial.C ((ℓ : ℕ) : ℤ) ∣ (kw_cfx_G ℓ ^ ℓ - kw_cfx_Gpow ℓ).coeff k

theorem kw_cfx_z_derivG :
    derivative (kw_cfx_G ℓ)
      = ∑ i : Fin ℓ, C (MvPolynomial.X i * ((i : ℕ) : MvPolynomial (Fin ℓ) ℤ))
          * X ^ ((i : ℕ) - 1)

theorem kw_cfx_z2 (m : ℕ) (hm : m + 1 < ℓ) :
    ∃ e : MvPolynomial (Fin ℓ) ℤ,
      (kw_cfx_G ℓ ^ (ℓ - 1) * derivative (kw_cfx_G ℓ)).coeff (ℓ * m + (ℓ - 1))
        = ((m + 1 : ℕ) : MvPolynomial (Fin ℓ) ℤ)
            * MvPolynomial.X (⟨m + 1, hm⟩ : Fin ℓ) ^ ℓ
          + ((ℓ : ℕ) : MvPolynomial (Fin ℓ) ℤ) * e

theorem kw_cfx_z3_natDegree_le :
    (kw_cfx_G ℓ ^ (ℓ - 1) * derivative (kw_cfx_G ℓ)).natDegree ≤ ℓ * (ℓ - 1)

theorem kw_cfx_z3_coeff_zero (m : ℕ) (hm : ℓ ≤ m + 1) :
    (kw_cfx_G ℓ ^ (ℓ - 1) * derivative (kw_cfx_G ℓ)).coeff (ℓ * m + (ℓ - 1)) = 0

def kw_cfx_tau (t : F) : kw_pke_pthPowers F ℓ

theorem kw_cfx_tau_coe (t : F) : ((kw_cfx_tau (ℓ := ℓ) t : kw_pke_pthPowers F ℓ)
    : F) = t ^ ℓ

def kw_cfx_vext (v : Fin ℓ → kw_pke_pthPowers F ℓ) (n : ℕ) :
    kw_pke_pthPowers F ℓ

theorem kw_cfx_vext_of_lt (v : Fin ℓ → kw_pke_pthPowers F ℓ) {n : ℕ} (h : n < ℓ) :
    kw_cfx_vext v n = v ⟨n, h⟩

def kw_cfx_phiP (v : Fin ℓ → kw_pke_pthPowers F ℓ) :
    MvPolynomial (Fin ℓ) ℤ →+* kw_pke_pthPowers F ℓ

theorem kw_cfx_phiP_X (v : Fin ℓ → kw_pke_pthPowers F ℓ) (j : Fin ℓ) :
    kw_cfx_phiP v (MvPolynomial.X j) = v j

def kw_cfx_phi (v : Fin ℓ → kw_pke_pthPowers F ℓ) :
    MvPolynomial (Fin ℓ) ℤ →+* F

theorem kw_cfx_phi_apply (v : Fin ℓ → kw_pke_pthPowers F ℓ)
    (x : MvPolynomial (Fin ℓ) ℤ) :
    kw_cfx_phi v x = ((kw_cfx_phiP v x : kw_pke_pthPowers F ℓ) : F)

def kw_cfx_Phi (t : F) (v : Fin ℓ → kw_pke_pthPowers F ℓ) :
    Polynomial (MvPolynomial (Fin ℓ) ℤ) →+* F

theorem kw_cfx_Phi_apply (t : F) (v : Fin ℓ → kw_pke_pthPowers F ℓ)
    (q : Polynomial (MvPolynomial (Fin ℓ) ℤ)) :
    kw_cfx_Phi t v q = Polynomial.eval₂ (kw_cfx_phi v) t q

theorem kw_cfx_t4_natCast_pow (n : ℕ) : ((n : F)) ^ ℓ = (n : F)

theorem kw_cfx_t1_Phi_G (t : F)
    (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
    (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
    (f : F) :
    kw_cfx_Phi t (kw_cart_repr t hsep hdeg f) (kw_cfx_G ℓ) = f

def kw_cfx_fstarOf (t : F) (v : Fin ℓ → kw_pke_pthPowers F ℓ) : F

theorem kw_cfx_t2_Phi_dG (t : F) (v : Fin ℓ → kw_pke_pthPowers F ℓ) :
    kw_cfx_Phi t v (derivative (kw_cfx_G ℓ)) = kw_cfx_fstarOf t v

theorem kw_cfx_t3_repr_Phi (t : F)
    (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
    (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
    (v : Fin ℓ → kw_pke_pthPowers F ℓ)
    (q : Polynomial (MvPolynomial (Fin ℓ) ℤ)) (N : ℕ) (hN : q.natDegree < ℓ * N) :
    kw_cart_repr t hsep hdeg (kw_cfx_Phi t v q)
      = fun r : Fin ℓ => ∑ m ∈ Finset.range N,
          kw_cfx_phiP v (q.coeff (ℓ * m + (r : ℕ))) * kw_cfx_tau (ℓ := ℓ) t ^ m := by
  have hpos := hℓ.out.pos
  refine kw_cart_repr_unique t hsep hdeg ?_
  have h0 : kw_cfx_Phi t v q
      = ∑ k ∈ Finset.range (ℓ * N), kw_cfx_phi v (q.coeff k) * t ^ k := by
    rw [kw_cfx_Phi_apply]
    exact eval₂_eq_sum_range' (kw_cfx_phi v) hN t
  calc kw_cfx_Phi t v q
      = ∑ k ∈ Finset.range (ℓ * N), kw_cfx_phi v (q.coeff k) * t ^ k := h0
    _ = ∑ p ∈ Finset.range N ×ˢ Finset.range ℓ,
          kw_cfx_phi v (q.coeff (ℓ * p.1 + p.2)) * t ^ (ℓ * p.1 + p.2) := by
        refine Finset.sum_nbij' (fun k => (k / ℓ, k % ℓ)) (fun p => ℓ * p.1 + p.2)
          ?_ ?_ ?_ ?_ ?_
        · intro k hk
          rw [Finset.mem_range] at hk
          rw [Finset.mem_product, Finset.mem_range, Finset.mem_range]
          refine ⟨?_, Nat.mod_lt _ hpos⟩
          rw [Nat.div_lt_iff_lt_mul hpos, Nat.mul_comm N ℓ]
          exact hk
        · intro p hp
          rw [Finset.mem_product, Finset.mem_range, Finset.mem_range] at hp
          rw [Finset.mem_range]
          show ℓ * p.1 + p.2 < ℓ * N
          have h1 : p.1 + 1 ≤ N := hp.1
          have h2 : ℓ * (p.1 + 1) ≤ ℓ * N := Nat.mul_le_mul_left ℓ h1
          rw [Nat.mul_succ] at h2
          omega
        · intro k _
          exact Nat.div_add_mod k ℓ
        · intro p hp
          rw [Finset.mem_product, Finset.mem_range, Finset.mem_range] at hp
          have hd : (ℓ * p.1 + p.2) / ℓ = p.1 := by
            rw [Nat.mul_add_div hpos, Nat.div_eq_of_lt hp.2, Nat.add_zero]
          have hm : (ℓ * p.1 + p.2) % ℓ = p.2 := by
            rw [Nat.mul_add_mod, Nat.mod_eq_of_lt hp.2]
          exact Prod.ext hd hm
        · intro k _
          change kw_cfx_phi v (q.coeff k) * t ^ k
              = kw_cfx_phi v (q.coeff (ℓ * (k / ℓ) + k % ℓ))
                  * t ^ (ℓ * (k / ℓ) + k % ℓ)
          rw [Nat.div_add_mod k ℓ]
    _ = ∑ m ∈ Finset.range N, ∑ r ∈ Finset.range ℓ,
          kw_cfx_phi v (q.coeff (ℓ * m + r)) * t ^ (ℓ * m + r) :=
        Finset.sum_product _ _ _
    _ = ∑ r ∈ Finset.range ℓ, ∑ m ∈ Finset.range N,
          kw_cfx_phi v (q.coeff (ℓ * m + r)) * t ^ (ℓ * m + r) :=
        Finset.sum_comm
    _ = ∑ r ∈ Finset.range ℓ,
          (∑ m ∈ Finset.range N, kw_cfx_phi v (q.coeff (ℓ * m + r)) * (t ^ ℓ) ^ m)
            * t ^ r := by
        refine Finset.sum_congr rfl fun r _ => ?_
        rw [Finset.sum_mul]
        refine Finset.sum_congr rfl fun m _ => ?_
        rw [pow_add, pow_mul, mul_assoc]
    _ = ∑ i : Fin ℓ,
          (((fun r : Fin ℓ => ∑ m ∈ Finset.range N,
              kw_cfx_phiP v (q.coeff (ℓ * m + (r : ℕ)))
                * kw_cfx_tau (ℓ := ℓ) t ^ m) i : kw_pke_pthPowers F ℓ) : F)
            * t ^ (i : ℕ) := by
        rw [← Fin.sum_univ_eq_sum_range (fun r =>
          (∑ m ∈ Finset.range N, kw_cfx_phi v (q.coeff (ℓ * m + r)) * (t ^ ℓ) ^ m)
            * t ^ r) ℓ]
        refine Finset.sum_congr rfl fun i _ => ?_
        congr 1
        push_cast
        refine Finset.sum_congr rfl fun m _ => ?_
        rw [kw_cfx_phi_apply, kw_cfx_tau_coe]

theorem kw_cfx_D_eq (t : F)
    (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
    (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
    (f : F) :
    KaehlerDifferential.D K F f
      = kw_cfx_fstarOf t (kw_cart_repr t hsep hdeg f)
          • KaehlerDifferential.D K F t

theorem kw_cfx_fstar_pow_char (t : F) (v : Fin ℓ → kw_pke_pthPowers F ℓ) :
    kw_cfx_fstarOf t v ^ ℓ
      = ((∑ m ∈ Finset.range (ℓ - 1),
            ((m + 1 : ℕ) : kw_pke_pthPowers F ℓ) * kw_cfx_vext v (m + 1) ^ ℓ
              * kw_cfx_tau (ℓ := ℓ) t ^ m : kw_pke_pthPowers F ℓ) : F)

theorem kw_cfx_repr_top (t : F)
    (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
    (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
    (v : Fin ℓ → kw_pke_pthPowers F ℓ) :
    kw_cart_repr t hsep hdeg
        (kw_cfx_Phi t v (kw_cfx_G ℓ ^ (ℓ - 1) * derivative (kw_cfx_G ℓ)))
        ⟨ℓ - 1, by have := hℓ.out.pos; omega⟩
      = ∑ m ∈ Finset.range (ℓ - 1),
          ((m + 1 : ℕ) : kw_pke_pthPowers F ℓ) * kw_cfx_vext v (m + 1) ^ ℓ
            * kw_cfx_tau (ℓ := ℓ) t ^ m := by
  have hpos := hℓ.out.pos
  have h2 := hℓ.out.two_le
  have hℓ1 : ℓ - 1 + 1 = ℓ := by omega
  have hmulsq : ℓ * ℓ = ℓ * (ℓ - 1) + ℓ := by
    calc ℓ * ℓ = ℓ * ((ℓ - 1) + 1) := by rw [hℓ1]
      _ = ℓ * (ℓ - 1) + ℓ := by rw [Nat.mul_succ]
  have hdeg' : (kw_cfx_G ℓ ^ (ℓ - 1) * derivative (kw_cfx_G ℓ)).natDegree
      < ℓ * ℓ := by
    have h := kw_cfx_z3_natDegree_le ℓ
    omega
  have ht3 := kw_cfx_t3_repr_Phi t hsep hdeg v
    (kw_cfx_G ℓ ^ (ℓ - 1) * derivative (kw_cfx_G ℓ)) ℓ hdeg'
  rw [ht3]
  change ∑ m ∈ Finset.range ℓ,
      kw_cfx_phiP v ((kw_cfx_G ℓ ^ (ℓ - 1) * derivative (kw_cfx_G ℓ)).coeff
        (ℓ * m + (ℓ - 1))) * kw_cfx_tau (ℓ := ℓ) t ^ m = _
  have hrange : Finset.range ℓ = Finset.range ((ℓ - 1) + 1) := by rw [hℓ1]
  rw [hrange, Finset.sum_range_succ]
  have htop : (kw_cfx_G ℓ ^ (ℓ - 1) * derivative (kw_cfx_G ℓ)).coeff
      (ℓ * (ℓ - 1) + (ℓ - 1)) = 0 :=
    kw_cfx_z3_coeff_zero ℓ (ℓ - 1) (by omega)
  rw [htop, map_zero, zero_mul, add_zero]
  refine Finset.sum_congr rfl fun m hm => ?_
  have hmlt : m + 1 < ℓ := by
    rw [Finset.mem_range] at hm
    omega
  obtain ⟨e, he⟩ := kw_cfx_z2 ℓ m hmlt
  rw [he, map_add, map_mul, map_mul, map_natCast, map_natCast, map_pow, kw_cfx_phiP_X]
  have hl0 : ((ℓ : ℕ) : kw_pke_pthPowers F ℓ) = 0 := by
    have h1 : (((ℓ : ℕ) : kw_pke_pthPowers F ℓ) : F) = ((ℓ : ℕ) : F) := by
      norm_cast
    have hF : ((ℓ : ℕ) : F) = 0 := CharP.cast_eq_zero F ℓ
    exact ZeroMemClass.coe_eq_zero.mp (h1.trans hF)
  rw [hl0, zero_mul, add_zero, kw_cfx_vext_of_lt v hmlt]

theorem kw_cfx_C_dlog_fixed (t : F)
    (hdt : KaehlerDifferential.D K F t ≠ 0)
    (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
    (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
    (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
    {f : F} (hf : f ≠ 0) :
    kw_cart_C (K := K) t hdt hspan hsep hdeg (kw_hwcd_dlog K f)
      = kw_hwcd_dlog K f