module

public import Papers.OaiReconstructionMilnorTheory.Helpers.IntersectionSetup
public import Mathlib.Data.Fin.VecNotation

/-! # Simple-field stability and the spectral consequences of an independent pair -/

public section

namespace Papers.OaiReconstructionMilnorTheory

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

-- @node: intersection_euler_mem_adjoin
/-- If [D sends X to X](hyp:hDX) and [z belongs to the field generated by X
over the power subfield](hyp:hz), then [the derivative of z also belongs to
that field](goal). -/
lemma intersection_euler_mem_adjoin
    (D : Derivation ↥(powSubfield p F) F F) {X z : F} (hDX : D X = X)
    (hz : z ∈ IntermediateField.adjoin ↥(powSubfield p F) {X}) :
    D z ∈ IntermediateField.adjoin ↥(powSubfield p F) {X} := by
  let M := IntermediateField.adjoin ↥(powSubfield p F) {X}
  induction hz using IntermediateField.adjoin_induction with
  | mem y hy =>
    rw [Set.mem_singleton_iff.mp hy, hDX]
    exact IntermediateField.subset_adjoin _ _ (Set.mem_singleton X)
  | algebraMap c => rw [D.map_algebraMap]; exact M.zero_mem
  | add a b _ _ ha hb => rw [map_add]; exact M.add_mem ha hb
  | inv a ha ih =>
    rw [Derivation.leibniz_inv, smul_eq_mul]
    exact M.mul_mem (M.neg_mem (M.toSubfield.pow_mem (M.inv_mem ha) 2)) ih
  | mul a b ha hb iha ihb =>
    rw [Derivation.leibniz, smul_eq_mul, smul_eq_mul]
    exact M.add_mem (M.mul_mem ha ihb) (M.mul_mem hb iha)

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

-- @node: intersection_independent_simple_inf
/-- If [p is prime](hyp:hp), [F has characteristic p](hyp:hF),
[F has finite dimension over its power subfield](hyp:hfinite), and
[X and Y are p-independent](hyp:hpair), then [the fields generated separately
by X and Y over the power subfield intersect in exactly the power subfield](goal). -/
lemma intersection_independent_simple_inf (hp : PrimeChar p) (hF : CharP F p)
    (hfinite : FiniteDimensional ↥(powSubfield p F) F) {X Y : F}
    (hpair : IsPIndependent p F ![X, Y]) :
    IntermediateField.adjoin ↥(powSubfield p F) {X} ⊓
      IntermediateField.adjoin ↥(powSubfield p F) {Y} = ⊥ := by
  obtain ⟨e, he, b, hb, hinit⟩ := pIndependent_extends_to_pBasis p hp hF hfinite ![X, Y] hpair
  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
  have hne : jX ≠ jY := by
    intro h
    have := congrArg Fin.val h
    simp [jX, jY] at this
  simpa only [hbX, hbY] using pBasis_simple_inf p hp b hb jX jY hne

-- @node: intersection_simple_spectral
/-- Suppose [p is prime](hyp:hp), [F has characteristic p](hyp:hF),
[F has finite dimension over its power subfield](hyp:hfinite),
[X and Y are p-independent](hyp:hpair), and [D sends X to X](hyp:hDX).
If [z belongs to the field generated by X over the power subfield](hyp:hz),
[z is nonzero](hyp:hz0), and [D sends z to a times z](hyp:ha), then
[z is a nonzero power-subfield multiple of X to some natural-number power n
below p, and a equals n viewed as an element of the power subfield](goal). -/
lemma intersection_simple_spectral (hp : PrimeChar p) (hF : CharP F p)
    (hfinite : FiniteDimensional ↥(powSubfield p F) F) {X Y : F}
    (hpair : IsPIndependent p F ![X, Y])
    (D : Derivation ↥(powSubfield p F) F F) (hDX : D X = X)
    {z : F} (hz : z ∈ IntermediateField.adjoin ↥(powSubfield p F) {X}) (hz0 : z ≠ 0)
    (a : powSubfield p F) (ha : D z = a • z) :
    ∃ c : powSubfield p F, c ≠ 0 ∧ ∃ n : ℕ, n < p ∧
      z = (c : F) * X ^ n ∧ a = (n : powSubfield p F) := by
  obtain ⟨e, he, b, hb, hinit⟩ := pIndependent_extends_to_pBasis p hp hF hfinite ![X, Y] hpair
  obtain ⟨E, _, hEuler⟩ := pBasis_euler_operators p hp hF b hb
  let jX : Fin e := Fin.castLE he (0 : Fin 2)
  have hbX : b jX = X := by simpa [jX] using hinit 0
  have hEX : E jX X = X := by
    have h := pBasis_euler_axis p hp b E 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 heq : E jX z = D z :=
    intersection_derivation_eq_on_adjoin p (E jX) D (hEX.trans hDX.symm) hz
  simpa only [hbX] using
    pBasis_euler_simple_spectral p hp hF b hb E hEuler jX z (hbX ▸ hz) hz0 a (heq.trans ha)

-- @node: intersection_off_pin_not_eigen
/-- Suppose [p is prime](hyp:hp), [F has characteristic p](hyp:hF),
[F has finite dimension over its power subfield](hyp:hfinite),
[X and Y are p-independent](hyp:hpair), [X is nonzero](hyp:hX),
[U is nonzero](hyp:hU), [D sends X to X](hyp:hDX), and
[U belongs to the field generated by X over the power subfield](hyp:hUm).
If [the class of U lies outside the modulo-p scalar span of the class of X](hyp:hoff),
then [the derivative of U differs from a times U for every power-subfield scalar a](goal). -/
lemma intersection_off_pin_not_eigen (hp : PrimeChar p) (hF : CharP F p)
    (hfinite : FiniteDimensional ↥(powSubfield p F) F) {X Y U : F}
    (hpair : IsPIndependent p F ![X, Y]) (hX : X ≠ 0) (hU : U ≠ 0)
    (D : Derivation ↥(powSubfield p F) F F) (hDX : D X = X)
    (hUm : U ∈ IntermediateField.adjoin ↥(powSubfield p F) {X})
    (hoff : ¬ FpMultiplesPin p X (cls p U))
    (a : powSubfield p F) : D U ≠ a • U := by
  intro ha
  obtain ⟨c, hc, n, hn, hUn, _⟩ :=
    intersection_simple_spectral p hp hF hfinite hpair D hDX hUm hU a ha
  have hc0 : (c : F) ≠ 0 := by exact_mod_cast hc
  apply hoff
  unfold FpMultiplesPin
  rw [hUn, cls_mul p (c : F) (X ^ n) hc0 (pow_ne_zero _ hX),
    cls_eq_zero_of_mem_powSubfield p hp hF c.property hc0, zero_add]
  have hpow : cls p (X ^ n) = (n : Coeff p) • cls p X := by
    simpa only [zpow_natCast, natCast_zsmul, Nat.cast_smul_eq_nsmul] using
      cls_zpow p X hX (n : ℤ)
  rw [hpow]
  exact Submodule.smul_mem _ _ (Submodule.subset_span (Set.mem_singleton _))

-- @node: intersection_euler_ratio_not_mem
/-- Suppose [p is prime](hyp:hp), [F has characteristic p](hyp:hF),
[F has finite dimension over its power subfield](hyp:hfinite),
[X and Y are p-independent](hyp:hpair), [X is nonzero](hyp:hX),
[U is nonzero](hyp:hU), [D sends X to X](hyp:hDX), and
[U belongs to the field generated by X over the power subfield](hyp:hUm).
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, lies outside the power subfield](goal). -/
lemma intersection_euler_ratio_not_mem (hp : PrimeChar p) (hF : CharP F p)
    (hfinite : FiniteDimensional ↥(powSubfield p F) F) {X Y U : F}
    (hpair : IsPIndependent p F ![X, Y]) (hX : X ≠ 0) (hU : U ≠ 0)
    (D : Derivation ↥(powSubfield p F) F F) (hDX : D X = X)
    (hUm : U ∈ IntermediateField.adjoin ↥(powSubfield p F) {X})
    (hoff : ¬ FpMultiplesPin p X (cls p U)) : U / D U - 1 ∉ powSubfield p F := by
  intro hA
  have hB : U / D U ∈ powSubfield p F := by
    simpa only [sub_add_cancel] using (powSubfield p F).add_mem hA (powSubfield p F).one_mem
  have ha : D U / U ∈ powSubfield p F := by
    simpa only [inv_div] using (powSubfield p F).inv_mem hB
  apply intersection_off_pin_not_eigen p hp hF hfinite hpair hX hU D hDX hUm hoff ⟨_, ha⟩
  change D U = (D U / U) * U
  exact (div_mul_cancel₀ _ hU).symm

end Papers.OaiReconstructionMilnorTheory