feat(Mathlib.NumberTheory.Cyclotomic.Three): add various results (#13798)

We add various results about the third cyclotomic field needed to prove flt3.

From the flt3 project at LFTCM2024.

Author: riccardobrasca

Mathlib/Algebra/CharP/CharAndCard.lean

@@ -82,3 +82,8 @@ theorem not_isUnit_prime_of_dvd_card {R : Type*} [CommRing R] [Fintype R] (p : 
   mt (isUnit_iff_not_dvd_char R p).mp
     (Classical.not_not.mpr ((prime_dvd_char_iff_dvd_card p).mpr hp))
 #align not_is_unit_prime_of_dvd_card not_isUnit_prime_of_dvd_card
+
+lemma charP_of_card_eq_prime {R : Type*} [NonAssocRing R] [Fintype R] (p : ℕ) [hp : Fact p.Prime]
+    (hR : Fintype.card R = p) : CharP R p :=
+  have := Fintype.one_lt_card_iff_nontrivial.1 (hR ▸ hp.1.one_lt)
+  (CharP.charP_iff_prime_eq_zero hp.1).2 (hR ▸ Nat.cast_card_eq_zero R)

Mathlib/Data/ZMod/Basic.lean

@@ -491,6 +491,21 @@ noncomputable def ringEquiv [Fintype R] (h : Fintype.card R = n) : ZMod n ≃+*
   RingEquiv.ofBijective _ (ZMod.castHom_bijective R h)
 #align zmod.ring_equiv ZMod.ringEquiv
 
+/-- The unique ring isomorphism between `ZMod p` and a ring `R` of cardinality a prime `p`.
+
+If you need any property of this isomorphism, first of all use `ringEquivOfPrime_eq_ringEquiv`
+below (after `have : CharP R p := ...`) and deduce it by the results about `ZMod.ringEquiv`.  -/
+noncomputable def ringEquivOfPrime [Fintype R] {p : ℕ} (hp : p.Prime) (hR : Fintype.card R = p) :
+    ZMod p ≃+* R :=
+  have : Nontrivial R := Fintype.one_lt_card_iff_nontrivial.1 (hR ▸ hp.one_lt)
+  -- The following line exists as `charP_of_card_eq_prime` in `Mathlib.Algebra.CharP.CharAndCard`.
+  have : CharP R p := (CharP.charP_iff_prime_eq_zero hp).2 (hR ▸ Nat.cast_card_eq_zero R)
+  ZMod.ringEquiv R hR
+
+@[simp]
+lemma ringEquivOfPrime_eq_ringEquiv [Fintype R] {p : ℕ} [CharP R p] (hp : p.Prime)
+    (hR : Fintype.card R = p) : ringEquivOfPrime R hp hR = ringEquiv R hR := rfl
+
 /-- The identity between `ZMod m` and `ZMod n` when `m = n`, as a ring isomorphism. -/
 def ringEquivCongr {m n : ℕ} (h : m = n) : ZMod m ≃+* ZMod n := by
   cases' m with m <;> cases' n with n

Mathlib/NumberTheory/Cyclotomic/Rat.lean

@@ -182,6 +182,28 @@ noncomputable def integralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K]
 /-- Abbreviation to see a primitive root of unity as a member of the ring of integers. -/
 abbrev toInteger {k : ℕ+} (hζ : IsPrimitiveRoot ζ k) : 𝓞 K := ⟨ζ, hζ.isIntegral k.pos⟩
 
+lemma coe_toInteger {k : ℕ+} (hζ : IsPrimitiveRoot ζ k) : hζ.toInteger.1 = ζ := rfl
+
+/-- `𝓞 K ⧸ Ideal.span {ζ - 1}` is finite. -/
+lemma finite_quotient_toInteger_sub_one [NumberField K] {k : ℕ+} (hk : 1 < k)
+    (hζ : IsPrimitiveRoot ζ k) : Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) := by
+  refine (finite_iff_nonempty_fintype _).2 ⟨?_⟩
+  refine Ideal.fintypeQuotientOfFreeOfNeBot _ (fun h ↦ ?_)
+  simp only [Ideal.span_singleton_eq_bot, sub_eq_zero, ← Subtype.coe_inj] at h
+  exact hζ.ne_one hk (RingOfIntegers.ext_iff.1 h)
+
+/-- We have that `𝓞 K ⧸ Ideal.span {ζ - 1}` has cardinality equal to the norm of `ζ - 1`.
+
+See the results below to compute this norm in various cases. -/
+lemma card_quotient_toInteger_sub_one [NumberField K] {k : ℕ+} (hk : 1 < k)
+    (hζ : IsPrimitiveRoot ζ k) :
+    Nat.card (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) =
+      (Algebra.norm ℤ (hζ.toInteger - 1)).natAbs := by
+  have := hζ.finite_quotient_toInteger_sub_one hk
+  let _ := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
+  rw [Nat.card_eq_fintype_card, ← Submodule.cardQuot_apply, ← Ideal.absNorm_apply,
+    Ideal.absNorm_span_singleton]
+
 lemma toInteger_isPrimitiveRoot {k : ℕ+} (hζ : IsPrimitiveRoot ζ k) :
     IsPrimitiveRoot hζ.toInteger k :=
   IsPrimitiveRoot.of_map_of_injective (by exact hζ) RingOfIntegers.coe_injective

Mathlib/NumberTheory/Cyclotomic/Three.lean

@@ -7,6 +7,7 @@ Authors: Riccardo Brasca, Pietro Monticone
 import Mathlib.NumberTheory.Cyclotomic.Embeddings
 import Mathlib.NumberTheory.Cyclotomic.Rat
 import Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
+import Mathlib.RingTheory.Fintype
 
 /-!
 # Third Cyclotomic Field
@@ -33,7 +34,9 @@ namespace IsCyclotomicExtension.Rat.Three
 variable {K : Type*} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K]
 variable {ζ : K} (hζ : IsPrimitiveRoot ζ ↑(3 : ℕ+)) (u : (𝓞 K)ˣ)
 local notation3 "η" => (IsPrimitiveRoot.isUnit (hζ.toInteger_isPrimitiveRoot) (by decide)).unit
-local notation3 "λ" => (η : 𝓞 K) - 1
+local notation3 "λ" => hζ.toInteger - 1
+
+lemma coe_eta : (η : 𝓞 K) = hζ.toInteger := rfl
 
 /-- Let `u` be a unit in `(𝓞 K)ˣ`, then `u ∈ [1, -1, η, -η, η^2, -η^2]`. -/
 -- Here `List` is more convenient than `Finset`, even if further from the informal statement.
@@ -62,15 +65,16 @@ theorem Units.mem : u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2] := by
     (isOfFinOrder_iff_pow_eq_one.2 ⟨n, hnpos, hn⟩)
   replace hr : r ∈ Finset.Ico 0 3 := Finset.mem_Ico.2 ⟨by simp, hr3⟩
   replace hru : ↑u = η ^ r ∨ ↑u = -η ^ r := by
-    rcases hru with (h | h)
+    rcases hru with h | h
     · left; ext; exact h
     · right; ext; exact h
-  fin_cases hr <;> rcases hru with (h | h) <;> simp [h]
+  fin_cases hr <;> rcases hru with h | h <;> simp [h]
 
 /-- We have that `λ ^ 2 = -3 * η`. -/
 private lemma lambda_sq : λ ^ 2 = -3 * η := by
   ext
-  calc (λ ^ 2 : K) = η ^ 2 + η + 1 - 3 * η := by ring
+  calc (λ ^ 2 : K) = η ^ 2 + η + 1 - 3 * η := by
+        simp only [RingOfIntegers.map_mk, IsUnit.unit_spec]; ring
   _ = 0 - 3 * η := by simpa using hζ.isRoot_cyclotomic (by decide)
   _ = -3 * η := by ring
 
@@ -109,3 +113,81 @@ theorem eq_one_or_neg_one_of_unit_of_congruent (hcong : ∃ n : ℤ, λ ^ 2 ∣
     have : (hζ.pow_of_coprime 2 (by decide)).toInteger = hζ.toInteger ^ 2 := by ext; simp
     simp only [this, PNat.val_ofNat, Nat.cast_ofNat, mul_neg, Int.cast_neg, ← neg_add, ←
       sub_eq_iff_eq_add.1 hx, Units.val_neg, val_pow_eq_pow_val, IsUnit.unit_spec, neg_neg]
+
+variable (x : 𝓞 K)
+
+/-- Let `(x : 𝓞 K)`. Then we have that `λ` divides one amongst `x`, `x - 1` and `x + 1`. -/
+lemma lambda_dvd_or_dvd_sub_one_or_dvd_add_one : λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1 := by
+  classical
+  have := hζ.finite_quotient_toInteger_sub_one (by decide)
+  let _ := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
+  let _ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing -- to speed up instance synthesis
+  let _ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup -- dito
+  have := Finset.mem_univ (Ideal.Quotient.mk (Ideal.span {λ}) x)
+  have h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3 := by
+    rw [← Nat.card_eq_fintype_card, hζ.card_quotient_toInteger_sub_one (by decide),
+      hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)]
+    simp only [PNat.val_ofNat, Nat.cast_ofNat, Int.reduceAbs]
+  rw [Finset.univ_of_card_le_three h3.le] at this
+  simp only [Finset.mem_insert, Finset.mem_singleton] at this
+  rcases this with h | h | h
+  · left
+    exact Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 h
+  · right; left
+    refine Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_
+    rw [RingHom.map_sub, h, RingHom.map_one, sub_self]
+  · right; right
+    refine Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_
+    rw [RingHom.map_add, h, RingHom.map_one, add_left_neg]
+
+/-- We have that `η ^ 2 + η + 1 = 0`. -/
+lemma eta_sq_add_eta_add_one : (η : 𝓞 K) ^ 2 + η + 1 = 0 := by
+  rw [eta_sq]
+  ring
+
+/-- We have that `x ^ 3 - 1 = (x - 1) * (x - η) * (x - η ^ 2)`. -/
+lemma cube_sub_one_eq_mul : x ^ 3 - 1 = (x - 1) * (x - η) * (x - η ^ 2) := by
+  symm
+  calc _ = x ^ 3 - x ^ 2 * (η ^ 2 + η + 1) + x * (η ^ 2 + η + η ^ 3) - η ^ 3 := by ring
+  _ = x ^ 3 - x ^ 2 * (η ^ 2 + η + 1) + x * (η ^ 2 + η + 1) - 1 := by
+    simp [show hζ.toInteger ^ 3 = 1 from hζ.toInteger_isPrimitiveRoot.pow_eq_one]
+  _ = x ^ 3 - 1 := by rw [eta_sq_add_eta_add_one hζ]; ring
+
+/-- We have that `λ` divides `x * (x - 1) * (x - (η + 1))`. -/
+lemma lambda_dvd_mul_sub_one_mul_sub_eta_add_one : λ ∣ x * (x - 1) * (x - (η + 1)) := by
+  rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with h | h | h
+  · exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_left h _) _
+  · exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_right h _) _
+  · refine dvd_mul_of_dvd_right ?_ _
+    rw [show x - (η + 1) = x + 1 - (η - 1 + 3) by ring]
+    exact dvd_sub h <| dvd_add dvd_rfl hζ.toInteger_sub_one_dvd_prime'
+
+/-- If `λ` divides `x - 1`, then `λ ^ 4` divides `x ^ 3 - 1`. -/
+lemma lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one {x : 𝓞 K} (h : λ ∣ x - 1) :
+    λ ^ 4 ∣ x ^ 3 - 1 := by
+  obtain ⟨y, hy⟩ := h
+  have : x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (η + 1))) := by
+    calc _ =  (x - 1) * (x - 1 - λ) * (x - 1 - λ * (η + 1)) := by
+          simp only [coe_eta, cube_sub_one_eq_mul hζ x]; ring
+    _ = _ := by rw [hy]; ring
+  rw [this, pow_succ]
+  exact mul_dvd_mul_left _ (lambda_dvd_mul_sub_one_mul_sub_eta_add_one hζ y)
+
+/-- If `λ` divides `x + 1`, then `λ ^ 4` divides `x ^ 3 + 1`. -/
+lemma lambda_pow_four_dvd_cube_add_one_of_dvd_add_one {x : 𝓞 K} (h : λ ∣ x + 1) :
+    λ ^ 4 ∣ x ^ 3 + 1 := by
+  replace h : λ ∣ -x - 1 := by
+    convert h.neg_right using 1
+    exact (neg_add' x 1).symm
+  convert (lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ h).neg_right using 1
+  ring
+
+/-- If `λ` does not divide `x`, then `λ ^ 4` divides `x ^ 3 - 1` or `x ^ 3 + 1`. -/
+lemma lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd {x : 𝓞 K} (h : ¬ λ ∣ x) :
+    λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1 := by
+  rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with H | H | H
+  · contradiction
+  · left
+    exact lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ H
+  · right
+    exact lambda_pow_four_dvd_cube_add_one_of_dvd_add_one hζ H

Mathlib/NumberTheory/FLT/Three.lean

@@ -120,8 +120,8 @@ open NumberField
 variable {K : Type*} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K]
 variable {ζ : K} (hζ : IsPrimitiveRoot ζ (3 : ℕ+))
 
-local notation3 "η" => hζ.toInteger
-local notation3 "λ" => η - 1
+local notation3 "η" => (IsPrimitiveRoot.isUnit (hζ.toInteger_isPrimitiveRoot) (by decide)).unit
+local notation3 "λ" => hζ.toInteger - 1
 
 /-- `FermatLastTheoremForThreeGen` is the statement that `a ^ 3 + b ^ 3 = u * c ^ 3` has no
 nontrivial solutions in `𝓞 K` for all `u : (𝓞 K)ˣ` such that `¬ λ ∣ a`, `¬ λ ∣ b` and `λ ∣ c`.

Mathlib/RingTheory/Fintype.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Mathlib.Data.Fintype.Units
+import Mathlib.Data.ZMod.Basic
 
 #align_import ring_theory.fintype from "leanprover-community/mathlib"@"1126441d6bccf98c81214a0780c73d499f6721fe"
 
@@ -12,6 +13,46 @@ import Mathlib.Data.Fintype.Units
 -/
 
 
+open Finset ZMod
+
+variable {R : Type*} [Ring R] [Fintype R] [DecidableEq R]
+
+lemma Finset.univ_of_card_le_two (h : Fintype.card R ≤ 2) :
+    (univ : Finset R) = {0, 1} := by
+  rcases subsingleton_or_nontrivial R
+  · exact le_antisymm (fun a _ ↦ by simp [Subsingleton.elim a 0]) (Finset.subset_univ _)
+  · refine (eq_of_subset_of_card_le (subset_univ _) ?_).symm
+    convert h
+    simp
+
+lemma Finset.univ_of_card_le_three (h : Fintype.card R ≤ 3) :
+    (univ : Finset R) = {0, 1, -1} := by
+  refine (eq_of_subset_of_card_le (subset_univ _) ?_).symm
+  rcases lt_or_eq_of_le h with h | h
+  · apply card_le_card
+    rw [Finset.univ_of_card_le_two (Nat.lt_succ_iff.1 h)]
+    intro a ha
+    simp only [mem_insert, mem_singleton] at ha
+    rcases ha with rfl | rfl <;> simp
+  · have : Nontrivial R := by
+      refine Fintype.one_lt_card_iff_nontrivial.1 ?_
+      rw [h]
+      norm_num
+    rw [card_univ, h, card_insert_of_not_mem, card_insert_of_not_mem, card_singleton]
+    · rw [mem_singleton]
+      intro H
+      rw [← add_eq_zero_iff_eq_neg, one_add_one_eq_two] at H
+      apply_fun (ringEquivOfPrime R Nat.prime_three h).symm at H
+      simp only [map_ofNat, map_zero] at H
+      replace H : ((2 : ℕ) : ZMod 3) = 0 := H
+      rw [natCast_zmod_eq_zero_iff_dvd] at H
+      norm_num at H
+    · intro h
+      simp only [mem_insert, mem_singleton, zero_eq_neg] at h
+      rcases h with (h | h)
+      · exact zero_ne_one h
+      · exact zero_ne_one h.symm
+
 open scoped Classical
 
 theorem card_units_lt (M₀ : Type*) [MonoidWithZero M₀] [Nontrivial M₀] [Fintype M₀] :