From 04b08fd055487d7f20962675e7c874ab6ff13482 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Tue, 22 Oct 2024 11:30:51 +0200 Subject: [PATCH] bump --- FltRegular/CaseII/Statement.lean | 2 +- .../NumberTheory/Cyclotomic/MoreLemmas.lean | 3 +- FltRegular/NumberTheory/Finrank.lean | 23 ++++-------- FltRegular/NumberTheory/Hilbert92.lean | 6 ++-- lake-manifest.json | 14 ++++++-- lakefile.lean | 36 +++++++++++++++---- 6 files changed, 55 insertions(+), 29 deletions(-) diff --git a/FltRegular/CaseII/Statement.lean b/FltRegular/CaseII/Statement.lean index 46fef029..72f75e13 100644 --- a/FltRegular/CaseII/Statement.lean +++ b/FltRegular/CaseII/Statement.lean @@ -12,7 +12,7 @@ variable {ζ : K} (hζ : IsPrimitiveRoot ζ p) namespace FltRegular include hp hreg in -lemma not_exists_solution (hm : 1 ≤ m) : +lemma not_exists_solution {m : ℕ} (hm : 1 ≤ m) : ¬∃ (x' y' z' : 𝓞 K) (ε₃ : (𝓞 K)ˣ), ¬((hζ.unit' : 𝓞 K) - 1 ∣ y') ∧ ¬((hζ.unit' : 𝓞 K) - 1 ∣ z') ∧ x' ^ (p : ℕ) + y' ^ (p : ℕ) = ε₃ * (((hζ.unit' : 𝓞 K) - 1) ^ m * z') ^ (p : ℕ) := by diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean index 6166e07f..c4f06443 100644 --- a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean @@ -38,7 +38,8 @@ lemma associated_zeta_sub_one_pow_prime : Associated ((hζ.unit' - 1 : 𝓞 K) ^ ((isPrimitiveRoot_of_mem_primitiveRoots hη).mem_nthRootsFinset hpri.out.pos) ((isPrimitiveRoot_of_mem_primitiveRoots hη).ne_one hpri.out.one_lt).symm -lemma isCoprime_of_not_zeta_sub_one_dvd (hx : ¬ (hζ.unit' : 𝓞 K) - 1 ∣ x) : IsCoprime ↑p x := by +lemma isCoprime_of_not_zeta_sub_one_dvd {x : 𝓞 K} (hx : ¬ (hζ.unit' : 𝓞 K) - 1 ∣ x) : + IsCoprime ↑p x := by letI := IsCyclotomicExtension.numberField {p} ℚ K rwa [← Ideal.isCoprime_span_singleton_iff, ← Ideal.span_singleton_eq_span_singleton.mpr (associated_zeta_sub_one_pow_prime hζ), diff --git a/FltRegular/NumberTheory/Finrank.lean b/FltRegular/NumberTheory/Finrank.lean index 3701cafc..e3a90999 100644 --- a/FltRegular/NumberTheory/Finrank.lean +++ b/FltRegular/NumberTheory/Finrank.lean @@ -6,19 +6,11 @@ import Mathlib.LinearAlgebra.FreeModule.PID import Mathlib.LinearAlgebra.Dimension.Localization open Module - section -universe u v - -variable (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] - -variable {R M} - -variable [StrongRankCondition R] [Module.Finite R M] +variable (R M : Type*) [Ring R] [AddCommGroup M] [Module R M] -instance torsion.module {R M} [Ring R] [AddCommGroup M] [Module R M] : - Module R (M ⧸ AddCommGroup.torsion M) := by +instance torsion.module : Module R (M ⧸ AddCommGroup.torsion M) := by letI : Submodule R M := { AddCommGroup.torsion M with smul_mem' := fun r m ⟨n, hn, hn'⟩ ↦ ⟨n, hn, by { simp only [Function.IsPeriodicPt, Function.IsFixedPt, add_left_iterate, add_zero, Nat.isUnit_iff, smul_comm n] at hn' ⊢; simp only [hn', smul_zero] }⟩ } @@ -26,15 +18,14 @@ instance torsion.module {R M} [Ring R] [AddCommGroup M] [Module R M] : end -variable {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] -variable [Module R M] (N : Submodule R M) +variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) lemma FiniteDimensional.finrank_quotient_of_le_torsion (hN : N ≤ Submodule.torsion R M) : finrank R (M ⧸ N) = finrank R M := congr_arg Cardinal.toNat (rank_quotient_eq_of_le_torsion hN) -lemma FiniteDimensional.finrank_map_of_le_torsion {M'} [AddCommGroup M'] [Module R M'] - (l : M →ₗ[R] M') [Module.Finite R N] - (hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M) : finrank R (N.map l) = finrank R N := by +lemma FiniteDimensional.finrank_map_of_le_torsion {M' : Type*} [AddCommGroup M'] [Module R M'] + (l : M →ₗ[R] M') [Module.Finite R N] (hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M) : + finrank R (N.map l) = finrank R N := by conv_lhs => rw [← N.range_subtype, ← LinearMap.range_comp, ← (LinearMap.quotKerEquivRange (l.comp N.subtype)).finrank_eq] apply FiniteDimensional.finrank_quotient_of_le_torsion @@ -68,7 +59,7 @@ instance [IsDomain R] [IsPrincipalIdealRing R] : Module.Free R (M ⧸ Submodule. lemma FiniteDimensional.finrank_add_finrank_quotient [IsDomain R] (N : Submodule R M) : finrank R (M ⧸ N) + finrank R N = finrank R M := by - rw [← Cardinal.natCast_inj.{v}, Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank, + rw [← Cardinal.natCast_inj, Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank, Submodule.finrank_eq_rank] exact HasRankNullity.rank_quotient_add_rank _ diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 67109acf..291af2fe 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -11,7 +11,7 @@ import Mathlib.RingTheory.Henselian open scoped NumberField nonZeroDivisors open FiniteDimensional NumberField -variable (p : ℕ+) {K : Type*} [Field K] +variable {s r : ℕ} (p : ℕ+) {K : Type*} [Field K] variable {k : Type*} [Field k] (hp : Nat.Prime p) open Module BigOperators Finset @@ -23,12 +23,12 @@ variable (G : Type*) [AddCommGroup G] local notation3 "A" => CyclotomicIntegers p /-The system of units is maximal if the quotient by its span leaves a torsion module (i.e. finite) -/ -abbrev systemOfUnits.IsMaximal {s : ℕ} {p : ℕ+} {G : Type*} [AddCommGroup G] +abbrev systemOfUnits.IsMaximal {p : ℕ+} {G : Type*} [AddCommGroup G] [Module (CyclotomicIntegers p) G] (sys : systemOfUnits (G := G) p s) := Fintype (G ⧸ Submodule.span (CyclotomicIntegers p) (Set.range sys.units)) noncomputable -def systemOfUnits.isMaximal [Module.Finite ℤ G] {s : ℕ} (hf : finrank ℤ G = s * (p - 1)) +def systemOfUnits.isMaximal [Module.Finite ℤ G] (hf : finrank ℤ G = s * (p - 1)) [Module A G] (sys : systemOfUnits (G := G) p s) : sys.IsMaximal := by apply Nonempty.some apply (@nonempty_fintype _ ?_) diff --git a/lake-manifest.json b/lake-manifest.json index 1e3e4976..b64b3513 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dd6b1019b5cef990161bf3edfebeb6b0be78044a", + "rev": "7c5548eeeb1748da5c2872dbd866d3acbaea4b3f", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,12 +75,22 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d43bc00b660d5456721455c8f4e4d1d2244f555b", + "rev": "970a6567fb2a41652d0ef34ee38c464dc2b76233", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, + {"url": "https://github.com/PatrickMassot/checkdecls.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce", + "name": "checkdecls", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": false, + "configFile": "lakefile.lean"}, {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, diff --git a/lakefile.lean b/lakefile.lean index 758848d5..b001f65b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,17 +1,41 @@ import Lake open Lake DSL -package «flt-regular» { - -- add any package configuration options here -} +def moreServerArgs := #[ + "-Dpp.unicode.fun=true", -- pretty-prints `fun a ↦ b` + "-DautoImplicit=false", + "-DrelaxedAutoImplicit=false" +] + +-- These settings only apply during `lake build`, but not in VSCode editor. +def moreLeanArgs := moreServerArgs + +-- These are additional settings which do not affect the lake hash, +-- so they can be enabled in CI and disabled locally or vice versa. +-- Warning: Do not put any options here that actually change the olean files, +-- or inconsistent behavior may result +def weakLeanArgs : Array String := + if get_config? CI |>.isSome then + #["-DwarningAsError=true"] + else + #[] + +package «flt-regular» where + leanOptions := #[ + ⟨`relaxedAutoImplicit, false⟩, -- prevents typos to be interpreted as new free variables + ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` + ⟨`autoImplicit, false⟩] require mathlib from git "https://github.com/leanprover-community/mathlib4.git" +require checkdecls from git + "https://github.com/PatrickMassot/checkdecls.git" @ "master" + require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" @[default_target] -lean_lib «FltRegular» { - -- add any library configuration options here -} +lean_lib «FltRegular» where + moreLeanArgs := moreLeanArgs + weakLeanArgs := weakLeanArgs