SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-10-16 11:37:05 -05:00
Code Issues Projects Releases Packages Wiki Activity

Merge pull request #84 from GTBarkley/grant

Browse source 
added WF_interval_le_prime
This commit is contained in:
GTBarkley 2023-06-15 21:58:00 -07:00 committed by GitHub
commit 4cd9bdee41
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 14 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
CommAlg/grant2.lean
View file

@ -54,9 +54,20 @@ def symbolicIdeal(Q : Ideal R) {hin : Q.IsPrime} (I : Ideal R) : Ideal R where
rw [←mul_assoc, mul_comm s, mul_assoc]
exact Ideal.mul_mem_left _ _ hs2
theorem WF_interval_le_prime (I : Ideal R) (P : Ideal R) [P.IsPrime]
(h : ∀ J ∈ (Set.Icc I P), J.IsPrime → J = P ):
WellFounded ((· < ·) : (Set.Icc I P) → (Set.Icc I P) → Prop ) := sorry
protected lemma LocalRing.height_le_one_of_minimal_over_principle
[LocalRing R] (q : PrimeSpectrum R) {x : R}
[LocalRing R] {x : R}
(h : (closedPoint R).asIdeal ∈ (Ideal.span {x}).minimalPrimes) :
q = closedPoint R ∨ Ideal.height q = 0 := by
Ideal.height (closedPoint R) ≤ 1 := by
-- by_contra hcont
-- push_neg at hcont
-- rw [Ideal.lt_height_iff'] at hcont
-- rcases hcont with ⟨c, hc1, hc2, hc3⟩
apply height_le_of_gt_height_lt
intro p hp
sorry