SerrePairing_pullbackAlong_eq_serrePairing_traceAlong.lean

theorem finsum_eq_finsum_sum_fiberAlong [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) {M : Type*} [AddCommMonoid M] (g : Place K F' → M)
    (hg : (Function.support g).Finite) :
    ∑ᶠ w, g w = ∑ᶠ v, ∑ w ∈ Place.fiberAlong φ hφ v, g w

theorem support_ite_kaehlerResidueTerm_finite (S : Set (Place K F')) (η : Ω[F'⁄K]) (f' : F') :
    (Function.support fun w => if w ∈ S then (0 : K) else kaehlerResidueTerm η (diagonalHom K F'
      f') w).Finite := by
  have hfin : (Function.support (kaehlerResidueTerm η (diagonalHom K F' f'))).Finite := by
    rcases eq_or_ne η 0 with rfl | hη
    · exact Set.Finite.subset Set.finite_empty fun w hw => hw (kaehlerResidueTerm_zero_left _ w)
    · exact kaehlerResidueTerm_support_finite_of_adeleSpace hη (diagonal_mem_adeleSpace f')
  refine hfin.subset fun w hw => ?_
  rw [Function.mem_support] at hw ⊢
  intro h
  apply hw
  rw [h, ite_self]

theorem serrePairing_pullbackAlong_eq_serrePairing_traceAlong'
    (hRT : ResidueTheorem K F) (hRT' : ResidueTheorem K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (htr : TraceIntegralAlong φ hφ)
    (hfib : FibreResidueIdentityAlong φ hφ)
    {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ)
    (ω : ↥(regularDifferentials K F))
    (hω' : Differential.pullbackAlong φ (ω : Ω[F⁄K]) ∈ regularDifferentials K F')
    (x' : cechH1 ((Place.restrictAlong φ hφ) ⁻¹' S₀) ((Place.restrictAlong φ hφ) ⁻¹' S₁) (0 :
      Divisor K F')) :
    serrePairing hRT' (preimage_restrictAlong_union_eq_univ φ hφ hcover)
        ⟨Differential.pullbackAlong φ (ω : Ω[F⁄K]), hω'⟩ x'
      = serrePairing hRT hcover ω (cechH1.traceAlong φ hφ htr S₀ S₁ x')

theorem _root_.AlgebraicCurve.serrePairing_pullbackAlong_eq_serrePairing_traceAlong
    {K : Type*} {F : Type*} {F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K F']
    [∀ v : Place K F, v.DCoordGenerates] [∀ w : Place K F', w.DCoordGenerates]
    [Nontrivial Ω[F⁄K]] [Nontrivial Ω[F'⁄K]]
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    [HasPrincipalDivisors K F] [HasPrincipalDivisors K F']
    (hRT : ResidueTheorem K F) (hRT' : ResidueTheorem K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (htr : TraceIntegralAlong φ hφ)
    (hfib : FibreResidueIdentityAlong φ hφ)
    {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ)
    (ω : ↥(regularDifferentials K F))
    (hω' : Differential.pullbackAlong φ (ω : Ω[F⁄K]) ∈ regularDifferentials K F')
    (x' : cechH1 ((Place.restrictAlong φ hφ) ⁻¹' S₀) ((Place.restrictAlong φ hφ) ⁻¹' S₁) (0 :
      Divisor K F')) :
    serrePairing hRT' (preimage_restrictAlong_union_eq_univ φ hφ hcover)
        ⟨Differential.pullbackAlong φ (ω : Ω[F⁄K]), hω'⟩ x'
      = serrePairing hRT hcover ω (cechH1.traceAlong φ hφ htr S₀ S₁ x')