Skip to content

Commit

Permalink
some comments on proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
@CBirkbeck
CBirkbeck committed Jul 1, 2024
1 parent e75f135 commit 0e3aad0
Showing 1 changed file with 31 additions and 1 deletion.
32 changes: 31 additions & 1 deletion FltRegular/CaseII/InductionStep.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,13 +33,17 @@ variable {m : ℕ} (e : x ^ (p : ℕ) + y ^ (p : ℕ) = ε * ((hζ.unit'.1 - 1)
variable (hy : ¬ hζ.unit'.1 - 1 ∣ y) (hz : ¬ hζ.unit'.1 - 1 ∣ z)
variable (η : nthRootsFinset p (𝓞 K))

/- We have `x,y,z` elements of `O_K` and we assume that we have $$x^p+y^p= ε * ((ζ-1)^(m+1)*z)^p$$-/

/- Let π = ζ -1, then π divides x^p+y^p. -/
lemma zeta_sub_one_dvd : π ∣ x ^ (p : ℕ) + y ^ (p : ℕ) := by
rw [e, mul_pow, ← pow_mul]
apply dvd_mul_of_dvd_right
apply dvd_mul_of_dvd_left
apply dvd_pow_self
simp

/- Let π = ζ -1, then π divides x+yη with η a primivite root of unity. -/
lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by
letI : Fact (Nat.Prime p) := hpri
letI := IsCyclotomicExtension.numberField {p} ℚ K
Expand All @@ -53,21 +57,25 @@ lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by
rw [Finset.prod_const, ← map_pow, Ideal.Quotient.eq_zero_iff_dvd] at h
exact hζ.zeta_sub_one_prime'.dvd_of_dvd_pow h

/- x+yη is divisible by ζ-1 in O_k -/
lemma div_one_sub_zeta_mem : IsIntegral ℤ ((x + y * η : 𝓞 K) / (ζ - 1)) := by
obtain ⟨⟨a, ha⟩, e⟩ := one_sub_zeta_dvd_zeta_pow_sub hp hζ e η
rw [e, mul_comm]
simp only [map_mul, NumberField.RingOfIntegers.map_mk, map_sub, IsPrimitiveRoot.coe_unit'_coe,
map_one]
rwa [mul_div_cancel_right₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)]

/- Make (x+yη)/(ζ-1) into an element of O_K -/
def div_zeta_sub_one : nthRootsFinset p (𝓞 K) → 𝓞 K :=
fun η ↦ ⟨(x + y * η.1) / (ζ - 1), div_one_sub_zeta_mem hp hζ e η⟩

/-Check that if you multiply by π = ζ -1 you get back the original-/
lemma div_zeta_sub_one_mul_zeta_sub_one (η) :
div_zeta_sub_one hp hζ e η * (π) = x + y * η := by
ext
simp [div_zeta_sub_one, div_mul_cancel₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)]

/- y is associated to (x+yη₁)/(ζ-1) - (x+yη₂)/(ζ-1) for η₁ ≠ η₂. -/
lemma div_zeta_sub_one_sub (η₁ η₂) (hη : η₁ ≠ η₂) :
Associated y (div_zeta_sub_one hp hζ e η₁ - div_zeta_sub_one hp hζ e η₂) := by
letI := IsCyclotomicExtension.numberField {p} ℚ K
Expand All @@ -81,6 +89,7 @@ lemma div_zeta_sub_one_sub (η₁ η₂) (hη : η₁ ≠ η₂) :
rw [Ne, ← Subtype.ext_iff.not]
exact hη

/- sending η to (x+yη)/(ζ-1) mod (π) = 𝔭 is injective. -/
lemma div_zeta_sub_one_Injective :
Function.Injective (fun η ↦ Ideal.Quotient.mk 𝔭 (div_zeta_sub_one hp hζ e η)) := by
letI : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
Expand All @@ -92,12 +101,14 @@ lemma div_zeta_sub_one_Injective :
dsimp only at e₂
rwa [← sub_eq_zero, ← map_sub, ← e, Ideal.Quotient.eq_zero_iff_dvd, u.isUnit.dvd_mul_right] at e₂

/- quot by ideal is finite since we are in a number field.-/
instance : Finite (𝓞 K ⧸ 𝔭) := by
haveI : Fact (Nat.Prime p) := hpri
letI := IsCyclotomicExtension.numberField {p} ℚ K
rw [← Ideal.absNorm_ne_zero_iff, Ne, Ideal.absNorm_eq_zero_iff, Ideal.span_singleton_eq_bot]
exact hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt

/- sending η to (x+yη)/(ζ-1) mod (π) = 𝔭 is bijective. -/
lemma div_zeta_sub_one_Bijective :
Function.Bijective (fun η ↦ Ideal.Quotient.mk 𝔭 (div_zeta_sub_one hp hζ e η)) := by
haveI : Fact (Nat.Prime p) := hpri
Expand All @@ -110,13 +121,15 @@ lemma div_zeta_sub_one_Bijective :
Ideal.absNorm_span_singleton, norm_Int_zeta_sub_one hζ hp]
rfl

/- if the image of one of the elements is zero then the corresponding x+yη is divisible by π^2-/
lemma div_zeta_sub_one_eq_zero_iff (η) :
Ideal.Quotient.mk 𝔭 (div_zeta_sub_one hp hζ e η) = 0 ↔ π ^ 2 ∣ x + y * η := by
letI := IsCyclotomicExtension.numberField {p} ℚ K
rw [Ideal.Quotient.eq_zero_iff_dvd, pow_two,
← div_zeta_sub_one_mul_zeta_sub_one hp hζ e,
mul_dvd_mul_iff_right (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)]

/- the gcd of x y called 𝔪 is coprime to 𝔭-/
lemma gcd_zeta_sub_one_eq_one : gcd 𝔪 𝔭 = 1 := by
have : Fact (Nat.Prime p) := hpri
rw [gcd_assoc]
Expand All @@ -125,6 +138,7 @@ lemma gcd_zeta_sub_one_eq_one : gcd 𝔪 𝔭 = 1 := by
· rw [irreducible_iff_prime]
exact hζ.prime_span_sub_one

/- the ideal (x+yη)/(ζ -1) is divisible by 𝔪 -/
lemma gcd_div_div_zeta_sub_one (η) : 𝔪 ∣ Ideal.span {div_zeta_sub_one hp hζ e η} := by
have : Fact (Nat.Prime p) := hpri
rw [← mul_one (Ideal.span {div_zeta_sub_one hp hζ e η}),
Expand All @@ -136,6 +150,7 @@ lemma gcd_div_div_zeta_sub_one (η) : 𝔪 ∣ Ideal.span {div_zeta_sub_one hp h
(Ideal.mem_sup_left (Ideal.subset_span (s := {x}) rfl))
(Ideal.mem_sup_right (Ideal.mul_mem_right _ _ (Ideal.subset_span (s := {y}) rfl)))

/- Give a name to ((x+yη)/(ζ -1))/𝔪, call it 𝔠 η -/
noncomputable
def div_zeta_sub_one_dvd_gcd : Ideal (𝓞 K) :=
(gcd_div_div_zeta_sub_one hp hζ e hy η).choose
Expand All @@ -160,6 +175,7 @@ lemma p_ne_zero : 𝔭 ≠ 0 := by
rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
exact hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt


lemma coprime_c_aux (η₁ η₂ : nthRootsFinset p (𝓞 K)) (hη : η₁ ≠ η₂) : (𝔦 η₁) ⊔ (𝔦 η₂) ∣ 𝔪 * 𝔭 := by
have : 𝔭 = Ideal.span (singleton <| (η₁ : 𝓞 K) - η₂) := by
rw [Ideal.span_singleton_eq_span_singleton]
Expand All @@ -177,6 +193,7 @@ lemma coprime_c (η₁ η₂ : nthRootsFinset p (𝓞 K)) (hη : η₁ ≠ η₂
rw [Ideal.mul_sup, Ideal.sup_mul, m_mul_c_mul_p, m_mul_c_mul_p, Ideal.mul_top]
exact coprime_c_aux hζ η₁ η₂ hη

/- x^p+y^p = 𝔭^((m+1)*p) * (z)^p, here 𝔷 = (z) (the ideal gen by z)-/
lemma span_pow_add_pow_eq :
Ideal.span {x ^ (p : ℕ) + y ^ (p : ℕ)} = (𝔭 ^ (m + 1) * 𝔷) ^ (p : ℕ) := by
simp only [e, ← Ideal.span_singleton_pow, ← Ideal.span_singleton_mul_span_singleton]
Expand All @@ -189,6 +206,7 @@ lemma gcd_m_p_pow_eq_one : gcd 𝔪 (𝔭 ^ (m + 1)) = 1 := by
gcd_zeta_sub_one_eq_one hζ hy]
simp only [add_pos_iff, or_true, one_pos]


lemma m_dvd_z : 𝔪 ∣ 𝔷 := by
rw [← one_mul 𝔷, ← gcd_m_p_pow_eq_one hζ hy (x := x) (m := m)]
apply dvd_gcd_mul_of_dvd_mul
Expand All @@ -212,6 +230,7 @@ lemma exists_ideal_pow_eq_c_aux :
rw [mul_comm _ 𝔷, mul_pow, z_div_m_spec hζ e hy, mul_pow, mul_pow, ← pow_mul, ← pow_mul,
add_mul, one_mul, pow_add, mul_assoc, mul_assoc, mul_assoc]

/- The ∏_η, 𝔠 η = (𝔷' 𝔭^m)^p with 𝔷 = 𝔪 𝔷' -/
lemma prod_c : ∏ η in Finset.attach (nthRootsFinset p (𝓞 K)), 𝔠 η = (𝔷' * 𝔭 ^ m) ^ (p : ℕ) := by
have e' := span_pow_add_pow_eq hζ e
rw [pow_add_pow_eq_prod_add_zeta_runity_mul
Expand All @@ -225,6 +244,7 @@ lemma prod_c : ∏ η in Finset.attach (nthRootsFinset p (𝓞 K)), 𝔠 η = (
← mul_left_inj' ((pow_ne_zero_iff hpri.out.ne_zero).mpr (p_ne_zero hζ) : _), e',
exists_ideal_pow_eq_c_aux]

/-each 𝔠 η is a pth power, which will be denoted by 𝔞 η below. -/
lemma exists_ideal_pow_eq_c : ∃ I : Ideal (𝓞 K), (𝔠 η) = I ^ (p : ℕ) := by
letI inst1 : @IsDomain (Ideal (𝓞 K)) CommSemiring.toSemiring := @Ideal.isDomain (𝓞 K) _ _
letI inst2 := @Ideal.instNormalizedGCDMonoid (𝓞 K) _ _
Expand All @@ -243,6 +263,7 @@ local notation "𝔞" => root_div_zeta_sub_one_dvd_gcd hp hζ e hy
lemma root_div_zeta_sub_one_dvd_gcd_spec : (𝔞 η) ^ (p : ℕ) = 𝔠 η :=
(exists_ideal_pow_eq_c hp hζ e hy η).choose_spec.symm

/-x+yη₁ / (x+yη₂) = 𝔠 η₁/ 𝔠 η₂ -/
lemma c_div_principal_aux (η₁ η₂ : nthRootsFinset p (𝓞 K)) :
((𝔦 η₁) / (𝔦 η₂) : FractionalIdeal (𝓞 K)⁰ K) = 𝔠 η₁ / 𝔠 η₂ := by
simp_rw [← m_mul_c_mul_p hp hζ e hy, FractionalIdeal.coeIdeal_mul]
Expand All @@ -262,6 +283,7 @@ lemma c_div_principal (η₁ η₂ : nthRootsFinset p (𝓞 K)) :
lemma a_div_principal (η₁ η₂ : nthRootsFinset p (𝓞 K)) :
Submodule.IsPrincipal ((𝔞 η₁ / 𝔞 η₂ : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) := by
apply isPrincipal_of_isPrincipal_pow_of_Coprime' _ hreg
/- the line above is where we use the p is regular.-/
rw [div_pow, ← FractionalIdeal.coeIdeal_pow, ← FractionalIdeal.coeIdeal_pow,
root_div_zeta_sub_one_dvd_gcd_spec, root_div_zeta_sub_one_dvd_gcd_spec]
exact c_div_principal hp hζ e hy η₁ η₂
Expand All @@ -270,6 +292,7 @@ noncomputable
def zeta_sub_one_dvd_root : nthRootsFinset p (𝓞 K) :=
(Equiv.ofBijective _ (div_zeta_sub_one_Bijective hp hζ e hy)).symm 0

/- This is the η₀ such that (x+yη₀)/(ζ-1) is zero mod 𝔭. which is unique-/
local notation "η₀" => zeta_sub_one_dvd_root hp hζ e hy

lemma zeta_sub_one_dvd_root_spec : Ideal.Quotient.mk 𝔭 (div_zeta_sub_one hp hζ e η₀) = 0 :=
Expand All @@ -281,6 +304,7 @@ lemma p_dvd_c_iff : 𝔭 ∣ (𝔠 η) ↔ η = η₀ := by
← Ideal.dvd_span_singleton, ← div_zeta_sub_one_dvd_gcd_spec (hy := hy),
← dvd_gcd_mul_iff_dvd_mul, gcd_comm, gcd_zeta_sub_one_eq_one hζ hy, one_mul]

/- All the others 𝔠 η are coprime to 𝔭...basically-/
lemma p_pow_dvd_c_eta_zero_aux [DecidableEq (𝓞 K)] :
gcd (𝔭 ^ (m * p)) (∏ η in Finset.attach (nthRootsFinset p (𝓞 K)) \ {η₀}, 𝔠 η) = 1 := by
rw [← Ideal.isCoprime_iff_gcd]
Expand All @@ -292,6 +316,7 @@ lemma p_pow_dvd_c_eta_zero_aux [DecidableEq (𝓞 K)] :
simp only [Finset.mem_sdiff, Finset.mem_singleton] at hη
exact hη.2 h

/- all the powers of 𝔭 have to be in 𝔠 η₀-/
lemma p_pow_dvd_c_eta_zero : 𝔭 ^ (m * p) ∣ 𝔠 η₀ := by
classical
rw [← one_mul (𝔠 η₀), ← p_pow_dvd_c_eta_zero_aux hp hζ e hy, dvd_gcd_mul_iff_dvd_mul, mul_comm _ (𝔠 η₀),
Expand All @@ -303,6 +328,8 @@ lemma p_dvd_a_iff : 𝔭 ∣ 𝔞 η ↔ η = η₀ := by
rw [← p_dvd_c_iff hp hζ e hy, ← root_div_zeta_sub_one_dvd_gcd_spec,
hζ.prime_span_sub_one.dvd_pow_iff_dvd hpri.out.ne_zero]

/- since the is only one 𝔞 η which is divisble by 𝔭 it has to be the η₀ one and it has to divide
to 𝔭^m power.-/
lemma p_pow_dvd_a_eta_zero : 𝔭 ^ m ∣ 𝔞 η₀ := by
rw [← pow_dvd_pow_iff_dvd hpri.out.ne_zero, root_div_zeta_sub_one_dvd_gcd_spec, ← pow_mul]
exact p_pow_dvd_c_eta_zero hp hζ e hy
Expand All @@ -311,6 +338,7 @@ noncomputable
def a_eta_zero_dvd_p_pow : Ideal (𝓞 K) :=
(p_pow_dvd_a_eta_zero hp hζ e hy).choose

/-𝔞₀ is the coprime to 𝔭 bit of 𝔞 η₀-/
local notation "𝔞₀" => a_eta_zero_dvd_p_pow hp hζ e hy

lemma a_eta_zero_dvd_p_pow_spec : 𝔭 ^ m * 𝔞₀ = 𝔞 η₀ :=
Expand Down Expand Up @@ -380,6 +408,7 @@ lemma a_div_a_zero_num_spec (hη : η ≠ η₀) : ¬ π ∣ α η hη :=
lemma a_div_a_zero_denom_spec (hη : η ≠ η₀) : ¬ π ∣ β η hη :=
(exists_not_dvd_spanSingleton_eq_a_div_a_zero hp hreg hζ e hy hz η hη).choose_spec.choose_spec.2.1

/- eqn 7.8 of Borevich-Shafarevich-/
lemma a_div_a_zero_eq (hη : η ≠ η₀) :
FractionalIdeal.spanSingleton (𝓞 K)⁰ (α η hη / β η hη : K) = 𝔞 η / 𝔞₀ :=
(exists_not_dvd_spanSingleton_eq_a_div_a_zero hp hreg hζ e hy hz η hη).choose_spec.choose_spec.2.2
Expand All @@ -402,6 +431,7 @@ lemma a_mul_denom_eq_a_zero_mul_num (hη : η ≠ η₀) :
rw [hβ]
exact dvd_zero _

/- eqn 7.9 of BS -/
lemma associated_eta_zero (hη : η ≠ η₀) :
Associated ((x + y * η₀) * α η hη ^ (p : ℕ))
((x + y * η) * π ^ (m * p) * β η hη ^ (p : ℕ)) := by
Expand Down Expand Up @@ -521,7 +551,7 @@ lemma exists_solution' :
¬ π ∣ y' ∧ ¬ π ∣ z' ∧ x' ^ (p : ℕ) + y' ^ (p : ℕ) = ε₃ * (π ^ m * z') ^ (p : ℕ) := by
obtain ⟨x', y', z', ε₁, ε₂, ε₃, hx', hy', hz', e'⟩ := exists_solution hp hreg hζ e hy hz
obtain ⟨ε', hε'⟩ : ∃ ε', ε₁ / ε₂ = ε' ^ (p : ℕ) := by
apply eq_pow_prime_of_unit_of_congruent hp hreg
apply eq_pow_prime_of_unit_of_congruent hp hreg --this is Kummers
have : p - 1 ≤ m * p := (Nat.sub_le _ _).trans
((le_of_eq (one_mul _).symm).trans (Nat.mul_le_mul_right p (one_le_m hp hζ e hy hz)))
obtain ⟨u, hu⟩ := (associated_zeta_sub_one_pow_prime hζ).symm
Expand Down

0 comments on commit 0e3aad0

Please sign in to comment.