module

public import Papers.OaiReconstructionMilnorTheory.Basic
public import Mathlib.Algebra.CharP.Algebra
public import Mathlib.FieldTheory.KummerPolynomial
public import Mathlib.RingTheory.Derivation.Basic
public import Mathlib.LinearAlgebra.LinearIndependent.Defs
public import Mathlib.Data.Fin.Tuple.Basic
public import Mathlib.Algebra.Group.Submonoid.Finsupp
public import Mathlib.LinearAlgebra.Dimension.OrzechProperty

/-! # Finite p-bases, monomials, and coordinate Euler derivations -/

@[expose] public section

namespace Papers.OaiReconstructionMilnorTheory

variable (p : ℕ) {F : Type*} [Field F]

/-- For [an exponent bound p](hyp:p), [a finite list b of field elements](hyp:b),
and [a list i of exponents from zero through p minus one](hyp:i),
[the associated monomial](goal) is the product of each entry of b raised to its exponent in i. -/
def pMonomial {e : ℕ} (b : Fin e → F) (i : Fin e → Fin p) : F :=
  ∏ j, b j ^ (i j : ℕ)

-- @node: pBasis_isIntegral
/-- If [p is prime](hyp:hp), then [every element s is integral over every
intermediate field M containing the subfield generated by p-th powers](goal). -/
lemma pBasis_isIntegral (hp : PrimeChar p)
    (M : IntermediateField ↥(pBasisPowSubfield p F) F) (s : F) : IsIntegral M s := by
  have hsp : s ^ p ∈ M := M.algebraMap_mem
    (⟨s ^ p, Subfield.subset_closure ⟨s, rfl⟩⟩ : pBasisPowSubfield p F)
  refine ⟨Polynomial.X ^ p - Polynomial.C (⟨s ^ p, hsp⟩ : M),
    Polynomial.monic_X_pow_sub_C _ hp.ne_zero, ?_⟩
  simp

-- @node: pBasis_adjunction_finrank
/-- If [p is prime](hyp:hp), [F has characteristic p](hyp:hF), and
[s lies outside the intermediate field M](hyp:hs), then [adjoining s to M has
degree p](goal), where M contains the subfield generated by p-th powers. -/
lemma pBasis_adjunction_finrank (hp : PrimeChar p) (hF : PBasisFieldChar p F)
    (M : IntermediateField ↥(pBasisPowSubfield p F) F) (s : F)
    (hs : PBasisAdjunction p M s) :
    Module.finrank M ↥(IntermediateField.adjoin M {s}) = p := by
  let : Fact p.Prime := ⟨hp⟩
  let : CharP F p := hF
  have hsp : s ^ p ∈ M := by
    exact M.algebraMap_mem
      (⟨s ^ p, Subfield.subset_closure ⟨s, rfl⟩⟩ : pBasisPowSubfield p F)
  let a : M := ⟨s ^ p, hsp⟩
  have hirr : Irreducible (Polynomial.X ^ p - Polynomial.C a) := by
    apply X_pow_sub_C_irreducible_of_prime hp
    intro b hb
    have heq : (b : F) ^ p = s ^ p := congrArg (fun x : M => (x : F)) hb
    have hbs : (b : F) = s := (frobenius F p).injective heq
    exact hs (hbs ▸ b.property)
  have hroot : Polynomial.aeval s (Polynomial.X ^ p - Polynomial.C a) = 0 := by
    simp [a]
  have hint : IsIntegral M s := pBasis_isIntegral p hp M s
  rw [IntermediateField.adjoin.finrank hint,
    ← minpoly.eq_of_irreducible_of_monic hirr hroot
      (Polynomial.monic_X_pow_sub_C a hp.ne_zero), Polynomial.natDegree_X_pow_sub_C]

-- @node: pBasis_adjunction_basis
/-- For [a prime exponent p](hyp:p,hp), [a field F of characteristic p](hyp:hF),
[an intermediate field M containing the power subfield](hyp:M), and
[an element s of F](hyp:s) with [s outside M](hyp:hs), [the basis of M with s
adjoined, indexed from zero through p minus one](goal), is obtained by
[taking the power basis of s](step:1) and [reindexing it using the degree p of
the adjunction](step:2). -/
noncomputable def pBasis_adjunction_basis (hp : PrimeChar p) (hF : PBasisFieldChar p F)
    (M : IntermediateField ↥(pBasisPowSubfield p F) F) (s : F)
    (hs : PBasisAdjunction p M s) : Module.Basis (Fin p) M ↥(IntermediateField.adjoin M {s}) :=
  let pb := IntermediateField.adjoin.powerBasis (pBasis_isIntegral p hp M s)
  pb.basis.reindex (finCongr (pb.finrank.symm.trans (pBasis_adjunction_finrank p hp hF M s hs)))

-- @node: pBasis_adjunction_basis_apply
/-- If [p is prime](hyp:hp), [F has characteristic p](hyp:hF), and
[s lies outside M](hyp:hs), then [the entry at index i in the adjunction basis
is the i-th power of s, viewed as an element of the field obtained by adjoining
s to M](goal). -/
lemma pBasis_adjunction_basis_apply (hp : PrimeChar p) (hF : PBasisFieldChar p F)
    (M : IntermediateField ↥(pBasisPowSubfield p F) F) (s : F)
    (hs : PBasisAdjunction p M s) (i : Fin p) :
    pBasis_adjunction_basis p hp hF M s hs i =
      IntermediateField.AdjoinSimple.gen M s ^ (i : ℕ) := by
  simp [pBasis_adjunction_basis, Module.Basis.reindex_apply, PowerBasis.basis_eq_pow]

-- @node: pIndependent_snoc
/-- If [p is prime](hyp:hp), [F has characteristic p](hyp:hF),
[the list s is p-independent](hyp:hs), and [x is outside the field generated by
s over the power subfield](hyp:hx), then [appending x to s gives a p-independent list](goal). -/
lemma pIndependent_snoc (hp : PrimeChar p) (hF : PBasisFieldChar p F)
    {r : ℕ} (s : Fin r → F) (hs : IsPIndependent p F s) (x : F)
    (hx : x ∉ IntermediateField.adjoin ↥(pBasisPowSubfield p F) (Set.range s)) :
    IsPIndependent p F (Fin.snoc s x) := by
  let C := pBasisPowSubfield p F
  let M := IntermediateField.adjoin ↥C (Set.range s)
  let N := IntermediateField.adjoin M {x}
  have hN : N.restrictScalars C = IntermediateField.adjoin ↥C (Set.range (Fin.snoc s x)) := by
    rw [Fin.range_snoc, ← Set.singleton_union, Set.union_comm]
    exact IntermediateField.adjoin_adjoin_left C (Set.range s) {x}
  constructor
  change Module.finrank C ↥(IntermediateField.adjoin ↥C (Set.range (Fin.snoc s x))) = p ^ (r + 1)
  rw [← hN]
  change Module.finrank C N = p ^ (r + 1)
  rw [← Module.finrank_mul_finrank C M N,
    pBasis_adjunction_finrank p hp hF M x hx, hs.degree, pow_succ]

-- @node: pIndependent_extends_to_pBasis
/-- If [p is prime](hyp:hp), [F has characteristic p](hyp:hF),
[F is finite dimensional over its power subfield](hyp:hfin), and
[s is a p-independent list](hyp:hs), then [there is a p-basis of F of length at
least the length of s whose initial entries are exactly s](goal). -/
lemma pIndependent_extends_to_pBasis (hp : PrimeChar p) (hF : PBasisFieldChar p F)
    (hfin : PBasisFiniteDegree p F) {r : ℕ} (s : Fin r → F)
    (hs : IsPIndependent p F s) :
    ∃ (e : ℕ) (h : r ≤ e) (b : Fin e → F),
      IsPBasis p F b ∧ ∀ i, b (Fin.castLE h i) = s i := by
  classical
  let C := pBasisPowSubfield p F
  let : FiniteDimensional C F := hfin
  have aux : ∀ (n r : ℕ) (s : Fin r → F), IsPIndependent p F s →
      Module.finrank ↥(IntermediateField.adjoin ↥C (Set.range s)) F = n →
      ∃ (e : ℕ) (h : r ≤ e) (b : Fin e → F),
        IsPBasis p F b ∧ ∀ i, b (Fin.castLE h i) = s i := by
    intro n
    induction n using Nat.strong_induction_on with
    | h n ih =>
      intro r s hs hn
      let M := IntermediateField.adjoin ↥C (Set.range s)
      by_cases htop : M = ⊤
      · exact ⟨r, le_rfl, s, ⟨hs.degree, htop⟩, fun _ => rfl⟩
      have hnotall : ¬ ∀ x : F, x ∈ M := by
        intro h
        exact htop (top_le_iff.mp (fun x _ => h x))
      obtain ⟨x, hx⟩ := not_forall.mp hnotall
      let N := IntermediateField.adjoin ↥C (Set.range (Fin.snoc s x))
      have hle : M ≤ N := by
        apply IntermediateField.adjoin.mono
        rw [Fin.range_snoc]
        exact Set.subset_insert x (Set.range s)
      have hxn : x ∈ N := by
        apply IntermediateField.subset_adjoin
        rw [Fin.range_snoc]
        exact Set.mem_insert x (Set.range s)
      have hlt : M < N := lt_of_le_of_ne hle (by
        intro heq
        exact hx (heq.symm ▸ hxn))
      have hdim : Module.finrank N F < n := by
        rw [← hn]
        exact IntermediateField.finrank_lt_of_gt hlt
      obtain ⟨e, he, b, hb, hbinit⟩ := ih _ hdim (r + 1) (Fin.snoc s x)
        (pIndependent_snoc p hp hF s hs x hx) rfl
      refine ⟨e, (Nat.le_succ r).trans he, b, hb, ?_⟩
      intro i
      have hi : Fin.castLE he i.castSucc = Fin.castLE ((Nat.le_succ r).trans he) i :=
        Fin.ext rfl
      simpa only [Fin.snoc_castSucc, hi] using hbinit i.castSucc
  exact aux _ r s hs rfl

-- @node: pMonomial_unbounded_mem_span
/-- If [p is prime](hyp:hp), then [every product of nonnegative integer powers
of the entries of b lies in the linear span, over the power subfield, of the
monomials whose exponents are less than p](goal). -/
lemma pMonomial_unbounded_mem_span (hp : PrimeChar p) {e : ℕ}
    (b : Fin e → F) (n : Fin e → ℕ) :
    (∏ j, b j ^ n j) ∈
      Submodule.span ↥(pBasisPowSubfield p F) (Set.range (pMonomial p b)) := by
  classical
  let c : pBasisPowSubfield p F :=
    ∏ j, (⟨b j ^ p, Subfield.subset_closure ⟨b j, rfl⟩⟩ :
      pBasisPowSubfield p F) ^ (n j / p)
  let i : Fin e → Fin p := fun j => ⟨n j % p, Nat.mod_lt _ hp.pos⟩
  have heq : (∏ j, b j ^ n j) = c • pMonomial p b i := by
    change (∏ j, b j ^ n j) = (pBasisPowSubfield p F).subtype c * pMonomial p b i
    simp only [c, pMonomial, map_prod, map_pow, Subfield.subtype_apply,
      ← Finset.prod_mul_distrib]
    apply Finset.prod_congr rfl
    intro j _
    dsimp [i]
    rw [← pow_mul, ← pow_add, Nat.div_add_mod]
  rw [heq]
  exact Submodule.smul_mem _ c (Submodule.subset_span ⟨i, rfl⟩)

-- @node: pMonomial_span_eq_adjoin
/-- If [p is prime](hyp:hp), then [the linear span over the power subfield of
the monomials in b with exponents less than p equals the field generated by b
over that subfield, viewed as a vector subspace](goal). -/
lemma pMonomial_span_eq_adjoin (hp : PrimeChar p) {e : ℕ} (b : Fin e → F) :
    Submodule.span ↥(pBasisPowSubfield p F) (Set.range (pMonomial p b)) =
      (IntermediateField.adjoin ↥(pBasisPowSubfield p F)
        (Set.range b)).toSubalgebra.toSubmodule := by
  classical
  let C := pBasisPowSubfield p F
  have hint : ∀ x : F, IsIntegral C x := by
    intro x
    refine ⟨Polynomial.X ^ p - Polynomial.C
      (⟨x ^ p, Subfield.subset_closure ⟨x, rfl⟩⟩ : C),
      Polynomial.monic_X_pow_sub_C _ hp.ne_zero, ?_⟩
    simp only [Polynomial.eval₂_sub, Polynomial.eval₂_X_pow, Polynomial.eval₂_C]
    change x ^ p - x ^ p = 0
    exact sub_self _
  rw [IntermediateField.adjoin_toSubalgebra_of_isAlgebraic (fun x _ => (hint x).isAlgebraic),
    Algebra.adjoin_eq_span]
  apply le_antisymm
  · apply Submodule.span_le.mpr
    rintro _ ⟨i, rfl⟩
    apply Submodule.subset_span
    exact Submonoid.prod_mem _ (fun j _ =>
      Submonoid.pow_mem _ (Submonoid.subset_closure (Set.mem_range_self j)) _)
  · apply Submodule.span_le.mpr
    intro x hx
    obtain ⟨n, rfl⟩ := Submonoid.exists_of_mem_closure_range b x hx
    exact pMonomial_unbounded_mem_span p hp b n

-- @node: pBasis_monomials
/-- If [p is prime](hyp:hp) and [b is a p-basis of F](hyp:hb), then
[the monomials in b with exponents less than p are linearly independent over
the power subfield and span all of F](goal). -/
lemma pBasis_monomials (hp : PrimeChar p) {e : ℕ} (b : Fin e → F)
    (hb : IsPBasis p F b) :
    LinearIndependent ↥(pBasisPowSubfield p F) (pMonomial p b) ∧
    Submodule.span ↥(pBasisPowSubfield p F) (Set.range (pMonomial p b)) = ⊤ := by
  have hspan := pMonomial_span_eq_adjoin p hp b
  rw [show IntermediateField.adjoin ↥(pBasisPowSubfield p F) (Set.range b) = ⊤ from
    hb.generation] at hspan
  have hd := hb.degree
  change Module.finrank ↥(pBasisPowSubfield p F)
    ↥(IntermediateField.adjoin ↥(pBasisPowSubfield p F) (Set.range b)) = p ^ e at hd
  rw [show IntermediateField.adjoin ↥(pBasisPowSubfield p F) (Set.range b) = ⊤ from
    hb.generation, IntermediateField.finrank_top'] at hd
  have htop : Submodule.span ↥(pBasisPowSubfield p F)
      (Set.range (pMonomial p b)) = ⊤ := by simpa using hspan
  refine ⟨linearIndependent_of_top_le_span_of_card_eq_finrank htop.ge ?_, htop⟩
  simp [hd]

-- @node: pMonomial_axis
/-- If [every exponent in i outside coordinate j is zero](hyp:hi), then
[the monomial indexed by i equals the j-th entry of b raised to the exponent
at coordinate j](goal). -/
lemma pMonomial_axis [NeZero p] {e : ℕ} (b : Fin e → F)
    (j : Fin e) (i : Fin e → Fin p) (hi : ∀ k, k ≠ j → i k = 0) :
    pMonomial p b i = b j ^ (i j : ℕ) := by
  classical
  apply Finset.prod_eq_single j
  · intro k _ hkj
    rw [hi k hkj]
    simp
  · simp

-- @node: pBasis_simple_span
/-- If [p is prime](hyp:hp), then [the field generated by the j-th entry of b
over the power subfield, viewed as a vector subspace, is the span of the bounded
monomials whose exponents vanish outside coordinate j](goal). -/
lemma pBasis_simple_span (hp : PrimeChar p) [NeZero p] {e : ℕ} (b : Fin e → F) (j : Fin e) :
    (IntermediateField.adjoin ↥(pBasisPowSubfield p F) {b j}).toSubalgebra.toSubmodule =
      Submodule.span ↥(pBasisPowSubfield p F)
        (pMonomial p b '' {i | ∀ k, k ≠ j → i k = 0}) := by
  classical
  let : NeZero p := ⟨hp.ne_zero⟩
  have h := pMonomial_span_eq_adjoin p hp (fun _ : Fin 1 => b j)
  have hr : Set.range (fun _ : Fin 1 => b j) = {b j} := by ext; simp
  rw [hr] at h
  rw [← h]
  congr 1
  ext x
  constructor
  · rintro ⟨i, rfl⟩
    refine ⟨Function.update 0 j (i 0), ?_, ?_⟩
    · intro k hkj
      simp [Function.update_of_ne hkj]
    · rw [pMonomial_axis p b j _ (by
        intro k hkj
        simp [Function.update_of_ne hkj])]
      simp [pMonomial]
  · rintro ⟨i, hi, rfl⟩
    refine ⟨fun _ => i j, ?_⟩
    rw [pMonomial_axis p b j i hi]
    simp [pMonomial]

-- @node: pBasis_simple_inf
/-- If [p is prime](hyp:hp), [b is a p-basis of F](hyp:hb), and
[j and k are distinct coordinates](hyp:hjk), then [the fields generated
separately by the j-th and k-th entries of b over the power subfield intersect
exactly in the power subfield](goal). -/
lemma pBasis_simple_inf (hp : PrimeChar p) {e : ℕ} (b : Fin e → F)
    (hb : IsPBasis p F b) (j k : Fin e) (hjk : j ≠ k) :
    IntermediateField.adjoin ↥(pBasisPowSubfield p F) {b j} ⊓
      IntermediateField.adjoin ↥(pBasisPowSubfield p F) {b k} = ⊥ := by
  classical
  let : NeZero p := ⟨hp.ne_zero⟩
  let C := pBasisPowSubfield p F
  obtain ⟨hli, hspan⟩ := pBasis_monomials p hp b hb
  let B : Module.Basis (Fin e → Fin p) C F := Module.Basis.mk hli hspan.ge
  have hB : (B : (Fin e → Fin p) → F) = pMonomial p b := by
    funext i
    exact Module.Basis.mk_apply _ _ _
  apply le_antisymm ?_ bot_le
  intro x hx
  have hxj : x ∈ Submodule.span C
      (B '' {i | ∀ l, l ≠ j → i l = 0}) := by
    rw [hB, ← pBasis_simple_span p hp b j]
    exact hx.1
  have hxk : x ∈ Submodule.span C
      (B '' {i | ∀ l, l ≠ k → i l = 0}) := by
    rw [hB, ← pBasis_simple_span p hp b k]
    exact hx.2
  have hx0 : x ∈ Submodule.span C (B '' {0}) := by
    rw [B.mem_span_image] at hxj hxk ⊢
    intro i hi
    have hij := hxj hi
    have hik := hxk hi
    apply Set.mem_singleton_iff.mpr
    funext l
    by_cases hlj : l = j
    · exact hik l (by simpa [hlj] using hjk)
    · exact hij l hlj
  have hzero : B 0 = (1 : F) := by rw [hB]; simp [pMonomial]
  rw [Set.image_singleton, hzero] at hx0
  obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hx0
  rw [IntermediateField.mem_bot]
  refine ⟨c, ?_⟩
  simpa [Algebra.smul_def] using hc

-- @node: pMonomial_reduce
/-- If [p is prime](hyp:hp), then [the product of the entries of b raised to
arbitrary nonnegative exponents n equals a scalar from the power subfield times
the monomial obtained by reducing each exponent modulo p](goal). -/
lemma pMonomial_reduce (hp : PrimeChar p) {e : ℕ} (b : Fin e → F)
    (n : Fin e → ℕ) :
    ∃ c : pBasisPowSubfield p F,
      (∏ k, b k ^ n k) = c • pMonomial p b
        (fun k => ⟨n k % p, Nat.mod_lt _ hp.pos⟩) := by
  classical
  refine ⟨∏ k, (⟨b k ^ p, Subfield.subset_closure ⟨b k, rfl⟩⟩ :
    pBasisPowSubfield p F) ^ (n k / p), ?_⟩
  change (∏ k, b k ^ n k) = (pBasisPowSubfield p F).subtype _ * _
  simp only [pMonomial, map_prod, map_pow, Subfield.subtype_apply,
    ← Finset.prod_mul_distrib]
  apply Finset.prod_congr rfl
  intro k _
  rw [← pow_mul, ← pow_add, Nat.div_add_mod]

-- @node: pBasis_euler_operators
/-- If [p is prime](hyp:hp), [F has characteristic p](hyp:hF), and
[b is a p-basis of F](hyp:hb), then [there is one derivation over the power
subfield for each coordinate, these derivations commute, and each acts on a
bounded monomial by multiplying it by its exponent at that coordinate](goal). -/
lemma pBasis_euler_operators (hp : PrimeChar p) (hF : PBasisFieldChar p F)
    {e : ℕ} (b : Fin e → F) (hb : IsPBasis p F b) :
    ∃ D : Fin e → Derivation ↥(pBasisPowSubfield p F) F F,
      (∀ j k x, D j (D k x) = D k (D j x)) ∧
      (∀ j i, D j (pMonomial p b i) =
        (((i j : ℕ) : ↥(pBasisPowSubfield p F))) • pMonomial p b i) := by
  classical
  let C := pBasisPowSubfield p F
  let : CharP F p := hF
  let : CharP C p := (C.subtype.charP_iff Subtype.val_injective p).mpr inferInstance
  obtain ⟨hli, hspan⟩ := pBasis_monomials p hp b hb
  let B : Module.Basis (Fin e → Fin p) C F := Module.Basis.mk hli hspan.ge
  have hB (i) : B i = pMonomial p b i := Module.Basis.mk_apply _ _ _
  let L : Fin e → F →ₗ[C] F := fun j =>
    B.constr C (fun i => ((i j : ℕ) : C) • B i)
  have hL (j i) : L j (pMonomial p b i) = ((i j : ℕ) : C) • pMonomial p b i := by
    simpa only [← hB] using B.constr_basis C (fun i => ((i j : ℕ) : C) • B i) i
  have hunbounded (j : Fin e) (n : Fin e → ℕ) :
      L j (∏ k, b k ^ n k) = (n j : C) • (∏ k, b k ^ n k) := by
    obtain ⟨c, hc⟩ := pMonomial_reduce p hp b n
    rw [hc, map_smul, hL]
    rw [CharP.cast_eq_mod C p (n j)]
    exact smul_comm _ _ _
  have hmul (j : Fin e) (x y : F) :
      L j (x * y) = x * L j y + y * L j x := by
    have hxy (i k : Fin e → Fin p) :
        L j (pMonomial p b i * pMonomial p b k) =
          pMonomial p b i * L j (pMonomial p b k) +
            pMonomial p b k * L j (pMonomial p b i) := by
      have hprod : pMonomial p b i * pMonomial p b k =
          ∏ l, b l ^ ((i l : ℕ) + (k l : ℕ)) := by
        simp only [pMonomial, pow_add, Finset.prod_mul_distrib]
      rw [hprod, hunbounded, ← hprod, hL, hL, Nat.cast_add]
      simp only [Algebra.smul_def, map_add]
      ring
    have hx : x ∈ Submodule.span C (Set.range (pMonomial p b)) := hspan ▸ Submodule.mem_top
    have hy : y ∈ Submodule.span C (Set.range (pMonomial p b)) := hspan ▸ Submodule.mem_top
    induction hx using Submodule.span_induction with
    | mem x hx =>
      obtain ⟨i, rfl⟩ := hx
      induction hy using Submodule.span_induction with
      | mem y hy => obtain ⟨k, rfl⟩ := hy; exact hxy i k
      | zero => simp
      | add y z _ _ ihy ihz => simp only [mul_add, map_add, ihy, ihz, add_mul]; ring
      | smul c y _ ih =>
        rw [mul_smul_comm, map_smul, ih, map_smul]
        simp only [Algebra.smul_def]
        ring
    | zero => simp
    | add x z _ _ ihx ihz =>
      simp only [add_mul, map_add, ihx, ihz, mul_add]
      ring
    | smul c x _ ih =>
      rw [smul_mul_assoc, map_smul, ih, map_smul]
      simp only [Algebra.smul_def]
      ring
  let D : Fin e → Derivation C F F := fun j =>
    Derivation.mk' (L j) (fun x y => by simpa only [smul_eq_mul] using hmul j x y)
  refine ⟨D, ?_, hL⟩
  intro j k x
  have hcomm : (L j).comp (L k) = (L k).comp (L j) := by
    apply B.ext
    intro i
    simp only [LinearMap.comp_apply, hB, hL, map_smul]
    exact smul_comm _ _ _
  exact LinearMap.congr_fun hcomm x

-- @node: pBasis_euler_axis
/-- If [p is prime](hyp:hp), [each derivation in D multiplies every bounded
monomial by its exponent at the derivation's coordinate](hyp:hD), and
[n is less than p](hyp:hn), then [the j-th derivation applied to c times the
n-th power of the j-th generator equals n times that same element](goal),
for c in the power subfield. -/
lemma pBasis_euler_axis (hp : PrimeChar p) {e : ℕ} (b : Fin e → F)
    (D : Fin e → Derivation ↥(pBasisPowSubfield p F) F F)
    (hD : ∀ j i, D j (pMonomial p b i) =
      (((i j : ℕ) : ↥(pBasisPowSubfield p F))) • pMonomial p b i)
    (j : Fin e) (c : pBasisPowSubfield p F) (n : ℕ) (hn : n < p) :
    D j ((c : F) * b j ^ n) = (n : ↥(pBasisPowSubfield p F)) • ((c : F) * b j ^ n) := by
  classical
  let : NeZero p := ⟨hp.ne_zero⟩
  let i : Fin e → Fin p := Function.update 0 j ⟨n, hn⟩
  have haxis : pMonomial p b i = b j ^ n := by
    simpa [i] using pMonomial_axis p b j i (by intro k hk; simp [i, hk])
  have hpower : D j (b j ^ n) = (n : ↥(pBasisPowSubfield p F)) • b j ^ n := by
    simpa [haxis, i] using hD j i
  change D j (c • b j ^ n) = (n : ↥(pBasisPowSubfield p F)) • (c • b j ^ n)
  rw [Derivation.map_smul, hpower, smul_comm]

-- @node: pBasis_euler_simple_spectral
/-- Suppose [p is prime](hyp:hp), [F has characteristic p](hyp:hF),
[b is a p-basis](hyp:hb), and [each derivation in D multiplies every bounded
monomial by its exponent at the derivation's coordinate](hyp:hD). If
[x belongs to the field generated by the j-th generator over the power subfield](hyp:hx),
[x is nonzero](hyp:hx0), and [the j-th derivation sends x to a times x](hyp:ha),
then [x is a nonzero power-subfield scalar times the n-th power of the j-th
generator for some n less than p, and a equals n in the power subfield](goal). -/
lemma pBasis_euler_simple_spectral (hp : PrimeChar p) (hF : PBasisFieldChar p F)
    {e : ℕ} (b : Fin e → F) (hb : IsPBasis p F b)
    (D : Fin e → Derivation ↥(pBasisPowSubfield p F) F F)
    (hD : ∀ j i, D j (pMonomial p b i) =
      (((i j : ℕ) : ↥(pBasisPowSubfield p F))) • pMonomial p b i)
    (j : Fin e) (x : F)
    (hx : x ∈ IntermediateField.adjoin ↥(pBasisPowSubfield p F) {b j}) (hx0 : x ≠ 0)
    (a : pBasisPowSubfield p F) (ha : D j x = a • x) :
    ∃ (c : pBasisPowSubfield p F), c ≠ 0 ∧
      ∃ n : ℕ, n < p ∧ x = (c : F) * b j ^ n ∧ a = (n : ↥(pBasisPowSubfield p F)) := by
  classical
  let C := pBasisPowSubfield p F
  let : NeZero p := ⟨hp.ne_zero⟩
  let : CharP F p := hF
  let : CharP C p := (C.subtype.charP_iff Subtype.val_injective p).mpr inferInstance
  obtain ⟨hli, hspan⟩ := pBasis_monomials p hp b hb
  let B : Module.Basis (Fin e → Fin p) C F := Module.Basis.mk hli hspan.ge
  have hB (i) : B i = pMonomial p b i := Module.Basis.mk_apply _ _ _
  have hsupport : ∀ i, B.repr x i ≠ 0 → ∀ k, k ≠ j → i k = 0 := by
    have hxspan : x ∈ Submodule.span C (B '' {i | ∀ k, k ≠ j → i k = 0}) := by
      simp_rw [hB]
      rw [← pBasis_simple_span p hp b j]
      exact hx
    intro i hi
    exact B.mem_span_image.mp hxspan (Finsupp.mem_support_iff.mpr hi)
  have hcoord (i) : B.repr (D j x) i = ((i j : ℕ) : C) * B.repr x i := by
    conv_lhs => rw [← B.sum_repr x]
    simp only [map_sum, Derivation.map_smul, hB, hD, map_smul]
    simp [← hB, mul_comm, Finsupp.single_apply]
  have hweight (i) (hi : B.repr x i ≠ 0) : ((i j : ℕ) : C) = a := by
    have heq := congrArg (fun y => B.repr y i) ha
    rw [hcoord, map_smul] at heq
    exact (mul_right_cancel₀ hi) heq
  obtain ⟨i, hi⟩ : ∃ i, B.repr x i ≠ 0 := by
    by_contra! hzero
    apply hx0
    apply B.repr.injective
    ext i
    simpa using hzero i
  have honly (k) (hk : B.repr x k ≠ 0) : k = i := by
    have hkj : k j = i j := by
      apply Fin.ext
      exact CharP.natCast_injOn_Iio C p (k j).isLt (i j).isLt
        ((hweight k hk).trans (hweight i hi).symm)
    funext l
    by_cases hl : l = j
    · simpa [hl] using hkj
    · rw [hsupport k hk l hl, hsupport i hi l hl]
  have hexpand : x = B.repr x i • B i := by
    conv_lhs => rw [← B.sum_repr x]
    apply Finset.sum_eq_single i
    · intro k _ hki
      have hz : B.repr x k = 0 := by
        by_contra hk
        exact hki (honly k hk)
      rw [hz, zero_smul]
    · simp
  refine ⟨B.repr x i, hi, (i j : ℕ), (i j).isLt, ?_, (hweight i hi).symm⟩
  calc
    x = B.repr x i • B i := hexpand
    _ = _ := by rw [hB, pMonomial_axis p b j i (hsupport i hi)]; rfl

-- @node: lem:p-basis
/-- If [p is prime](hyp:hp) and [F has characteristic p](hyp:hF), then
[every strict simple adjunction over an intermediate field containing the
power subfield has degree p; if F is finite dimensional over the power
subfield, every p-independent list extends to a p-basis, and every p-basis of
length e gives degree p to the power e and a basis of bounded monomials,
together with commuting coordinate derivations that multiply monomials by
their coordinate exponents](goal). [On each field generated by one basis
element, the corresponding derivation vanishes exactly on the power subfield,
its nonzero eigenvectors with eigenvalues in the power subfield are exactly
the nonzero power-subfield multiples of powers with exponent less than p,
and it multiplies each such scalar multiple by its exponent; fields generated
by distinct basis elements intersect exactly in the power subfield](goal). -/
lemma pBasis_structure (hp : PrimeChar p) (hF : PBasisFieldChar p F) :
    (∀ (M : IntermediateField ↥(pBasisPowSubfield p F) F) (s : F),
      PBasisAdjunction p M s → Module.finrank M ↥(IntermediateField.adjoin M {s}) = p) ∧
    (PBasisFiniteDegree p F →
      (∀ (r : ℕ) (s : Fin r → F), IsPIndependent p F s →
        ∃ (e : ℕ) (h : r ≤ e) (b : Fin e → F), -- @realizes e(length of the extending p-basis)
          IsPBasis p F b ∧ ∀ i, b (Fin.castLE h i) = s i) ∧
      ∀ (e : ℕ) (b : Fin e → F), IsPBasis p F b →
        Module.finrank ↥(pBasisPowSubfield p F) F = p ^ e ∧
        LinearIndependent ↥(pBasisPowSubfield p F) (pMonomial p b) ∧
        Submodule.span ↥(pBasisPowSubfield p F) (Set.range (pMonomial p b)) = ⊤ ∧
        (∃ D : Fin e → Derivation ↥(pBasisPowSubfield p F) F F, -- @realizes D_j(C-derivations)
          (∀ j k x, D j (D k x) = D k (D j x)) ∧
          (∀ j i, D j (pMonomial p b i) =
            (((i j : ℕ) : ↥(pBasisPowSubfield p F))) •
              pMonomial p b i) ∧ -- @realizes D_j(Euler formula)
          (∀ j, ∀ x ∈ IntermediateField.adjoin ↥(pBasisPowSubfield p F) {b j},
            D j x = 0 ↔ x ∈ (⊥ : IntermediateField ↥(pBasisPowSubfield p F) F)) ∧
          (∀ j, ∀ x ∈ IntermediateField.adjoin ↥(pBasisPowSubfield p F) {b j}, x ≠ 0 →
            ((∃ a : ↥(pBasisPowSubfield p F), D j x = a • x) ↔
              ∃ c : ↥(pBasisPowSubfield p F), c ≠ 0 ∧ -- @realizes c(nonzero coefficient in C)
                ∃ i : ℕ, i < p ∧ x = (c : F) * b j ^ i)) ∧
          ∀ j (c : ↥(pBasisPowSubfield p F)) (i : ℕ), i < p →
            D j ((c : F) * b j ^ i) =
              ((i : ↥(pBasisPowSubfield p F))) • ((c : F) * b j ^ i)) ∧
        ∀ j k, j ≠ k → -- @realizes k(basis index distinct from j)
          IntermediateField.adjoin ↥(pBasisPowSubfield p F) {b j} ⊓
            IntermediateField.adjoin ↥(pBasisPowSubfield p F) {b k} = ⊥) := by
  refine ⟨pBasis_adjunction_finrank p hp hF, ?_⟩
  intro hfin
  refine ⟨fun r s hs => pIndependent_extends_to_pBasis p hp hF hfin s hs, ?_⟩
  intro e b hb
  have hd := hb.degree
  change Module.finrank ↥(pBasisPowSubfield p F)
    ↥(IntermediateField.adjoin ↥(pBasisPowSubfield p F) (Set.range b)) = p ^ e at hd
  rw [show IntermediateField.adjoin ↥(pBasisPowSubfield p F) (Set.range b) = ⊤ from
    hb.generation, IntermediateField.finrank_top'] at hd
  obtain ⟨hli, hspan⟩ := pBasis_monomials p hp b hb
  refine ⟨hd, hli, hspan, ?_⟩
  refine ⟨?_, pBasis_simple_inf p hp b hb⟩
  obtain ⟨D, hcomm, hEuler⟩ := pBasis_euler_operators p hp hF b hb
  refine ⟨D, hcomm, hEuler, ?_, ?_, ?_⟩
  · intro j x hx
    constructor
    · intro hzero
      by_cases hx0 : x = 0
      · simp [hx0]
      obtain ⟨c, hc, n, hn, hxn, hweight⟩ :=
        pBasis_euler_simple_spectral p hp hF b hb D hEuler j x hx hx0 0 (by simpa using hzero)
      let C := pBasisPowSubfield p F
      let : CharP F p := hF
      let : CharP C p := (C.subtype.charP_iff Subtype.val_injective p).mpr inferInstance
      have hn0 : n = 0 := CharP.natCast_injOn_Iio C p hn hp.pos (by simpa using hweight.symm)
      rw [hn0, pow_zero, mul_one] at hxn
      rw [hxn, IntermediateField.mem_bot]
      exact ⟨c, rfl⟩
    · intro hxbase
      obtain ⟨c, rfl⟩ := IntermediateField.mem_bot.mp hxbase
      exact (D j).map_algebraMap c
  · intro j x hx hx0
    constructor
    · rintro ⟨a, ha⟩
      obtain ⟨c, hc, n, hn, hxn, _⟩ :=
        pBasis_euler_simple_spectral p hp hF b hb D hEuler j x hx hx0 a ha
      exact ⟨c, hc, n, hn, hxn⟩
    · rintro ⟨c, hc, n, hn, rfl⟩
      exact ⟨n, pBasis_euler_axis p hp b D hEuler j c n hn⟩
  · exact pBasis_euler_axis p hp b D hEuler

end Papers.OaiReconstructionMilnorTheory