module

public import Papers.OaiReconstructionMilnorTheory.Helpers.IntersectionSetup
public import Papers.OaiReconstructionMilnorTheory.Helpers.IntersectionSpectrum

/-! # Assembly of the unique power correction from the intersection witness -/

public section

namespace Papers.OaiReconstructionMilnorTheory

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

-- @node: prop:intersection
/-- For [elements X, Y, U, and V of F](hyp:X,Y,U,V), suppose [p is prime](hyp:hp),
[F has characteristic p](hyp:hF), [F has finite degree over its subfield C
generated by p-th powers](hyp:hfinite), and [X and Y are nonzero and
p-independent](hyp:hpair). Suppose also that [U and V are nonzero elements of
C(X) and C(Y), respectively, whose Milnor classes lie outside the respective
coefficient spans of the classes of X and Y](hyp:helements), and [there are
nonzero a in C(Y/X) and b in C(V/U) with X times a equal to U times b](hyp:hwitness).
Then [there is an integer n between one and p minus one such that, among
exponents in that range, U to the m-th power lies in the C-span of one and X
to the m-th power exactly when m equals n, and the analogous condition for
V and Y holds exactly when m equals n; moreover, U to the n-th power is an
affine combination of one and X to the n-th power with both coefficients
nonzero in C, and the same holds for V and Y](goal). -/
lemma intersection_unique_power (X Y U V : F)
    (hp : PrimeChar p) (hF : IntersectionFieldChar p F)
    (hfinite : IntersectionFiniteDegree p F) (hpair : IntersectionPairInputs p X Y)
    (helements : IntersectionElements p X Y U V) (hwitness : IntersectionWitness p X Y U V) :
    ∃ n : ℕ, 1 ≤ n ∧ n < p ∧ -- @realizes n(power-correction exponent between 1 and p-1)
      (∀ m, 1 ≤ m → m < p → (AffPow (intersectionPowSubfield p F) X U m ↔ m = n)) ∧
      (∀ m, 1 ≤ m → m < p → (AffPow (intersectionPowSubfield p F) Y V m ↔ m = n)) ∧
      (∃ a ∈ intersectionPowSubfield p F, ∃ b ∈ intersectionPowSubfield p F,
        a ≠ 0 ∧ b ≠ 0 ∧ U ^ n = a + b * X ^ n) ∧
      (∃ a ∈ intersectionPowSubfield p F, ∃ b ∈ intersectionPowSubfield p F,
        a ≠ 0 ∧ b ≠ 0 ∧ V ^ n = a + b * Y ^ n) := by
  obtain ⟨DX, DY, hDX, hDY, hkerX, hkerY, hDXY, hDYX, hcomm⟩ :=
    intersection_pair_euler_kernel p hp hF hfinite hpair
  have hDYU : DY U = 0 :=
    intersection_derivation_zero_on_adjoin p DY hDYX helements.1.1
  have hDXV : DX V = 0 :=
    intersection_derivation_zero_on_adjoin p DX hDXY helements.2.1.1
  have hDU : DX U ≠ 0 := by
    intro hz
    have hc := hkerX U helements.1.1 hz
    apply helements.2.2.1
    unfold FpMultiplesPin
    rw [cls_eq_zero_of_mem_powSubfield p hp hF hc helements.1.2]
    exact Submodule.zero_mem _
  have hDV : DY V ≠ 0 := by
    intro hz
    have hc := hkerY V helements.2.1.1 hz
    apply helements.2.2.2
    unfold FpMultiplesPin
    rw [cls_eq_zero_of_mem_powSubfield p hp hF hc helements.2.1.2]
    exact Submodule.zero_mem _
  have hdeltaX : (DX + DY) X = X := by simp [Derivation.add_apply, hDX, hDYX]
  have hdeltaY : (DX + DY) Y = Y := by simp [Derivation.add_apply, hDY, hDXY]
  have hdeltaU : ((U / DX U) • DX + (V / DY V) • DY) U = U := by
    simp [Derivation.add_apply, Derivation.smul_apply, smul_eq_mul, hDYU, hDU]
  have hdeltaV : ((U / DX U) • DX + (V / DY V) • DY) V = V := by
    simp [Derivation.add_apply, Derivation.smul_apply, smul_eq_mul, hDXV, hDV]
  obtain ⟨Z, hZ, hdelta, hdelta'⟩ := intersection_witness_eigen p
    (DX + DY) ((U / DX U) • DX + (V / DY V) • DY)
    hpair.1 hdeltaX hdeltaY hdeltaU hdeltaV hwitness
  obtain ⟨hqsum, hqweighted⟩ :=
    intersection_witness_q_relations p DX DY hZ hdelta hdelta'
  have hqXzero : (DX + DY) (DX Z / Z) = 0 := by
    apply intersection_logarithmic_invariant p (DX + DY) DX hdelta
    simp only [Derivation.add_apply, map_add]
    rw [hcomm]
  have hqYzero : (DX + DY) (DY Z / Z) = 0 := by
    apply intersection_logarithmic_invariant p (DX + DY) DY hdelta
    simp only [Derivation.add_apply, map_add]
    rw [hcomm]
  have hAX : U / DX U - 1 ≠ 0 :=
    intersection_euler_ratio_sub_one_ne_zero p hp hF DX hpair.1 helements.1.2
      hDX hDU helements.1.1 hkerX helements.2.2.1
  have hAY : V / DY V - 1 ≠ 0 :=
    intersection_euler_ratio_sub_one_ne_zero p hp hF DY hpair.2.1 helements.2.1.2
      hDY hDV helements.2.1.1 hkerY helements.2.2.2
  have hDYAX : DY (U / DX U - 1) = 0 := by
    have hd : DY (DX U) = 0 := by rw [← hcomm, hDYU, map_zero]
    simp [map_sub, Derivation.leibniz_div, hDYU, hd]
  have hDXAY : DX (V / DY V - 1) = 0 := by
    have hd : DX (DY V) = 0 := by rw [hcomm, hDXV, map_zero]
    simp [map_sub, Derivation.leibniz_div, hDXV, hd]
  have hweight : DX (U / DX U - 1) / (U / DX U - 1) =
      DY (V / DY V - 1) / (V / DY V - 1) :=
    intersection_common_logarithmic_weight p DX DY hAX hAY hqsum hqweighted
      hqXzero hqYzero hDYAX hDXAY
  have hmonomials : ∃ m : ℕ, 1 ≤ m ∧ m < p ∧
      ∃ cX ∈ powSubfield p F, ∃ cY ∈ powSubfield p F,
        (1 + cX * X ^ m) * DX U = U ∧
        (1 + cY * Y ^ m) * DY V = V := by
    let MX := IntermediateField.adjoin ↥(powSubfield p F) {X}
    let MY := IntermediateField.adjoin ↥(powSubfield p F) {Y}
    let AX := U / DX U - 1
    let AY := V / DY V - 1
    have hAXm : AX ∈ MX := MX.sub_mem
      (MX.div_mem helements.1.1 (intersection_euler_mem_adjoin p DX hDX helements.1.1)) MX.one_mem
    have hAYm : AY ∈ MY := MY.sub_mem
      (MY.div_mem helements.2.1.1
        (intersection_euler_mem_adjoin p DY hDY helements.2.1.1)) MY.one_mem
    have hwm : DX AX / AX ∈ MX ⊓ MY := by
      constructor
      · exact MX.div_mem (intersection_euler_mem_adjoin p DX hDX hAXm) hAXm
      · rw [hweight]
        exact MY.div_mem (intersection_euler_mem_adjoin p DY hDY hAYm) hAYm
    rw [intersection_independent_simple_inf p hp hF hfinite hpair.2.2] at hwm
    obtain ⟨a, ha⟩ := IntermediateField.mem_bot.mp hwm
    have hwC : DX AX / AX ∈ powSubfield p F := ha ▸ a.property
    let w : powSubfield p F := ⟨DX AX / AX, hwC⟩
    have hspecX : DX AX = w • AX := by
      change DX AX = (DX AX / AX) * AX
      exact (div_mul_cancel₀ _ hAX).symm
    have hspecY : DY AY = w • AY := by
      change DY AY = (DX AX / AX) * AY
      rw [hweight, div_mul_cancel₀ _ hAY]
    have hpairYX : IsPIndependent p F ![Y, X] := by
      constructor
      have hrange : Set.range ![Y, X] = Set.range ![X, Y] := by
        ext z
        simp [or_comm]
      change Module.finrank ↥(powSubfield p F)
        ↥(IntermediateField.adjoin ↥(powSubfield p F) (Set.range ![Y, X])) = p ^ 2
      rw [hrange]
      exact hpair.2.2.degree
    obtain ⟨cX, hcX, m, hmp, hAmX, hwmX⟩ :=
      intersection_simple_spectral p hp hF hfinite hpair.2.2 DX hDX hAXm hAX w hspecX
    obtain ⟨cY, hcY, r, hrp, hAmY, hwmY⟩ :=
      intersection_simple_spectral p hp hF hfinite hpairYX DY hDY hAYm hAY w hspecY
    let : CharP F p := hF
    have hrm : r = m := by
      apply CharP.natCast_injOn_Iio F p hrp hmp
      simpa only [map_natCast] using
        congrArg (powSubfield p F).subtype (hwmY.symm.trans hwmX)
    have hm : 1 ≤ m := by
      by_contra hn
      have hm0 : m = 0 := by omega
      have hconst : AX ∈ powSubfield p F := by simpa [hAmX, hm0] using cX.property
      exact intersection_euler_ratio_not_mem p hp hF hfinite hpair.2.2 hpair.1
        helements.1.2 DX hDX helements.1.1 helements.2.2.1 hconst
    refine ⟨m, hm, hmp, cX, cX.property, cY, cY.property, ?_, ?_⟩
    · have heq : 1 + (cX : F) * X ^ m = U / DX U := by
        rw [← hAmX]
        dsimp [AX]
        ring
      rw [heq, div_mul_cancel₀ _ hDU]
    · have heq : 1 + (cY : F) * Y ^ m = V / DY V := by
        rw [← hrm, ← hAmY]
        dsimp [AY]
        ring
      rw [heq, div_mul_cancel₀ _ hDV]
  have hexists : ∃ n : ℕ, 1 ≤ n ∧ n < p ∧
      AffPow (intersectionPowSubfield p F) X U n ∧
      AffPow (intersectionPowSubfield p F) Y V n := by
    obtain ⟨m, hm, hmp, cX, hcX, cY, hcY, hlogX, hlogY⟩ := hmonomials
    refine ⟨p - m, by omega, by omega, ?_, ?_⟩
    · exact intersection_integrate_euler p hF DX hDX hpair.1 helements.1.2
        helements.1.1 hkerX hcX hmp hlogX
    · exact intersection_integrate_euler p hF DY hDY hpair.2.1 helements.2.1.2
        helements.2.1.1 hkerY hcY hmp hlogY
  obtain ⟨n, hn, hnp, hUn, hVn⟩ := hexists
  refine ⟨n, hn, hnp, ?_, ?_, ?_, ?_⟩
  · intro m hm hmp
    constructor
    · intro hUm
      exact intersection_affPow_unique_of_euler p hp hF DX hDX hpair.1
        helements.1.2 helements.2.2.1 hm hmp hn hnp hUm hUn
    · rintro rfl
      exact hUn
  · intro m hm hmp
    constructor
    · intro hVm
      exact intersection_affPow_unique_of_euler p hp hF DY hDY hpair.2.1
        helements.2.1.2 helements.2.2.2 hm hmp hn hnp hVm hVn
    · rintro rfl
      exact hVn
  · obtain ⟨a, ha, b, hb, hab⟩ := hUn
    obtain ⟨ha0, hb0⟩ := intersection_affPow_coefficients_ne_zero p hp hF hpair.1
      helements.1.2 helements.2.2.1 hn hnp ha hb hab
    exact ⟨a, ha, b, hb, ha0, hb0, hab⟩
  · obtain ⟨a, ha, b, hb, hab⟩ := hVn
    obtain ⟨ha0, hb0⟩ := intersection_affPow_coefficients_ne_zero p hp hF hpair.2.1
      helements.2.1.2 helements.2.2.2 hn hnp ha hb hab
    exact ⟨a, ha, b, hb, ha0, hb0, hab⟩

end Papers.OaiReconstructionMilnorTheory