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

Modified some types to make them implicit

Browse source
This commit is contained in:
Sayantan Santra 2023-06-16 11:22:21 -07:00
parent 65d6e05f08
commit f76ff450e7
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
CommAlg/krull.lean
View file

@ -49,10 +49,12 @@ 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 : ℕ) : @[simp]
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 : ℕ∞) : @[simp]
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 ℕ∞)
@[simp] @[simp]
@ -91,7 +93,8 @@ lemma height_bot_eq {D: Type _} [CommRing D] [IsDomain D] : height (⊥ : PrimeS
/-- The Krull dimension of a ring being ≥ n is equivalent to there being an /-- The Krull dimension of a ring being ≥ n is equivalent to there being an
ideal of height ≥ n. -/ ideal of height ≥ n. -/
lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : @[simp]
lemma le_krullDim_iff {R : Type _} [CommRing R] {n : ℕ} :
n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by
constructor constructor
· unfold krullDim · unfold krullDim
@ -246,7 +249,7 @@ lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h :
/-- Krull dimension is ≤ 0 if and only if all primes are maximal. -/ /-- Krull dimension is ≤ 0 if and only if all primes are maximal. -/
lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
show ((_ : WithBot ℕ∞) ≤ (0 : ℕ)) ↔ _ show ((_ : WithBot ℕ∞) ≤ (0 : ℕ)) ↔ _
rw [krullDim_le_iff R 0] rw [krullDim_le_iff]
constructor <;> intro h I constructor <;> intro h I
. contrapose! h . contrapose! h
have ⟨𝔪, h𝔪⟩ := I.asIdeal.exists_le_maximal (IsPrime.ne_top I.IsPrime) have ⟨𝔪, h𝔪⟩ := I.asIdeal.exists_le_maximal (IsPrime.ne_top I.IsPrime)
@ -353,7 +356,7 @@ lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry
applies only to dimension zero rings and domains of dimension 1. -/ applies only to dimension zero rings and domains of dimension 1. -/
lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by
show _ → ((_ : WithBot ℕ∞) ≤ (1 : ℕ)) show _ → ((_ : WithBot ℕ∞) ≤ (1 : ℕ))
rw [krullDim_le_iff R 1] rw [krullDim_le_iff]
intro H p intro H p
apply le_of_not_gt apply le_of_not_gt
intro h intro h
@ -375,7 +378,7 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1
exact Ring.DimensionLEOne.principal_ideal_ring R exact Ring.DimensionLEOne.principal_ideal_ring R
/-- The ring of polynomials over a field has dimension one. -/ /-- The ring of polynomials over a field has dimension one. -/
lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by lemma polynomial_over_field_dim_one {K : Type _} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by
rw [le_antisymm_iff] rw [le_antisymm_iff]
let X := @Polynomial.X K _ let X := @Polynomial.X K _
constructor constructor