Divisor_pushforwardAlong_liesOver_of_liesOver.lean

theorem mem_restrictAlong_iff (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (w : Place K F') (f : F) :
    f ∈ (w.restrictAlong φ hφ).toValuationSubring ↔ φ f ∈ w.toValuationSubring

theorem inertiaDegAlong_eq_one [IsAlgClosed K] [IsCurveOver K F] [IsCurveOver K F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w : Place K F') :
    w.inertiaDegAlong φ hφ = 1

theorem pushforwardAlong_apply [IsAlgClosed K] [IsCurveOver K F] [IsCurveOver K F'] [DecidableEq
  (Place K F)]
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (D : Divisor K F') (v : Place K F) :
    Divisor.pushforwardAlong φ hφ D v = ∑ w ∈ D.support, if w.restrictAlong φ hφ = v then D w else
      0 := by
  have h1 : ∀ w : Place K F', (w.inertiaDegAlong φ hφ : ℤ) = 1 := fun w => by
    rw [inertiaDegAlong_eq_one φ hφ w, Nat.cast_one]
  let := algebraAlong φ
  have := isScalarTower_along φ
  have := isIntegral_along φ hφ
  change Divisor.pushforward F D v = _
  rw [Divisor.pushforward_apply]
  refine Finset.sum_congr rfl fun w _ => ?_
  have h1w : (w.inertiaDeg F : ℤ) = 1 := h1 w
  by_cases hw : w.restrict F = v
  · rw [ite_eq_left hw, ite_eq_left (show w.restrictAlong φ hφ = v from hw), h1w, mul_one]
  · rw [ite_eq_right hw, ite_eq_right (show ¬ w.restrictAlong φ hφ = v from hw)]

theorem _root_.AlgebraicCurve.Divisor.pushforwardAlong_liesOver_of_liesOver
    (K F F' E FE F'E : Type*) [Field K] [Field F] [Field F'] [Field E] [Field FE] [Field F'E]
    [Algebra K F] [Algebra K F'] [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE]
      [IsScalarTower K E FE] [IsScalarTower K F FE]
    [Algebra E F'E] [Algebra F' F'E] [Algebra K F'E] [IsScalarTower K E F'E] [IsScalarTower K F'
      F'E]
    [IsAlgClosed K] [CharZero K] [IsAlgClosed E]
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional ↥(IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfg' : ∃ x : F', Transcendental K x ∧ FiniteDimensional ↥(IntermediateField.adjoin K ({x} :
      Set F')) F')
    (hfgE : ∃ x : FE, Transcendental E x ∧ FiniteDimensional ↥(IntermediateField.adjoin E ({x} :
      Set FE)) FE)
    (hfgE' : ∃ x : F'E, Transcendental E x ∧ FiniteDimensional ↥(IntermediateField.adjoin E ({x} :
      Set F'E)) F'E)
    [AlgebraicCurve.IsCurveOver K F] [AlgebraicCurve.IsCurveOver K F'] [AlgebraicCurve.IsCurveOver
      E FE] [AlgebraicCurve.IsCurveOver E F'E]
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (hgen' : IntermediateField.adjoin E (Set.range (algebraMap F' F'E)) = ⊤)
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (φE : FE →ₐ[E] F'E) (hφE :
      φE.toRingHom.IsIntegral)
    (hcomm : ∀ f : F, φE (algebraMap F FE f) = algebraMap F' F'E (φ f))
    (D : AlgebraicCurve.Divisor K F') (DE : AlgebraicCurve.Divisor E F'E)
    (hover : ∀ (w' : AlgebraicCurve.Place E F'E) (w : AlgebraicCurve.Place K F'),
      w'.toValuationSubring.comap (algebraMap F' F'E) = w.toValuationSubring → DE w' = D w)
    (hoff : ∀ w' : AlgebraicCurve.Place E F'E,
      (∀ w : AlgebraicCurve.Place K F', w'.toValuationSubring.comap (algebraMap F' F'E) ≠
        w.toValuationSubring) → DE w' = 0) :
    (∀ (v' : AlgebraicCurve.Place E FE) (v : AlgebraicCurve.Place K F),
        v'.toValuationSubring.comap (algebraMap F FE) = v.toValuationSubring →
        AlgebraicCurve.Divisor.pushforwardAlong φE hφE DE v' =
          AlgebraicCurve.Divisor.pushforwardAlong φ hφ D v) ∧
    (∀ v' : AlgebraicCurve.Place E FE,
        (∀ v : AlgebraicCurve.Place K F, v'.toValuationSubring.comap (algebraMap F FE) ≠
          v.toValuationSubring) →
        AlgebraicCurve.Divisor.pushforwardAlong φE hφE DE v' = 0)