feat(KrullDimension): concrete calculations (#19210)

Part of #15524. This adds concrete calculations of the height and Krull Dimension for Nat, Int, WithTop, WithBot and ENat.

From the Carleson project.

Mathlib/Order/KrullDimension.lean

@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang, Fangming Li, Joachim Breitner
 -/
 
-import Mathlib.Order.RelSeries
-import Mathlib.Order.Minimal
+import Mathlib.Algebra.Order.Group.Int
 import Mathlib.Data.ENat.Lattice
+import Mathlib.Order.Minimal
+import Mathlib.Order.RelSeries
 
 /-!
 # Krull dimension of a preordered set and height of an element
@@ -648,4 +649,157 @@ lemma coheight_bot_eq_krullDim [OrderBot α] : coheight (⊥ : α) = krullDim α
 
 end krullDim
 
+/-!
+## Concrete calculations
+-/
+
+section calculations
+
+variable {α : Type*} [Preorder α]
+
+/-
+These two lemmas could possibly be used to simplify the subsequent calculations,
+especially once the `Set.encard` api is richer.
+
+(Commented out to avoid importing modules purely for `proof_wanted`.)
+proof_wanted height_of_linearOrder {α : Type*} [LinearOrder α] (a : α) :
+  height a = (Set.Iio a).encard
+
+proof_wanted coheight_of_linearOrder {α : Type*} [LinearOrder α] (a : α) :
+  coheight a = (Set.Ioi a).encard
+-/
+
+@[simp] lemma height_nat (n : ℕ) : height n = n := by
+  induction n using Nat.strongRecOn with | ind n ih =>
+  apply le_antisymm
+  · apply height_le_coe_iff.mpr
+    simp +contextual only [ih, Nat.cast_lt, implies_true]
+  · exact length_le_height_last (p := LTSeries.range n)
+
+@[simp] lemma coheight_of_noMaxOrder [NoMaxOrder α] (a : α) : coheight a = ⊤ := by
+  obtain ⟨f, hstrictmono⟩ := Nat.exists_strictMono ↑(Set.Ioi a)
+  apply coheight_eq_top_iff.mpr
+  intro m
+  use {length := m, toFun := fun i => if i = 0 then a else f i, step := ?step }
+  case h => simp [RelSeries.head]
+  case step =>
+    intro ⟨i, hi⟩
+    by_cases hzero : i = 0
+    · subst i
+      exact (f 1).prop
+    · suffices f i < f (i + 1) by simp [Fin.ext_iff, hzero, this]
+      apply hstrictmono
+      omega
+
+@[simp] lemma height_of_noMinOrder [NoMinOrder α] (a : α) : height a = ⊤ :=
+  -- Implementation note: Here it's a bit easier to define the coheight variant first
+  coheight_of_noMaxOrder (α := αᵒᵈ) a
+
+@[simp] lemma krullDim_of_noMaxOrder [Nonempty α] [NoMaxOrder α] : krullDim α = ⊤ := by
+  simp [krullDim_eq_iSup_coheight, coheight_of_noMaxOrder]
+
+@[simp] lemma krullDim_of_noMinOrder [Nonempty α] [NoMinOrder α] : krullDim α = ⊤ := by
+  simp [krullDim_eq_iSup_height, height_of_noMinOrder]
+
+lemma coheight_nat (n : ℕ) : coheight n = ⊤ := coheight_of_noMaxOrder ..
+
+lemma krullDim_nat : krullDim ℕ = ⊤ := krullDim_of_noMaxOrder ..
+
+lemma height_int (n : ℤ) : height n = ⊤ := height_of_noMinOrder ..
+
+lemma coheight_int (n : ℤ) : coheight n = ⊤ := coheight_of_noMaxOrder ..
+
+lemma krullDim_int : krullDim ℤ = ⊤ := krullDim_of_noMaxOrder ..
+
+@[simp] lemma height_coe_withBot (x : α) : height (x : WithBot α) = height x + 1 := by
+  apply le_antisymm
+  · apply height_le
+    intro p hlast
+    wlog hlenpos : p.length ≠ 0
+    · simp_all
+    -- essentially p' := (p.drop 1).map unbot
+    let p' : LTSeries α := {
+      length := p.length - 1
+      toFun := fun ⟨i, hi⟩ => (p ⟨i+1, by omega⟩).unbot (by
+        apply LT.lt.ne_bot (a := p.head)
+        apply p.strictMono
+        exact compare_gt_iff_gt.mp rfl)
+      step := fun i => by simpa [WithBot.unbot_lt_iff] using p.step ⟨i + 1, by omega⟩ }
+    have hlast' : p'.last = x := by
+      simp only [RelSeries.last, Fin.val_last, WithBot.unbot_eq_iff, ← hlast, Fin.last]
+      congr
+      omega
+    suffices p'.length ≤ height p'.last by
+      simpa [p', hlast'] using this
+    apply length_le_height_last
+  · rw [height_add_const]
+    apply iSup₂_le
+    intro p hlast
+    let p' := (p.map _ WithBot.coe_strictMono).cons ⊥ (by simp)
+    apply le_iSup₂_of_le p' (by simp [p', hlast]) (by simp [p'])
+
+@[simp] lemma coheight_coe_withTop (x : α) : coheight (x : WithTop α) = coheight x + 1 :=
+  height_coe_withBot (α := αᵒᵈ) x
+
+@[simp] lemma height_coe_withTop (x : α) : height (x : WithTop α) = height x := by
+  apply le_antisymm
+  · apply height_le
+    intro p hlast
+    -- essentially p' := p.map untop
+    let p' : LTSeries α := {
+      length := p.length
+      toFun := fun i => (p i).untop (by
+        apply WithTop.lt_top_iff_ne_top.mp
+        apply lt_of_le_of_lt
+        · exact p.monotone (Fin.le_last _)
+        · rw [RelSeries.last] at hlast
+          simp [hlast])
+      step := fun i => by simpa only [WithTop.untop_lt_iff, WithTop.coe_untop] using p.step i }
+    have hlast' : p'.last = x := by
+      simp only [RelSeries.last, Fin.val_last, WithTop.untop_eq_iff, ← hlast]
+    suffices p'.length ≤ height p'.last by
+      rw [hlast'] at this
+      simpa [p'] using this
+    apply length_le_height_last
+  · apply height_le
+    intro p hlast
+    let p' := p.map _ WithTop.coe_strictMono
+    apply le_iSup₂_of_le p' (by simp [p', hlast]) (by simp [p'])
+
+@[simp] lemma coheight_coe_withBot (x : α) : coheight (x : WithBot α) = coheight x :=
+  height_coe_withTop (α := αᵒᵈ) x
+
+@[simp] lemma krullDim_WithTop [Nonempty α] : krullDim (WithTop α) = krullDim α + 1 := by
+  rw [← height_top_eq_krullDim, krullDim_eq_iSup_height_of_nonempty, height_eq_iSup_lt_height]
+  norm_cast
+  simp_rw [WithTop.lt_top_iff_ne_top]
+  rw [ENat.iSup_add, iSup_subtype']
+  symm
+  apply Equiv.withTopSubtypeNe.symm.iSup_congr
+  simp
+
+@[simp] lemma krullDim_withBot [Nonempty α] : krullDim (WithBot α) = krullDim α + 1 := by
+  conv_lhs => rw [← krullDim_orderDual]
+  conv_rhs => rw [← krullDim_orderDual]
+  exact krullDim_WithTop (α := αᵒᵈ)
+
+@[simp]
+lemma krullDim_enat : krullDim ℕ∞ = ⊤ := by
+  show (krullDim (WithTop ℕ) = ⊤)
+  simp only [krullDim_WithTop, krullDim_nat]
+  rfl
+
+@[simp]
+lemma height_enat (n : ℕ∞) : height n = n := by
+  cases n with
+  | top => simp only [← WithBot.coe_eq_coe, height_top_eq_krullDim, krullDim_enat, WithBot.coe_top]
+  | coe n => exact (height_coe_withTop _).trans (height_nat _)
+
+@[simp]
+lemma coheight_coe_enat (n : ℕ) : coheight (n : ℕ∞) = ⊤ := by
+  apply (coheight_coe_withTop _).trans
+  simp only [Nat.cast_id, coheight_nat, top_add]
+
+end calculations
+
 end Order