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

changed all rings from Type to Type _

Browse source
This commit is contained in:
leopoldmayer 2023-06-13 14:26:19 -07:00
parent 7da199c95b
commit a941cce12f
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
CommAlg/krull.lean
View file

@ -25,11 +25,11 @@ variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I noncomputable def krullDim (R : Type _) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl
lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl lemma krullDim_def (R : Type _) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl
lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl lemma krullDim_def' (R : Type _) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl
noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice
@ -39,16 +39,16 @@ lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤
show J' < J show J' < J
exact lt_of_lt_of_le hJ' I_le_J exact lt_of_lt_of_le hJ' I_le_J
lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) : lemma krullDim_le_iff (R : Type _) [CommRing R] (n : ℕ) :
krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
lemma krullDim_le_iff' (R : Type) [CommRing R] (n : ℕ∞) : lemma krullDim_le_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
lemma le_krullDim_iff (R : Type) [CommRing R] (n : ℕ) : lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
lemma le_krullDim_iff' (R : Type) [CommRing R] (n : ℕ∞) : lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
@[simp] @[simp]