English
Nonexistence result for a polynomial Fermat–Catalan type equation in a polynomial ring over a field, generalizing FLT for certain exponents.
Русский
Не существует решений полиномного уравнения Фермат–Каталана в кольце полиномов над полем, обобщая Фермат для некоторых степеней.
LaTeX
$$$\text{Polynomial FLT Cat} \Rightarrow \text{no nontrivial } a,b,c \text{ with coprime condition and } a^p+b^q=c^r.$$$
Lean4
/-- **Polynomial ABC theorem.** -/
protected theorem abc {a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b)
(hsum : a + b + c = 0) :
(natDegree a + 1 ≤ (radical (a * b * c)).natDegree ∧
natDegree b + 1 ≤ (radical (a * b * c)).natDegree ∧ natDegree c + 1 ≤ (radical (a * b * c)).natDegree) ∨
derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0 :=
by
set w := wronskian a b with wab
have hbc : IsCoprime b c := by
rw [add_eq_zero_iff_neg_eq] at hsum
rw [← hsum, IsCoprime.neg_right_iff]
convert IsCoprime.add_mul_left_right hab.symm 1
rw [mul_one]
have hsum' : b + c + a = 0 := by rwa [add_rotate] at hsum
have hca : IsCoprime c a := by
rw [add_eq_zero_iff_neg_eq] at hsum'
rw [← hsum', IsCoprime.neg_right_iff]
convert IsCoprime.add_mul_left_right hbc.symm 1
rw [mul_one]
have wbc : w = wronskian b c := wronskian_eq_of_sum_zero hsum
have wca : w = wronskian c a := by
rw [add_rotate] at hsum
simpa only [← wbc] using wronskian_eq_of_sum_zero hsum
have abc_dr_dvd_w : divRadical (a * b * c) ∣ w :=
by
have adr_dvd_w := divRadical_dvd_wronskian_left a b
have bdr_dvd_w := divRadical_dvd_wronskian_right a b
have cdr_dvd_w := divRadical_dvd_wronskian_right b c
rw [← wab] at adr_dvd_w bdr_dvd_w
rw [← wbc] at cdr_dvd_w
rw [divRadical_mul (hca.symm.mul_left hbc), divRadical_mul hab]
exact (hca.divRadical.symm.mul_left hbc.divRadical).mul_dvd (hab.divRadical.mul_dvd adr_dvd_w bdr_dvd_w) cdr_dvd_w
by_cases hw : w = 0
· right
rw [hw] at wab wbc
obtain ⟨ga, gb⟩ := hab.wronskian_eq_zero_iff.mp wab.symm
obtain ⟨_, gc⟩ := hbc.wronskian_eq_zero_iff.mp wbc.symm
exact ⟨ga, gb, gc⟩
· left
-- use `abc_subcall` three times, using the symmetry in `a, b, c`
refine ⟨?_, ?_, ?_⟩
· rw [mul_rotate] at abc_dr_dvd_w ⊢
apply abc_subcall wbc <;> assumption
· rw [← mul_rotate] at abc_dr_dvd_w ⊢
apply abc_subcall wca <;> assumption
· apply abc_subcall wab <;> assumption
