DivisorialWeilPairingData_pair_pullbackAlong_eq_pair_pushforwardAlongHom_of_isPurelyInseparable.lean

theorem hratF [IsAlgClosed K] [IsCurveOver K F] (v : Place K F) : v.IsRational

def normAlong (u : F →ₐ[K] F') (g : F') : F

theorem ord_map_eq [HasPrincipalDivisors K F'] (u : F →ₐ[K] F')
    (hu : u.toRingHom.IsIntegral) {n : ℕ} {a : F} {A : Divisor K F}
    (ha : ∀ v : Place K F, v.ord a = n * A v) (w : Place K F') :
    w.ord (u a) = n * (Divisor.pullbackAlong u hu A) w

theorem map_ne_zero' (u : F →ₐ[K] F') {a : F} (ha : a ≠ 0) : u a ≠ 0

theorem ord_norm_eq [HasPrincipalDivisors K F'] (u : F →ₐ[K] F')
    (hu : u.toRingHom.IsIntegral) (hfin : FiniteAlong K u)
    (hN : NormFormulaAlong K u hfin) {n : ℕ} {g : F'} (hg : g ≠ 0) {D' : Divisor K F'}
    (hD' : ∀ w : Place K F', w.ord g = n * D' w) (v : Place K F) :
    v.ord (normAlong u g) = n * (Divisor.pushforwardAlong u hu D') v

theorem normAlong_ne_zero (u : F →ₐ[K] F') (hfin : FiniteAlong K u)
    {g : F'} (hg : g ≠ 0) : normAlong u g ≠ 0

theorem pullbackAlong_eq_zero [HasPrincipalDivisors K F'] {u : F →ₐ[K] F'}
    {hu : u.toRingHom.IsIntegral} {A : Divisor K F} {w : Place K F'}
    (hA : A (w.restrictAlong u hu) = 0) :
    Divisor.pullbackAlong u hu A w = 0

theorem pushforwardAlong_apply_eq_zero {u : F →ₐ[K] F'} {hu : u.toRingHom.IsIntegral}
    {B : Divisor K F'} {v : Place K F}
    (h : ∀ w : Place K F', w.restrictAlong u hu = v → B w = 0) :
    Divisor.pushforwardAlong u hu B v = 0

theorem mk_pullbackAlong_eq [HasPrincipalDivisors K F] [HasPrincipalDivisors K F'] (u : F →ₐ[K] F')
    (hu : u.toRingHom.IsIntegral)
    (hFI : FundamentalIdentityAlong K u hu) (D E : Divisor.degZero (K := K) (F := F))
    (h : Pic0.mk D = Pic0.mk E) :
    Pic0.mk (⟨Divisor.pullbackAlong u hu (D : Divisor K F),
        Divisor.pullbackAlong_mem_degZero u hu hFI D.2⟩ :
        Divisor.degZero (K := K) (F := F')) =
      Pic0.mk ⟨Divisor.pullbackAlong u hu (E : Divisor K F),
        Divisor.pullbackAlong_mem_degZero u hu hFI E.2⟩

theorem pair_pullbackAlong_eq_pair_pushforwardAlongHom_of_isPurelyInseparable
    {K F : Type*} [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [IsCurveOver K F]
    {F' : Type*} [Field F'] [Algebra K F'] [IsCurveOver K F']
    (u : F →ₐ[K] F') (hu : u.toRingHom.IsIntegral)
    (hFI : FundamentalIdentityAlong K u hu) (hfin : FiniteAlong K u)
    (hN : NormFormulaAlong K u hfin)
    (hpi : let : Algebra F F' := algebraAlong u; IsPurelyInseparable F F')
    {n : ℕ} [NeZero n] (e' : DivisorialWeilPairingData K F' n) (e : DivisorialWeilPairingData K F n)
    (x : Pic0 K F) (hx : (n : ℤ) • x = 0)
    (y : Pic0 K F') (hy : (n : ℤ) • y = 0)
    (D₀ : Divisor.degZero (K := K) (F := F)) (hD₀ : Pic0.mk D₀ = x)
    (x' : Pic0 K F') (hx'def : x' = Pic0.mk ⟨Divisor.pullbackAlong u hu (D₀ : Divisor K F),
        Divisor.pullbackAlong_mem_degZero u hu hFI D₀.2⟩) (hx' : (n : ℤ) • x' = 0)
    (hy₀ : (n : ℤ) • Pic0.pushforwardAlongHom u hu hfin hN y = 0) :
    e'.pair ⟨x', Pic0.mem_torsion.mpr hx'⟩ ⟨y, Pic0.mem_torsion.mpr hy⟩
      = e.pair ⟨x, Pic0.mem_torsion.mpr hx⟩
        ⟨Pic0.pushforwardAlongHom u hu hfin hN y, Pic0.mem_torsion.mpr hy₀⟩ := by
  classical
  have : HasPrincipalDivisors K F := IsCurveOver.hasPrincipalDivisors
  have : HasPrincipalDivisors K F' := IsCurveOver.hasPrincipalDivisors
  obtain ⟨DB, hDBmk, -, -⟩ := e'.move ⟨y, Pic0.mem_torsion.mpr hy⟩ ∅
  obtain ⟨b, hb0, hbord⟩ :=
    DivisorialWeilPairingData.exists_witness (K := K) ⟨y, Pic0.mem_torsion.mpr hy⟩ DB hDBmk
  obtain ⟨DA, hDAmk, -, hDAavoid⟩ := e.move ⟨x, Pic0.mem_torsion.mpr hx⟩
    ((DB : Divisor K F').support.image fun w => w.restrictAlong u hu)
  obtain ⟨a, ha0, haord⟩ :=
    DivisorialWeilPairingData.exists_witness (K := K) ⟨x, Pic0.mem_torsion.mpr hx⟩ DA hDAmk
  have hDAmk' : Pic0.mk DA = x := hDAmk
  have hDBmk' : Pic0.mk DB = y := hDBmk
  have hkey : ∀ w : Place K F', (DB : Divisor K F') w ≠ 0 →
      (DA : Divisor K F) (w.restrictAlong u hu) = 0 := by
    intro w hw
    by_contra hne
    exact hDAavoid _ (Finsupp.mem_support_iff.mpr hne)
      (Finset.mem_image_of_mem _ (Finsupp.mem_support_iff.mpr hw))
  have hord1 : ∀ w : Place K F',
      w.ord (u a) = n * (Divisor.pullbackAlong u hu (DA : Divisor K F)) w :=
    fun w => ord_map_eq u hu haord w
  have hdisj : ∀ w : Place K F',
      Divisor.pullbackAlong u hu (DA : Divisor K F) w = 0 ∨ (DB : Divisor K F') w = 0 := by
    intro w
    by_cases hB : (DB : Divisor K F') w = 0
    · exact Or.inr hB
    · exact Or.inl (pullbackAlong_eq_zero (hkey w hB))
  have hord2₀ : ∀ v : Place K F,
      v.ord (normAlong u b) = n * (Divisor.pushforwardAlong u hu (DB : Divisor K F')) v :=
    fun v => ord_norm_eq u hu hfin hN hb0 hbord v
  have hdisj₀ : ∀ v : Place K F,
      (DA : Divisor K F) v = 0 ∨ Divisor.pushforwardAlong u hu (DB : Divisor K F') v = 0 := by
    intro v
    by_cases hA : (DA : Divisor K F) v = 0
    · exact Or.inl hA
    · refine Or.inr (pushforwardAlong_apply_eq_zero fun w hwv => ?_)
      by_contra hB
      apply hA
      rw [← hwv]
      exact hkey w hB
  set d : WeilDatum K F' n :=
    ⟨Divisor.pullbackAlong u hu (DA : Divisor K F), (DB : Divisor K F'), u a, b,
      map_ne_zero' u ha0, hb0, hord1, hbord, hdisj, fun w _ => hratF w⟩ with hd
  set d₀ : WeilDatum K F n :=
    ⟨(DA : Divisor K F), Divisor.pushforwardAlong u hu (DB : Divisor K F'), a, normAlong u b,
      ha0, normAlong_ne_zero u hfin hb0, haord, hord2₀, hdisj₀, fun v _ => hratF v⟩ with hd₀
  have hclassL : d.classLeft = ⟨x', Pic0.mem_torsion.mpr hx'⟩ := by
    refine Subtype.ext ?_
    change Pic0.mk _ = x'
    rw [hx'def]
    have h := mk_pullbackAlong_eq u hu hFI DA D₀ (hDAmk'.trans hD₀.symm)
    refine Eq.trans (congrArg Pic0.mk (Subtype.ext rfl)) h
  have hclassR : d.classRight = ⟨y, Pic0.mem_torsion.mpr hy⟩ := by
    refine Subtype.ext ?_
    change Pic0.mk _ = y
    rw [← hDBmk']
    exact congrArg Pic0.mk (Subtype.ext rfl)
  have hclassL₀ : d₀.classLeft = ⟨x, Pic0.mem_torsion.mpr hx⟩ := by
    refine Subtype.ext ?_
    change Pic0.mk _ = x
    rw [← hDAmk']
    exact congrArg Pic0.mk (Subtype.ext rfl)
  have hclassR₀ : d₀.classRight =
      ⟨Pic0.pushforwardAlongHom u hu hfin hN y, Pic0.mem_torsion.mpr hy₀⟩ := by
    refine Subtype.ext ?_
    change Pic0.mk _ = Pic0.pushforwardAlongHom u hu hfin hN y
    rw [← hDBmk', Pic0.pushforwardAlongHom_mk]
    exact congrArg Pic0.mk (Subtype.ext rfl)
  have h1 := e'.compatible d
  rw [hclassL, hclassR] at h1
  have h2 := e.compatible d₀
  rw [hclassL₀, hclassR₀] at h2
  rw [h1, h2]
  exact pairing_eq_pairing_of_pullbackAlong_of_pushforwardAlong_of_isPurelyInseparable
    u hu hfin hpi hFI hratF hratF d d₀ rfl rfl rfl rfl