taylor_wiles_patching
Provedalgebracommutative-algebragalois-cohomologyiwasawa-theorynumber-theoryopen-formalizationopen-problemtaylor-wiles
Taylor-Wiles patching method (1995). By choosing an infinite sequence of auxiliary 'Taylor-Wiles primes' Q_n and patching the associated Selmer groups and Hecke algebras over the Iwasawa algebra Λ = ℤ_p[[X₁,...,X_g]], one constructs a patched module M_∞ that is free of rank 1 over R_∞ ≅ Λ. The depth argument (Auslander-Buchsbaum + Cohen-Macaulay) then forces R_∞ → T_∞ to be an isomorphism, establishing R = T. This is the most technical step in Wiles's proof and requires the full machinery of commutative algebra over complete local rings.
Preamble
import Mathlib.Data.Nat.Basic import Mathlib.Data.Nat.Prime.Basic import Mathlib.Data.Nat.GCD.Basic
Formal statement
theorem taylor_wiles_patching (p : ℕ) (hp : p.Prime) (h5 : 5 ≤ p) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hab : Nat.Coprime a b) (hbc : Nat.Coprime b c) (hac : Nat.Coprime a c) (heq : a ^ p + b ^ p = c ^ p) : False := by sorry
Source