Lean source · full declarationtheorem _root_.AlgebraicCurve.Divisor.exists_symmValue_rows_kernel_iff
{K₀ k F : Type*} [Field K₀] [Field k] [Field F] [Algebra K₀ k] [Algebra k F]
{j : F} (hj : Transcendental k j)
[FiniteDimensional (IntermediateField.adjoin k ({j} : Set F)) F]
[Algebra.IsSeparable (IntermediateField.adjoin k ({j} : Set F)) F] [CharZero k]
(hfin : ∀ x : F, x ≠ 0 → {v : Place k F | x ∉ v.toValuationSubring}.Finite)
(hrat : ∀ (v : Place k F) (x : F), j ∈ v.toValuationSubring →
IsIntegral (Algebra.adjoin k ({j} : Set F)) x →
∃ c : k, x = algebraMap k F c ∨ 0 < v.ord (x - algebraMap k F c))
(n : ℕ) (b : Fin n → F)
(hbli : ∀ c : Fin n → Polynomial k,
(∑ i : Fin n, Polynomial.aeval j (c i) * b i) = 0 → ∀ i, c i = 0)
(hbsp : ∀ x : F, ∃ (q : Polynomial k) (c : Fin n → Polynomial k), q ≠ 0 ∧
x * Polynomial.aeval j q = ∑ i : Fin n, Polynomial.aeval j (c i) * b i)
(d : Polynomial K₀) (hd : d ≠ 0) (A : Fin n → Matrix (Fin n) (Fin n) (Polynomial K₀))
(hmul : ∀ i i' : Fin n, b i * b i' * Polynomial.aeval j (d.map (algebraMap K₀ k))
= ∑ i'' : Fin n, Polynomial.aeval j ((A i i'' i').map (algebraMap K₀ k)) * b i'')
(q₀ : Polynomial K₀) (v₀ : Place k F) (g e mdeg : ℕ) :
∃ (Θ : Polynomial K₀) (a : ℕ) (cL₀ : Fin a → Polynomial K₀) (cL : Fin a → Fin n → Polynomial K₀)
(χ : Fin a → Polynomial (Polynomial K₀))
(M : ℕ) (Rm : Fin M → ℕ) (Y : (l : Fin M) → Fin (Rm l) → Fin n × Fin (mdeg + 1) → k)
(R : Fin (g + 1) → ℕ)
(P : (r : Fin (g + 1)) → Fin (R r) → Fin n × Fin (mdeg + 1) →
MvPolynomial (Fin (a + 1) × Fin ((r : ℕ) + 1)) K₀),
(∀ s, (χ s).Monic) ∧
∀ (D : Divisor k F), (∀ v, 0 ≤ D v) → Divisor.degree D = (g : ℤ) →
∃ (r : Fin (g + 1)) (l : Fin M) (pt : Fin (r : ℕ) → Place k F)
(val : Fin (r : ℕ) × Fin (a + 1) → k)
(r' : ℕ) (pt' : Fin r' → Place k F) (jv' : Fin r' → k),
(∀ t, 0 ≤ (pt t).ord j ∧
(pt t).ord (Polynomial.aeval j (Θ.map (algebraMap K₀ k))) = 0) ∧
(∀ t', 0 < (pt' t').ord (Polynomial.aeval j (Θ.map (algebraMap K₀ k)))) ∧
(∀ v : Place k F, 0 ≤ v.ord j → D v =
((∑ t, Finsupp.single (pt t) (1 : ℤ))
+ ∑ t', Finsupp.single (pt' t') (1 : ℤ) : Divisor k F) v) ∧
(∀ t, 0 < (pt t).ord (j - algebraMap k F (val (t, 0)))) ∧
(∀ t (s : Fin a), 0 < (pt t).ord
((Polynomial.aeval j ((cL₀ s).map (algebraMap K₀ k))
+ ∑ i : Fin n, Polynomial.aeval j ((cL s i).map (algebraMap K₀ k)) * b i)
- algebraMap k F (val (t, s.succ)))) ∧
(∀ t', 0 < (pt' t').ord (j - algebraMap k F (jv' t'))) ∧
(∀ t (s : Fin a), Polynomial.eval₂ (Polynomial.eval₂RingHom (algebraMap K₀ k) (val (t,
0)))
(val (t, s.succ)) (χ s) = 0) ∧
∀ u : Fin n × Fin (mdeg + 1) → k,
((∀ ρ : Fin (R r), ∑ col, MvPolynomial.aeval
(fun ak : Fin (a + 1) × Fin ((r : ℕ) + 1) =>
(∏ t : Fin (r : ℕ), (Polynomial.X - Polynomial.C (val (t, ak.1)))).coeff ak.2)
(P r ρ col) * u col = 0) ∧
(∀ ρ : Fin (Rm l), ∑ col, Y l ρ col * u col = 0)) ↔
(u = 0 ∨ ∀ v : Place k F,
0 ≤ (D - (e : ℤ) • Finsupp.single v₀ 1 : Divisor k F) v
+ v.ord ((∑ i : Fin n, Polynomial.aeval j
(∑ dd : Fin (mdeg + 1), Polynomial.C (u (i, dd)) * Polynomial.X ^ (dd : ℕ)) *
b i)
* (Polynomial.aeval j
((∏ t : Fin (r : ℕ), (Polynomial.X - Polynomial.C (val (t, 0))))
* (∏ t', (Polynomial.X - Polynomial.C (jv' t')))
* q₀.map (algebraMap K₀ k)))⁻¹)) := by
classical
have hjne : j ≠ 0 := fun h => hj (h ▸ isAlgebraic_zero)
rcases Nat.eq_zero_or_pos n with hn0 | hn
· subst hn0
exfalso
obtain ⟨q, c, hq, hqe⟩ := hbsp 1
rw [Finset.univ_eq_empty, Finset.sum_empty, one_mul] at hqe
exact hj ⟨q, hq, hqe⟩
rcases eq_or_ne q₀ 0 with hq₀0 | hq₀
· subst hq₀0
have hIdb₀ := mwALGMdev.mwALGM_isIntegral_db hj n b hbsp d hd A hmul
have hdegnz₀ : ∀ v : Place k F, v.deg ≠ 0 :=
fun v => Place.deg_ne_zero_of_finiteDimensional_adjoin j hj v
let ncol : ℕ := n * (mdeg + 1)
let ec : Fin n × Fin (mdeg + 1) ≃ Fin ncol := finProdFinEquiv
refine ⟨d, 0, Fin.elim0, Fin.elim0, Fin.elim0, 2, fun _ => ncol,
fun l ρ col => if (l : ℕ) = 0 then 0 else (if ρ = ec col then 1 else 0),
fun _ => 0, fun _ => Fin.elim0, fun s => s.elim0, ?_⟩
intro D heff hdeg
obtain ⟨r, hrle, pt, val, βpt, r', pt', jv', hpt, hpt', henum, hval0, hvalL, hjv', hβpt,
hdord⟩ := mwALGMdev.mwALGM_enum hj hrat n b d hd hIdb₀ d hd (dvd_refl d) 0 Fin.elim0
Fin.elim0 (fun s => s.elim0) (fun s => s.elim0) hdegnz₀ g D heff hdeg
have hfeq0 : ∀ (gU : F) (p : Polynomial k) (v : Place k F),
v.ord (gU * (Polynomial.aeval j
(p * (0 : Polynomial K₀).map (algebraMap K₀ k)))⁻¹) = 0 := by
intro gU p v
simp only [Polynomial.map_zero, mul_zero, map_zero, inv_zero, Place.ord_zero]
by_cases heffv : ∀ v, 0 ≤ (D - (e : ℤ) • Finsupp.single v₀ 1 : Divisor k F) v
· refine ⟨⟨r, Nat.lt_succ_of_le hrle⟩, 0, pt, val, r', pt', jv',
hpt, hpt', henum, hval0, fun t s => s.elim0, hjv', fun t s => s.elim0, fun u => ?_⟩
refine ⟨fun _ => Or.inr fun v => ?_,
fun _ => ⟨fun ρ => ρ.elim0, fun ρ => by
simp only [Fin.val_zero, ite_true, zero_mul, Finset.sum_const_zero]⟩⟩
rw [hfeq0 _ _ v, add_zero]; exact heffv v
· refine ⟨⟨r, Nat.lt_succ_of_le hrle⟩, 1, pt, val, r', pt', jv',
hpt, hpt', henum, hval0, fun t s => s.elim0, hjv', fun t s => s.elim0, fun u => ?_⟩
have hl1 : ((1 : Fin 2) : ℕ) ≠ 0 := one_ne_zero
constructor
· rintro ⟨_, hY⟩
left
funext col
have h := hY (ec col)
simp only [ite_eq_right hl1, ite_mul, one_mul, zero_mul, ← ec.eq_symm_apply,
Finset.sum_ite_eq, Finset.mem_univ, ite_true, Equiv.symm_apply_apply] at h
exact h
· rintro (hu0 | hord)
· subst hu0
exact ⟨fun ρ => ρ.elim0, fun ρ => by
simp only [Pi.zero_apply, mul_zero, Finset.sum_const_zero]⟩
· exact absurd (fun v => by
have h := hord v; rw [hfeq0 _ _ v, add_zero] at h; exact h) heffv
have hIdb := mwALGMdev.mwALGM_isIntegral_db hj n b hbsp d hd A hmul
obtain ⟨Δ, hΔ, hG⟩ :=
mwALGMdev.mwALGM_gram_denom hj n b hbli hbsp d hd A hmul
set Θ : Polynomial K₀ := Δ * d * q₀ with hΘdef
have hΘ : Θ ≠ 0 := mul_ne_zero (mul_ne_zero hΔ hd) hq₀
have hdΘ : d ∣ Θ := (Dvd.intro_left Δ rfl).mul_right q₀
have hK₀char : CharZero K₀ :=
(RingHom.charZero_iff (algebraMap K₀ k).injective).mpr inferInstance
have hθchoice : ∃ (θ : Fin (n * (g + 1) + 1) → K₀), Function.Injective θ ∧
∀ (s : Fin (n * (g + 1) + 1)) (c : k),
(Polynomial.aeval j (Polynomial.X.map (algebraMap K₀ k))
+ ∑ i : Fin n, Polynomial.aeval j ((Polynomial.C (θ s ^ (i.val + 1)) * d).map
(algebraMap K₀ k)) * b i)
≠ algebraMap k F c :=
mwALGMdev.mwALGM_theta_choice hK₀char n b d g
(fun β θc hθc => AlgebraicCurve.Place.mwALGN_exists_nonconst_form hj β θc hθc)
let a : ℕ := n * (g + 1) + 1
obtain ⟨θ, hθinj, hLnc⟩ := hθchoice
let cL₀ : Fin a → Polynomial K₀ := fun _ => Polynomial.X
let cL : Fin a → Fin n → Polynomial K₀ := fun s i => Polynomial.C (θ s ^ (i.val + 1)) * d
have hcLd : ∀ s i, d ∣ cL s i := fun s i => Dvd.intro_left _ rfl
have hχlane : ∀ s : Fin a, ∃ (M : Matrix (Fin n) (Fin n) (Polynomial K₀))
(χ : Polynomial (Polynomial K₀)), χ.Monic ∧
(∀ (m : ℕ) (i : Fin n),
(Polynomial.aeval j ((cL₀ s).map (algebraMap K₀ k))
+ ∑ i' : Fin n, Polynomial.aeval j (((fun i => Polynomial.C (θ s ^ (i.val + 1))) i'
* d).map (algebraMap K₀ k)) * b i') ^ m
* (Polynomial.aeval j (d.map (algebraMap K₀ k)) * b i)
= ∑ i' : Fin n, Polynomial.aeval j (((M ^ m) i' i).map (algebraMap K₀ k))
* (Polynomial.aeval j (d.map (algebraMap K₀ k)) * b i')) ∧
Polynomial.eval₂
((Polynomial.aeval j).toRingHom.comp (Polynomial.mapRingHom (algebraMap K₀ k)))
(Polynomial.aeval j ((cL₀ s).map (algebraMap K₀ k))
+ ∑ i' : Fin n, Polynomial.aeval j (((fun i => Polynomial.C (θ s ^ (i.val + 1))) i'
* d).map (algebraMap K₀ k)) * b i')
χ = 0 := by
intro s
exact mwALGMdev.mwALGM_exists_mulMatrix_chi hj n b hbsp d hd A hmul
(cL₀ s) (fun i => Polynomial.C (θ s ^ (i.val + 1)))
choose Ms χ hχmon hpow hkill using hχlane
obtain ⟨M, Rm, Y, hMenu⟩ :=
mwALGCdev.mwALGC_menu hj hfin n b hbli hbsp Θ hΘ q₀ hq₀ v₀ g e mdeg
refine ⟨Θ, a, cL₀, cL, χ, M, Rm, Y, fun r => a * n * (r : ℕ),
fun r ρ col => mwALGCdev.mwALGC_chowFamily a n mdeg Ms (r : ℕ)
(mwALGCdev.mwALGC_heqvN a n (r : ℕ) ρ) col, hχmon, ?_⟩
intro D heff hdeg
have hdegnz : ∀ v : Place k F, v.deg ≠ 0 :=
fun v => Place.deg_ne_zero_of_finiteDimensional_adjoin j hj v
obtain ⟨r, hrle, pt, val, βpt, r', pt', jv', hpt, hpt', henum, hval0, hvalL, hjv', hβpt, hdord⟩ :=
mwALGMdev.mwALGM_enum hj hrat n b d hd hIdb Θ hΘ hdΘ a cL₀ cL hcLd hLnc hdegnz g D heff hdeg
obtain ⟨l, hMenuD⟩ := hMenu D heff hdeg r pt r' pt' (fun t => val (t, 0)) jv'
hpt hpt' henum hval0 hjv'
have hrlt : r < g + 1 := Nat.lt_succ_of_le hrle
refine ⟨⟨r, hrlt⟩, l, pt, val, r', pt', jv', hpt, hpt', henum, hval0, hvalL, hjv', ?_, ?_⟩
· intro t s
have hjmem : j ∈ (pt t).toValuationSubring := (pt t).mem_of_ord_nonneg hjne (hpt t).1
have hIform := mwALGMdev.mwALGM_isIntegral_form hj n b hbsp d hd A hmul
(cL₀ s) (fun i => Polynomial.C (θ s ^ (i.val + 1)))
have hLsmem : (Polynomial.aeval j ((cL₀ s).map (algebraMap K₀ k))
+ ∑ i' : Fin n, Polynomial.aeval j
(((fun i => Polynomial.C (θ s ^ (i.val + 1))) i' * d).map (algebraMap K₀ k)) * b i')
∈ (pt t).toValuationSubring :=
(pt t).mem_toValuationSubring_of_isIntegral_adjoin hjmem hIform
exact mwALGMdev.mwALGM_pin_eval₂_eq_zero (pt t) hjmem hLsmem (Or.inr (hval0 t))
(Or.inr (hvalL t s)) (χ s) (hkill s)
· have hdj0 : Polynomial.aeval j (d.map (algebraMap K₀ k)) ≠ 0 := fun h0 =>
hj ⟨d.map (algebraMap K₀ k),
(Polynomial.map_ne_zero_iff (algebraMap K₀ k).injective).mpr hd, h0⟩
set L : Fin a → F := fun s =>
Polynomial.aeval j ((Polynomial.X : Polynomial K₀).map (algebraMap K₀ k))
+ ∑ i : Fin n, Polynomial.aeval j
((Polynomial.C (θ s ^ (i.val + 1)) * d).map (algebraMap K₀ k)) * b i with hLdef
have hLreg : ∀ (s : Fin a) (v : Place k F), j ∈ v.toValuationSubring →
L s ∈ v.toValuationSubring := fun s v hjv =>
v.mem_toValuationSubring_of_isIntegral_adjoin hjv
(mwALGMdev.mwALGM_isIntegral_form hj n b hbsp d hd A hmul
Polynomial.X (fun i => Polynomial.C (θ s ^ (i.val + 1))))
refine mwALGCdev.mwALGC_ker n b q₀ v₀ e mdeg Θ a Ms (Rm l) (Y l) D r val r' jv' hMenuD ?_ ?_
· intro u hu hdvd v hvbad
rw [not_or, not_or, not_lt, not_lt] at hvbad
obtain ⟨hvj, hvΘ', hvne⟩ := hvbad
have hjmemv : j ∈ v.toValuationSubring := v.mem_of_ord_nonneg hjne hvj
have hvΘ : v.ord (Polynomial.aeval j (Θ.map (algebraMap K₀ k))) = 0 :=
le_antisymm hvΘ' (v.ord_nonneg_of_mem (mwALGMdev.mwALGM_aeval_mem v hjmemv _))
set gU : F := ∑ i : Fin n, Polynomial.aeval j
(∑ dd : Fin (mdeg + 1), Polynomial.C (u (i, dd)) * Polynomial.X ^ (dd : ℕ)) * b i
with hgUdef
have hgU0 : gU ≠ 0 := by
rintro hgU0
apply hu
funext ⟨i, dd⟩
change u (i, dd) = 0
have h := hbli _ hgU0 i
have hcoeff : (∑ dd : Fin (mdeg + 1),
Polynomial.C (u (i, dd)) * Polynomial.X ^ (dd : ℕ)).coeff (dd : ℕ) = 0 := by
rw [h]; exact Polynomial.coeff_zero _
simpa only [Polynomial.finsetSum_coeff, Polynomial.coeff_C_mul, Polynomial.coeff_X_pow,
mul_ite, mul_one, mul_zero, Fin.val_inj, Finset.sum_ite_eq, Finset.mem_univ,
ite_true] using hcoeff
have hE : ∀ s : Fin a,
(∏ t : Fin r, ((Polynomial.aeval j ((Polynomial.X : Polynomial K₀).map (algebraMap K₀ k))
+ ∑ i : Fin n, Polynomial.aeval j
((Polynomial.C (θ s ^ (i.val + 1)) * d).map (algebraMap K₀ k)) * b i)
- algebraMap k F (val (t, s.succ)))) * gU
= ∑ i' : Fin n, Polynomial.aeval j (∑ col : Fin n × Fin (mdeg + 1),
Polynomial.C (u col) * mwALGCdev.mwALGC_Ek a n mdeg Ms r val s i' col.1 col.2)
* b i' := by
intro s
have hEe := mwALGMdev.mwALGM_Eexpand n b (Polynomial.aeval j (d.map (algebraMap K₀ k))) hdj0
mdeg r (Polynomial.aeval j ((Polynomial.X : Polynomial K₀).map (algebraMap K₀ k))
+ ∑ i : Fin n, Polynomial.aeval j
((Polynomial.C (θ s ^ (i.val + 1)) * d).map (algebraMap K₀ k)) * b i)
(Ms s) (hpow s) (fun t => val (t, s.succ)) u
simp only [mwALGCdev.mwALGC_Ek]
exact hEe
exact AlgebraicCurve.Place.mwALGN_ker_good hj hrat n b d hd hIdb Δ hΔ hG q₀ hq₀ Θ hΘdef v₀ e
a θ hθinj g
(Nat.lt_succ_self _) D hrle pt val βpt pt' jv' hpt hpt' henum hval0 hvalL hjv' hβpt hgU0
(fun s i' => ∑ col : Fin n × Fin (mdeg + 1),
Polynomial.C (u col) * mwALGCdev.mwALGC_Ek a n mdeg Ms r val s i' col.1 col.2)
hE hdvd v hvj hvΘ hvne
· intro u hu hord
set gU : F := ∑ i : Fin n, Polynomial.aeval j
(∑ dd : Fin (mdeg + 1), Polynomial.C (u (i, dd)) * Polynomial.X ^ (dd : ℕ)) * b i
with hgUdef
have hE : ∀ s : Fin a, (∏ t : Fin r, (L s - algebraMap k F (val (t, s.succ)))) * gU
= ∑ i' : Fin n, Polynomial.aeval j (∑ col : Fin n × Fin (mdeg + 1),
Polynomial.C (u col) * mwALGCdev.mwALGC_Ek a n mdeg Ms r val s i' col.1 col.2)
* b i' := by
intro s
have hEe := mwALGMdev.mwALGM_Eexpand n b (Polynomial.aeval j (d.map (algebraMap K₀ k)))
hdj0 mdeg r (L s) (Ms s) (hpow s) (fun t => val (t, s.succ)) u
simp only [mwALGCdev.mwALGC_Ek]
exact hEe
refine mwALGMdev.mwALGM_ker_chow hj n b hbli d hd Δ hΔ q₀ hq₀ Θ hΘdef v₀ e D a pt val pt'
jv' hpt henum hval0 L hLreg hvalL hjv' gU
(fun s i' => ∑ col : Fin n × Fin (mdeg + 1),
Polynomial.C (u col) * mwALGCdev.mwALGC_Ek a n mdeg Ms r val s i' col.1 col.2)
hE hord ?_
intro S hS hSΔ N gg E' hE' hx
exact AlgebraicCurve.Place.mwALGN_dvd_of_forall_mem hj b hbli
(Δ.map (algebraMap K₀ k))
(d.map (algebraMap K₀ k))
((Polynomial.map_ne_zero_iff (algebraMap K₀ k).injective).mpr hd)
hG (fun x hxmem => mwALGMdev.mwALGM_isIntegral_adjoin_of_forall_mem hxmem)
S hS hSΔ E' hE' hx