comparing definitions of height

This commit is contained in:
GTBarkley 2023-06-11 06:00:13 +00:00
parent d1c10a2d3a
commit 8b28694f0e

View file

@ -1,12 +1,31 @@
import Mathlib.Order.KrullDimension
import Mathlib.Order.JordanHolder
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
import Mathlib.Order.Height
def hello : IO Unit := do
IO.println "Hello, World!"
#eval hello
#check (p q : PrimeSpectrum _) → (p ≤ q)
#check Preorder (PrimeSpectrum _)
-- Dimension of a ring
#check krullDim (PrimeSpectrum _)
-- Length of a module
#check krullDim (Submodule _ _)
#check JordanHolderLattice
variable {α : Type _} [Preorder α] (s : Set α)
-- there should be a coercion from WithTop to WithBot (WithTop ) but it doesn't seem to work
-- it looks like this might be because someone changed the instance from CoeCT to Coe during the port
lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop )) = krullDim s := by
intro hs
unfold Set.chainHeight
unfold krullDim
have hKrullSome : ∃n, krullDim s = some n := by
sorry
-- norm_cast
sorry