diff --git a/FltRegular/NumberTheory/SystemOfUnits.lean b/FltRegular/NumberTheory/SystemOfUnits.lean index 26b2d77e..2e4992e2 100644 --- a/FltRegular/NumberTheory/SystemOfUnits.lean +++ b/FltRegular/NumberTheory/SystemOfUnits.lean @@ -51,11 +51,11 @@ lemma spanA_eq_spanA [Module A G] {R : ℕ} (f : Fin R → G) : refine ⟨⟨a, ⟨0, hp.pred_pos⟩⟩, ?_⟩ simp only [MonoidAlgebra.of_apply, pow_zero, ha] exact one_smul A _ - · rw [Submodule.span_le (R := A)] + · rw [Submodule.span_le] intro x ⟨⟨a, b⟩, hx⟩ simp only [← hx, MonoidAlgebra.of_apply, SetLike.mem_coe] refine Submodule.smul_mem _ _ ?_ - apply Submodule.subset_span (R := A) + apply Submodule.subset_span use a def _root_.Submodule.stabilizer {R M} (S) @@ -124,13 +124,57 @@ lemma spanA_eq_spanZ [Module A G] {R : ℕ} (f : Fin R → G) : · intro a _ hx exact mem_spanS p hp G _ f hx -lemma ex_not_mem [Module A G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) (hr : r ≠ 0) : - ∃ g, ∀ (k : ℤ), ¬(k • g ∈ Submodule.span A (Set.range S.units)) := by - change ∃ g, ∀ (k : ℤ), ¬(k • g ∈ (Submodule.span A (Set.range S.units) : Set G)) +lemma finrank_lt [Module A G] {R : ℕ} (f : Fin R → G) (hR : R < r) : + finrank ℤ + (Submodule.span ℤ (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • f e.1))) < + finrank ℤ G := by + by_cases hr : r = 0 + · linarith + have : R * (p - 1) < finrank ℤ G := by + rw [hf] + exact Nat.mul_lt_mul hR rfl.le hp.pred_pos + refine lt_of_le_of_lt ?_ this + let M := Submodule.span ℤ + (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • f e.1)) + let I := Module.Free.ChooseBasisIndex ℤ G + have : Finite I := by + replace hf : finrank ℤ G ≠ 0 := fun h0 ↦ by + apply hr + simp only [h0, ge_iff_le, zero_eq_mul, tsub_eq_zero_iff_le] at hf + cases hf with + | inl h => exact h + | inr h => linarith [hp.one_lt] + rw [finrank, Module.Free.rank_eq_card_chooseBasisIndex, Cardinal.toNat_ne_zero] at hf + exact Cardinal.mk_lt_aleph0_iff.mp hf.2 + let _ : Fintype I := Fintype.ofFinite I + let BG := Module.Free.chooseBasis ℤ G + let BM := Submodule.basisOfPid BG M + rw [FiniteDimensional.finrank_eq_card_basis BM.2] + have key : ∀ (e : Fin R × (Fin (p - 1))), (zeta p) ^ e.2.1 • f e.1 ∈ M := fun e ↦ by + refine Submodule.subset_span ⟨e, rfl⟩ + let F : Fin R × (Fin (p - 1)) → M := fun (e : Fin R × (Fin (p - 1))) ↦ ⟨_, key e⟩ + let T := Set.range F + let _ : Fintype T := Fintype.ofFinite _ + have hT : Submodule.span ℤ T = ⊤ := by + refine Submodule.eq_top_iff'.2 (fun m ↦ ?_) + exact Submodule.span_induction' (R := ℤ) (M := G) + (s := (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • f e.1))) + (p := fun g hg ↦ ⟨g, hg⟩ ∈ Submodule.span ℤ T) (fun _ ⟨_, he⟩ ↦ Submodule.subset_span + (by simp [← he])) (Submodule.zero_mem _) (fun g₁ hg₁ g₂ hg₂ H₁ H₂ ↦ Submodule.add_mem _ H₁ H₂) + (fun k g hg h ↦ Submodule.smul_mem _ _ h) _ + refine le_trans (Basis.le_span'' BM.2 hT) (le_trans (Fintype.card_range_le _) ?_) + simp + +lemma ex_not_mem [Module A G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) : + ∃ g, ∀ (k : ℤ), k ≠ 0 → ¬(k • g ∈ Submodule.span A (Set.range S.units)) := by + by_cases hr : r = 0 + · linarith + change ∃ g, ∀ (k : ℤ), k ≠ 0 → ¬(k • g ∈ (Submodule.span A (Set.range S.units) : Set G)) rw [spanA_eq_spanZ p hp G S.units] let M := Submodule.span ℤ (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • S.units e.1)) - have : Finite (Module.Free.ChooseBasisIndex ℤ G) := by + let I := Module.Free.ChooseBasisIndex ℤ G + have : Finite I := by replace hf : finrank ℤ G ≠ 0 := fun h0 ↦ by apply hr simp only [h0, ge_iff_le, zero_eq_mul, tsub_eq_zero_iff_le] at hf @@ -139,26 +183,44 @@ lemma ex_not_mem [Module A G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) ( | inr h => linarith [hp.one_lt] rw [finrank, Module.Free.rank_eq_card_chooseBasisIndex, Cardinal.toNat_ne_zero] at hf exact Cardinal.mk_lt_aleph0_iff.mp hf.2 - let BG := Module.Free.chooseBasis ℤ G - have : Module.Finite ℤ G := Module.Finite.of_basis BG - let BM := Submodule.basisOfPid BG M - sorry + let rankM := (Submodule.smithNormalForm (Module.Free.chooseBasis ℤ G) M).1 + let snf := (Submodule.smithNormalForm (Module.Free.chooseBasis ℤ G) M).2 + let ι := snf.f + have hlt : rankM < Nat.card I := by + let _ : Fintype I := Fintype.ofFinite I + rw [Nat.card_eq_fintype_card, ← FiniteDimensional.finrank_eq_card_basis snf.bM] + convert finrank_lt p hp G r hf S.units hR + rw [FiniteDimensional.finrank_eq_card_basis snf.bN] + simp + have key : ∃ (i : I), ¬(i ∈ Set.range ι) := by + suffices : Set.Nonempty (Set.univ \ (Set.range ι)) + · obtain ⟨z, hz⟩ := this + exact ⟨z, hz.2⟩ + apply Set.diff_nonempty_of_ncard_lt_ncard + convert hlt + · rw [← Set.image_univ, Set.ncard_image_of_injective _ (Function.Embedding.injective ι), + Set.ncard_univ] + simp only [Nat.card_eq_fintype_card, Fintype.card_fin] + · exact Set.ncard_univ (Module.Free.ChooseBasisIndex ℤ G) + · exact Set.finite_range _ + obtain ⟨i, hi⟩ := key + refine ⟨snf.bM i, fun k h0 hk ↦ ?_⟩ + have := Basis.SmithNormalForm.repr_eq_zero_of_nmem_range snf ⟨_, hk⟩ hi + simp [h0] at this lemma existence' [Module A G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) : Nonempty (systemOfUnits p G (R + 1)) := by - by_cases hr : r = 0 - · linarith - obtain ⟨g, hg⟩ := ex_not_mem p hp G r hf S hR hr + obtain ⟨g, hg⟩ := ex_not_mem p hp G r hf S hR refine ⟨⟨Fin.cases g S.units, ?_⟩⟩ refine LinearIndependent.fin_cons' g S.units S.linearIndependent (fun a y hy ↦ ?_) by_contra' ha letI := Fact.mk hp - obtain ⟨n, _, f, Hf⟩ := CyclotomicIntegers.exists_dvd_int p _ ha + obtain ⟨n, h0, f, Hf⟩ := CyclotomicIntegers.exists_dvd_int p _ ha replace hy := congr_arg (f • ·) hy simp only at hy rw [smul_zero, smul_add, smul_smul, mul_comm f, ← Hf, ← eq_neg_iff_add_eq_zero, intCast_smul] at hy - apply hg n + apply hg _ h0 rw [hy] exact Submodule.neg_mem _ (Submodule.smul_mem _ _ y.2)