SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 07:38:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

Merge pull request #80 from GTBarkley/grant

Browse source 
swapped inequalities in lt_height_iff
This commit is contained in:
GTBarkley 2023-06-15 20:54:39 -07:00 committed by GitHub
commit 37e9cf46de
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 23 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
CommAlg/krull.lean
View file

@ -112,31 +112,32 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
/-- The height of a prime `𝔭` is greater than `n` if and only if there is a chain of primes less than `𝔭` /-- The height of a prime `𝔭` is greater than `n` if and only if there is a chain of primes less than `𝔭`
with length `n + 1`. -/ with length `n + 1`. -/
lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by n < height 𝔭 ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
rcases n with _ | n match n with
. constructor <;> intro h <;> exfalso | ⊤ =>
constructor <;> intro h <;> exfalso
. exact (not_le.mpr h) le_top . exact (not_le.mpr h) le_top
. tauto . tauto
have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by | (n : ℕ) =>
symm have (m : ℕ∞) : n < m ↔ (n + 1 : ℕ∞) ≤ m := by
show (n + 1 ≤ m ↔ _ ) symm
apply ENat.add_one_le_iff show (n + 1 ≤ m ↔ _ )
exact ENat.coe_ne_top _ apply ENat.add_one_le_iff
rw [this] exact ENat.coe_ne_top _
unfold Ideal.height rw [this]
show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞)) unfold Ideal.height
rw [{J | J < 𝔭}.le_chainHeight_iff] show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _ rw [{J | J < 𝔭}.le_chainHeight_iff]
constructor <;> rintro ⟨c, hc⟩ <;> use c show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
. tauto constructor <;> rintro ⟨c, hc⟩ <;> use c
. change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc . tauto
norm_cast at hc . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
tauto norm_cast at hc
tauto
/-- Form of `lt_height_iff''` for rewriting with the height coerced to `WithBot ℕ∞`. -/ /-- Form of `lt_height_iff''` for rewriting with the height coerced to `WithBot ℕ∞`. -/
lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by (n : WithBot ℕ∞) < height 𝔭 ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
show (_ < _) ↔ _
rw [WithBot.coe_lt_coe] rw [WithBot.coe_lt_coe]
exact lt_height_iff' exact lt_height_iff'
@ -198,7 +199,7 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal
rw [hcontr] at h rw [hcontr] at h
exact h h𝔪.1 exact h h𝔪.1
use 𝔪p use 𝔪p
show (_ : WithBot ℕ∞) > (0 : ℕ∞) show (0 : ℕ∞) < (_ : WithBot ℕ∞)
rw [lt_height_iff''] rw [lt_height_iff'']
use [I] use [I]
constructor constructor
@ -209,7 +210,7 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal
rwa [hI'] rwa [hI']
. simp . simp
. contrapose! h . contrapose! h
change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h change (0 : ℕ∞) < (_ : WithBot ℕ∞) at h
rw [lt_height_iff''] at h rw [lt_height_iff''] at h
obtain ⟨c, _, hc2, hc3⟩ := h obtain ⟨c, _, hc2, hc3⟩ := h
norm_cast at hc3 norm_cast at hc3