DivisionDifference.lean

theorem evalFun_sub (f : F) (E E' : Divisor K F)
    (hE : ∀ v ∈ E.support, v.evalAt f ≠ 0)
    (hE' : ∀ v ∈ E'.support, v.evalAt f ≠ 0) :
    evalFun f (E' - E) = evalFun f E' / evalFun f E

theorem evalFun_div (f g : F) (D : Divisor K F) (hf : f ≠ 0) (hg : g ≠ 0)
    (hrat : ∀ v ∈ D.support, v.IsRational)
    (hfD : ∀ v ∈ D.support, v.ord f = 0)
    (hgD : ∀ v ∈ D.support, v.ord g = 0) :
    evalFun (f / g) D = evalFun f D / evalFun g D

def divisionDifference
    (n : ℕ) (D E E' B : Divisor K F) (f g g' : F)
    (hf : f ≠ 0) (hg : g ≠ 0) (hg' : g' ≠ 0)
    (hfdiv : ∀ v : Place K F, v.ord f = (n : ℤ) * D v)
    (hgdiv : ∀ v : Place K F, v.ord g = (n : ℤ) * E v - B v)
    (hg'div : ∀ v : Place K F, v.ord g' = (n : ℤ) * E' v - B v)
    (hDE : ∀ v : Place K F, D v = 0 ∨ E v = 0)
    (hDE' : ∀ v : Place K F, D v = 0 ∨ E' v = 0)
    (hrat : ∀ v : Place K F, v.IsRational) : WeilDatum K F n where
  D₁ := D
  D₂ := E' - E
  f₁ := f
  f₂ := g' / g
  f₁_ne_zero := hf
  f₂_ne_zero := div_ne_zero hg' hg
  ord_f₁ := hfdiv
  ord_f₂ := fun v => by
    rw [div_eq_mul_inv, v.ord_mul hg' (inv_ne_zero hg), v.ord_inv,
      hg'div v, hgdiv v, Finsupp.sub_apply]
    ring
  disjoint := fun v => by
    by_cases hD : D v = 0
    · exact Or.inl hD
    · exact Or.inr (by rw [Finsupp.sub_apply, (hDE' v).resolve_left hD,
        (hDE v).resolve_left hD, sub_self])
  rational := fun v _ => hrat v

theorem pairing_divisionDifference
    (n : ℕ) (D E E' B : Divisor K F) (f g g' : F)
    (hf : f ≠ 0) (hg : g ≠ 0) (hg' : g' ≠ 0)
    (hfdiv : ∀ v : Place K F, v.ord f = (n : ℤ) * D v)
    (hgdiv : ∀ v : Place K F, v.ord g = (n : ℤ) * E v - B v)
    (hg'div : ∀ v : Place K F, v.ord g' = (n : ℤ) * E' v - B v)
    (hDE : ∀ v : Place K F, D v = 0 ∨ E v = 0)
    (hDE' : ∀ v : Place K F, D v = 0 ∨ E' v = 0)
    (hDB : ∀ v : Place K F, D v = 0 ∨ B v = 0) :
    (divisionDifference n D E E' B f g g' hf hg hg' hfdiv hgdiv hg'div
      hDE hDE' (fun v => v.isRational_of_isAlgClosed)).pairing =
      (Divisor.evalFun f E' / Divisor.evalFun g' D) /
        (Divisor.evalFun f E / Divisor.evalFun g D) := by
  have hfE : ∀ v ∈ E.support, v.evalAt f ≠ 0 := by
    intro v hv
    apply v.evalAt_ne_zero_of_ord_eq_zero (v.isRational_of_isAlgClosed) hf
    rw [hfdiv v, (hDE v).resolve_right (Finsupp.mem_support_iff.mp hv), mul_zero]
  have hfE' : ∀ v ∈ E'.support, v.evalAt f ≠ 0 := by
    intro v hv
    apply v.evalAt_ne_zero_of_ord_eq_zero (v.isRational_of_isAlgClosed) hf
    rw [hfdiv v, (hDE' v).resolve_right (Finsupp.mem_support_iff.mp hv), mul_zero]
  have hgD : ∀ v ∈ D.support, v.ord g = 0 := by
    intro v hv
    rw [hgdiv v, (hDE v).resolve_left (Finsupp.mem_support_iff.mp hv),
      (hDB v).resolve_left (Finsupp.mem_support_iff.mp hv), mul_zero, sub_self]
  have hg'D : ∀ v ∈ D.support, v.ord g' = 0 := by
    intro v hv
    rw [hg'div v, (hDE' v).resolve_left (Finsupp.mem_support_iff.mp hv),
      (hDB v).resolve_left (Finsupp.mem_support_iff.mp hv), mul_zero, sub_self]
  change Divisor.evalFun f (E' - E) / Divisor.evalFun (g' / g) D = _
  rw [Divisor.evalFun_sub f E E' hfE hfE', Divisor.evalFun_div g' g D hg' hg
    (fun v _ => v.isRational_of_isAlgClosed) hg'D hgD]
  exact div_div_div_comm _ _ _ _

theorem exists_semilinearDivisionDifference
    (n : ℕ) (D E B : Divisor K F) (f g : F) (hf : f ≠ 0) (hg : g ≠ 0)
    (hfdiv : ∀ v : Place K F, v.ord f = (n : ℤ) * D v)
    (hgdiv : ∀ v : Place K F, v.ord g = (n : ℤ) * E v - B v)
    (hDE : ∀ v : Place K F, D v = 0 ∨ E v = 0)
    (hDB : ∀ v : Place K F, D v = 0 ∨ B v = 0)
    (σ : SemilinearAut K F) (hσf : σ • f = f)
    (hσD : σ • D = D) (hσB : σ • B = B) :
    ∃ d : WeilDatum K F n,
      d.D₁ = D ∧ d.D₂ = σ • E - E ∧ d.f₁ = f ∧ d.f₂ = (σ • g) / g ∧
      d.pairing = baseAut σ (Divisor.evalFun f E / Divisor.evalFun g D) /
        (Divisor.evalFun f E / Divisor.evalFun g D)