SerrePairing_traceAlong_eq_serrePairing_pullbackAlong.lean

theorem finsum_eq_finsum_sum_fiberAlong_t2 [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 kaehlerResidueTerm_fsmul_left_t2 (u : L) (η : Ω[L⁄K]) (α : Place K L → L) (w : Place K L) :
    kaehlerResidueTerm (u • η) α w = kaehlerResidueTerm η (mulAdele K u α) w

theorem mulAdele_diagonalHom (u g : L) : mulAdele K u (diagonalHom K L g) = diagonalHom K L (u *
  g)

theorem support_ite_kaehlerResidueTerm_finite_t2 [HasCanonicalDivisor (K := K) (F := L)]
    [HasPrincipalDivisors K L] (S : Set (Place K L)) (η : Ω[L⁄K]) (g : L) :
    (Function.support fun w => if w ∈ S then (0 : K) else kaehlerResidueTerm η (diagonalHom K L g)
      w).Finite := by
  have hfin : (Function.support (kaehlerResidueTerm η (diagonalHom K L g))).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 g)
  refine hfin.subset fun w hw => ?_
  rw [Function.mem_support] at hw ⊢
  intro h
  apply hw
  rw [h, ite_self]

theorem exists_eq_smul_pullbackAlong [IsCurveOver K F'] (φ : F →ₐ[K] F') (hsep : SeparableAlong K φ)
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) (ω' : Ω[F'⁄K]) :
    ∃ u : F', ω' = u • Differential.pullbackAlong φ ω₀

theorem serrePairing_traceAlong_eq_serrePairing_pullbackAlong'
    {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]] [IsCurveOver K F']
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    [HasPrincipalDivisors K F]
    (hRT : ResidueTheorem K F) (hRT' : ResidueTheorem K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hsep : SeparableAlong K φ)
    (hfib : FibreResidueIdentityAlong φ hφ)
    {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ)
    (ω' : ↥(regularDifferentials K F'))
    (hω : Differential.traceAlong φ (ω' : Ω[F'⁄K]) ∈ regularDifferentials K F)
    (x : cechH1 S₀ S₁ (0 : Divisor K F)) :
    serrePairing hRT hcover ⟨Differential.traceAlong φ (ω' : Ω[F'⁄K]), hω⟩ x
      = serrePairing hRT' (preimage_restrictAlong_union_eq_univ φ hφ hcover) ω'
          (cechH1.pullbackAlong φ hφ S₀ S₁ x)

theorem _root_.AlgebraicCurve.serrePairing_traceAlong_eq_serrePairing_pullbackAlong
    {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]] [IsCurveOver K F']
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    [HasPrincipalDivisors K F]
    (hRT : ResidueTheorem K F) (hRT' : ResidueTheorem K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hsep : SeparableAlong K φ)
    (hfib : FibreResidueIdentityAlong φ hφ)
    {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ)
    (ω' : ↥(regularDifferentials K F'))
    (hω : Differential.traceAlong φ (ω' : Ω[F'⁄K]) ∈ regularDifferentials K F)
    (x : cechH1 S₀ S₁ (0 : Divisor K F)) :
    serrePairing hRT hcover ⟨Differential.traceAlong φ (ω' : Ω[F'⁄K]), hω⟩ x
      = serrePairing hRT' (preimage_restrictAlong_union_eq_univ φ hφ hcover) ω'
          (cechH1.pullbackAlong φ hφ S₀ S₁ x)