JacobianVarieties.WeilPairing.Proofs.InseparableWeilPairing.Ws23WeilAdjPI.main
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.InseparableWeilPairing
open AlgebraicCurve
namespace Ws23WeilAdjPI
open AlgebraicCurveLean source · full declaration
theorem main
{K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
[HasPrincipalDivisors K F] [HasPrincipalDivisors K F']
(u : F →ₐ[K] F') (hu : u.toRingHom.IsIntegral) (hfin : FiniteAlong K u)
(hpi : let _ : Algebra F F' := algebraAlong u; IsPurelyInseparable F F')
(hFI : FundamentalIdentityAlong K u hu)
(hratF : ∀ v : Place K F, v.IsRational) (hratF' : ∀ w : Place K F', w.IsRational)
{n : ℕ} (d : WeilDatum K F' n) (d₀ : WeilDatum K F n)
(hD₁ : d.D₁ = Divisor.pullbackAlong u hu d₀.D₁) (hf₁ : d.f₁ = u d₀.f₁)
(hD₂ : d₀.D₂ = Divisor.pushforwardAlong u hu d.D₂)
(hf₂ : d₀.f₂ = (let _ : Algebra F F' := algebraAlong u; Algebra.norm F d.f₂)) :
d.pairing = d₀.pairing := by
let := algebraAlong u
have := isScalarTower_along u
have := isIntegral_along u hu
have : Module.Finite F F' := hfin
have : IsPurelyInseparable F F' := hpi
have : FundamentalIdentity K F F' := hFI
have hD₁w : ∀ w : Place K F', d.D₁ w = w.ramificationIndex F * d₀.D₁ (w.restrict F) := by
intro w
rw [hD₁]
exact Divisor.pullback_apply d₀.D₁ w
have hnum : Divisor.evalFun d.f₁ d.D₂ = Divisor.evalFun d₀.f₁ d₀.D₂ := by
rw [hf₁, hD₂]
refine Divisor.evalFun_algebraMap_pushforward d₀.f₁_ne_zero d.D₂ (fun w _ => hratF' w)
(fun w _ => hratF _) (fun w hw => ?_)
have h2 : d.D₂ w ≠ 0 := Finsupp.mem_support_iff.mp hw
have h1 : d.D₁ w = 0 := (d.disjoint w).resolve_right h2
rw [hD₁w w] at h1
have he : (w.ramificationIndex F : ℤ) ≠ 0 := by
have := w.ramificationIndex_pos (F := F)
exact_mod_cast this.ne'
have h0 : d₀.D₁ (w.restrict F) = 0 := (mul_eq_zero.mp h1).resolve_left he
rw [d₀.ord_f₁, h0, mul_zero]
have hden : Divisor.evalFun d.f₂ d.D₁ = Divisor.evalFun d₀.f₂ d₀.D₁ := by
rw [hD₁, hf₂]
refine Divisor.evalFun_pullback_of_isPurelyInseparable d.f₂_ne_zero d₀.D₁ (fun v _ => hratF v)
(fun v _ w _ => hratF' w) (fun v hv w hw => ?_)
have hwv : w.restrict F = v := Place.mem_fiber.mp hw
have hv' : d₀.D₁ v ≠ 0 := Finsupp.mem_support_iff.mp hv
have he : (w.ramificationIndex F : ℤ) ≠ 0 := by
have := w.ramificationIndex_pos (F := F)
exact_mod_cast this.ne'
have h1 : d.D₁ w ≠ 0 := by
rw [hD₁w w, hwv]
exact mul_ne_zero he hv'
have h2 : d.D₂ w = 0 := (d.disjoint w).resolve_left h1
rw [d.ord_f₂, h2, mul_zero]
rw [WeilDatum.pairing, WeilDatum.pairing, hnum, hden]