module

public import Papers.OaiReconstructionMilnorTheory.Helpers.PBasis
public import Papers.OaiReconstructionMilnorTheory.Helpers.Symbols
public import Mathlib.Data.Fin.VecNotation
public import Mathlib.Algebra.Field.ZMod

/-! # The two-variable intersection configuration and its unique power correction -/

@[expose] public section

namespace Papers.OaiReconstructionMilnorTheory

-- @env: S4
variable (p : ℕ) {F : Type*} [Field F]

-- @node: def:intersection-power-subfield
/-- For [an exponent p](hyp:p) and [a field F](hyp:F), the
[power subfield](goal) is the subfield generated by all p-th powers in F. -/
abbrev intersectionPowSubfield (F : Type*) [Field F] : Subfield F :=
  powSubfield p F -- @realizes C(F^p in the intersection configuration)

-- @node: ass:intersection-field
/-- For [a field F](hyp:F) and [a natural number p](hyp:p), the
[characteristic condition](goal) says that F has characteristic p. -/
def IntersectionFieldChar (F : Type*) [Field F] : Prop := CharP F p

-- @node: ass:intersection-finite-degree
/-- For [a field F](hyp:F) and [an exponent p](hyp:p), the
[finite-degree condition](goal) says that F has finite dimension over the subfield
generated by its p-th powers. -/
def IntersectionFiniteDegree (F : Type*) [Field F] : Prop :=
  FiniteDimensional ↥(intersectionPowSubfield p F) F -- @realizes F(finite degree over F^p)

-- @node: ass:intersection-pair-inputs
/-- For [an exponent p](hyp:p) and [two field elements X and Y](hyp:X,Y), the
[independent-pair condition](goal) requires [X to be nonzero](step:1),
[Y to be nonzero](step:2), and [the pair to be p-independent](step:3), meaning
their monomials with each exponent below p are linearly independent over the power subfield. -/
def IntersectionPairInputs (X Y : F) : Prop := -- @realizes X(carrier F) @realizes Y(carrier F)
  X ≠ 0 ∧ -- @realizes X(nonzero field element)
  Y ≠ 0 ∧ -- @realizes Y(nonzero field element)
  IsPIndependent p F ![X, Y] -- @realizes X(p-independent with Y) @realizes Y(p-independent with X)

-- @node: ass:pin-2
/-- For [a modulus p](hyp:p), [a field element X](hyp:X), and
[a degree-one Milnor class x](hyp:x), the [span condition](goal) says that x is
a scalar multiple of the class of X over the integers modulo p. -/
def FpMultiplesPin (X : F) (x : MilnorOne F p) : Prop :=
  x ∈ Submodule.span (Coeff p) {cls p X}

-- @node: ass:intersection-elements
/-- For [an exponent p](hyp:p), [coordinates X and Y](hyp:X,Y), and
[elements U and V](hyp:U,V), the [intersection-element condition](goal) requires
[U to be nonzero in the field generated by X over the power subfield](step:1),
[V to be nonzero in the field generated by Y over the power subfield](step:2),
[the class of U to lie outside the modulo-p scalar span of the class of X](step:3), and
[the class of V to lie outside the modulo-p scalar span of the class of Y](step:4). -/
def IntersectionElements (X Y U V : F) : Prop := -- @realizes U(carrier F) @realizes V(carrier F)
  (U ∈ IntermediateField.adjoin ↥(intersectionPowSubfield p F) {X} ∧
    U ≠ 0) ∧ -- @realizes U(nonzero element of C(X))
  (V ∈ IntermediateField.adjoin ↥(intersectionPowSubfield p F) {Y} ∧
    V ≠ 0) ∧ -- @realizes V(nonzero element of C(Y))
  ¬ FpMultiplesPin p X (cls p U) ∧ -- @realizes U(class outside the F_p span of [X])
  ¬ FpMultiplesPin p Y (cls p V) -- @realizes V(class outside the F_p span of [Y])

-- @node: ass:intersection-witness
/-- For [an exponent p](hyp:p) and [field elements X, Y, U, and V](hyp:X,Y,U,V), an
[intersection witness](goal) consists of coefficients a and b such that
[a belongs to the field generated by Y/X over the power subfield](step:1),
[a is nonzero](step:2),
[b belongs to the field generated by V/U over the power subfield](step:3),
[b is nonzero](step:4), and [X times a equals U times b](step:5). -/
def IntersectionWitness (X Y U V : F) : Prop :=
  ∃ a b : F,
    a ∈ IntermediateField.adjoin ↥(intersectionPowSubfield p F) {Y / X} ∧ a ≠ 0 ∧
    b ∈ IntermediateField.adjoin ↥(intersectionPowSubfield p F) {V / U} ∧ b ≠ 0 ∧
    X * a = U * b

/-- For [a coefficient subfield C](hyp:C), [field elements Z and W](hyp:Z,W), and
[an exponent m](hyp:m), the [affine power condition](goal) says that there are
coefficients a and b with [a in C](step:1), [b in C](step:2), and
[W to the m-th power equal to a plus b times Z to the m-th power](step:3). -/
def AffPow (C : Subfield F) (Z W : F) (m : ℕ) : Prop :=
  ∃ a ∈ C, ∃ b ∈ C, W ^ m = a + b * Z ^ m

-- @node: intersection_pin_of_power
/-- If [p is prime](hyp:hp), [U is nonzero](hyp:hU), [n is at least one](hyp:hn),
[n is below p](hyp:hnp), and [the class of U to the n-th power is in the
modulo-p scalar span of the class of X](hyp:h), then [the class of U is in
that same span](goal). -/
lemma intersection_pin_of_power (hp : PrimeChar p) {X U : F} (hU : U ≠ 0)
    {n : ℕ} (hn : 1 ≤ n) (hnp : n < p)
    (h : FpMultiplesPin p X (cls p (U ^ n))) : FpMultiplesPin p X (cls p U) := by
  let : Fact p.Prime := ⟨hp⟩
  have hn0 : (n : Coeff p) ≠ 0 := by
    intro hz
    have := CharP.natCast_injOn_Iio (Coeff p) p hnp hp.pos (by simpa using hz)
    omega
  have hpow : cls p (U ^ n) = (n : Coeff p) • cls p U := by
    simpa only [zpow_natCast, natCast_zsmul, Nat.cast_smul_eq_nsmul] using
      cls_zpow p U hU (n : ℤ)
  unfold FpMultiplesPin at h ⊢
  rw [hpow] at h
  have hinv := (Submodule.span (Coeff p) {cls p X}).smul_mem ((n : Coeff p)⁻¹) h
  simpa only [smul_smul, inv_mul_cancel₀ hn0, one_smul] using hinv

-- @node: intersection_affPow_coefficients_ne_zero
/-- If [p is prime](hyp:hp), [F has characteristic p](hyp:hF),
[X is nonzero](hyp:hX), [U is nonzero](hyp:hU), and
[the class of U lies outside the modulo-p scalar span of the class of X](hyp:hoff),
then, whenever [n is at least one](hyp:hn), [n is below p](hyp:hnp),
[a belongs to the power subfield](hyp:ha), [b belongs to the power subfield](hyp:hb),
and [U to the n-th power equals a plus b times X to the n-th power](hyp:heq),
[both a and b are nonzero](goal). -/
lemma intersection_affPow_coefficients_ne_zero (hp : PrimeChar p) (hF : CharP F p)
    {X U : F} (hX : X ≠ 0) (hU : U ≠ 0)
    (hoff : ¬ FpMultiplesPin p X (cls p U)) {n : ℕ} (hn : 1 ≤ n) (hnp : n < p)
    {a b : F} (ha : a ∈ powSubfield p F) (hb : b ∈ powSubfield p F)
    (heq : U ^ n = a + b * X ^ n) : a ≠ 0 ∧ b ≠ 0 := by
  have hpow (z : F) (hz : z ≠ 0) :
      cls p (z ^ n) = (n : Coeff p) • cls p z := by
    simpa only [zpow_natCast, natCast_zsmul, Nat.cast_smul_eq_nsmul] using
      cls_zpow p z hz (n : ℤ)
  have hUn : U ^ n ≠ 0 := pow_ne_zero _ hU
  constructor
  · intro ha0
    have hb0 : b ≠ 0 := by
      intro hb0
      exact hUn (by simpa only [ha0, hb0, zero_mul, zero_add] using heq)
    apply hoff
    apply intersection_pin_of_power p hp hU hn hnp
    rw [heq, ha0, zero_add, cls_mul p b (X ^ n) hb0 (pow_ne_zero _ hX),
      cls_eq_zero_of_mem_powSubfield p hp hF hb hb0, zero_add, hpow X hX]
    exact Submodule.smul_mem _ _ (Submodule.subset_span (Set.mem_singleton _))
  · intro hb0
    have ha0 : a ≠ 0 := by
      intro ha0
      exact hUn (by simpa only [ha0, hb0, zero_mul, zero_add] using heq)
    apply hoff
    apply intersection_pin_of_power p hp hU hn hnp
    have hUa : U ^ n = a := by simpa [hb0] using heq
    rw [hUa, cls_eq_zero_of_mem_powSubfield p hp hF ha ha0]
    exact Submodule.zero_mem _

-- @node: intersection_affPow_logarithmic
/-- Suppose [p is prime](hyp:hp), [F has characteristic p](hyp:hF), and
[the derivation D sends X to X](hyp:hDX). If [n is at least one](hyp:hn),
[n is below p](hyp:hnp), [a is in the power subfield](hyp:ha),
[b is in the power subfield](hyp:hb), and
[U to the n-th power equals a plus b times X to the n-th power](hyp:heq), then
[U to the power n minus one, multiplied by the derivative of U, equals b times X to the n-th power](goal). -/
lemma intersection_affPow_logarithmic (hp : PrimeChar p) (hF : CharP F p)
    (D : Derivation ↥(powSubfield p F) F F) {X U : F} (hDX : D X = X)
    {n : ℕ} (hn : 1 ≤ n) (hnp : n < p) {a b : F}
    (ha : a ∈ powSubfield p F) (hb : b ∈ powSubfield p F)
    (heq : U ^ n = a + b * X ^ n) :
    U ^ (n - 1) * D U = b * X ^ n := by
  let : CharP F p := hF
  have hn0 : (n : F) ≠ 0 := by
    intro hz
    have := CharP.natCast_injOn_Iio F p hnp hp.pos (by simpa using hz)
    omega
  have hDa : D a = 0 := D.map_algebraMap (⟨a, ha⟩ : powSubfield p F)
  have hDb : D b = 0 := D.map_algebraMap (⟨b, hb⟩ : powSubfield p F)
  have hXp : X ^ (n - 1) * X = X ^ n := by
    rw [← pow_succ, Nat.sub_add_cancel hn]
  have hd := congrArg D heq
  simp only [map_add, Derivation.leibniz, Derivation.leibniz_pow, hDa, hDb, hDX,
    smul_eq_mul, nsmul_eq_mul, zero_add, zero_mul, mul_zero, add_zero] at hd
  apply mul_left_cancel₀ hn0
  calc
    (n : F) * (U ^ (n - 1) * D U) = b * ((n : F) * (X ^ (n - 1) * X)) := by
      simpa only [mul_assoc] using hd
    _ = (n : F) * (b * X ^ n) := by rw [hXp]; ring

-- @node: intersection_affPow_unique_of_euler
/-- Suppose [p is prime](hyp:hp), [F has characteristic p](hyp:hF),
[D sends X to X](hyp:hDX), [X is nonzero](hyp:hX), [U is nonzero](hyp:hU), and
[the class of U lies outside the modulo-p scalar span of the class of X](hyp:hoff).
If [r is at least one](hyp:hr), [r is below p](hyp:hrp),
[n is at least one](hyp:hn), [n is below p](hyp:hnp), and
[U to the r-th power is an affine function of X to the r-th power over the power subfield](hyp:hrelr)
while [the analogous affine relation holds at exponent n](hyp:hreln), then
[r equals n](goal). -/
lemma intersection_affPow_unique_of_euler (hp : PrimeChar p) (hF : CharP F p)
    (D : Derivation ↥(powSubfield p F) F F) {X U : F}
    (hDX : D X = X) (hX : X ≠ 0) (hU : U ≠ 0)
    (hoff : ¬ FpMultiplesPin p X (cls p U))
    {r n : ℕ} (hr : 1 ≤ r) (hrp : r < p) (hn : 1 ≤ n) (hnp : n < p)
    (hrelr : AffPow (powSubfield p F) X U r)
    (hreln : AffPow (powSubfield p F) X U n) : r = n := by
  let : CharP F p := hF
  obtain ⟨a, ha, b, hb, hUr⟩ := hrelr
  obtain ⟨c, hc, d, hd, hUn⟩ := hreln
  obtain ⟨ha0, hb0⟩ := intersection_affPow_coefficients_ne_zero p hp hF hX hU hoff hr hrp ha hb hUr
  obtain ⟨hc0, hd0⟩ := intersection_affPow_coefficients_ne_zero p hp hF hX hU hoff hn hnp hc hd hUn
  have hlogr := intersection_affPow_logarithmic p hp hF D hDX hr hrp ha hb hUr
  have hlogn := intersection_affPow_logarithmic p hp hF D hDX hn hnp hc hd hUn
  have hlogr' : U ^ r * D U = U * (b * X ^ r) := by
    conv_lhs => rw [← Nat.sub_add_cancel hr, pow_succ']
    calc
      U * U ^ (r - 1) * D U = U * (U ^ (r - 1) * D U) := by ring
      _ = _ := by rw [hlogr]
  have hlogn' : U ^ n * D U = U * (d * X ^ n) := by
    conv_lhs => rw [← Nat.sub_add_cancel hn, pow_succ']
    calc
      U * U ^ (n - 1) * D U = U * (U ^ (n - 1) * D U) := by ring
      _ = _ := by rw [hlogn]
  have hcross : a * d * X ^ n = c * b * X ^ r := by
    have hmul : U * (U ^ r * (d * X ^ n)) = U * (U ^ n * (b * X ^ r)) := by
      calc
        _ = U ^ r * (U ^ n * D U) := by rw [hlogn']; ring
        _ = U ^ n * (U ^ r * D U) := by ring
        _ = _ := by rw [hlogr']; ring
    have h := mul_left_cancel₀ hU hmul
    rw [hUr, hUn] at h
    linear_combination h
  have hDconst (v : F) (hv : v ∈ powSubfield p F) : D v = 0 :=
    D.map_algebraMap (⟨v, hv⟩ : powSubfield p F)
  have hDXpow (k : ℕ) (hk : 1 ≤ k) : D (X ^ k) = (k : F) * X ^ k := by
    simp only [Derivation.leibniz_pow, hDX, smul_eq_mul, nsmul_eq_mul]
    rw [← pow_succ, Nat.sub_add_cancel hk]
  have hdiff := congrArg D hcross
  simp only [Derivation.leibniz, hDconst a ha, hDconst b hb,
    hDconst c hc, hDconst d hd, hDXpow r hr, hDXpow n hn,
    smul_eq_mul, zero_mul, mul_zero, add_zero, zero_add] at hdiff
  have hweight : (r : F) = (n : F) := by
    apply mul_right_cancel₀ (mul_ne_zero (mul_ne_zero hc0 hb0) (pow_ne_zero _ hX))
    calc
      (r : F) * (c * b * X ^ r) = c * b * ((r : F) * X ^ r) := by ring
      _ = a * d * ((n : F) * X ^ n) := hdiff.symm
      _ = (n : F) * (c * b * X ^ r) := by rw [← hcross]; ring
  exact CharP.natCast_injOn_Iio F p hrp hnp hweight

-- @node: intersection_integrate_euler
/-- Suppose [F has characteristic p](hyp:hF), [D sends X to X](hyp:hDX),
[X is nonzero](hyp:hX), [U is nonzero](hyp:hU),
[U belongs to the field generated by X over the power subfield](hyp:hUm), and
[every element of that field killed by D belongs to the power subfield](hyp:hkernel).
If [c belongs to the power subfield](hyp:hc), [m is below p](hyp:hmp), and
[one plus c times X to the m-th power, multiplied by the derivative of U, equals U](hyp:hlog),
then [U to the power p minus m is an affine function of X to the same power,
with coefficients in the power subfield](goal). -/
lemma intersection_integrate_euler (hF : CharP F p)
    (D : Derivation ↥(powSubfield p F) F F) {X U : F}
    (hDX : D X = X) (hX : X ≠ 0) (hU : U ≠ 0)
    (hUm : U ∈ IntermediateField.adjoin ↥(powSubfield p F) {X})
    (hkernel : ∀ z ∈ IntermediateField.adjoin ↥(powSubfield p F) {X},
      D z = 0 → z ∈ powSubfield p F)
    {c : F} (hc : c ∈ powSubfield p F) {m : ℕ} (hmp : m < p)
    (hlog : (1 + c * X ^ m) * D U = U) :
    AffPow (powSubfield p F) X U (p - m) := by
  let : CharP F p := hF
  let n := p - m
  have hn : 1 ≤ n := by dsimp [n]; omega
  have hnm : n + m = p := Nat.sub_add_cancel hmp.le
  let H := X ^ n + c * X ^ p
  have hH : H = X ^ n * (1 + c * X ^ m) := by
    dsimp [H]
    rw [mul_add, mul_one]
    congr 1
    rw [← mul_assoc, mul_comm (X ^ n) c, mul_assoc, ← pow_add, hnm]
  have hB0 : 1 + c * X ^ m ≠ 0 := by
    intro hz
    rw [hz, zero_mul] at hlog
    exact hU hlog.symm
  have hH0 : H ≠ 0 := by rw [hH]; exact mul_ne_zero (pow_ne_zero _ hX) hB0
  have hDc : D c = 0 := D.map_algebraMap (⟨c, hc⟩ : powSubfield p F)
  have hDp : D (X ^ p) = 0 := by
    simp [Derivation.leibniz_pow, nsmul_eq_mul]
  have hDn : D (X ^ n) = (n : F) * X ^ n := by
    simp only [Derivation.leibniz_pow, hDX, smul_eq_mul, nsmul_eq_mul]
    rw [← pow_succ, Nat.sub_add_cancel hn]
  have hDH : D H = (n : F) * X ^ n := by
    simp only [H, map_add, Derivation.leibniz, hDn, hDc, hDp,
      smul_eq_mul, mul_zero, add_zero]
  have hcross : H * D (U ^ n) = U ^ n * D H := by
    rw [Derivation.leibniz_pow, nsmul_eq_mul, smul_eq_mul, hDH, hH]
    calc
      _ = (n : F) * X ^ n * U ^ (n - 1) * ((1 + c * X ^ m) * D U) := by ring
      _ = (n : F) * X ^ n * U ^ n := by
        rw [hlog, mul_assoc, ← pow_succ, Nat.sub_add_cancel hn]
      _ = _ := by ring
  have hDquot : D (U ^ n / H) = 0 := by
    rw [Derivation.leibniz_div]
    simp only [smul_eq_mul]
    rw [hcross, sub_self, mul_zero]
  let M := IntermediateField.adjoin ↥(powSubfield p F) {X}
  have hXm : X ∈ M := IntermediateField.subset_adjoin _ _ (Set.mem_singleton X)
  have hcm : c ∈ M := M.algebraMap_mem (⟨c, hc⟩ : powSubfield p F)
  have hHm : H ∈ M := M.add_mem (M.toSubfield.pow_mem hXm n) (M.mul_mem hcm (M.toSubfield.pow_mem hXm p))
  have hq : U ^ n / H ∈ powSubfield p F :=
    hkernel _ (M.div_mem (M.toSubfield.pow_mem hUm n) hHm) hDquot
  refine ⟨(U ^ n / H) * c * X ^ p,
    (powSubfield p F).mul_mem ((powSubfield p F).mul_mem hq hc)
      (Subfield.subset_closure ⟨X, rfl⟩), U ^ n / H, hq, ?_⟩
  calc
    U ^ n = (U ^ n / H) * H := (div_mul_cancel₀ _ hH0).symm
    _ = _ := by dsimp [H]; ring

-- @node: intersection_derivation_zero_on_adjoin
/-- If [D kills x](hyp:hx) and [z belongs to the field generated by x over
the power subfield](hyp:hz), then [D kills z](goal). -/
lemma intersection_derivation_zero_on_adjoin
    (D : Derivation ↥(powSubfield p F) F F) {x z : F} (hx : D x = 0)
    (hz : z ∈ IntermediateField.adjoin ↥(powSubfield p F) {x}) : D z = 0 := by
  induction hz using IntermediateField.adjoin_induction with
  | mem y hy => simpa only [Set.mem_singleton_iff.mp hy] using hx
  | algebraMap c => exact D.map_algebraMap c
  | add a b _ _ ha hb => simp only [map_add, ha, hb, add_zero]
  | inv a _ ha => simp only [Derivation.leibniz_inv, ha, smul_zero]
  | mul a b _ _ ha hb => simp only [Derivation.leibniz, ha, hb, smul_zero, add_zero]

-- @node: intersection_witness_eigen
/-- If [X is nonzero](hyp:hX), [D sends X to X](hyp:hDX),
[D sends Y to Y](hyp:hDY), [E sends U to U](hyp:hEU), [E sends V to V](hyp:hEV), and
[there are nonzero a in the field generated by Y/X and b in the field generated
by V/U over the power subfield with X times a equal to U times b](hyp:hw), then
[there is a nonzero Z that both D and E send to Z](goal). -/
lemma intersection_witness_eigen (D E : Derivation ↥(powSubfield p F) F F)
    {X Y U V : F} (hX : X ≠ 0)
    (hDX : D X = X) (hDY : D Y = Y) (hEU : E U = U) (hEV : E V = V)
    (hw : IntersectionWitness p X Y U V) :
    ∃ Z : F, Z ≠ 0 ∧ D Z = Z ∧ E Z = Z := by
  obtain ⟨a, b, ha, ha0, hb, hb0, hab⟩ := hw
  have hDratio : D (Y / X) = 0 := by
    rw [Derivation.leibniz_div, hDX, hDY]
    simp only [smul_eq_mul, mul_comm X Y, sub_self, mul_zero]
  have hEratio : E (V / U) = 0 := by
    rw [Derivation.leibniz_div, hEU, hEV]
    simp only [smul_eq_mul, mul_comm U V, sub_self, mul_zero]
  have hDa := intersection_derivation_zero_on_adjoin p D hDratio ha
  have hEb := intersection_derivation_zero_on_adjoin p E hEratio hb
  refine ⟨X * a, mul_ne_zero hX ha0, ?_, ?_⟩
  · simp only [Derivation.leibniz, hDX, hDa, smul_eq_mul, mul_zero, zero_add]
    ring
  · rw [hab]
    simp only [Derivation.leibniz, hEU, hEb, smul_eq_mul, mul_zero, zero_add]
    ring

-- @node: intersection_witness_q_relations
/-- If [Z is nonzero](hyp:hZ), [the sum of the derivations DX and DY sends Z to Z](hyp:hdelta),
and [their weighted sum, with weights U divided by DX applied to U and V divided
by DY applied to V, also sends Z to Z](hyp:hdelta'), then
[the logarithmic derivatives of Z sum to one, and their weighted sum with
each of those weights reduced by one is zero](goal). -/
lemma intersection_witness_q_relations
    (DX DY : Derivation ↥(powSubfield p F) F F) {U V Z : F}
    (hZ : Z ≠ 0)
    (hdelta : (DX + DY) Z = Z)
    (hdelta' : ((U / DX U) • DX + (V / DY V) • DY) Z = Z) :
    DX Z / Z + DY Z / Z = 1 ∧
      (U / DX U - 1) * (DX Z / Z) + (V / DY V - 1) * (DY Z / Z) = 0 := by
  simp only [Derivation.add_apply, Derivation.smul_apply, smul_eq_mul] at hdelta hdelta'
  constructor
  · rw [← add_div, hdelta, div_self hZ]
  · have hsub : (U / DX U - 1) * DX Z + (V / DY V - 1) * DY Z = 0 := by
      linear_combination hdelta' - hdelta
    calc
      _ = ((U / DX U - 1) * DX Z + (V / DY V - 1) * DY Z) / Z := by ring
      _ = 0 := by rw [hsub, zero_div]

-- @node: intersection_logarithmic_invariant
/-- If [D sends Z to Z](hyp:hDZ) and [applying D after E to Z gives the same
result as applying E after D](hyp:hcomm), then [D kills the quotient of E applied
to Z by Z](goal). -/
lemma intersection_logarithmic_invariant
    (D E : Derivation ↥(powSubfield p F) F F) {Z : F}
    (hDZ : D Z = Z) (hcomm : D (E Z) = E (D Z)) : D (E Z / Z) = 0 := by
  rw [Derivation.leibniz_div, hcomm, hDZ]
  simp only [smul_eq_mul, mul_comm Z (E Z), sub_self, mul_zero]

-- @node: intersection_euler_ratio_sub_one_ne_zero
/-- Suppose [p is prime](hyp:hp), [F has characteristic p](hyp:hF),
[X is nonzero](hyp:hX), [U is nonzero](hyp:hU), [D sends X to X](hyp:hDX),
[the derivative of U is nonzero](hyp:hDU),
[U belongs to the field generated by X over the power subfield](hyp:hUm), and
[every element of that field killed by D lies in the power subfield](hyp:hkernel).
If [the class of U lies outside the modulo-p scalar span of the class of X](hyp:hoff),
then [U divided by its derivative, minus one, is nonzero](goal). -/
lemma intersection_euler_ratio_sub_one_ne_zero (hp : PrimeChar p) (hF : CharP F p)
    (D : Derivation ↥(powSubfield p F) F F) {X U : F}
    (hX : X ≠ 0) (hU : U ≠ 0) (hDX : D X = X) (hDU : D U ≠ 0)
    (hUm : U ∈ IntermediateField.adjoin ↥(powSubfield p F) {X})
    (hkernel : ∀ z ∈ IntermediateField.adjoin ↥(powSubfield p F) {X},
      D z = 0 → z ∈ powSubfield p F)
    (hoff : ¬ FpMultiplesPin p X (cls p U)) : U / D U - 1 ≠ 0 := by
  intro hz
  have hDUeq : D U = U := ((div_eq_one_iff_eq hDU).mp (sub_eq_zero.mp hz)).symm
  have hDquot : D (U / X) = 0 := by
    rw [Derivation.leibniz_div, hDUeq, hDX]
    simp only [smul_eq_mul, mul_comm X U, sub_self, mul_zero]
  let M := IntermediateField.adjoin ↥(powSubfield p F) {X}
  have hXm : X ∈ M := IntermediateField.subset_adjoin _ _ (Set.mem_singleton X)
  have hc := hkernel (U / X) (M.div_mem hUm hXm) hDquot
  have hprod : U = (U / X) * X := (div_mul_cancel₀ U hX).symm
  apply hoff
  unfold FpMultiplesPin
  rw [hprod, cls_mul p (U / X) X (div_ne_zero hU hX) hX,
    cls_eq_zero_of_mem_powSubfield p hp hF hc (div_ne_zero hU hX), zero_add]
  exact Submodule.subset_span (Set.mem_singleton _)

-- @node: intersection_q_ne_zero
/-- If [AX is nonzero](hyp:hAX), [AY is nonzero](hyp:hAY),
[qX and qY sum to one](hyp:hsum), and [AX times qX plus AY times qY is zero](hyp:hweighted),
then [both qX and qY are nonzero](goal). -/
lemma intersection_q_ne_zero {AX AY qX qY : F} (hAX : AX ≠ 0) (hAY : AY ≠ 0)
    (hsum : qX + qY = 1) (hweighted : AX * qX + AY * qY = 0) :
    qX ≠ 0 ∧ qY ≠ 0 := by
  constructor
  · intro hz
    have hy : qY = 1 := by simpa only [hz, zero_add] using hsum
    exact hAY (by simpa only [hz, hy, mul_zero, mul_one, zero_add] using hweighted)
  · intro hz
    have hx : qX = 1 := by simpa only [hz, add_zero] using hsum
    exact hAX (by simpa only [hz, hx, mul_zero, mul_one, add_zero] using hweighted)

-- @node: intersection_common_logarithmic_weight
/-- Suppose [AX is nonzero](hyp:hAX), [AY is nonzero](hyp:hAY),
[qX and qY sum to one](hyp:hsum), [AX times qX plus AY times qY is zero](hyp:hweighted),
[the sum of DX and DY kills qX](hyp:hqX), [that sum also kills qY](hyp:hqY),
[DY kills AX](hyp:hDYAX), and [DX kills AY](hyp:hDXAY). Then
[the derivative of AX under DX divided by AX equals the derivative of AY under DY divided by AY](goal). -/
lemma intersection_common_logarithmic_weight
    (DX DY : Derivation ↥(powSubfield p F) F F) {AX AY qX qY : F}
    (hAX : AX ≠ 0) (hAY : AY ≠ 0)
    (hsum : qX + qY = 1) (hweighted : AX * qX + AY * qY = 0)
    (hqX : (DX + DY) qX = 0) (hqY : (DX + DY) qY = 0)
    (hDYAX : DY AX = 0) (hDXAY : DX AY = 0) :
    DX AX / AX = DY AY / AY := by
  have hqx := (intersection_q_ne_zero hAX hAY hsum hweighted).1
  have hratio : AX / AY = -qY / qX := by
    apply (div_eq_div_iff hAY hqx).2
    linear_combination hweighted
  have hzero : (DX + DY) (AX / AY) = 0 := by
    rw [hratio, Derivation.leibniz_div, map_neg, hqX, hqY]
    simp
  have hnum : AY * DX AX - AX * DY AY = 0 := by
    simp only [Derivation.leibniz_div, Derivation.add_apply, hDYAX, hDXAY,
      add_zero, zero_add, smul_eq_mul] at hzero
    exact (mul_eq_zero.mp hzero).resolve_left (pow_ne_zero 2 (inv_ne_zero hAY))
  apply (div_eq_div_iff hAX hAY).2
  linear_combination hnum

-- @node: intersection_pair_euler_kernel
/-- If [p is prime](hyp:hp), [F has characteristic p](hyp:hF),
[F has finite degree over its power subfield](hyp:hfinite), and
[X and Y are nonzero and p-independent](hyp:hpair), then
[there are two commuting derivations over the power subfield, the first sending
X to X and killing Y, the second sending Y to Y and killing X, such that each
derivation kills only elements of the power subfield within the simple field
generated by its own coordinate](goal). -/
lemma intersection_pair_euler_kernel (hp : PrimeChar p) (hF : IntersectionFieldChar p F)
    (hfinite : IntersectionFiniteDegree p F) {X Y : F}
    (hpair : IntersectionPairInputs p X Y) :
    ∃ DX DY : Derivation ↥(powSubfield p F) F F,
      DX X = X ∧ DY Y = Y ∧
      (∀ z ∈ IntermediateField.adjoin ↥(powSubfield p F) {X},
        DX z = 0 → z ∈ powSubfield p F) ∧
      (∀ z ∈ IntermediateField.adjoin ↥(powSubfield p F) {Y},
        DY z = 0 → z ∈ powSubfield p F) ∧
      DX Y = 0 ∧ DY X = 0 ∧ (∀ z, DX (DY z) = DY (DX z)) := by
  classical
  obtain ⟨e, he, b, hb, hinit⟩ :=
    pIndependent_extends_to_pBasis p hp hF hfinite ![X, Y] hpair.2.2
  obtain ⟨_, hstructure⟩ := pBasis_structure p hp hF
  obtain ⟨_, hfull⟩ := hstructure hfinite
  obtain ⟨_, _, _, hD, _⟩ := hfull e b hb
  obtain ⟨D, hcomm, hEuler, hkernel, _, _⟩ := hD
  let jX : Fin e := Fin.castLE he (0 : Fin 2)
  let jY : Fin e := Fin.castLE he (1 : Fin 2)
  have hbX : b jX = X := by simpa [jX] using hinit 0
  have hbY : b jY = Y := by simpa [jY] using hinit 1
  refine ⟨D jX, D jY, ?_, ?_, ?_, ?_, ?_, ?_, hcomm jX jY⟩
  · have h := pBasis_euler_axis p hp b D hEuler jX 1 1 hp.one_lt
    simpa only [OneMemClass.coe_one, pow_one, one_mul, Nat.cast_one, one_smul, hbX] using h
  · have h := pBasis_euler_axis p hp b D hEuler jY 1 1 hp.one_lt
    simpa only [OneMemClass.coe_one, pow_one, one_mul, Nat.cast_one, one_smul, hbY] using h
  · intro z hz hzero
    have hzbase := (hkernel jX z (hbX ▸ hz)).mp hzero
    obtain ⟨c, hc⟩ := IntermediateField.mem_bot.mp hzbase
    exact hc ▸ c.property
  · intro z hz hzero
    have hzbase := (hkernel jY z (hbY ▸ hz)).mp hzero
    obtain ⟨c, hc⟩ := IntermediateField.mem_bot.mp hzbase
    exact hc ▸ c.property

  · let : NeZero p := ⟨hp.ne_zero⟩
    let i : Fin e → Fin p := Function.update 0 jY ⟨1, hp.one_lt⟩
    have hne : jX ≠ jY := by intro h; have := congrArg Fin.val h; simp [jX, jY] at this
    have haxis : pMonomial p b i = b jY := by
      simpa [i] using pMonomial_axis p b jY i (by intro k hk; simp [i, hk])
    have h := hEuler jX i
    simpa [haxis, i, hne, hbY] using h
  · let : NeZero p := ⟨hp.ne_zero⟩
    let i : Fin e → Fin p := Function.update 0 jX ⟨1, hp.one_lt⟩
    have hne : jY ≠ jX := by intro h; have := congrArg Fin.val h; simp [jX, jY] at this
    have haxis : pMonomial p b i = b jX := by
      simpa [i] using pMonomial_axis p b jX i (by intro k hk; simp [i, hk])
    have h := hEuler jY i
    simpa [haxis, i, hne, hbX] using h

-- @node: intersection_pair_euler
/-- If [p is prime](hyp:hp), [F has characteristic p](hyp:hF),
[F has finite degree over its power subfield](hyp:hfinite), and
[X and Y are nonzero and p-independent](hyp:hpair), then
[there are derivations DX and DY over the power subfield that send X to X and
Y to Y, respectively](goal). -/
lemma intersection_pair_euler (hp : PrimeChar p) (hF : IntersectionFieldChar p F)
    (hfinite : IntersectionFiniteDegree p F) {X Y : F}
    (hpair : IntersectionPairInputs p X Y) :
    ∃ DX DY : Derivation ↥(powSubfield p F) F F, DX X = X ∧ DY Y = Y := by
  obtain ⟨e, he, b, hb, hinit⟩ :=
    pIndependent_extends_to_pBasis p hp hF hfinite ![X, Y] hpair.2.2
  obtain ⟨D, _, hEuler⟩ := pBasis_euler_operators p hp hF b hb
  let jX : Fin e := Fin.castLE he (0 : Fin 2)
  let jY : Fin e := Fin.castLE he (1 : Fin 2)
  have hbX : b jX = X := by simpa [jX] using hinit 0
  have hbY : b jY = Y := by simpa [jY] using hinit 1
  refine ⟨D jX, D jY, ?_, ?_⟩
  · have h := pBasis_euler_axis p hp b D hEuler jX 1 1 hp.one_lt
    simpa only [OneMemClass.coe_one, pow_one, one_mul, Nat.cast_one, one_smul, hbX] using h
  · have h := pBasis_euler_axis p hp b D hEuler jY 1 1 hp.one_lt
    simpa only [OneMemClass.coe_one, pow_one, one_mul, Nat.cast_one, one_smul, hbY] using h

end Papers.OaiReconstructionMilnorTheory