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

new: Made some progress on the isField.dim_zero lemma

Browse source
This commit is contained in:
Sayantan Santra 2023-06-12 23:58:40 -07:00
parent 65b343ef42
commit e3a7639399
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F
1 changed files with 13 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
CommAlg/sayantan.lean
View file

@ -57,9 +57,19 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0)
simp [height] at h simp [height] at h
by_contra x by_contra x
rw [Ring.not_isField_iff_exists_prime] at x rw [Ring.not_isField_iff_exists_prime] at x
obtain ⟨P, ⟨h, primeP⟩⟩ := x obtain ⟨P, ⟨h1, primeP⟩⟩ := x
have PgtBot : P > ⊥ := Ne.bot_lt h have PgtBot : P > ⊥ := Ne.bot_lt h1
sorry have pos_height : ↑(Set.chainHeight {J | J < P}) > 0 := by
have : ⊥ ∈ {J | J < P} := PgtBot
have : {J | J < P}.Nonempty := Set.nonempty_of_mem this
-- have : {J | J < P} ≠ ∅ := Set.Nonempty.ne_empty this
rw [←Set.one_le_chainHeight_iff] at this
exact Iff.mp ENat.one_le_iff_pos this
have zero_height : ↑(Set.chainHeight {J | J < P}) = 0 := by
-- Probably need to use Sup_le or something here
sorry
have : ↑(Set.chainHeight {J | J < P}) ≠ 0 := Iff.mp pos_iff_ne_zero pos_height
contradiction
lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
constructor constructor