Skip to content

Commit 3a246a4

Browse files
pink10000pink10000
committed
fix theorem for minimal primes to IsMin
1 parent a5fb76d commit 3a246a4

File tree

2 files changed

+98
-61
lines changed

2 files changed

+98
-61
lines changed

‎LeanCommAlg/Basic.lean‎

Lines changed: 13 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ noncomputable def height [h : I.IsPrime] : WithBot ℕ∞ :=
2323

2424
#check height
2525

26-
lemma singleton_of_minimal_prime [h : I.IsPrime] :
26+
@[simp] lemma singleton_of_minimal_prime [h : I.IsPrime] :
2727
I ∈ minimalPrimes R → {J : PrimeSpectrum R | J.asIdeal ≤ I} = {⟨I, h⟩} := by
2828
intro hmin
2929
rcases hmin with ⟨hl, hr⟩
@@ -38,20 +38,17 @@ lemma singleton_of_minimal_prime [h : I.IsPrime] :
3838
apply le_antisymm hJ this
3939
. intro hJ
4040
apply le_iff_lt_or_eq.mpr; right; apply hJ
41-
42-
-- Minimal prime proof
43-
theorem minimal_prime_IsMin
44-
(I : Ideal R) (P : Ideal R) (Pmin : P ∈ Ideal.minimalPrimes I) : IsMin P := by
45-
rw [Ideal.minimalPrimes] at Pmin
46-
rcases Pmin with ⟨hPrime, hMinimal⟩
47-
intros Q hQ
48-
have QPrime : Q.IsPrime := by
49-
sorry
50-
have IleQ : I ≤ Q := by
51-
sorry
52-
specialize hMinimal ?_
53-
apply Q; simp [IleQ, QPrime];
54-
exact hMinimal (by assumption)
41+
42+
@[simp] theorem minimal_prime_is_min_over_I
43+
(I P : Ideal R) (hP : P ∈ Ideal.minimalPrimes I) :
44+
∀ Q : Ideal R, Q.IsPrime → I ≤ Q → Q ≤ P → Q = P := by
45+
rw [Ideal.minimalPrimes] at hP
46+
rcases hP with ⟨hPPrime, hPMinimal⟩
47+
intro Q a IQ QP
48+
simp_all
49+
ext x; constructor
50+
· intro xQ; apply QP xQ
51+
· intro xP; exact hPMinimal a IQ QP xP
5552

5653
lemma height_zero_of_minimal_prime [h : I.IsPrime] :
5754
I ∈ minimalPrimes R → height I = 0 := by
@@ -62,7 +59,7 @@ lemma height_zero_of_minimal_prime [h : I.IsPrime] :
6259
rcases hmin with ⟨hl, hr⟩
6360
dsimp at hr
6461
rw [height, Order.height, this]
65-
simp
62+
simp_all
6663
intros lt hy
6764
rw [RelSeries.length_eq_zero]
6865
sorry

‎lake-manifest.json‎

Lines changed: 85 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -1,52 +1,92 @@
11
{"version": "1.1.0",
22
"packagesDir": ".lake/packages",
33
"packages":
4-
[{"url": "https://github.com/leanprover-community/batteries",
4+
[{"url": "https://github.com/leanprover/doc-gen4",
55
"type": "git",
66
"subDir": null,
7-
"scope": "leanprover-community",
8-
"rev": "f46c0445cc86ad2bc973edf8c5b2bd88bd91913b",
9-
"name": "batteries",
7+
"scope": "",
8+
"rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c",
9+
"name": "«doc-gen4»",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "main",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/PatrickMassot/checkdecls.git",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "",
18+
"rev": "8e459c606cbf19248c6a59956570f051f05e6067",
19+
"name": "checkdecls",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": null,
22+
"inherited": false,
23+
"configFile": "lakefile.lean"},
24+
{"url": "https://github.com/leanprover-community/mathlib4.git",
25+
"type": "git",
26+
"subDir": null,
27+
"scope": "",
28+
"rev": "a1f01bd5d16151d917c810909a2aa2e7b7ad64a0",
29+
"name": "mathlib",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": null,
32+
"inherited": false,
33+
"configFile": "lakefile.lean"},
34+
{"url": "https://github.com/mhuisi/lean4-cli",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "",
38+
"rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
39+
"name": "Cli",
1040
"manifestFile": "lake-manifest.json",
1141
"inputRev": "main",
1242
"inherited": true,
1343
"configFile": "lakefile.toml"},
14-
{"url": "https://github.com/leanprover-community/quote4",
44+
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
1545
"type": "git",
1646
"subDir": null,
17-
"scope": "leanprover-community",
18-
"rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
19-
"name": "Qq",
47+
"scope": "",
48+
"rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014",
49+
"name": "UnicodeBasic",
2050
"manifestFile": "lake-manifest.json",
21-
"inputRev": "master",
51+
"inputRev": "main",
2252
"inherited": true,
2353
"configFile": "lakefile.lean"},
24-
{"url": "https://github.com/leanprover-community/aesop",
54+
{"url": "https://github.com/dupuisf/BibtexQuery",
2555
"type": "git",
2656
"subDir": null,
27-
"scope": "leanprover-community",
28-
"rev": "de91b59101763419997026c35a41432ac8691f15",
29-
"name": "aesop",
57+
"scope": "",
58+
"rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b",
59+
"name": "BibtexQuery",
3060
"manifestFile": "lake-manifest.json",
3161
"inputRev": "master",
3262
"inherited": true,
33-
"configFile": "lakefile.toml"},
34-
{"url": "https://github.com/leanprover-community/ProofWidgets4",
63+
"configFile": "lakefile.lean"},
64+
{"url": "https://github.com/acmepjz/md4lean",
3565
"type": "git",
3666
"subDir": null,
37-
"scope": "leanprover-community",
38-
"rev": "1383e72b40dd62a566896a6e348ffe868801b172",
39-
"name": "proofwidgets",
67+
"scope": "",
68+
"rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
69+
"name": "MD4Lean",
4070
"manifestFile": "lake-manifest.json",
41-
"inputRev": "v0.0.46",
71+
"inputRev": "main",
4272
"inherited": true,
4373
"configFile": "lakefile.lean"},
44-
{"url": "https://github.com/leanprover/lean4-cli",
74+
{"url": "https://github.com/leanprover-community/plausible",
4575
"type": "git",
4676
"subDir": null,
47-
"scope": "leanprover",
48-
"rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
49-
"name": "Cli",
77+
"scope": "leanprover-community",
78+
"rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
79+
"name": "plausible",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "main",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover-community",
88+
"rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
89+
"name": "LeanSearchClient",
5090
"manifestFile": "lake-manifest.json",
5191
"inputRev": "main",
5292
"inherited": true,
@@ -61,45 +101,45 @@
61101
"inputRev": "main",
62102
"inherited": true,
63103
"configFile": "lakefile.toml"},
64-
{"url": "https://github.com/leanprover-community/LeanSearchClient",
104+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
65105
"type": "git",
66106
"subDir": null,
67107
"scope": "leanprover-community",
68-
"rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
69-
"name": "LeanSearchClient",
108+
"rev": "1383e72b40dd62a566896a6e348ffe868801b172",
109+
"name": "proofwidgets",
70110
"manifestFile": "lake-manifest.json",
71-
"inputRev": "main",
111+
"inputRev": "v0.0.46",
72112
"inherited": true,
73-
"configFile": "lakefile.toml"},
74-
{"url": "https://github.com/leanprover-community/plausible",
113+
"configFile": "lakefile.lean"},
114+
{"url": "https://github.com/leanprover-community/aesop",
75115
"type": "git",
76116
"subDir": null,
77117
"scope": "leanprover-community",
78-
"rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
79-
"name": "plausible",
118+
"rev": "de91b59101763419997026c35a41432ac8691f15",
119+
"name": "aesop",
80120
"manifestFile": "lake-manifest.json",
81-
"inputRev": "main",
121+
"inputRev": "master",
82122
"inherited": true,
83123
"configFile": "lakefile.toml"},
84-
{"url": "https://github.com/leanprover-community/mathlib4.git",
124+
{"url": "https://github.com/leanprover-community/quote4",
85125
"type": "git",
86126
"subDir": null,
87-
"scope": "",
88-
"rev": "cee87aa25cfbd8e4c3cd89bc26cce86e927e36dc",
89-
"name": "mathlib",
127+
"scope": "leanprover-community",
128+
"rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
129+
"name": "Qq",
90130
"manifestFile": "lake-manifest.json",
91-
"inputRev": null,
92-
"inherited": false,
131+
"inputRev": "master",
132+
"inherited": true,
93133
"configFile": "lakefile.lean"},
94-
{"url": "https://github.com/PatrickMassot/checkdecls.git",
134+
{"url": "https://github.com/leanprover-community/batteries",
95135
"type": "git",
96136
"subDir": null,
97-
"scope": "",
98-
"rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce",
99-
"name": "checkdecls",
137+
"scope": "leanprover-community",
138+
"rev": "f46c0445cc86ad2bc973edf8c5b2bd88bd91913b",
139+
"name": "batteries",
100140
"manifestFile": "lake-manifest.json",
101-
"inputRev": null,
102-
"inherited": false,
103-
"configFile": "lakefile.lean"}],
141+
"inputRev": "main",
142+
"inherited": true,
143+
"configFile": "lakefile.toml"}],
104144
"name": "lean_comm_alg",
105145
"lakeDir": ".lake"}

0 commit comments

Comments
 (0)